Logical Relations for Session-Typed Concurrency

TL;DR

This paper extends logical relations to recursive session types in concurrent, non-terminating settings, enabling reasoning about information flow security with a new stratified logical relation and a supporting type system.

Contribution

It introduces a stratified logical relation for recursive session types, addressing non-termination and concurrency, and develops a practical type system for information flow control.

Findings

Logical relation is sound and complete for progress-sensitive noninterference.

The type system supports secrecy-polymorphic processes and is implemented in a type checker.

The logical relation's stratification ensures closure under parallel composition.

Abstract

Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an observer is shown. A powerful enabler for such proofs are logical relations. Logical relations only recently were adopted for session types -- but exclusively for terminating languages. This paper scales logical relations to general recursive session types. It develops a logical relation for progress-sensitive noninterference (PSNI) for intuitionistic linear logic session types (ILLST), tackling the challenges non-termination and concurrency pose, and shows that logical equivalence is sound and complete with regard to closure of weak bisimilarity under parallel composition, using a biorthogonality argument. A distinguishing feature of the logical relation is its stratification with an observation index (as opposed to a step or unfolding index), a crucial shift to make the logical relation closed under parallel composition in a concurrent setting. To demonstrate practicality of the logical relation, the paper develops an information flow control (IFC) refinement type system for ILLST, with support of secrecy-polymorphic processes, and shows that well-typed programs are self-related by the logical relation and thus enjoy PSNI. The refinement type system has been implemented in a type checker, featuring local security theories to support secrecy-polymorphic processes.