A Protocol Compiler for Secure Sessions in ML

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 declarations down to ML modules securely implementing the sessions. Every run of a well-typed program executing a session through its generated module is guaranteed to follow the session specification, despite any low-level attempt by coalitions 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 session for a conference management system. 1 Sessions for distributed programming Programming networked, independent systems is complex: when systems communicate through an untrusted network, and do not trust each other, enforcing security properties is hard. As a first step to simplify this task, ...

• Type: Conference
• Year: 2007
• Where: TGC
• Authors: Ricardo Corin, Pierre-Malo Deniélou
• Keywords: Applied Computing, Complex Session, Distributed Programming, Session Specifications, TGC 2007