Communication networks are quintessential concurrent and distributed systems, posing verification challenges concerning network protocols, reliability, resilience and fault-tolerance, and security. While techniques based on logic and process calculi have been employed in the verification of various protocols, there is a mismatch between the abstractions used in these approaches and the essential structure of networks. In particular, the formal models do not accurately capture the organization of networks in terms of (fast but dumb) table-based switches forwarding structured messages, with intelligence/control located only at the end-points. To bridge this gap, we propose an extension of the axiomatic basis of communication proposed by Karsten et al. In this paper, a simple model of abstract switches and table-based prefix rewriting is characterized axiomatically using temporal logic. This formulation is able to address reconfigurations over time of the network. We illustrate our framework with simple examples drawn from SDNs, IPv6 mobility and anonymous routing protocols.
Variants of the must testing approach have been successfully applied in service oriented computing for analysing the compliance between (contracts exposed by) clients and servers or, more generally, between two peers. It has however been argued that multiparty scenarios call for more permissive notions of compliance because partners usually do not have full coordination capabilities. We propose two new testing preorders, which are obtained by restricting the set of potential observers. For the first preorder, called uncoordinated, we allow only sets of parallel observers that use different parts of the interface of a given service and have no possibility of intercommunication. For the second preorder, that we call individualistic, we instead rely on parallel observers that perceive as silent all the actions that are not in the interface of interest. We have that the uncoordinated preorder is coarser than the classical must testing preorder and finer than the individualistic one. We also provide a characterisation in terms of decorated traces for both preorders: the uncoordinated preorder is defined in terms of must-sets and Mazurkiewicz traces while the individualistic one is described in terms of classes of filtered traces that only contain designated visible actions and must-sets.
This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1) an on-the-fly lazy predicate abstraction technique for BIP; (2) a novel explicit state reduction technique, called simultaneous set reduction, that can be combined with lazy predicate abstraction to prune the search space of abstract reachability analysis; (3) a prototype tool implementing all the proposed techniques. We also conduct thorough experimental evaluation, which demonstrates the effectiveness of our proposed approach.
Fault diagnosis is becoming increasingly important and difficult with the growing pervasiveness and complexity of computer systems. We propose in this paper a general semantic framework for fault ascription, a precise form of fault diagnosis that relies on counterfactual analysis for identifying necessary and sufficient causes of faults in component-based systems. Our framework relies on configuration structures to handle concurrent systems, partial and distributed observations in a uniform way. It defines basic conditions for a counterfactual analysis of necessary and sufficient causes, and it presents a refined analysis that conforms to our basic conditions while avoiding various infelicities.
Secure two-party computation allows two distrusting parties to compute a function, without revealing their inputs to each other. Traditionally, the security properties desired in this context, and the corresponding security proofs, are based on a notion of simulation, which can be symbolic or computational. Either way, the proofs of security are intricate, requiring first to find a simulator, and then to prove a notion of indistinguishability. Furthermore, even for classic protocols such as Yao’s (based on garbled circuits and oblivious transfer), we do not have adequate symbolic models for cryptographic primitives and protocol roles, that can form the basis for automated security proofs. We propose new models in applied pi-calculus to address these gaps. Our contributions, formulated in the context of Yao’s protocol, include: an equational theory for specifying the primitives of garbled computation and oblivious transfer; process specifications for the roles of the two parties in Yao’s protocol; definitions of security that are more clear and direct: result integrity, input agreement (both based on correspondence assertions) and input privacy (based on observational equivalence). We put these models together and illustrate their use with ProVerif, providing a first automated verification of security for Yao’s two-party computation protocol.
We study parameterized verification problems for concurrent systems with data enriched with a permission model for invoking remote services. Processes are modelled via register automata. Communication is achieved by rendez-vous with value passing. Permissions are represented as graphs with an additional conflict relation to specify incompatible access rights. The resulting model is inspired by communication architectures underlying operating systems for mobile devices. We consider decision problems involving permission violations and data tracking formulated for an arbitrary number of processes and use reductions to well structured transition systems to obtain decidable fragments of the model.
As JavaScript is highly dynamic by nature, static information flow analyses are often too coarse to deal with the dynamic constructs of the language. To cope with this challenge, we present and prove the soundness of a new hybrid typing analysis for securing information flow in a JavaScript-like language. Our analysis combines static and dynamic typing in order to avoid rejecting programs due to imprecise typing information. Program regions that cannot be precisely typed at static time are wrapped inside an internal boundary statement used by the semantics to interleave the execution of statically verified code with the execution of code that must be dynamically checked.
The security validation of practical computer systems calls for the ability to specify and verify information flow policies that are dependent on data content. Such policies play an important role in concurrent, communicating systems: consider a scenario where messages are sent to different processes according to their tagging. We devise a security type system that enforces content-dependent information flow policies in the presence of communication and concurrency. The type system soundly guarantees a compositional noninterference property. All theoretical results have been formally proved in the Coq proof assistant [9].
Client-side JavaScript programs often interact with the web page into which they are included, as well as with the browser itself, through APIs such as the DOM API, the XMLHttpRequest API, and the W3C Geolocation API. Precise reasoning about JavaScript security must therefore take API invocation into account. However, the continuous emergence of new APIs, and the heterogeneity of their forms and features, renders API behavior a moving target that is particularly hard to capture. To tackle this problem, we propose a methodology for modularly extending sound JavaScript information flow monitors with a generic API. Hence, to verify whether an extended monitor complies with the proposed noninterference property requires only to prove that the API satisfies a predefined set of conditions. In order to illustrate the practicality of our methodology, we show how an information flow monitor-inlining compiler can take into account the invocation of arbitrary APIs, without changing the code or the proofs of the original compiler. We provide an implementation of such a compiler with an extension for handling a fragment of the DOM Core Level 1 API. Furthermore, our implementation supports the addition of monitor extensions for new APIs at runtime.
We study the search problem for optimal schedulers for the linear temporal logic (LTL) with future discounting. The logic, introduced by Almagor, Boker and Kupferman, is a quantitative variant of LTL in which an event in the far future has only discounted contribution to a truth value (that is a real number in the unit interval [0, 1]). The precise problem we study---it naturally arises e.g. in search for a scheduler that recovers from an internal error state as soon as possible---is the following: given a Kripke frame, a formula and a number in [0, 1] called a margin, find a path of the Kripke frame that is optimal with respect to the formula up to the prescribed margin (a truly optimal path may not exist). We present an algorithm for the problem; it works even in the extended setting with propositional quality operators, a setting where (threshold) model-checking is known to be undecidable.
We extend π -calculus with real-time by adding clocks and assigning time-stamps to actions. The resulting formalism, timed π -calculus, provides a simple and novel way to annotate transition rules of π -calculus with timing constraints. Timed π -calculus is an expressive way of describing mobile, concurrent, real-time systems in which the behavior of systems is modeled by finite or infinite sequences of timed events. We develop an operational semantics as well as a notion of timed bisimilarity for the proposed language. We present the properties of timed bisimilarity; in particular, expansion theorem for real-time, concurrent, mobile processes is investigated.
A novel approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each individual gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at static time either yields composed services enjoying the required properties or detects the individuals responsible for possible violations. To do that in the asynchronous case we resort to techniques from Operational Research.
Database replication is a technique employed to enhance both performance and availability of database systems. The Deferred Update Replication (DUR) technique offers strong consistency (i.e. serializability) and uses an optimistic concurrency control with a lazy replication strategy relying on atomic broadcast communication. Due to its good performance, DUR has been used in the construction of several database replication protocols and is often chosen as a basic technique for several extensions considering modern environments. The correctness of the DUR technique, i.e. if histories accepted by DUR are serializable, has been discussed by different authors in the literature. However, a more comprehensive discussion involving the completeness of DUR w.r.t. serializability was lacking. As a first contribution, this paper provides an operational semantics of the DUR technique which serves as foundation to reason about DUR and its derivatives. Second, using this model the correctness of DUR w.r.t. serializability is shown. Finally, we discuss the completeness of DUR w.r.t. serializability and show that for any serializable history there is an equivalent history accepted by DUR. Moreover, we show that transactions aborted by DUR could not be accepted without changing the order of already committed transactions.
Static analysis techniques based on session types discern concurrent programs that ensure the fidelity of protocol sessions – for each input (output) end point of a session there is exactly an output (input) end point available – being expressive enough to represent the standard $$\pi $$ -calculus and several typing disciplines. More advanced type systems, enforcing properties as deadlock-freedom or even progress, sensibly reduce the set of typed processes, thus mining the expressiveness of the analysis. Herein, we propose a first step towards a compromise solution to this problem: a session based type checking algorithm that releases some deadlocks (when co-actions on the same channel occur in sequence in a thread). This procedure may help the software development process: the typing algorithm detects a deadlock, but instead of rejecting the code, fixes it by looking into the session types and producing new safe code that obeys the protocols and is deadlock-free.
We study two operational semantics for relaxed memory models. Our first formalization is based on the notion of write-buffers which is pervasive in the memory models literature. We instantiate the (Total Store Ordering) TSO and (Partial Store Ordering) PSO memory models in this framework. Memory models that support more aggressive relaxations (e.g. read-to-read reordering) are not easily described with write-buffers. Our second framework is based on a general notion of speculative computation. In particular we allow the prediction of function arguments, and execution ahead of time (e.g. by branch prediction). While technically more involved than write-buffers, this model is more expressive and can encode all the Sparc family of memory models: TSO, PSO and (Relaxed Memory Ordering) RMO. We validate the adequacy of our instantiations of TSO and PSO by formally comparing their write-buffer and speculative formalizations. The use of operational semantics techniques is paramount for the tractability of these proofs.
Useful security properties arise from sealing data to specific units of code. Modern processors featuring Intel’s TXT and AMD’s SVM achieve this by a process of measured and protected execution. Only code which has the correct measurement can access the data, and this code runs in an environment protected from observation and interference. We present a modelling language with primitives for protected execution, along with its semantics. We characterise an attacker who has access to all the capabilities of the hardware. In order to achieve automatic analysis of systems using protected execution without attempting to search an infinite state space, we define transformations that reduce the number of times the attacker needs to use protected execution to a pre-determined bound. Given reasonable assumptions we prove the soundness of the transformation: no secrecy attacks are lost by applying it. We then describe using the StatVerif extensions to ProVerif to model the bounded invocations of protected execution. We show the analysis of realistic systems, for which we provide case studies.
Modal transition systems are an elegant way to formalise the design process of a system through refinement and composition. Here we propose to adapt this methodology to asynchronous composition via Petri nets. The Petri nets that we consider have distinguished labels for inputs, outputs, internal communications and silent actions and "must" and "may" modalities for transitions. The input/output labels show the interaction capabilities of a net to the outside used to build larger nets by asynchronous composition via communication channels. The modalities express constraints for Petri net refinement taking into account observational abstraction from silent transitions. Modal I/O-Petri nets are equipped with a modal transition system semantics. We show that refinement is preserved by asynchronous composition and by hiding of communication channels. We study compatibility properties which express communication requirements for composed systems and we show that these properties are decidable, they are preserved in larger contexts and also by modal refinement. On this basis we propose a methodology for the specification of distributed systems in terms of modal I/O-Petri nets which supports incremental design, encapsulation of components, stepwise refinement and independent implementability.
A novel, scalable, on-the-fly model-checking procedure is presented to verify bounded PCTL properties of selected individuals in the context of very large systems of independent interacting objects. The proposed procedure combines on-the-fly model checking techniques with deterministic mean-field approximation in discrete time. The asymptotic correctness of the procedure is shown and some results of the application of a prototype implementation of the FlyFast model-checker are presented.
Modular and local reasoning about object-oriented programs has been widely studied for programing languages such as C# and Java. Once source programs have been proven, the next verification challenge is to ensure that the code produced by the compiler is correct. Since verifying a compiler can be extremely complex, this paper uses proof-transforming compilation , an alternative approach which automatically generates certificates , a bytecode proof, from proofs in the source language. The paper develops a bytecode logic using separation logic, and proof translation from proofs of object-oriented programs to bytecode. The translation also handles proofs for concurrent programs. The bytecode logic and the proof transformation are proven sound.
Information-flow control (IFC) is a security mechanism conceived to allow untrusted code to manipulate sensitive data without compromising confidentiality. Unfortunately, untrusted code might exploit some covert channels in order to reveal information. In this paper, we focus on the LIO concurrent IFC system. By leveraging the effects of hardware caches (e.g., the CPU cache), LIO is susceptible to attacks that leak information through the internal timing covert channel. We present a resumption-based approach to address such attacks. Resumptions provide fine-grained control over the interleaving of thread computations at the library level. Specifically, we remove cache-based attacks by enforcing that every thread yield after executing an “instruction,” i.e., atomic action. Importantly, our library allows for porting the full LIO library—our resumption approach handles local state and exceptions, both features present in LIO. To amend for performance degradations due to the library-level thread scheduling, we provide two novel primitives. First, we supply a primitive for securely executing pure code in parallel. Second, we provide developers a primitive for controlling the granularity of “instructions”; this allows developers to adjust the frequency of context switching to suit application demands.
