Sriram Rajamani, , Microsoft, India
We present work by the RSE group at MSR India. We start by describing Yogi, a property checker that combines static and dynamic analysis. Then, we move beyond verification and testing and look at broader problems. Program Analyses either static or dynamic have traditionally analyzed only code. However, we have a lot of data about our software--ranging from data about our development processes, including bug databases and version control, to data from profiles of runs, to data about how users use the software. If we combine analysis of the program together with analysis of such data, we can solve very interesting new problems. We present 3 such tools based on this general theme:
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Francesco Logozzo, , Microsoft, USA
I will discuss the goals and the internals of Clousot, the static analyzer based on abstract interpretation that we have been developing at MSR in the last few years.
Clousot is the "official" static checker of the CodeContracts project. CodeContracts allow the programmer to specify Contracts (preconditions, postconditions and object invariant) in a language-agnostic way, without requiring any change in compiler, platform, IDE, ... and in general to the usual routine professional programmer are so used to. Clousot integrates in the IDE and it is (fast enough to) run as a compilation step.
Unlike previous contract verifiers Clousot *is not* based on a theorem prover, but on abstract interpretation. This gives a set of advantages, the most important being:
Clousot can be downloaded for free as part of the CodeContracts tools at http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx (Commercial license) and http://research.microsoft.com/en-us/projects/contracts/ (Academic license).
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Roberto Bagnara, , University of Parma, Italy
Time and place:
11:30am Amphitheatre H-1002
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Alan Mycroft, Invited researcher, University of Cambridge, United Kingdom
Properties of programs can be formulated using various techniques: dataflow analysis, abstract interpretation and type-like inference systems. This paper reconstructs strictness analysis (establishing when function parameters are evaluated in a lazy language) as a dataflow analysis, initially at first order, then at higher order by expressing the dataflow properties as an effect system. Strictness properties so expressed give a clearer operational understanding and enable a range of additional optimisations including implicational strictness. At first order strictness effects have the expected principality properties (best-property inference) and can be computed simply; without polymorphic effects principality is lost at higher order. However, adding both polymorphic effects and polymorphic type instantiation to restore principality exposes novel issues.
This is joint work with Tom Schrijvers.
Time and place:
3:00pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Murdoch Gabbay, , Heriot-Watt University, United Kingdom
One area which has consistently thrown up challenges in computer science has been the treatment of names and binding. Names can represent variable symbols in inductive proofs on syntax, but they also feature when reasoning about memory locations, or semi-structured data with pointers, or message-passing in security protocols, and elsewhere. Propagation of names describes connectedness and information flow.
Nominal techniques are based on nominal sets, an relatively elementary extension of "ordinary" sets (i.e. collections of elements). For this reason, nominal techniques have been particularly good for developing relatively elementary extensions of first-order systems to handle names and binding.
I will briefly survey the "nominal" literature and then describe recent work with Gilles Dowek and Dominic Mulligan aimed at developing an extension of first-order logic with names and binding, which we call Permissive Nominal Logic. This preserves the flavour of first-order logic but (we believe) allows a particularly clean, simple, and intuitive representation of axioms and proofs involving names and binding.
See the associated paper.
Time and place:
1:00pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Uri Juhasz, , Tel Aviv University, Israel
Time and place:
2:00pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Alvaro Arenas, , E-Science Centre, STFC Rutherford Appleton Laboratory, United Kingdom
Time and place:
1:00pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Martin Leucker, , Institut für Informatik, Technische Universität 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
Diego Garbervetsky, Professor, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad De Buenos Aires, Argentina.
Time and place:
1:30pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Rob Hierons, Professor of Computing, School of Information Systems, Computing and Mathematics, Brunel University, Uxbridge, Middlesex, UK
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Luis Moniz Pereira, Research Professor, Centro de Inteligencia Artificial (CENTRIA), Universidade Nova de Lisboa, Portugal
Time and place:
11:30am Amphitheatre H-1005
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Pierre Ganty, Post-doctoral Researcher, University of California at Los Angeles, USA
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Julia Lawall, Lektor, DIKU University of Copenhagen, Denmark
Reasoning about program control-flow paths is an important functionality of a number of recent program matching languages and associated searching and transformation tools. Temporal logic provides a well-defined means of expressing properties of control-flow paths in programs, and indeed an extension of the temporal logic CTL has been applied to the problem of specifying and verifying the transformations commonly performed by optimizing compilers. Nevertheless, in developing the Coccinelle program transformation tool for performing Linux collateral evolutions in systems code, we have found that existing variants of CTL do not adequately support rules that transform subterms other than the ones matching an entire formula. Being able to transform any of the subterms of a matched term seems essential in the domain targeted by Coccinelle.
In this work, we propose an extension to CTL named CTL-VW (CTL with variables and witnesses) that is a suitable basis for the semantics and implementation of the Coccinelle's program matching language. Our extension to CTL includes existential quantification over program fragments, which allows metavariables in the program matching language to range over different values within different control-flow paths, and a notion of witnesses that record such existential bindings for use in the subsequent program transformation process. We formalize CTL-VW and describe its use in the context of Coccinelle. We then assess the performance of the approach in practice, using a transformation rule that fixes several reference count bugs in Linux code.
Time and place:
10:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Amal Ahmed, Research Assistant Professor, Toyota Technical Institute, Chicago, USA
Logical relations are a promising proof technique for establishing many important properties of programs, programming languages, and language implementations. They have been used to show type safety, to prove that one implementation of an abstract data type (ADT) can be safely replaced by another, to show that languages for information-flow security ensure confidentiality, and to establish the correctness of compiler transformations and optimizations.
Yet, despite three decades of research and much agreement about their potential benefits, logical relations have only been applied to "toy" languages, because the method has not easily scaled to important linguistic features, including recursive types, mutable references, and (impredicative) generics. Previous approaches have tried to address some of these features through sophisticated mathematical machinery (domain or category theory) which makes the results difficult to formalize and/or extend.
In this talk, I will describe *step-indexed* logical relations which support all of the language features mentioned above and yet permit simple proofs based on operational reasoning, without the need for complicated mathematics. To illustrate the effectiveness of step-indexed logical relations, I will discuss three new contexts where I have been able to successfully apply them: secure multi-language interoperability; imperative self-adjusting computation, a mechanism for efficiently updating the results of a computation in response to changes to some of its inputs; and security-preserving compilation, which ensures that compiled code is no more vulnerable to attacks launched at the level of the target language than the original code is to attacks launched at the level of the source language.
Time and place:
11:00am IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Zaynah Dargaye, PhD Student, INRIA Rocquencourt, France
In the context of mechanized verification of a compiler for a functional language, we have experienced the influence of the semantic preservation proof on the definition of intermediate languages and their semantics.
This is a compiler for the purely functional fragment of untyped ML, formally verified into the Coq system. In the spirit of the CompCert compiler, our compiler is realistic. On top of being an expressive language (recursive functions, pattern matching) and capable of optimizations such as uncurrying, CPS and tailcall compilation optimization, the generated code is also able to interact with an automatic memory manager using a GC
Concretly, we developed a frontend which target language is the first intermediate language of the CompCert backend (Cminor). That allows us to produce PowerPC assembly code. The mini-ML frontend is a chain of successive transformations. For each transformation, we have prooved that it preserves semantics. Composing the proof of semantics preservation of all transformation gives us the semantics preservation of the frontend. This talk is about an overview of the frontend for miniML, with two zoom. First, we will focus on the uncurrying optimisation which is implemented as in the Objective Caml system. Secondly, we decribe the interaction with an automatic memory manager into two transformations using two purely functional languages.
Time and place:
3:30pm IMDEA conference room
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Laurent Mauborgne, Associate Professor, École Normale Supérieure, Paris, France
Time and place:
3:30pm Room 3307
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Deepak Garg, PhD candidate, Computer Science Departament, Carnegie Mellon University, USA
Logic is emerging as an important tool in the design and implementation of secure systems. It can be used not only to reason about correctness of system components and protocols, but also to directly enforce integrity and confidentiality in both code and data. This talk presents two applications of logic, one in each of these two areas.
First, the talk describes the architecture and implementation of a file system that uses proof-carrying authorization (PCA) to protect the integrity and confidentiality of stored data. PCA allows rigorous and administratively lightweight enforcement of complex access policies using logic. However, it is challenging to make PCA efficient enough for practical use in a low-level system. It is argued and demonstrated here that PCA can be combined with conditional capabilities to obtain sufficient efficiency, without losing any of its benefits. The talk also covers a tool for proof search in an expressive authorization logic, which helps make the implementation practical for end users.
Second, the talk presents a logic-based framework for modeling and proving properties of secure systems at a high level of abstraction. The framework is intended to help system builders rule out errors at the design level. It includes a formal language to model system components, and a Hoare-style logic to prove their safety properties in the face of arbitrary adversaries. Drawing upon ideas from work in security protocol analysis, the framework combines symbolic reasoning about cryptographic primitives, network communication, shared memory, access control, and dynamically loaded code in a novel and technically challenging manner.
Time and place:
12:00pm Amphitheatre H-1001
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Aleks Nanevski, Post-doctoral Researcher, Microsoft Research, Cambridge, United Kingdom
Two main properties make type systems an effective and scalable formal method. First, important classes of programming errors are eliminated by statically enforcing the correct use of values. Second, types facilitate modular software development by serving as specifications of program components, while hiding the component's actual implementation. Implementations with the same type can be interchanged, thus facilitating software reuse and evolution.
Mainstream type systems focus on specifying relatively simple properties that admit type inference and checking with little or no input from the programmer. Unfortunately, this leaves a number of properties, including data structure invariants and API protocols outside of their reach, and also restricts the practical programming features that can be safely supported. For example, most simply-typed languages cannot safely allow low-level operations such as pointer arithmetic or explicit memory management.
In this talk, I will describe Hoare Type Theory (HTT) which combined dependent types of a system like Coq with features for specification and verification of low-level stateful operations in the style of Hoare Logic.
Such a combination is desirable for several reasons. On the type-theoretic side, it makes it possible to integrate stateful behaviour into dependent type theories that have so far been purely functional. On the Hoare Logic side, it makes is possible to use the higher-order data abstraction and information hiding mechanisms of type theory, which are essential for scaling any kind of verification effort. For example, by combining type-theoretic abstractions with Hoare-logic types, we are able to capture the specifications for local higher-order state, as well as encode the main ideas from Separation Logic.
From the technical standpoint, it is interesting that the design of HTT relates in an essential way some of the most venerable ideas from programming language theory such as Dijkstra's predicate transformers, Curry-Howard isomorphism and monads. I will discuss the implementation of HTT, verification of various examples that I have carried out, as well as the possibilities for scaling HTT to support further programming features, such as concurrency.
Time and place:
11:00am Amphitheatre H-1005
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Ralf Lämmel, Professor (W3), University of Koblenz-Landau, Germany
Time and place:
12:00pm Amphitheatre H-1005
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Alexey Gotsman, PhD candidate, University of Cambridge, United Kingdom
Time and place:
11:00am Amphitheatre H-1001
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain