Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency

TL;DR

Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency presents SINTEGRITY, a session-typed IFC system that permits safe pc downgrading through regrading, backed by integrity annotations. It introduces synchronization-pattern checks to ensure regrading safety and develops a comprehensive logical-relations-based proof of progress-sensitive noninterference (PSNI) for well-typed processes under asynchronous dynamics. A security-polymorphic type system, a formal calculus, and a verified type checker together enable secure composition of components with different regrading policies. The work advances prior IFC session-type approaches by integrating integrity-guided regrading with compositional guarantees, enabling flexible, timing-attack-resistant information-flow control in concurrent settings.

Abstract

Noninterference guarantees that an attacker cannot infer secrets by interacting with a program. Information flow control (IFC) type systems assert noninterference by tracking the level of information learned (pc) and disallowing communication to entities of lesser or unrelated level than the pc. Control flow constructs such as loops are at odds with this pattern because they necessitate downgrading the pc upon recursion to be practical. In a concurrent setting, however, downgrading is not generally safe. This paper utilizes session types to track the flow of information and contributes an IFC type system for message-passing concurrent processes that allows downgrading the pc upon recursion. To make downgrading safe, the paper introduces regrading policies. Regrading policies are expressed in terms of integrity labels, which are also key to safe composition of entities with different regrading policies. The paper develops the type system and proves progress-sensitive noninterference for well-typed processes, ruling out timing attacks that exploit the relative order of messages. The type system has been implemented in a type checker, which supports security-polymorphic processes using local security theories.

Figures (17)

• Figure 1: Bank survey: (a) process configuration, (b)/(c) red/green tactic, (d) session types.
• Figure 2: Secure process implementations of analyzer and surveyor (see \ref{['fig:analyzer']}), accepted by $\mathsf{SINTEGRITY}$, but rejected by existing IFC session type systems.
• Figure 3: Insecure hasty analyzer $\mathsf{A_H}$ and reckless analyzer $\mathsf{A_R}$, rejected by $\mathsf{SINTEGRITY}$.
• Figure 4: Process term typing rules of $\mathsf{SINTEGRITY}$.
• Figure 5: Signature checking rules of $\mathsf{SINTEGRITY}$.

Theorems & Definitions (14)

• Theorem 1: Fundamental theorem
• Lemma 2: Compositionality
• Theorem 3: Adequacy
• Definition 4: Concrete security lattice and security theory
• Definition 5: Order-preserving substitution
• Definition 6
• Lemma 7
• Theorem 8: Progress
• Theorem 9: Preservation
• Definition 10: Running integrity of nodes