From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper
We show that fine-grained and coarse-grained dynamic information-flow control (IFC) systems are equally expressive. 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. This result addresses a longstanding open problem in IFC: whether coarse-grained dynamic IFC techniques are less expressive than fine-grained dynamic IFC techniques (they are not!). The translations also 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.
Slides (POPL19.pdf) | 4.2MiB |
Fri 18 JanDisplayed time zone: Belfast change
15:21 - 16:27 | |||
15:21 22mTalk | LWeb: Information Flow Security for Multi-Tier Web Applications Research Papers James Parker University of Maryland, Niki Vazou IMDEA Software Institute, Michael Hicks University of Maryland, College Park Link to publication DOI Media Attached File Attached | ||
15:43 22mTalk | From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper Research Papers Marco Vassena Chalmers University of Technology, Alejandro Russo Chalmers University of Technology, Sweden, Deepak Garg Max Planck Institute for Software Systems, Vineet Rajani MPI-SWS, Deian Stefan University of California San Diego Link to publication DOI Media Attached File Attached | ||
16:05 22mTalk | Modalities, Cohesion, and Information Flow Research Papers Alex Kavvos Wesleyan University Link to publication DOI Pre-print File Attached |