Session Logical Relations for Noninterference

by Dr. Stephanie Balzer

Abstract

In this talk I introduce the audience to linear session types through the lens of noninterference. Session types, as the types of message-passing concurrency, naturally capture what information is learned by the exchange of messages, facilitating the development of a flow-senstive information flow control (IFC) type system guaranteeing noninterference. Noninterference ensures that an observer (adversary) cannot infer any secrets from made observations. I will explain the key ideas underlying the development of the IFC type system as well as the construction of the logical relation conceived to prove noninterference. The type system is based on intuitionistic linear logic and enriched with possible worlds to impose invariants on run-time configurations of processes, leading to a stratification in line with the security lattice. The logical relation generalizes existing developments for session-typed languages to open configuration to allow for a more subtle statement of program equivalence.

Joint work with Farzaneh Derakhshan and Limin Jia.

School of Computer and Cyber Sciences Augusta University