On Dynamic Flow-Sensitive Floating-Label Systems

TL;DR

This paper extends the LIO language-based floating-label system with flow-sensitive references, enabling safe label changes and automatic upgrades, including in concurrent settings, while maintaining non-interference guarantees.

Contribution

It introduces a safe, flow-sensitive reference mechanism with automatic upgrades in a dynamic IFC system, extending to concurrency and preserving security guarantees.

Findings

Safe label manipulation considering reference and label labels

Automatic upgrade mechanism reduces manual label management

Non-interference proven for both sequential and concurrent systems

Abstract

Flow-sensitive analysis for information-flow control (IFC) allows data structures to have mutable security labels, i.e., labels that can change over the course of the computation. This feature is often used to boost the permissiveness of the IFC monitor, by rejecting fewer runs of programs, and to reduce the burden of explicit label annotations. However, adding flow-sensitive constructs (e.g., references or files) to a dynamic IFC system is subtle and may also introduce high-bandwidth covert channels. In this work, we extend LIO---a language-based floating-label system---with flow-sensitive references. The key insight to safely manipulating the label of a reference is to not only consider the label on the data stored in the reference, i.e., the reference label, but also the label on the reference label itself. Taking this into consideration, we provide an upgrade primitive that can be used to change the label of a reference in a safe manner. We additionally provide a mechanism for automatic upgrades to eliminate the burden of determining when a reference should be upgraded. This approach naturally extends to a concurrent setting, which has not been previously considered by dynamic flow-sensitive systems. For both our sequential and concurrent calculi we prove non-interference by embedding the flow-sensitive system into the original, flow-insensitive LIO calculus---a surprising result on its own.