Research

I am currently a Postdoc at Imperial College in the Department of Computing in Nobuko Yoshida's team.

I am interested in giving to programmers language tools such as new primitives, type systems, compilers, etc., that make it easier to write robust, safe and secure distributed programs and, at the same time, provide strong (formal) guarantees about the resulting code (distributed type safety and enforcement of security properties).

Keywords: Programming languages, semantics, type systems, concurrency, language-based security, mechanized proofs.
Co-authors: Karthik Bhargavan, Ricardo Corin, Cédric Fournet, James J. Leifer, Nobuko Yoshida.

Extended abstract [ pdf ] Long version [ pdf ] Slides [ pdf ]
Joint work with Nobuko Yoshida.
In 38th International Symposium on Principle of Programming Languages (POPL), January 2011.
Web page.
Abstract

Multiparty session types enforce structured safe communications between several participants, as long as their number is fixed when the session starts. In order to handle common distributed interaction patterns such as cloud algorithms or peer-to-peer protocols, we propose a new role-based multiparty session type theory where roles are defined as classes of local behaviours that an arbitrary number of participants can dynamically join and leave. We offer programmers a polling operation that gives access to the current set of a role's participants in order to fork processes. Our type system with universal types for polling can handle this dynamism and retain type safety. A multiparty locking mechanism is introduced to provide communication safety, but also to ensure a stronger progress property for joining participants that has never been guaranteed in previous systems. Finally, we present some implementation mechanisms used in our prototype extension of ML.

Extended abstract [ pdf ] Long version [ pdf ]
Joint work with Nobuko Yoshida.
In 21st International Conference on Concurrency Theory (CONCUR), August 2010.
Web page.
Abstract

Many communication-centred systems today rely on asynchronous messaging among distributed peers to make efficient use of parallel execution and resource access. With such asynchrony, the communication buffers can happen to grow inconsiderately over time. This paper proposes a static verification methodology based on multiparty session types which can efficiently compute the upper bounds on buffer sizes. Our analysis relies on a uniform causality audit of the entire collaboration pattern -- an examination that is not always possible from each end-point type. We extend this method to design algorithms that allocate communication channels in order to optimise the memory requirements of session executions. From these analyses, we propose two refinements methods which respect buffer bounds: a global protocol refinement that automatically inserts confirmation messages to guarantee stipulated buffer sizes and a local protocol refinement to optimise asynchronous messaging without buffer overflow. Finally our work is applied to overcome a buffer overflow problem of the multi-buffering algorithm. taken from parallel algorithms and Web services usecases.

Extended abstract [ pdf ] Long version [ pdf ] Slides [ pdf ]
Joint work with Nobuko Yoshida, Andi Bejleri and Raymond Hu.
In Foundations of Software Science and Computational Structures (FoSSaCS), March 2010.
Web page.
Abstract

For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from Godel's System T to express a wide range of communication patterns while keeping type checking decidable. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.

Extended abstract [ pdf ]
Joint work with Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and James Leifer.
In 22nd IEEE Computer Security Foundations Symposium (CSF22), July 2009.
Project web page.
Specifications and generated code for the session examples of the paper.
Abstract

We present the design and implementation of a compiler that, given high-level multiparty session de- scriptions, generates custom cryptographic protocols. Our sessions specify pre-arranged patterns of mes- sage exchanges and data accesses between distributed participants. They provide each participant with strong security guarantees for all their messages. Our compiler generates code for sending and receiv- ing these messages, with cryptographic operations and checks, in order to enforce these guarantees against any adversary that may control both the network and some session participants. We verify that the generated code is secure by relying on a recent type system for cryptography. Most of the proof is performed by mechanized type checking and does not rely on the correctness of our compiler. We obtain the strongest session security guarantees to date in a model that captures the executable details of protocol code. We illustrate and evaluate our approach on a series of protocols inspired by web services.

Journal article [ pdf ]
In Journal of Computer Security, 2008-11-19, p. 573-636.
Joint work with Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and James Leifer.
This full paper merges the results from the following two papers, provides the proofs, and includes additional details and examples. (It is a slighly extended version of a paper to appear in the Journal of Computer Security).

Extended abstract [ pdf ] Slides [pdf ]
Joint work with Ricardo Corin.
In G. Barthe and C. Fournet, editors, TGC'07, Sophia Antipolis, France, Lecture Notes in Computer Science, Springer Verlag, November 2007
Project web page.
Abstract

Distributed applications can be structured using sessions that specify flows of messages between roles. We design a small specific language to declare sessions. We then build a compiler, called s2ml, that transforms these declara- tions down to ML modules securely implementing the sessions. Every run of a well-typed program executing a session through its generated module is guaran- teed to follow the session specification, despite any low-level attempt by coali- tions of remote peers to deviate from their roles. We detail the inner workings of our compiler, along with our design choices, and illustrate the usage of s2ml with two examples: a simple remote procedure call session, and a complex ses- sion for a conference management system.

Extended abstract [ pdf ]
Joint work with Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and James Leifer.
20th IEEE Computer Security Foundations Symposium (CSF20), pp 170--186. July 2007
Project web page.
Abstract

Distributed applications can be structured as parties that exchange messages according to some pre-arranged communication patterns. These sessions (or contracts, or protocols) simplify distributed programming: when coding a role for a given session, each party just has to follow the intended message flow, under the assumption that the other parties are also compliant. In an adversarial setting, remote parties may not be trusted to play their role. Hence, defensive implementations also have to monitor one another, in order to detect any deviation from the assigned roles of a session. This task involves low-level coding below session abstractions, thus giving up most of their benefits. We explore language-based support for sessions. We extend the ML language with session types that express flows of messages between roles, such that well-typed programs always play their roles. We compile session type declarations to cryptographic communication protocols that can shield programs from any low-level attempt by coalitions of remote peers to deviate from their roles.

Extended abstract [ pdf | ps.gz ] Proc. ICFP 2006. © ACM, 2006.
(Please contact me for the slides or the technical report.)
Joint work with James J. Leifer.
Abstract

In most programming languages, type abstraction is guaranteed by syntactic scoping in a single program, but is not preserved by marshalling during distributed communication. A solution is to generate hash types at compile time that consist of a fingerprint of the source code implementing the data type. These hash types can be tupled with a marshalled value and compared efficiently at unmarshall time to guarantee abstraction safety. In this paper, we extend a core calculus of ML-like modules, functions, distributed communication, and hash types, to integrate structural subtyping, user- declared subtyping between abstract types, and bounded existential types. Our semantics makes two contributions: (1) the explicit tracking of the interaction between abstraction boundaries and subtyping; (2) support for user-declared module upgrades with propagation of the resulting subhashing relation throughout the network during communication. We prove type preservation, progress, determinacy, and erasure for our system.

See the appropriate web page (in French).

[ Rapport pdf (662ko) | Transparents pdf (384ko) ]
Stage effectué sous la direction de James J. Leifer et Jean-Jacques Lévy.

A secure session to ML (Ocaml/F#) compiler prototype.
See the project web page for details and download link.

A small environment to learn how to program.
See the project web page for details and download link.