Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDiscovering ePassport Vulnerabilities using Bisimilarity
80
0
0.0
(
0
)
Added by
Ross Horne
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We uncover privacy vulnerabilities in the ICAO 9303 standard implemented by ePassports worldwide. These vulnerabilities, confirmed by ICAO, enable an ePassport holder who recently passed through a checkpoint to be reidentified without opening their ePassport. This paper explains how bisimilarity was used to discover these vulnerabilities, which exploit the BAC protocol - the original ICAO 9303 standard ePassport authentication protocol - and remains valid for the PACE protocol, which improves on the security of BAC in the latest ICAO 9303 standards. In order to tackle such bisimilarity problems, we develop here a chain of methods for the applied $pi$-calculus including a symbolic under-approximation of bisimilarity, called open bisimilarity, and a modal logic, called classical FM, for describing and certifying attacks. Evidence is provided to argue for a new scheme for specifying such unlinkability problems that more accurately reflects the capabilities of an attacker.
rate research
Read More
Internet of Things (IoT) applications drive the behavior of IoT deployments according to installed sensors and actuators. It has recently been shown that IoT deployments are vulnerable to physical interactions, caused by design flaws or malicious intent, that can have severe physical consequences. Yet, extant approaches to securing IoT do not translate the app source code into its physical behavior to evaluate physical interactions. Thus, IoT consumers and markets do not possess the capability to assess the safety and security risks these interactions present. In this paper, we introduce the IoTSeer security service for IoT deployments, which uncovers undesired states caused by physical interactions. IoTSeer operates in four phases (1) translation of each actuation command and sensor event in an app source code into a hybrid I/O automaton that defines an apps physical behavior, (2) combining apps in a novel composite automaton that represents the joint physical behavior of interacting apps, (3) applying grid-based testing and falsification to validate whether an IoT deployment conforms to desired physical interaction policies, and (4) identification of the root cause of policy violations and proposing patches that guide users to prevent them. We use IoTSeer in an actual house with 13 actuators and six sensors with 37 apps and demonstrate its effectiveness and performance.
This paper is the first thorough investigation into the coarsest notion of bisimilarity for the applied pi-calculus that is a congruence relation: open barbed bisimilarity. An open variant of labelled bisimilarity (quasi-open bisimilarity), better suited to constructing bisimulations, is proven to coincide with open barbed bisimilarity. These bisimilary congruences are shown to be characterised by an intuitionistic modal logic that can be used, for example, to describe an attack on privacy whenever a privacy property is violated. Open barbed bisimilarity provides a compositional approach to verifying cryptographic protocols, since properties proven can be reused in any context, including under input prefix. Furthermore, open barbed bisimilarity is sufficiently coarse for reasoning about security and privacy properties of cryptographic protocols; in constrast to the finer bisimilarity congruence, open bisimilarity, which cannot verify certain privacy properties.
Exploitation of heap vulnerabilities has been on the rise, leading to many devastating attacks. Conventional heap patch generation is a lengthy procedure, requiring intensive manual efforts. Worse, fresh patches tend to harm system dependability, hence deterring users from deploying them. We propose a heap patching system that simultaneously has the following prominent advantages: (1) generating patches without manual efforts; (2) installing patches without altering the code (so called code-less patching); (3) handling various heap vulnerability types; (4) imposing a very low overhead; and (5) no dependency on specific heap allocators. As a separate contribution, we propose targeted calling context encoding, which is a suite of algorithms for optimizing calling context encoding, an important technique with applications in many areas. The system properly combines heavyweight offline attack analysis with lightweight online defense generation, and provides a new countermeasure against heap attacks. The evaluation shows that the system is effective and efficient.
Concurrent constraint programming (ccp) is a well-established model for concurrency that singles out the fundamental aspects of asynchronous systems whose agents (or processes) evolve by posting and querying (partial) information in a global medium. Bisimilarity is a standard behavioural equivalence in concurrency theory. However, only recently a well-behaved notion of bisimilarity for ccp, and a ccp partition refinement algorithm for deciding the strong version of this equivalence have been proposed. Weak bisimiliarity is a central behavioural equivalence in process calculi and it is obtained from the strong case by taking into account only the actions that are observable in the system. Typically, the standard partition refinement can also be used for deciding weak bisimilarity simply by using Milners reduction from weak to strong bisimilarity; a technique referred to as saturation. In this paper we demonstrate that, because of its involved labeled transitions, the above-mentioned saturation technique does not work for ccp. We give an alternative reduction from weak ccp bisimilarity to the strong one that allows us to use the ccp partition refinement algorithm for deciding this equivalence.
The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynchs probabilistic bisimilarity for probabilistic automata. In this paper, we present a characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condons simple policy iteration on these games. The correctness of Condons approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in $textbf{UP} cap textbf{coUP}$ and textbf{PPAD}. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. The characterization of the probabilistic bisimilarity distance mentioned above crucially uses a dual presentation of the Hausdorff distance due to Memoli. As an additional contribution, in this paper we show that Memolis result can be used also to prove that the bisimilarity distance bounds the difference in the maximal (or minimal) probability of two states to satisfying arbitrary $omega$-regular properties, expressed, eg., as LTL formulas.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
