Ebook: Verification of Infinite-State Systems with Applications to Security

The recent years have brought a number of advances in the development of infinitestate verification, using techniques such as symbolic or parameterized representations, symmetry reductions, abstractions, constraint-based approaches, combinations of model checking and theorem proving. The active state of research on this topic provides a good time-point to increase impact by bringing together leading scientists and practitioners from these individual approaches.

The NATO Advanced Research Workshop “Verification of Infinite State Systems with Applications to Security VISSAS 2005”, which was held in Timişoara, România, on March 17–22, 2005, aimed to give an overview of the state of the art and of the current research directions, and to provide a forum for researchers interested in the development of mathematical techniques for the analysis of infinite state systems.

The success of this workshop was not only due to the excellent lectures, but also due to the participants taking part in the discussions at the workshop, the exchange of different views, and the recognition of the similarity of a number of different view points. These were some of the most important contributions of the workshop.

It is our pleasure to thank here all the people who helped to make the workshop a full success. This includes the lecturers, the participants, and the members of the organizing staff. Special thanks go to IeAT, the host of our workshop.

Finally, we would like to acknowledge the financial support received from NATO, and the excellent cooperation with IOS Press in the preparation of this volume.

March 2005, Edmund Clarke, Marius Minea, Ferucio Laurenţiu Ţiplea

In order to compute the reachability set of infinite-state models, one needs a technique for exploring infinite sequences of transitions in finite time, as well as a symbolic representation for the finite and infinite sets of configurations that are to be handled. The representation problem can be solved by automata-based methods, which consist in representing a set by a finite-state machine recognizing its elements, suitably encoded as words over a finite alphabet. Automata-based set representations have many advantages: They are expressive, easy to manipulate, and admit a canonical form.

In this survey, we describe two automata-based structures that have been developed for representing sets of numbers (or, more generally, of vectors): The Number Decision Diagram (NDD) for integer values, and the Real Vector Automaton (RVA) for real numbers. We discuss the expressiveness of these structures, present some construction algorithms, and give a brief introduction to some related acceleration techniques.

We give a short overview on the recent research activity on regular model checking, an automata-based framework for the automatic verification of infinitestate systems, and its application to the verification of programs with dynamic linked structures.

Cryptographic protocols are mandatory for garateeing security properties of open systems that communicate with their environment. The study of the semantic models and the algorithmic verification of these protocols is a chalenging and fascinating research topic that combines the theory of program and system semantics, automata theory, rewriting theory, logics and their decision problems, cryptography, complexity theory, ….

In this paper, we present some of the results developed at VERIMAG for the automatic verification of cryptographic protocols.

Model checking has been successfully employed for verification of industrial hardware systems. Recently, model checking techniques have also enjoyed limited success in verifying software systems, viz., device drivers. However, there are several hurdles which must be overcome before model checking can be used to handle industrial-scale software systems. This article reviews some of the prominent model checking techniques being used for verification of software and summarizes the existing challenges in the field.

We give an algorithmic calculus of the reachability relations on clock values defined by timed automata. Our approach is a modular one, by computing unions, compositions and reflexive-transitive closure (star) of “atomic” relations. The essential tool is a new representation technique for n-clock relations – the 2n-automata – and our strategy is to show the closure under union, composition and star of the class of 2n-automata that represent reachability relations in timed automata.

We have to resort to increasingly smaller specks of matter to store, process, and transport information because we have to reduce the physical dimensions of our devices and their power dissipation. At the same time we have to develop increasingly more powerful computers and more secure and reliable communication systems. Thus, sooner or later we have to build computers and communication systems based upon quantum effects and think about verification of their properties. Quantum information has special properties: the state of a quantum system cannot be measured or copied without disturbing it; quantum state can be entangled, two systems have a definite state though neither has a state of its own; superposition - we cannot reliably distinguish non-orthogonal states of a quantum system. In this paper we discuss the concepts of quantum states and measurements, present Bell states, and Bell's inequality.

Testing is the most commonly used method for debugging software. We survey here several techniques that are used for assisting the tester in generating a test suite that reflects his intuition about potential problems in the software. Then we show how to enfore and monitor these test cases.

We show that two published coin-flipping protocols are breakable in the sense that one of the parties can pre-determine the result of the coin-flip. The way in which the protocols fail is illustrative of subtle ways in which a protocol designer may combine secure cryptographic primitives - such as one-way functions and encryption - in a way that produces an insecure cryptographic protocol.

In the twenty-five years since its invention, model checking has evolved into a powerful framework for the analysis of computer hardware and software. The integration of model checkers into the industrial development chain has raised new methodological questions about model checking, including the use of model checkers to analyze underspecified or unknown systems and the truthfulness of positive verification results. In this paper, we survey recent technical approaches to these questions – temporal logic query solving and vacuity detection – both of which transcend the classical picture of model checking. We focus on temporal logic queries with unique strongest solutions, describe fragments of CTL and LTL query languages with this property, a symbolic query solving algorithm for CTL, and an application of query solving to vacuity detection.

The paper discusses some possible approaches to measuring security of timed and probabilistic models of systems. We discuss problems concerning the leak of information and the resistance of executions of security policies, and propose quantitative characteristics of security. Algorithmic questions related to the computation of these characteristics are formulated for finite transition models.

Security protocols are prescribed sequences of interactions between entities designed to provide various security services across distributed systems. Security protocols are often wrong due to the extremely subtle properties they are supposed to ensure. Deciding whether or not a security protocol assures secrecy is one of the main challenge in this area.

In this paper we survey the most important decidability and complexity results regarding the secrecy problem for various classes of security protocols, such as bounded protocols, finite-sessions protocols, normal protocols, and tagged protocols. All the results are developed under the same formalism. Several flawed statements claimed in the literature are corrected. Simplified proofs and reductions, as well as slight extensions of some known results, are also provided.

This paper presents a new contribution to the model-checking of multithreaded programs with recursive procedure calls, result passing between recursive procedures, dynamic creation of parallel processes, and synchronisation between parallel threads. To represent such programs accurately, we define the model SPAD that can be seen as the extension with synchronisation of the class PAD (the subclass of the rewrite systems PRS where parallel composition is not allowed in the lefthand sides of the rules). We consider in this paper the reachability problem of this model, which is undecidable. As in [BET03a,BET04], we reduce this problem to the computation of abstractions of the sets of execution paths of the program, and we propose a generic technique that can compute different abstractions (of different precisions and different costs) of these sets.

Traditional model checking produces one counterexample to illustrate a violation of a property by a model of the system. Some applications benefit from having all counterexamples, not just one. We call this set of counterexamples a scenario graph. In this paper we present two different algorithms for producing scenario graphs and explain how scenario graphs are a natural representation for attack graphs used in the security community.