On Dynamic Flow-Sensitive Floating-Label Systems
This work addresses security issues in dynamic flow-sensitive systems for programming language researchers, though it appears incremental as it builds on existing LIO frameworks.
The authors tackled the challenge of safely adding flow-sensitive references to dynamic information-flow control systems, which can introduce covert channels, by extending the LIO system with a safe upgrade primitive and automatic upgrades, and proved non-interference for both sequential and concurrent settings.
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.