Skip to main content
Kent Academic Repository

From fine- to coarse-grained dynamic information flow control and back

Vassena, Marco, Russo, Alejandro, Garg, Deepak, Rajani, Vineet, Stefan, Deian (2019) From fine- to coarse-grained dynamic information flow control and back. Proceedings of the ACM on Programming Languages, 3 (POPL). pp. 1-31. ISSN 2475-1421. E-ISSN 2475-1421. (doi:10.1145/3290389) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:90644)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL:
https://doi.org/10.1145/3290389

Abstract

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.

Item Type: Article
DOI/Identification number: 10.1145/3290389
Uncontrolled keywords: Information-flow control; verified source-to-source transformations; Agda
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Amy Boaler
Date Deposited: 06 Oct 2021 08:23 UTC
Last Modified: 04 Mar 2024 16:33 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/90644 (The current URI for this page, for reference purposes)

University of Kent Author Information

Rajani, Vineet.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.