In this talk, we present an efficient static analysis based on Abstract Interpretation that aims at proving the absence of run-time errors in embedded multi-threaded C programs. Our method is based on a singe-thread analysis, enriched to infer and propagate abstract thread interferences. We prove that our method is sound with respect to a sequentially consistent semantics but also some weakly consistent memory models. We also show how partitioning techniques can model mutual exclusion and thread priorities. Finally, we present our prototype, AstréeA, based on the Astrée analyzer, as well as preliminary experimental results analyzing a large industrial program. AstréeA's web site is at http://www.astreea.ens.fr/

Consider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic solution that needs neither a pre-existing protocol description nor manual annotation of source code. First, symbolically execute the C program to obtain symbolic descriptions for the network messages sent by the protocol. Second, apply algebraic rewriting to obtain a process calculus description. Third, run an existing protocol analyser (ProVerif) to prove security properties or find attacks. We analyse only a single execution path, so our results are limited to protocols with no significant branching. Our results provide the first computationally sound verification of weak secrecy and authentication for (single execution paths of) C code.

Computer systems are often difficult to debug and understand. A common way of gaining insight into system behavior is to inspect execution logs and documentation. Unfortunately, manual inspection of logs is an arduous process and documentation is often incomplete and out of sync with the implementation. In this talk I will describe Synoptic, a tool that helps developers by inferring a concise and accurate system model. Unlike most related work, Synoptic does not require developer-written scenarios, specifications, negative execution examples, or other complex user input. Synoptic processes the logs most systems already produce and requires developers only to specify a set of regular expressions for parsing the logs.

Synoptic has two unique features. First, the model it produces satisfies three kinds of temporal invariants mined from the logs, improving accuracy over related approaches. Second, Synoptic uses refinement and coarsening to explore the space of models. This improves model efficiency and precision, compared to using just one approach. We empirically evaluated Synoptic through two user experience studies and found that Synoptic-generated models helped developers to verify known bugs, diagnose new bugs, and increase their confidence in the correctness of their systems. None of the developers in our evaluation had a background in formal methods but were able to easily use Synoptic and detect implementation bugs in as little as a few minutes.

Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specifying with abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these constructs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and very well integrated inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.

This feature has been extensively used in formalization projects about mathematics (algebra, equational theories) and programming languages. I'll give an overview of its current applications and the current research directions: improvements of unification and the relation of type classes and logic programming.

It is notoriously difficult to make distributed systems reliable. This becomes even harder in the case of the widely-deployed systems that are heterogeneous (multiple implementations) and federated (multiple administrative entities). The set of routers in charge of the Internet's inter-domain routing is a prime example of such a system.

We argue that a key step in making these systems reliable is the need to automatically explore the system behavior to check for potential faults. In this talk, I will describe the design and implementation of DiCE, a system for online testing of heterogeneous and federated distributed systems. DiCE runs concurrently with the production system by leveraging distributed checkpoints and isolated communication channels. DiCE orchestrates the exploration of relevant system states by controlling the inputs that drive system actions. While respecting privacy among different administrative entities, DiCE detects faults by checking for violations of properties that capture the desired system behavior. We demonstrate the ease of integrating DiCE with a BGP router and a DNS server, the building blocks of two vital services in the Internet. Our evaluation in the testbed shows that DiCE quickly and successfully detects three important classes of faults, resulting from configuration mistakes, policy conflicts and programming errors.

Joint work with Marco Canini, Vojin Jovanovic, Daniele Venzano, Gautam Kumar, Dejan Novakovic, Boris Spasojevic, and Olivier Crameri.

Despite the benefits of cloud computing, its potential customers are concerned with data mismanagement risks that stem from the accidental or intentional activity of cloud software administrators. Although trusted computing could provide customers with stronger guarantees that cloud services are more resilient to these threats, this technology is ill-suited for the cloud since it exposes too many internal details of the cloud infrastructure, and hinders fault tolerance and load-balancing flexibility. To solve these limitations and enable the design of trustworthy cloud services, we present a system called Excalibur. Excalibur provides policy-sealed data, a new trusted computing primitive which enables data to be sealed (i.e., encrypted to a customer-defined policy) such that it can only be unsealed (i.e., decrypted) by nodes whose configurations match the policy; the configuration of nodes is bound to trusted computing hardware, making the primitive resilient to the actions of cloud administrators. Excalibur uses novel cryptographic protocols, and makes judicious use of existing trusted computing primitives. To demonstrate that Excalibur is practical, we used it in the Eucalyptus open-source cloud platform in order to provide customers with greater confidence that data is processed exclusively by the nodes that meet their preferences.

The ASCENS project (http://www.ascens-ist.eu/) researches foundations of and software-engineering methods for ensembles - distributed autonomous systems operating in complex environments which can dynamically adapt to changes in their environment or requirements. We will discuss the notions of adaptation, awareness and emergence which play an important role in the development of ensembles. These terms will be made precise by giving a system model for ensembles on which a mathematical theory of adaptation and awareness can be based. Using this theory we can precisely distinguish different kinds of adaptation, such as adaptation to environment, network or goals, and we can discuss how adaptation, awareness and self-awareness are related.

The automated generation of test cases for heap allocated, complex, structures is particularly difficult. Various state of the art tools tackle this problem by bounded exhaustive exploration of potential test cases, using constraint solving mechanisms based on techniques such as search, model checking, symbolic execution and combinations of these.

In this talk, we will describe some technical issues associated with effectively generating bounded exhaustive test suites using constraint solving ( e.g. the elimination of isomorphic structures), and how these are tackled in practice. We will also present a technique for improving the generation, which employs a test criterion for pruning the search: a test criterion is incorporated in the constraint based mechanism so that the exploration of potential test cases can be pruned without missing coverable classes of inputs. We present the technique, together with some case studies illustrating its performance for some black box testing criteria.

In the talk I will present a series of abstractions that can be used to obtain approximated verification algorithms for parameterized systems with global conditions and different types of topology (ordered/unordered arrays, trees, graphs). The verification algorithms perform a symbolic exploration of a possibly infinite-state space and exploit the theory of well-quasi orderings for ensuring the theoretical termination of the analysis.

Model checking based on Craig's interpolants ultimately relies on efficient engines, such as SMT-Solvers, to log proofs of unsatisfiability and to derive the desired interpolant by means of a set of algorithms known in literature. These algorithms, however, are designed for proofs that do not contain mixed predicates. In this talk I will present a technique for transforming the propositional proof produced by an SMT-Solver in such a way that mixed predicates are eliminated. There exists a number of cases in which mixed predicates arise as a consequence of state-of-the-art solving procedures (e.g., lemma on demand, theory combination, etc.). In such cases our technique can be applied to allow the reuse of known interpolation algorithms. I will then present a new approach to proof reduction, situated among the purely post-processing methods. The main idea is to reduce the proof size by eliminating redundancies of occurrences of pivots along the proof paths. This is achieved by matching and rewriting local contexts into simpler ones. In our approach, rewriting can be easily customized in the way local contexts are matched, in the amount of transformations to be performed, or in the different application of the rewriting rules. I will provide experimental evaluation of our technique on a set of SMT and SAT benchmarks, which shows considerable reduction in the proofs size.

Cyber Physical Systems (CPS) is a term broadly used to define systems in which the cyber world consisting of computation and communication is tightly connected to the physical world. These systems have applications in Automotives, Medical Devices, Aeronautics and Robotics among several other areas. These systems are often deployed in safety-critical systems and hence their reliable performance is of utmost importance.

Verifying CPS is challenging due to the presence of continuous components modeling the physical world. The complexity of verification of these systems increases with the complexity of the continuous components, and is undecidable for a relatively simple class of systems. In fact, the problem of computing one-step successors which is a basic step in various state space exploration based verification techniques is undecidable for complex dynamical systems. Hence, the verification of these systems relies on developing techniques which can compute good approximations of these systems efficiently. I will describe some of my work on approximation techniques for the verification of CPS. In particular, I will talk about a technique for approximating general CPS by polynomial systems, and some results on how this process of approximation can be efficiently automated. I will also describe a counter-example guided abstraction refinement technique for hybrid systems which automatically refines an abstraction when it is not sufficient to prove the correctness of the system. I will discuss various cyber physical systems which have been analysed using these techniques.

We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints on concurrent systems.The problem of synthesizing a distributed controller is, in general, undecidable, and the local knowledge of the processes may not directly suffice to control them to achieve the global constraint. We calculate when processes can decide, autonomously, to take or block an action so that the global constraint will not be violated. When the separate processes cannot make this decision alone, it may be possible to coordinate several processes in order to achieve more knowledge together and make combined decisions. A fixed coordination will severely degrade the concurrency; thus, the coordinations we use are temporary. Since the overhead for such coordinations is expensive, we strive to minimize their number, again using model checking. We show how this framework is applied to the design of controllers that guarantee a priority policy among transitions.

Invariants play a key role in verifying properties of imperative programs. Inductive reasoning is essential to verifying properties of recursive programs. Relationship between derivation of loop invariants and speculation of lemmas in inductive reasoning is explored. Abstraction is an effective heuristic for approximating program behavior in order to derive invariants. Interaction among developing abstractions, inductive reasoning, and generating invariants is investigated.

One of the key challenges in automated software verification is obtaining a conservative, yet sufficiently precise understanding of the contents of data structures in the heap. A particularly important and widely-used class of heap data structures is containers, which support operations such as inserting, retrieving, removing, and iterating over elements. Examples of containers include arrays, lists, vectors, sets, maps, stacks, queues, etc.

In this talk, I will describe a sound, precise, scalable, and fully-automatic static analysis technique for reasoning about the contents of container data structures. This technique is capable of tracking position-value and key-value correlations, supports reasoning about arbitrary nestings of these data structures, and integrates container reasoning directly into a heap analysis, allowing, for the first time, the verification of complex programs that manipulate heap objects through container data structures. More specifically, I will describe a symbolic heap abstraction that augments a graph representation of the heap with logical formulas and that reduces some of the difficulty of heap reasoning to standard logic operations, such as existential quantifier elimination and satisfiability. I will present experimental results demonstrating that our technique is very useful for verifying memory safety in complex heap- and container-manipulating C and C++ programs that use arrays and other container data structures from the STL and QT libraries.

A path-sensitive static analysis considers each possible execution path through a program separately, potentially yielding much more precise results than an analysis that makes fewer distinctions among paths. While precise path-sensitive reasoning is known to be necessary to prove many interesting facts about programs, fully path-sensitive analyses have not scaled well because standard representations of program paths quickly grow out of control.

In this talk, I will describe two techniques that allow path-sensitive program analyses to scale. I will first introduce on-line constraint simplification, which eliminates redundant subparts of logical formulas used to distinguish execution paths. In practice, the formulas used to describe program paths are highly redundant; thus, techniques for keeping path formulas concise can have a dramatic impact on analysis scalability. A second, complementary technique reduces formula size even further: Because static analyses are typically only interested in answering may (i.e., satisfiability) and must (i.e., validity) queries, I will show how to extract from the original path formulas a pair of satisfiabilty- and validity-preserving formulas that contain many fewer variables and that are as good as the original path formula for answering may and must queries about the program. I will demonstrate that these techniques allow a fully path-sensitive analysis to scale to very large, multi-million line programs for the first time.

Constraint solvers such as Boolean SAT or modular arithmetic solvers are increasingly playing a key role in the construction of reliable and secure software.

In this talk, I will present two solvers STP and HAMPI. STP is a solver for the quantifier-free theory of bit-vectors and arrays, a theory whose satisfiability problem is NP-complete. STP has been used in developing a variety of new software engineering techniques from areas such as formal methods, program analysis and testing. STP enabled a new and exciting testing technique known as Concolic testing. STP-enabled Concolic testers have been used to find hundreds of previously unknown errors in Unix utilities, C/C++ libraries, media players, and commercial software, some with approximately a million lines of code. HAMPI is a solver for a rich theory of equality over bounded string variables, bounded regular expressions and context-free grammars, another theory whose satisfiability problem is NP-complete. HAMPI is primarily aimed at analysis of string-manipulating programs such as web applications and scripts. HAMPI has been used to find many unknown SQL injection vulnerabilities in applications with more than 100,000 lines of PHP code using static and dynamic analysis.

I will discuss the techniques that make these solvers scale to formulas with millions of variables and constraints derived from real-world software engineering applications. I will also discuss some related theoretical results. Finally, I will talk about what the future for solvers might look like with a focus on multi-cores and programming language design.

Software is constantly modified during its life cycle, posing serious risks because changes might not behave as expected or might introduce erroneous side effects. Regression testing can be used to identify existing functionality broken by changes, but it does not necessarily discover new effects introduced by changes. To test these new effects, developers must augment the existing test suite (i.e., assess this test suite and create new tests as needed).

In this talk, I will present my work on change-effects analysis, a new kind of program analysis that enables test-suite augmentation and program merging, among other tasks. Change-effects analysis uses dependence analysis and symbolic execution to compute the conditions under which the program state is modified by a change and this effect propagates through the rest of the program. These conditions describe not only which program elements are affected by changes but also how those elements are affected. I will also discuss a new method for symbolically executing program paths in groups instead of individually, which improves the scalability of change-effects analysis and has many other exciting applications. I will present empirical results showing that change-effects analysis is much more effective than traditional methods for testing changes and detecting conflicts during program merging. I will conclude this talk by discussing challenges and opportunities for future research on change-effects analysis.

We show how to extract sensitive cryptographic keys from a variety of commercially available tamper resistant cryptographic security tokens and smartcards, exploiting vulnerabilities in their RSA PKCS#11 based APIs. The attacks are performed by Tookan, an automated tool we have developed, which reverse-engineers the particular token in use to deduce its functionality, constructs a model of its API for a model checker, and then executes any attack trace found by the model checker directly on the token. We describe the operation of Tookan and give results of testing the tool on 18 commercially available tokens: 10 were vulnerable to attack, while the other 8 had severely restricted functionality. Response from manufacturers has varied from registering the vulnerability with MITRE and announcing a patch programme to a complete lack of response. We discuss how Tookan may be used to verify patches to insecure devices, and give a secure configuration that we have implemented in a patch to a software token simulator. This is the first such configuration to appear in the literature that does not require any new cryptographic mechanisms to be added to the standard. We comment on lessons for future key management APIs.

Joint work with Matteo Bortolozzo, Matteo Centenaro, and Riccardo Focardi.

Formal verification is described as the branch of computer science that formally establishes the correctness of systems. Generally, formal verification consists of suitably formalizing the system, followed by verifying it. In this talk, I shall describe two different ways how formal verification may contribute to other fields of computer science, beyond proving correctness.

Firstly, the process of formalization leads to interesting insights about the system, often ignored while designing the system. These insights may produce new, interesting ideas in designing more efficient systems, or theoretically proving properties about the system. As an example, I shall describe how formal verification of software transactional memories led to interesting notions like permissiveness, notions of correctness parametrized by relaxed memory models, and transactional prediction.

Secondly, I shall argue that the beautiful techniques at the core of efficient verification can also be exported to other fields. As an example, I shall show how to use abstraction-refinement techniques, commonly used to prove correctness of programs, to build efficient static schedulers for the cloud.

Managed languages such as Java and C# are being considered for use in hard real-time systems. A hurdle to their widespread adoption is the lack of garbage collection algorithms that offer predictable space-and-time performance in the face of fragmentation. This presentation starts with my Stopless algorithm, which was the world's first lock-free concurrent copying real-time garbage collector, and continues through the evolution of this approach. My subsequent Chicken and Clover algorithms improve on the Stopless design with opportunistic and probabilistic guarantees respectively. Finally, I present Schism, the world's first wait-free concurrent copying garbage collector with proven time and space bounds. An implementation of these algorithms in two production-strength compiler infrastructures (Microsoft Bartok and Fiji VM) will be discussed, and a thorough evaluation of the collectors' throughput and predictability characteristics will be presented. All four algorithms are shown to exhibit predictability and throughput that exceeds that of previous approaches to concurrent defragmentation.

In security and compliance, it is often necessary to ensure that agents and systems comply to complex policies. An example from financial reporting is the requirement that every transaction t of a customer c, who has within the last 30 days been involved in a suspicious transaction t', must be reported as suspicious within 2 days. We present an approach to monitoring such policies formulated in an expressive fragment of metric first-order temporal logic. We also report on case studies in security and compliance monitoring and use these to evaluate both the suitability of this fragment for expressing complex, realistic policies and the efficiency of our monitoring algorithm.(Joint work with Felix Klaedtke and Samuel Mueller)