Information Flow Control in Cyclic Process Networks

TL;DR

This work extends information-flow control (IFC) to cyclic, asynchronous, message-passing systems by integrating IFC with linear session types in an APCP-like process language. It introduces running secrecy annotations and a secrecy lattice to statically prevent high-to-low leaks, even in cyclic networks, and treats deadlocks as a potential side channel through deadlock-sensitive noninterference ($DSNI$). A novel logical relation grounded in linear logic is developed to prove DSNI for well-typed processes and to relate process behaviors across arbitrary contexts. The main theorem shows that well-typedness guarantees DSNI, enabling secure, protocol-safe communications in realistic cyclic networks and addressing a key gap in prior tree-only IFC/type systems. The work also compares to related lineages of session-typed IFC and lays groundwork for future extensions to recursion and non-determinism while preserving strong noninterference guarantees.

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.

Figures (7)

• Figure 1: Collaborating governments: three scenarios.
• Figure 2: Structural congruence (top) and reduction (bottom); cf. \ref{['d:procSCRedd']}.
• Figure 3: Typing rules; cf. \ref{['d:typeSys']}.
• Figure 4: Term relation.
• Figure 5: Value interpretation, output cases ($\textcolor{RoyalBlue}{\mathsf{1}},\textcolor{RoyalBlue}{\mathsf{{\oplus}}},\textcolor{RoyalBlue}{\mathsf{\mathbin{\otimes}}}$).

Theorems & Definitions (42)

• Definition 1: Syntax
• Example 2
• Definition 3: Reduction Semantics
• Example 4
• Definition 5: Types
• Definition 6: Type System
• Example 7
• Example 8
• Lemma 9
• Lemma 9: Substitution