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:

1. Merlin: which combines static analysis with probabilistic inference to infer security specification inference, and find security errors in programs
2. Holmes: where we use path profiling together with a statistical model to find root causes of errors
3. DebugAdvisor: where we use data from version control, bug databases etc, and combine information retrieval together with tricks specific to programmatic structures and find relevant information for people doing debugging

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:

1. Automatic inference of sound loop invariants (no need for tedious programmer annotations)
2. Predictability (the analysis follows the semantics of the program)
3. Scalability (the analysis is tuned on the properties of interest)

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).

Automated termination analysis of software programs has been a hot research topic for two decades. And still it is, as witnessed by the Terminator project recently set up by Microsoft (http://research.microsoft.com/terminator/). The reason of such interest is due to the fact that the property of termination of a program fragment is not less important than, say, properties concerning the absence of run-time errors. For instance, critical reactive systems (such as fly-by-wire avionics systems) must maintain a continuous interaction with the environment: failure to terminate of some program components can stop the interaction the same way as if an unexpected, unrecoverable run-time error occurred. The classical technique for proving termination of a generic computer program involves the synthesis of a "ranking function" for each loop of the program. In this seminar we introduce the basic techniques for the automatic synthesis of ranking functions, presenting them in the context of imperative programs and with a unifying approach that helps clarifying the existing literature.

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.

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.

One of the main difficulties with modular analysis is the issue of aliasing. Several systems have been proposed that allow modular analysis by restricting the programs to have heaps that are a tree or "almost tree". We propose a system that allows analysing programs with DAGS and possibly general graphs by forcing the exposure of sharing rather than restricting it altogether. We allow indirect modification of subcomponents of an aggregate component at the price of more verbose specification.

Collaborative systems such as Grids enable seamless resource sharing across multiple organisations, constituting the basic infrastructure for today's data-intensive scientific collaborations. This talk presents security challenges when sharing data in Grids and introduces the usage control framework as a potential solution for such challenges. Usage control is a new authorisation paradigm that encompasses and extends several access control models. We introduce a process description language used as a policy specification language and show its suitability to model usage policies for Grids. We also describe the use of reputation systems for Grids and show how reputation can be combined with usage control. Our reputation model is based on utility computing, representing users' feedback as utility functions that reflect the satisfaction a user perceives after consuming a service. It will be shown how the system can be used to rate users according to their compliance with resource usage policies.

Abstraction is one of the key techniques for model checking. In this presentation, we briefly review two-valued as well as three-valued abstraction techniques. We then turn our attention towards multi-valued logics. In multi-valued logics interpreted over multi-valued Kripke structures, the semantics of a formula is no longer just true or false but one of many truth values. To make multi-valued model checking feasible in practice, abstraction and refinement techniques are essential in this setting as well. In this talk, we address abstraction and refinement techniques in the setting of multi-valued model checking for the mu-calculus.

In this talk I will present a series of techniques to automatically compute parametric certificates of dynamic memory utilization for Java like programs. Core to these techniques is the utilization of program invariants which are used as a mean to approximate visits to memory consuming statements and to bind information provided by the different methods of the application under analysis. The approach is implemented in a prototype tool that allows us to experimentally evaluate the efficiency and accuracy of the method on several Java benchmarks with encouraging results. I will pinpoint some challenges we have to face during the implementation of these techniques and I will discuss what we think are the advantages and limitations of our approach.

Software testing is widely recognised to be an expensive, error prone and time consuming process and this has led to much interest in automated test generation. In recent years, search based techniques such as Genetic Algorithms have been applied to a range of test automation problems but much of this work has concerned white-box testing. This talk will provide an overview of recent progress in Search Based Software Testing (SBST) in the context of model based testing. Specifically, it will review work on the use of SBST methods in testing from finite state machines and extended finite state machines.

This work proposes the application of preferences over abductive logic programs as an appealing declarative formalism to model choice situations. In particular, both a priori and a posteriori handling of preferences between abductive extensions of a theory are addressed as complementary and essential mechanisms in a broader framework for abductive reasoning. Furthermore, both of these choice mechanisms are combined with other formalisms for decision making, like economic decision theory, resulting in theories containing the best advantages from both qualitative and quantitative formalisms. Several examples are presented throughout to illustrate the methodologies described. These have been tested in our implementation, which we explain in detail.

An asynchronous or "event-driven'' program is one that contains procedure calls which are not directly executed from the call site, but stored and executed later by an external scheduler. By providing a low-overhead way to manage concurrent interactions, asynchronous programs form the core of many server programs, embedded systems, and popular programming styles for the web (Ajax). Unfortunately, such programs can be hard to write and maintain as sequential control flow needs to be split into several disjoint handlers. They are a challenge for static analysis tools as they are infinite state: both the program stack and the number of outstanding asynchronous requests may be unbounded. We show that safety and liveness properties can be checked effectively for the class of Boolean asynchronous programs, thus enabling automatic static techniques to check for correctness or for errors.
(slides)

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.

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.

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.

The main difficulty in abstract interpretation is to handle disjunctions: on one hand, keeping precise disjunctive informations is very costly, and on the other hand, approximating disjunctions is the main source of imprecision in abstractions. We propose on demand semantic disjunctions, where disjunctions are based on semantic properties such as some values of the reachable states or more complex properties of the traces of the program leading to these states. Such disjunctions allow for parametric refinements of existing analyses while keeping scalability. We discuss implementation issues and show the interest of such techniques in the ASTRÉE analyzer.

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.

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.

Algebraic data types and catamorphisms (folds) play a central role in functional programming as they allow programmers to define recursive data structures and operations on them uniformly by structural recursion. Likewise, in object-oriented (OO) programming, recursive hierarchies of object types with virtual methods play a central role for the same reason. There is a semantical correspondence between these two situations which we reveal and formalize categorically. To this end, we assume a coalgebraic model of OO programming with functional objects. The development may be helpful in deriving refactorings that turn sufficiently disciplined functional programs into OO programs of a designated shape and vice versa. (Joint work with Ondrej Rypacek)

Reasoning about concurrent programs is made difficult by the number of possible interactions between threads. This is especially true for heap-manipulating programs, in which threads can interact in subtle ways via dynamically-allocated data structures. I will present novel thread-modular logics and analyses for concurrent heap-manipulating programs that address this challenge. The logics and the analyses can be used to reason about or automatically verify a number of safety properties (memory safety, data race freedom, absence of memory leaks) and have been successfully used as a key ingredient in methods for verifying liveness properties. I will also discuss my approach to their design in which program logics and program analyses share the underlying reasoning principles.