Extended abstract
[ pdf
]
Slides [pdf
]
TGC'07
Joint work with Ricardo Corin.
Project web page.
Extended abstract
[ pdf
]
20th IEEE Computer Security Foundations Symposium (CSF20), pp 170--186. July 2007
Joint work with Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and James Leifer.
Project web page.
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.
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.
[ Rapport pdf (662ko)
| Transparents pdf (384ko)
]
Stage effectué sous la direction de
James J. Leifer et
Jean-Jacques Lévy.