Stages MPRI, 2006

Proposed by francesco.zappa_nardelli (at), Moscova Research Team, INRIA Rocquencourt.

Theme 1. Programming Abstractions for Security

These stages are part of a research project carried on at new INRIA-MSR joint centre. For an overview of the big plan refer to the description of the project Secure Distributed Computations and their Proofs. These stages will be supervised by Cédric Fournet (MSR) and myself.

Two PhD grants are available.

Secure Auditing

Large parts of security subsystems are devoted to logging and auditing computations, in order to provide properties such as persistence and non repudiation for transactions, for instance. They are meant to provide at least reliable, strong evidence in case something goes wrong in a distributed computation, providing e.g. a proof that a protocol participant attempted to cheat. However, the actual properties that may be obtained by auditing are delicate to state, test, or verify. We would like to characterize this kind of property and explore language-based support (compilers, type systems, model-checking) to automate the auditing process and its formal validation.

Oblivious transfer

Oblivious transfer (OT) protocols have been thoroughly studied by cryptographers, as a building block for secure multiparty computations with strong secrecy requirements. Roughly, in the protocol there is a sender that holds 2 secret messages and agrees on revealing one of the secrets to the receiver. The receiver on the other hand wants to choose one secret, without revealing which one he is choosing. We would like to give formal semantics to OT, so that we can prove the correctness of some protocols claimed to be OT, and study their integration into more complex protocols and programs.

Blinded computations

In order to perform some secure distributed computation, mutually-suspicious participants need to process the same information at diverse levels of confidentiality and integrity. In order to achieve the target integrity levels and provide robustness, several machines may perform & check the same computation; however, due to confidentiality restrictions, not all machines may be given access to the data (cf. the Jif/Split compiler): in such cases, some parts of the computation are cryptographically blinded. We would like to develop a clean, language-based computational model, ideally relating information-flow specifications to lower level cryptographic assumptions.

Contact me for detailed descriptions.

Theme 2. Program logic and low-level imperative languages

Program verification is the ``holy grail'' of software reliability: it allows one to formally prove that, for all possible runs of the program, a property holds. Floyd and Hoare pioneered the use of logics for program specification, by relating the logical descriptions of the states of a machine before and after the execution of a command. Despite its many advantages, program verification is rarely used in practice. One key reason for this lack of use is that current program verification techniques do not scale. References and pointers are a particular impediment for scalability, as they allow apparently unrelated pieces of code to affect each other's behaviour. Local concurrency, and racy and non-blocking concurrent programming, have until recently been beyond its scope. However, recently, O'Hearn, Reynolds and Yang have developed an approach called local reasoning that allows dealing with pointers and references, and has the potential to scale. The key observation is that separate program texts which work on separate sections of the store can be reasoned about independently. This idea can be embedded in an appropriate substructural logic, called separation logics, that presents a connective to model the disjointness of two portions of the store. Preliminary investigations of extensions of separation logics to local concurrency suggest that it is possible to design a logic suited to reason about concurrent cooperative programming.

As formal proofs of programs tend to be large, they must be mechanised. An ongoing research project involving Francesco Zappa Nardelli (Moscova, INRIA Rocquencourt), Andrew Appel (Princeton U., US), Sandrine Blazy (Gallium, INRIA Rocqencourt) and Matthew Parkinson (Cambridge U., UK), is building a mechanised framework to prove the correctness of concurrent programs written in a large subset of C, using Posix threads, and communicating via shared memory, using separation logics. Focussing on a realistic programming language raises new challenges, related to the presence of side-effects in expressions and functions, and to the complexity of the semantics. At the same this makes possible to prove properties of real programs, and not only of examples written in a toy language. The development is done inside the Coq theorem prover.

Several stages are possible here, along different research directions. Contact me for detailed descriptions.

Theme 3. Formal semantics of full-scale programming languages

In collaboration with Peter Sewell (Cambridge University). Contact me for a description of this line of research.

Last updated: