Types for Information Flow Control: Labeling Granularity and Semantic Models
This work addresses foundational issues in language-based security for researchers, providing theoretical insights into the equivalence of different IFC approaches, but it is incremental as it builds on existing type systems without introducing a new paradigm.
The paper tackles the problem of comparing fine-grained and coarse-grained type systems for information flow control, showing they are equally expressive through semantics- and type-preserving translations, with a surprising backward translation requiring a construct like 'toLabeled'. It also extends logical relation models to higher-order state to prove soundness for both systems and the translations.
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.