Skip to main content
Kent Academic Repository

Types for Information Flow Control: Labeling Granularity and Semantic Models

Rajani, Vineet, Garg, Deepak (2018) Types for Information Flow Control: Labeling Granularity and Semantic Models. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF). . IEEE ISBN 978-1-5386-6681-4. E-ISBN 978-1-5386-6680-7. (doi:10.1109/csf.2018.00024) (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:90641)

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:
http://dx.doi.org/10.1109/CSF.2018.00024

Abstract

Language-based information flow control (IFC) tracks dependencies within a program using sensitivity labels and prohibits public outputs from depending on secret inputs. In particular, literature has proposed several type systems for tracking these dependencies. On one extreme, there are fine-grained type systems (like Flow Caml) that label all values individually and track dependence at the level of individual values. On the other extreme are coarse-grained type systems (like HLIO) that track dependence coarsely, by associating a single label with an entire computation context and not labeling all values individually. In this paper, we show that, despite their glaring differences, both these styles are, in fact, equally expressive. To do this, we show a semantics- and type-preserving translation from a coarse-grained type system to a fine-grained one and vice-versa. The forward translation isn't surprising, but the backward translation is: It requires a construct to arbitrarily limit the scope of a context label in the coarse-grained type system (e.g., HLIO's "toLabeled" construct). As a separate contribution, we show how to extend work on logical relation models of IFC types to higher-order state. We build such logical relations for both the fine-grained type system and the coarse-grained type system. We use these relations to prove the two type systems and our translations between them sound.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1109/csf.2018.00024
Uncontrolled keywords: Security; Computational modeling; Lattices; Labeling; Semantics; Standards; Software systems; Information-flow-control; type-systems; logical-relations; granularity; translations
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:16 UTC
Last Modified: 04 Mar 2024 17:47 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/90641 (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.