Willard Rafnsson
IT University of Copenhagen
Types for Information-Flow Control in Functional Programming Languages
Information flow control (IFC) is central to computer security. The objective of IFC is to prevent unauthorized flows of information, e.g. flows of secret information to public outputs of a computation.
In this talk, we present the state-of-the-art of type systems for IFC in functional programming languages. We do this by considering two extreme approaches. One extreme, taken in Flow Caml (IFC for ML), is to label all values individually and track dependencies at the level of values. The other extreme, taken in HLIO (IFC for Haskell), is to only assign a single label to a whole computation context (a monad), and to track dependencies at the level of computations (via. bind).
Surprisingly, despite their glaring differences, these approaches are equally expressive. To demonstrate this, we sketch a translation between the two above-mentioned type systems, that is both semantics- and types-preserving.
