Flexible Dynamic Information Flow Control in the Presence of Exceptions
This work addresses security concerns in language-based systems for developers and researchers, offering a novel approach to information flow control with exceptions and mutable references.
The paper tackles the problem of dynamic information flow control in programming languages by introducing LIO, a labeled IO monad that tracks and restricts data access based on labels and clearance, and it provides formal semantics and proofs for confidentiality and integrity in a λ-calculus with an implementation in Haskell.
We describe a new, dynamic, floating-label approach to language-based information flow control. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality. The current label floats to exceed the labels of all data observed and restricts what can be modified. Unlike other language-based work, LIO also bounds the current label with a current clearance that provides a form of discretionary access control. Computations may encapsulate and pass around the results of computations with different labels. In addition, the LIO monad offers a simple form of labeled mutable references and exception handling. We give precise semantics and prove confidentiality and integrity properties of a call-by-name λ-calculus and provide an implementation in Haskell.