Antoine Miné, Junior researcher, École Normale Supérieure, Paris, France
Time and place:
3:00pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Misha Aizatulin, PhD Student, Open University, United Kingdom
Time and place:
3:00pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Ivan Beschastnikh, PhD candidate, University of Washington, USA
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.
Time and place:
10:45am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Matthieu Sozeau, PhD Student, INRIA Rocquencourt, France
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Dejan Kostic, Assistant Professor, Ecole Polytechnique Federale de Lausanne, Switzerland
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Rodrigo Rodrigues, Assistant Research Professor, Max Planck Institute for Software Systems, Germany
Time and place:
3:00pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Martin Wirsing (in cooperation with Matthias Hoelzl), Professor, Ludwig-Maximilians University of München, Germany
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Nazareno Aguirre, Professor, Universidad Nacional de Río IV, Argentina
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Reinhard Wilhelm, Professor, Saarland University, Germany
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Giorgio Delzanno, Associate Professor, Università di Genova, Italia
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Natasha Sharygina, Assistant Professor, Università della Svizzera Italiana, Lugano, Switzerland
Time and place:
10:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Pavithra Prabhakar, PhD Student, University of Illinois at Urbana Champaign, USA
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Doron Peled, Professor, Bar Ilan University, Israel
Time and place:
3:30pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Deepak Kapur, Professor, University of New Mexico, USA
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Isil Dillig, PhD Student, Stanford University, USA
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Thomas Dillig, PhD Student, Stanford University, USA
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Vijay Ganesh, Postdoctoral Scholar, MIT Cambridge, MA, USA
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Raul Santelices, PhD Student, Georgia Institute of Technology, USA
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Graham Steel, Researcher, INRIA Rocquencourt, France
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Vasu Singh, Postdoctoral Scholar, Institute of Science and Technology (IST)
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.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Filip Pizlo, PhD Student, Purdue University, USA
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
David Basin, Professor, ETH Zurich, Switzerland
Time and place:
3:00pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain