Types for Information Flow Control: Labeling Granularity and Semantic Models

TL;DR

This paper demonstrates that fine-grained and coarse-grained language-based information flow control type systems are equally expressive by providing translations and extending logical relation models to higher-order state.

Contribution

It establishes the equivalence of different granularity levels in IFC type systems through semantics-preserving translations and extends logical relations to higher-order state.

Findings

Fine-grained and coarse-grained systems are equally expressive.

Translations between the two systems preserve semantics and types.

Logical relations are extended to higher-order state for soundness proofs.

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.