Session Types for Access and Information Flow Control

摘要

We consider a calculus for multiparty sessions with delegation, en-riched with security levels for session participants and data. We propose a type system that guarantees both session safety and a form of access control. More-over, this type system ensures secure information flow, including controlled forms of declassification. In particular, the type system prevents leaks that could result from an unrestricted use of the control constructs of the calculus, such as session opening, selection, branching and delegation. We illustrate the use of our type system with a number of examples, which reveal an interesting interplay between the constraints used in security type systems and those used in session types to ensure properties like communication safety and session fidelity.