Nonmalleable Progress Leakage

TL;DR

This paper introduces nonmalleable progress leakage (NMPL), a new security notion that allows controlled progress leakage in information-flow control systems, combining progress-sensitive security with secure downgrading to prevent malicious interference.

Contribution

It defines NMPL, a novel security property, and develops the first type system to enforce NMPL while permitting some progress leakage, verified in Rocq.

Findings

First type system for NMPL enforcement

Formal verification of theorems in Rocq

Identification of secure progress downgrade locations

Abstract

Information-flow control systems often enforce progress-insensitive noninterference, as it is simple to understand and enforce. Unfortunately, real programs need to declassify results and endorse inputs, which noninterference disallows, while preventing attackers from controlling leakage, including through progress channels, which progress-insensitivity ignores. This work combines ideas for progress-sensitive security with secure downgrading (declassification and endorsement) to identify a notion of securely downgrading progress information. We use hyperproperties to distill the separation between progress-sensitive and progress-insensitive noninterference and combine it with nonmalleable information flow, an existing (progress-insensitive) definition of secure downgrading, to define nonmalleable progress leakage (NMPL). We present the first information-flow type system to allow some progress leakage while enforcing NMPL, and we show how to infer the location of secure progress downgrades. All theorems are verified in Rocq.