From Fine- to Coarse-Grained Dynamic Information Flow Control and Back, a Tutorial on Dynamic Information Flow

TL;DR

This tutorial demonstrates that the granularity of dynamic information flow control (IFC) systems, whether fine- or coarse-grained, does not inherently limit their precision or permissiveness, through formal translations and proofs.

Contribution

It introduces semantics-preserving translations between fine- and coarse-grained dynamic IFC languages, showing their equivalence in security guarantees and improving IFC system usability.

Findings

Coarse- and fine-grained IFC systems can be translated into each other without loss of security.

The translations enable automatic retrofitting of legacy applications to coarse-grained IFC.

The approach reduces label annotation burden in fine-grained systems.

Abstract

This tutorial provides a complete and homogeneous account of the latest advances in fine- and coarse-grained dynamic information-flow control (IFC) security. Since the 70s, the programming language and the operating system communities have proposed different IFC approaches. IFC operating systems track information flows in a coarse-grained fashion, at the granularity of a process. In contrast, traditional language-based approaches to IFC are fine-grained: they track information flows at the granularity of program variables. For decades, researchers believed coarse-grained IFC to be strictly less permissive than fine-grained IFC -- coarse-grained IFC systems seem inherently less precise because they track less information -- and so granularity appeared to be a fundamental feature of IFC systems. We show that the granularity of the tracking system does not fundamentally restrict how precise or permissive dynamic IFC systems can be. To this end, we mechanize two mostly standard languages, one with a fine-grained dynamic IFC system and the other with a coarse-grained dynamic IFC system, and prove a semantics-preserving translation from each language to the other. In addition, we derive the standard security property of non-interference of each language from that of the other via our verified translation. These translations stand to have important implications on the usability of IFC approaches. The coarse- to fine-grained direction can be used to remove the label annotation burden that fine-grained systems impose on developers, while the fine- to coarse-grained translation shows that coarse-grained systems -- which are easier to design and implement -- can track information as precisely as fine-grained systems and provides an algorithm for automatically retrofitting legacy applications to run on existing coarse-grained systems.