Models And TYpes for Secure Sessions

COLOR - 2009 project

Project description

The goal of the project is to study models and type systems for safe and secure sessions. A session is an abstraction for various forms of “structured communication” which may occur in a parallel and distributed computing environment. Examples of sessions are a client-service negotiation, a financial transaction, or a multiparty interaction among different services within a web application.

Language-based support for sessions has now become the subject of active research. Primitives for enabling programmers to code sessions in a flexible way, as well as type systems (session types) ensuring the compliance of programs to session specifications, have already been studied for various calculi and languages.

The key properties ensured by session types are the consistency of the communication patterns exhibited by the various partners (implying the absence of communication errors at run time), and progress, assuring the absence of deadlock, so that each terminating session completes with success.

Little attention has been paid so far to security issues within session types. This is an evident weakness, since properties such as confidentiality and integrity of data become all the more crucial in an open, unreliable environment such as that of global networks, where communicating partners may not trust each other.

The MATYSS project will address the question of incorporating secure information flow requirements within session types, in the setting of a name-passing process calculus (akin to the π-calculus) with asynchronous communication and multiparty sessions.

For more details, see the full proposal.

Contact: Ilaria Castellani