Abstract This work develops a type of local analysis that can prove concurrent systems deadlock free. As opposed to examining the overall behaviour of a system, local analysis consists of examining the behaviour of small parts of the system to yield a given property. We analyse pairs of interacting components to approximate system reachability and propose a new sound but incomplete/approximate framework that checks deadlock and local-deadlock freedom. By replacing exact reachability by this approximation, it looks for deadlock (or local-deadlock) candidates, namely, blocked (locally-blocked) system states that lie within our approximation. This characterisation improves on the precision of current approximate techniques. In particular, it can tackle non-hereditary deadlock-free systems, namely, deadlock-free systems that have a deadlocking subsystem. These are neglected by most approximate techniques. Furthermore, we demonstrate how SAT checkers can be used to efficiently implement our framework, which, typically, scales better than current techniques for deadlock-freedom analysis. This is demonstrated by a series of practical experiments.

We present an extension of FDR, the model checker for the process algebra CSP, that exploits symmetry to reduce the size of the state space searched. We define what it means for a process to be symmetric with respect to a group of permutations on the transition labels. We factor the state space of the search by symmetry equivalence, mapping each state to a representative of its equivalence class, thereby considering all symmetric states together. We prove a powerful syntactic result, identifying conditions under which a process will be symmetric in a particular type. We show how to implement such a search using the powerful technique of supercombinators used in the implementation of FDR: we identify conditions on a supercombinator for it to be symmetric and explain how to apply a permutation to a state. Finally, we present a novel efficient technique for calculating representatives of equivalence classes, which normally finds unique representatives; our experiments suggest that this technique typically works faster than other techniques and in particular scales better.

This article investigates how the use of approximations can make the formal verification of concurrent systems scalable. We propose the idea of synchronisation analysis to automatically capture global invariants and approximate reachability. We calculate invariants on how components participate on global system synchronisations and use a notion of consistency between these invariants to establish whether components can effectively communicate to reach some system state. Our synchronisation-analysis techniques try to show either that a system state is unreachable by demonstrating that components cannot agree on the order they participate in system rules or that a system state is unreachable by demonstrating components cannot agree on the number of times they participate on system rules. These fully automatic techniques are applied to check deadlock and local-deadlock freedom in the PairStatic framework. It extends Pair (a recent framework where we use pure pairwise analysis of components and SAT checkers to check deadlock and local-deadlock freedom) with techniques to carry out synchronisation analysis. So, not only can it compute the same local invariants that Pair does, it can leverage global invariants found by synchronisation analysis, thereby improving the reachability approximation and tightening our verifications. We implement PairStatic in our DeadlOx tool using SAT/SMT and demonstrate the improvements they create in checking (local) deadlock freedom.

Abstract We present and compare several algorithms for computing the maximal strong bisimulation, the maximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulation of a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well as the operational semantics of programs in other languages with operational semantics described by such GLTSs and relying only on observational equivalence. They can therefore be used to combat the space explosion problem faced in explicit model checking for such languages. We concentrate on algorithms which work efficiently when implemented rather than on ones which have low asymptotic growth.

Abstract Many security protocols are built as the composition of an application-layer protocol and a secure transport protocol, such as TLS. There are several approaches to proving the correctness of such protocols. One popular approach is verification by abstraction, in which the correctness of the application-layer protocol is proven under the assumption that the transport layer satisfies certain properties, such as confidentiality. Following this approach, we adapt the strand spaces model in order to analyse application-layer protocols that depend on secure transport protocols; we consider both bilaterally and unilaterally authenticating secure transport protocols, such as bilateral and unilateral TLS. The paper’s main contribution is a proof of the model’s soundness. In particular, we prove that, subject to a suitable independence assumption, if there is an attack against the application-layer protocol when layered on top of a particular secure transport protocol, then there is an attack against the abstracted model of the application-layer protocol. In contrast to existing work in this area, the independence assumption consists of eight statically checkable conditions, meaning that it is not necessary to consider all possible runs of the protocol.

Technology is present in every area of our lives and, for many, life without it has become unthinkable. As a consequence of this dependence and the extent to which technology devices (computers, tablets and smartphones) are being used for work and social activities, a clear coupling between devices and their owners can now be observed. By coupling, we specifically refer to the fact that information present on a person's device, be it user-generated or created by the native OS, can produce great insight into their life. In this paper, we look to exploit this coupling to investigate whether connections between technology devices recorded in system log-files, can be used to make inferences about the social relationships between device owners. A key motivation here is to better understand and elucidate the privacy risks associated with the digital footprints that we as humans (often inadvertently) create. Our work draws upon Social Network Analysis and basic Computer Forensics to develop and achieve the inference goals. From our preliminary experimentation, we demonstrate that human social relationships can indeed be inferred even within our limited initial scope. To further investigate the level of privacy exposure from technology-level links, we outline a more comprehensive plan of experimentation that will be conducted in future work.