On the expressiveness and semantics of information flow types

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 ${\text{SLIO}}^{\ast }$ , 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 ${\text{SLIO}}^{\ast }$ to FG is straightforward since FG tracks dependence at a granularity finer than ${\text{SLIO}}^{\ast }$ does. However, the translation from FG to ${\text{SLIO}}^{\ast }$ is quite involved and relies extensively on label quantification. We further examine the reason for this complexity using a slight variant of ${\text{SLIO}}^{\ast }$ , 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, ${\text{SLIO}}^{\ast }$ and CG, which we use to prove these type systems sound and also to prove the translations between them correct.