Simon Gay, Department of Computing Science, University of Glasgow

Title:

Session Types, Typestate, and Security

Abstract:

Session types are type-theoretic specifications of communication protocols, allowing the sequence and type of messages on a channel to be specified and verified by static type checking. Some connections with security have been developed, in two directions: (1) cryptographic implementation of secure sessions; (2) enhancement of session types with correspondence assertions in order to provide authenticity guarantees. However, there is more to be done in this area.

Typestate is the more general idea that the possible operations on an object depend on its state; a given method might not always be available, and only certain specified sequences of method calls should be allowed. Again, the aim is to incorporate typestate into static type systems. Session types can be regarded as the application of typestate to communication channels. Typestate systems can be used to guarantee correct use of APIs, by converting informal documentation into compiler-checkable specifications. The potential connection with security, as yet unexplored, is that a cryptographic API is likely to specify required sequences of calls.

In this talk I will introduce the ideas of session types and typestate, outline existing and potential connections with security, and try to inspire others to develop these connection further.