Section: Overall Objectives

Introduction

The research in Moscova which was traditionaly centered around the theory and practice of concurrent programming in the context of distributed and mobile systems, is now retargeted around two main themes: weak memory models and secure distributed computations. Our ambitious long-term goal is still to program safely concurrent applications on top of new multi-core architectures and to program secure global computations on top of wide-area networks.

In in the past years, we designed several concurrent programming languages (Jocaml, Acute) together with tools to study their semantics (OTT). Our languages are not as used as the known Java or $C\#$ which allow downloading of programs, but our languages also allow migrations of active programs. Moreover the join primitives of Jocaml have been implemented inside polyphonic $C\#$, in $F\#$ and Visual Basic. These studies and implementations demonstrated that there is still a need for a deep understanding of the underlying hardware and for an intensive use of programming primitives for security.

On the concurrency side, our implementations relied on locks and sequential consistency. This means that the semantics of our concurrent languages were defined in terms of interleaving of sequential instruction steps in each thread of programs. However this is no longer correct with modern architectures which allow delayed write operations in memory and permutation of reads and writes not related to the same memory location (TSO, PSO, RMO architectures). Therefore the semantics of concurrent languages need be revisited to take into account these new features. In this area, we have pursued our productive cooperation with U. of Cambridge (Peter Sewell) and with J. Alglave (now at Oxford).

For security, we already looked at programming primitives to define contracts for multiparty secure sessions or for logs auditing which could resist to malicious participants in strongly typed programming languages (Ocaml or $F\#$). Thus the use of these high-level primitives inside programming languages lighten the burden of close inspection for complex security protocols. All the effort is now carried by the correctness proof of the compiling phase from the source text of programs to low-level exchanges of messages using cryptographic operations. These correctness proofs are incredibly complex, and therefore one needs tools to help them. This is a great part of the work done in 2011 in our project-team. We developed several versions of the F7 language on top of $F\#$, a Caml-like language with types annotated by logical formulas. We used F7 to develop the work on secure audits of logs and to prove the correctness of implementations of SSL/TLS.

On the software side, we pursue the maintenance for the development of Jocaml with additional constructs for object-oriented programming, and for Hevea (a fast LaTeX to HTML translator). We also continue the development of OTT – one tool for the working semanticist – which has a growing set of users. More innovative are the softwares developed along the two main themes of our present research: the Memevents-Litmus-Diy-Dont suite of tools for efficient analyses of weak memory models, the F7 typechecker, and the secure multi-party sessions packages.

In 2011, the ERC Starting Grant (CRYSP) of Karthikeyan Bhargavan started with visit of Sergio Maffeis (6 months) and arrival of Alfredo Pironti (as postdoc). Nataliya Guts defended her PhD on 11 January 2011 and then started a postdoc at U. of Maryland with Mike Hicks. Jérémy Planul (ENS-Lyon and MPRI) will defend his PhD on 8 February 2012.

Since August 2006, J.-J. Lévy is also director of the Microsoft Research-INRIA Joint Centre, in Orsay. K. Bhargavan, N. Guts, J. Leifer, J. Planul, A. Pironti and F. Zappa Nardelli are also active in this centre, as members of the Secure Distributed Computations and their Proofs, headed by C. Fournet (Many members of the Joint Centre are former members of project-team Moscova).

Finally, we are in a phase of remodelling our project-team, since Moscova is 12-year old and J.-J. Lévy will retire on February 2012. A proposal for a new project (Prosecco) about Security headed by K. Bhargavan is under discussions.