Secure Implementations for Typed Session Abstractions

Papers and Talks

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. CSF'09. (Technical Report coming soon.) 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 descriptions, generates custom cryptographic protocols. Our sessions specify pre-arranged patterns of message 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 receiving 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.

A Secure Compiler for Session Abstractions. Technical Report, May 2008. This full paper merges the results from the two papers below, 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). 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.

A Protocol Compiler for Secure Sessions in ML, 3rd Symposium on Trustworthy Global Computing (TGC 2007), November 5-6, 2007. This paper describes the usage and inner workings of our compiler, illustrating it with two running examples: an RPC session and a Conference Management System session. See also the TGC'07 slides. Abstract

Secure Implementations for Typed Session Abstractions, 20th IEEE Computer Security Foundations Symposium (CSF20), pp 170--186. July 2007. See also the CSF20 slides. 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.

Tools

sessions-1.0.tgz (initial release), June 2007.

People

Example