Information Flow Control in Cyclic Process Networks

TL;DR

This paper introduces a novel information flow control type system for message-passing concurrent programs, supporting cyclic process networks, deadlock-sensitive noninterference, and integrating session types for protocol safety.

Contribution

It extends prior work by supporting cyclic process networks, enabling more permissive and secure IFC control, and incorporating deadlock considerations into noninterference guarantees.

Findings

Supports cyclic process networks in IFC type system

Proves deadlock-sensitive noninterference (DSNI)

Develops a linear logic-based logical relation for cyclic networks

Abstract

Protection of confidential data is an important security consideration of today's applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC type system for message-passing concurrent programs, the computational model of choice for many of today's applications such as cloud computing and IoT applications. Such applications typically either implicitly or explicitly codify protocols according to which message exchange must happen, and to statically ensure protocol safety, behavioral type systems such as session types can be used. This paper marries IFC with session typing and contributes over prior work in the following regards: (1) support of realistic cyclic process networks as opposed to the restriction to tree-shaped networks, (2) more permissive, yet entirely secure, IFC control, exploiting cyclic process networks, and (3) considering deadlocks as another form of side channel, and asserting deadlock-sensitive noninterference (DSNI) for well-typed programs. To prove DSNI, the paper develops a novel logical relation that accounts for cyclic process networks. The logical relation is rooted in linear logic, but drops the tree-topology restriction imposed by prior work.