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

This tutorial provides a complete and homogeneous account of the latestadvances in fine- and coarse-grained dynamic information-flow control (IFC)security. Since the 70s, the programming language and the operating systemcommunities have proposed different IFC approaches. IFC operating systems trackinformation 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. Fordecades, researchers believed coarse-grained IFC to be strictly less permissivethan fine-grained IFC -- coarse-grained IFC systems seem inherently lessprecise because they track less information -- and so granularity appeared tobe a fundamental feature of IFC systems. We show that the granularity of thetracking system does not fundamentally restrict how precise or permissivedynamic IFC systems can be. To this end, we mechanize two mostly standardlanguages, one with a fine-grained dynamic IFC system and the other with acoarse-grained dynamic IFC system, and prove a semantics-preserving translationfrom each language to the other. In addition, we derive the standard securityproperty of non-interference of each language from that of the other via ourverified translation. These translations stand to have important implicationson the usability of IFC approaches. The coarse- to fine-grained direction canbe used to remove the label annotation burden that fine-grained systems imposeon developers, while the fine- to coarse-grained translation shows thatcoarse-grained systems -- which are easier to design and implement -- can trackinformation as precisely as fine-grained systems and provides an algorithm forautomatically retrofitting legacy applications to run on existingcoarse-grained systems.