Showing 1–16 of 16 results for author: Etalle, S

Challenges in Designing Exploit Mitigations for Deeply Embedded Systems

Authors: Ali Abbasi, Jos Wetzels, Thorsten Holz, Sandro Etalle

Abstract: Memory corruption vulnerabilities have been around for decades and rank among the most prevalent vulnerabilities in embedded systems. Yet this constrained environment poses unique design and implementation challenges that significantly complicate the adoption of common hardening techniques. Combined with the irregular and involved nature of embedded patch management, this results in prolonged vuln… ▽ More Memory corruption vulnerabilities have been around for decades and rank among the most prevalent vulnerabilities in embedded systems. Yet this constrained environment poses unique design and implementation challenges that significantly complicate the adoption of common hardening techniques. Combined with the irregular and involved nature of embedded patch management, this results in prolonged vulnerability exposure windows and vulnerabilities that are relatively easy to exploit. Considering the sensitive and critical nature of many embedded systems, this situation merits significant improvement. In this work, we present the first quantitative study of exploit mitigation adoption in 42 embedded operating systems, showing the embedded world to significantly lag behind the general-purpose world. To improve the security of deeply embedded systems, we subsequently present μArmor, an approach to address some of the key gaps identified in our quantitative analysis. μArmor raises the bar for exploitation of embedded memory corruption vulnerabilities, while being adoptable on the short term without incurring prohibitive extra performance or storage costs. △ Less

Submitted 5 July, 2020; originally announced July 2020.

Comments: Published in 4th IEEE European Symposium on Security and Privacy (EuroS&P'19)

Network intrusion detection systems for in-vehicle network - Technical report

Authors: Guillaume Dupont, Jerry den Hartog, Sandro Etalle, Alexios Lekidis

Abstract: Modern vehicles are complex safety critical cyber physical systems, that are connected to the outside world, with all security implications that brings. To enhance vehicle security several network intrusion detection systems (NIDS) have been proposed for the CAN bus, the predominant type of in-vehicle network. The in-vehicle CAN bus, however, is a challenging place to do intrusion detection as mes… ▽ More Modern vehicles are complex safety critical cyber physical systems, that are connected to the outside world, with all security implications that brings. To enhance vehicle security several network intrusion detection systems (NIDS) have been proposed for the CAN bus, the predominant type of in-vehicle network. The in-vehicle CAN bus, however, is a challenging place to do intrusion detection as messages provide very little information; interpreting them requires specific knowledge about the implementation that is not readily available. In this technical report we collect how existing solutions address this challenge by providing an organized inventory of various CAN NIDSs present in the literature, categorizing them based on what information they extract from the network and how they build their model. △ Less

Submitted 27 May, 2019; originally announced May 2019.

Towards Realistic Threat Modeling: Attack Commodification, Irrelevant Vulnerabilities, and Unrealistic Assumptions

Authors: Luca Allodi, Sandro Etalle

Abstract: Current threat models typically consider all possible ways an attacker can penetrate a system and assign probabilities to each path according to some metric (e.g. time-to-compromise). In this paper we discuss how this view hinders the realness of both technical (e.g. attack graphs) and strategic (e.g. game theory) approaches of current threat modeling, and propose to steer away by looking more car… ▽ More Current threat models typically consider all possible ways an attacker can penetrate a system and assign probabilities to each path according to some metric (e.g. time-to-compromise). In this paper we discuss how this view hinders the realness of both technical (e.g. attack graphs) and strategic (e.g. game theory) approaches of current threat modeling, and propose to steer away by looking more carefully at attack characteristics and attacker environment. We use a toy threat model for ICS attacks to show how a realistic view of attack instances can emerge from a simple analysis of attack phases and attacker limitations. △ Less

Submitted 14 January, 2018; originally announced January 2018.

Comments: Proceedings of the 2017 Workshop on Automated Decision Making for Active Cyber Defense

GEM: a Distributed Goal Evaluation Algorithm for Trust Management

Authors: Daniel Trivellato, Nicola Zannone, Sandro Etalle

Abstract: Trust management is an approach to access control in distributed systems where access decisions are based on policy statements issued by multiple principals and stored in a distributed manner. In trust management, the policy statements of a principal can refer to other principals' statements; thus, the process of evaluating an access request (i.e., a goal) consists of finding a "chain" of policy s… ▽ More Trust management is an approach to access control in distributed systems where access decisions are based on policy statements issued by multiple principals and stored in a distributed manner. In trust management, the policy statements of a principal can refer to other principals' statements; thus, the process of evaluating an access request (i.e., a goal) consists of finding a "chain" of policy statements that allows the access to the requested resource. Most existing goal evaluation algorithms for trust management either rely on a centralized evaluation strategy, which consists of collecting all the relevant policy statements in a single location (and therefore they do not guarantee the confidentiality of intensional policies), or do not detect the termination of the computation (i.e., when all the answers of a goal are computed). In this paper we present GEM, a distributed goal evaluation algorithm for trust management systems that relies on function-free logic programming for the specification of policy statements. GEM detects termination in a completely distributed way without disclosing intensional policies, thereby preserving their confidentiality. We demonstrate that the algorithm terminates and is sound and complete with respect to the standard semantics for logic programs. △ Less

Submitted 1 October, 2012; originally announced October 2012.

Comments: To appear in Theory and Practice of Logic Programming (TPLP)

Journal ref: Theory and Practice of Logic Programming 14 (2014) 293-337

APHRODITE: an Anomaly-based Architecture for False Positive Reduction

Authors: Damiano Bolzoni, Sandro Etalle

Abstract: We present APHRODITE, an architecture designed to reduce false positives in network intrusion detection systems. APHRODITE works by detecting anomalies in the output traffic, and by correlating them with the alerts raised by the NIDS working on the input traffic. Benchmarks show a substantial reduction of false positives and that APHRODITE is effective also after a "quick setup", i.e. in the rea… ▽ More We present APHRODITE, an architecture designed to reduce false positives in network intrusion detection systems. APHRODITE works by detecting anomalies in the output traffic, and by correlating them with the alerts raised by the NIDS working on the input traffic. Benchmarks show a substantial reduction of false positives and that APHRODITE is effective also after a "quick setup", i.e. in the realistic case in which it has not been "trained" and set up optimally △ Less

Submitted 7 April, 2006; originally announced April 2006.

Report number: TR-CTIT-06-13

Poseidon: a 2-tier Anomaly-based Intrusion Detection System

Authors: Damiano Bolzoni, Emmanuele Zambon, Sandro Etalle, Pieter Hartel

Abstract: We present Poseidon, a new anomaly based intrusion detection system. Poseidon is payload-based, and presents a two-tier architecture: the first stage consists of a Self-Organizing Map, while the second one is a modified PAYL system. Our benchmarks on the 1999 DARPA data set show a higher detection rate and lower number of false positives than PAYL and PHAD. We present Poseidon, a new anomaly based intrusion detection system. Poseidon is payload-based, and presents a two-tier architecture: the first stage consists of a Self-Organizing Map, while the second one is a modified PAYL system. Our benchmarks on the 1999 DARPA data set show a higher detection rate and lower number of false positives than PAYL and PHAD. △ Less

Submitted 3 February, 2006; v1 submitted 11 November, 2005; originally announced November 2005.

Report number: TR-CTIT-05-53

Nonmonotonic Trust Management for P2P Applications

Authors: M. Czenko, H. Tran, J. Doumen, S. Etalle, P. Hartel, J. den Hartog

Abstract: Community decisions about access control in virtual communities are non-monotonic in nature. This means that they cannot be expressed in current, monotonic trust management languages such as the family of Role Based Trust Management languages (RT). To solve this problem we propose RT-, which adds a restricted form of negation to the standard RT language, thus admitting a controlled form of non-m… ▽ More Community decisions about access control in virtual communities are non-monotonic in nature. This means that they cannot be expressed in current, monotonic trust management languages such as the family of Role Based Trust Management languages (RT). To solve this problem we propose RT-, which adds a restricted form of negation to the standard RT language, thus admitting a controlled form of non-monotonicity. The semantics of RT- is discussed and presented in terms of the well-founded semantics for Logic Programs. Finally we discuss how chain discovery can be accomplished for RT-. △ Less

Submitted 21 October, 2005; originally announced October 2005.

Comments: This paper appears in the proceedings of the 1st International Workshop on Security and Trust Management (STM 2005). To appear in ENTCS

Report number: TR-CTIT-05-22 ACM Class: F.4.1; I.2.3; I.2.4

Integrity Constraints in Trust Management

Authors: Sandro Etalle, William H. Winsborough

Abstract: We introduce the use, monitoring, and enforcement of integrity constraints in trust management-style authorization systems. We consider what portions of the policy state must be monitored to detect violations of integrity constraints. Then we address the fact that not all participants in a trust management system can be trusted to assist in such monitoring, and show how many integrity constraint… ▽ More We introduce the use, monitoring, and enforcement of integrity constraints in trust management-style authorization systems. We consider what portions of the policy state must be monitored to detect violations of integrity constraints. Then we address the fact that not all participants in a trust management system can be trusted to assist in such monitoring, and show how many integrity constraints can be monitored in a conservative manner so that trusted participants detect and report if the system enters a policy state from which evolution in unmonitored portions of the policy could lead to a constraint violation. △ Less

Submitted 23 March, 2005; originally announced March 2005.

Comments: An extended abstract appears in the proc. of the 10th ACM Symp. on Access Control Models and Technologies (SACMAT). 2005

ACM Class: K.6.5; D.4.6

Timed Analysis of Security Protocols

Authors: R. Corin, S. Etalle, P. H. Hartel, A. Mader

Abstract: We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol, where timing information allows the study of different attack scenarios. We model check the protocols using UPPAAL. Further, a taxonomy is obtained by studying and categorising protocols from the wel… ▽ More We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol, where timing information allows the study of different attack scenarios. We model check the protocols using UPPAAL. Further, a taxonomy is obtained by studying and categorising protocols from the well known Clark Jacob library and the Security Protocol Open Repository (SPORE) library. Finally, we present some new challenges and threats that arise when considering time in the analysis, by providing a novel protocol that uses time challenges and exposing a timing attack over an implementation of an existing security protocol. △ Less

Submitted 30 October, 2005; v1 submitted 17 March, 2005; originally announced March 2005.

An Audit Logic for Accountability

Authors: J. G. Cederquist, R. Corin, M. A. C. Dekker, S. Etalle, J. I. den Hartog

Abstract: We describe and implement a policy language. In our system, agents can distribute data along with usage policies in a decentralized architecture. Our language supports the specification of conditions and obligations, and also the possibility to refine policies. In our framework, the compliance with usage policies is not actively enforced. However, agents are accountable for their actions, and ma… ▽ More We describe and implement a policy language. In our system, agents can distribute data along with usage policies in a decentralized architecture. Our language supports the specification of conditions and obligations, and also the possibility to refine policies. In our framework, the compliance with usage policies is not actively enforced. However, agents are accountable for their actions, and may be audited by an authority requiring justifications. △ Less

Submitted 28 April, 2005; v1 submitted 24 February, 2005; originally announced February 2005.

Comments: To appear in Proceedings of IEEE Policy 2005

A Trace Logic for Local Security Properties

Authors: Ricardo Corin, Antonio Durante, Sandro Etalle, Pieter Hartel

Abstract: We propose a new simple \emph{trace} logic that can be used to specify \emph{local security properties}, i.e. security properties that refer to a single participant of the protocol specification. Our technique allows a protocol designer to provide a formal specification of the desired security properties, and integrate it naturally into the design process of cryptographic protocols. Furthermore,… ▽ More We propose a new simple \emph{trace} logic that can be used to specify \emph{local security properties}, i.e. security properties that refer to a single participant of the protocol specification. Our technique allows a protocol designer to provide a formal specification of the desired security properties, and integrate it naturally into the design process of cryptographic protocols. Furthermore, the logic can be used for formal verification. We illustrate the utility of our technique by exposing new attacks on the well studied protocol TMN. △ Less

Submitted 30 November, 2004; v1 submitted 5 November, 2004; originally announced November 2004.

Comments: New version

Transformations of CCP programs

Authors: Sandro Etalle, Maurizio Gabbrielli, Maria Chiara Meo

Abstract: We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations which guarantee that the input/output CCP semantics is preserved also when distinguishing deadlocked computations from successful ones and when considering intermediate results of (possibly) non-terminating computations. The system allows us to o… ▽ More We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations which guarantee that the input/output CCP semantics is preserved also when distinguishing deadlocked computations from successful ones and when considering intermediate results of (possibly) non-terminating computations. The system allows us to optimize CCP programs while preserving their intended meaning: In addition to the usual benefits that one has for sequential declarative languages, the transformation of concurrent programs can also lead to the elimination of communication channels and of synchronization points, to the transformation of non-deterministic computations into deterministic ones, and to the crucial saving of computational space. Furthermore, since the transformation system preserves the deadlock behavior of programs, it can be used for proving deadlock freeness of a given program wrt a class of queries. To this aim it is sometimes sufficient to apply our transformations and to specialize the resulting program wrt the given queries in such a way that the obtained program is trivially deadlock free. △ Less

Submitted 10 July, 2001; originally announced July 2001.

Comments: To appear in ACM TOPLAS

ACM Class: I.2.2; D.1.3; D.3.2

Properties of Input-Consuming Derivations

Authors: Annalisa Bossi, Sandro Etalle, Sabina Rossi

Abstract: We study the properties of input-consuming derivations of moded logic programs. Input-consuming derivations can be used to model the behavior of logic programs using dynamic scheduling and employing constructs such as delay declarations. We consider the class of nicely-moded programs and queries. We show that for these programs a weak version of the well-known switching lemma holds also for in… ▽ More We study the properties of input-consuming derivations of moded logic programs. Input-consuming derivations can be used to model the behavior of logic programs using dynamic scheduling and employing constructs such as delay declarations. We consider the class of nicely-moded programs and queries. We show that for these programs a weak version of the well-known switching lemma holds also for input-consuming derivations. Furthermore, we show that, under suitable conditions, there exists an algebraic characterization of termination of input-consuming derivations. △ Less

Submitted 23 January, 2001; originally announced January 2001.

Comments: 33 pages

ACM Class: D.1.6; D.3.1; F.3.2

Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling

Authors: Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-Georg Smaus

Abstract: In logic programming, dynamic scheduling refers to a situation where the selection of the atom in each resolution (computation) step is determined at runtime, as opposed to a fixed selection rule such as the left-to-right one of Prolog. This has applications e.g. in parallel programming. A mechanism to control dynamic scheduling is provided in existing languages in the form of delay declarations… ▽ More In logic programming, dynamic scheduling refers to a situation where the selection of the atom in each resolution (computation) step is determined at runtime, as opposed to a fixed selection rule such as the left-to-right one of Prolog. This has applications e.g. in parallel programming. A mechanism to control dynamic scheduling is provided in existing languages in the form of delay declarations. Input-consuming derivations were introduced to describe dynamic scheduling while abstracting from the technical details. In this paper, we first formalise the relationship between delay declarations and input-consuming derivations, showing in many cases a one-to-one correspondence. Then, we define a model-theoretic semantics for input-consuming derivations of simply-moded programs. Finally, for this class of programs, we provide a necessary and sufficient criterion for termination. △ Less

Submitted 23 January, 2001; originally announced January 2001.

Comments: 25 pages, long version of paper with same title at ESOP 2001

ACM Class: D.1.3; D.1.6; F.3.2

On Modular Termination Proofs of General Logic Programs

Authors: Annalisa Bossi, Nicoletta Cocco, Sandro Etalle, Sabina Rossi

Abstract: We propose a modular method for proving termination of general logic programs (i.e., logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider programs consisting of a hierarchy of modules and supply a general result for proving termination by dealing with each module separately. For programs which a… ▽ More We propose a modular method for proving termination of general logic programs (i.e., logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider programs consisting of a hierarchy of modules and supply a general result for proving termination by dealing with each module separately. For programs which are in a certain sense well-behaved, namely well-moded or well-typed programs, we derive both a simple verification technique and an iterative proof method. Some examples show how our system allows for greatly simplified proofs. △ Less

Submitted 30 July, 2001; v1 submitted 11 May, 2000; originally announced May 2000.

Comments: 29 pages. To appear in Theory and Practice of Logic Programming

Report number: University of Venice Technical Report CS2000-8 ACM Class: D.2; D.3; F.3.1; F.3.2

The (Lazy) Functional Side of Logic Programming

Authors: S. Etalle, J. Mountjoy

Abstract: The possibility of translating logic programs into functional ones has long been a subject of investigation. Common to the many approaches is that the original logic program, in order to be translated, needs to be well-moded and this has led to the common understanding that these programs can be considered to be the ``functional part'' of logic programs. As a consequence of this it has become wi… ▽ More The possibility of translating logic programs into functional ones has long been a subject of investigation. Common to the many approaches is that the original logic program, in order to be translated, needs to be well-moded and this has led to the common understanding that these programs can be considered to be the ``functional part'' of logic programs. As a consequence of this it has become widely accepted that ``complex'' logical variables, the possibility of a dynamic selection rule, and general properties of non-well-moded programs are exclusive features of logic programs. This is not quite true, as some of these features are naturally found in lazy functional languages. We readdress the old question of what features are exclusive to the logic programming paradigm by defining a simple translation applicable to a wider range of logic programs, and demonstrate that the current circumscription is unreasonably restrictive. △ Less

Submitted 20 March, 2000; originally announced March 2000.

Comments: 23 pages

Report number: CS-00-02 ACM Class: D.1.1; D.1.6; D.3.2; F.3.3