hide
Free keywords:
Computer Science, Programming Languages, cs.PL,Computer Science, Cryptography and Security, cs.CR
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.
