Session Logical Relations for Noninterference

TL;DR

This paper introduces a type system for linear session types that enforces noninterference by tracking secrecy levels within process configurations, ensuring confidentiality in communication protocols.

Contribution

It develops a novel information flow control type system aligned with intuitionistic linear logic, incorporating secrecy levels to enforce noninterference in session-typed processes.

Findings

Type system guarantees noninterference through secrecy level stratification.

Processes form a secrecy-aware configuration tree ensuring security invariants.

Logical relation for session types enables nuanced equivalence reasoning.

Abstract

Information flow control type systems statically restrict the propagation of sensitive data to ensure end-to-end confidentiality. The property to be shown is noninterference, asserting that an attacker cannot infer any secrets from made observations. Session types delimit the kinds of observations that can be made along a communication channel by imposing a protocol of message exchange. These protocols govern the exchange along a single channel and leave unconstrained the propagation along adjacent channels. This paper contributes an information flow control type system for linear session types. The type system stands in close correspondence with intuitionistic linear logic. Intuitionistic linear logic typing ensures that process configurations form a tree such that client processes are parent nodes and provider processes child nodes. To control the propagation of secret messages, the type system is enriched with secrecy levels and arranges these levels to be aligned with the configuration tree. Two levels are associated with every process: the maximal secrecy denoting the process' security clearance and the running secrecy denoting the highest level of secret information obtained so far. The computational semantics naturally stratifies process configurations such that higher-secrecy processes are parents of lower-secrecy ones, an invariant enforced by typing. Noninterference is stated in terms of a logical relation that is indexed by the secrecy-level-enriched session types. The logical relation contributes a novel development of logical relations for session typed languages as it considers open configurations, allowing for more nuanced equivalence statement.