Skip to main content

On the expressiveness and semantics of information flow types

Rajani, Vineet, Garg, Deepak (2020) On the expressiveness and semantics of information flow types. Journal of Computer Security, 28 (1). pp. 129-156. ISSN 1875-8924. E-ISSN 1875-8924. (doi:10.3233/JCS-191382) (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:90647)

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.3233/JCS-191382

Abstract

Information Flow Control (IFC) is a form of dependence analysis that tracks and prohibits dependence of public outputs on secret inputs. Such a dependence analysis is often carried out using a type system. IFC type systems can track dependence (via confidentiality labels) at varying levels of granularity. On one extreme, there are fine-grained type systems that track dependence at the level of individual values. They label individual values. On the other extreme, there are coarse-grained type systems that track dependence at the level of entire computations. These type systems do not label individual values but instead label entire sub-computations. An important foundational question is one of the relative expressiveness of these two classes of IFC type systems. In this paper we show that, despite the glaring differences in how they track dependence, the two classes of type systems are actually equally expressive. We do this by showing translations from FG, a fine-grained IFC type system derived from SLAM (In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (1998)), to SLIO∗, a coarse-grained IFC type system derived from HLIO (In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP) (2015)), and vice-versa. The translation from SLIO∗ to FG is straightforward since FG tracks dependence at a granularity finer than SLIO∗ does. However, the translation from FG to SLIO∗ is quite involved and relies extensively on label quantification. We further examine the reason for this complexity using a slight variant of SLIO∗, called CG, to which FG can be translated more easily. As a separate, more foundational contribution we show how to extend logical relation models of information flow to languages with higher-order state. Specifically, we build world-indexed (Kripke) logical relations for FG, SLIO∗ and CG, which we use to prove these type systems sound and also to prove the translations between them correct.

Item Type: Article
DOI/Identification number: 10.3233/JCS-191382
Uncontrolled keywords: Information flow control; type systems; typed translation; logical relations; type system expressiveness
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:35 UTC
Last Modified: 08 Oct 2021 11:09 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/90647 (The current URI for this page, for reference purposes)
  • Depositors only (login required):