arXiv · 1207.1457
Flexible Dynamic Information Flow Control in the Presence of Exceptions
Abstract
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 \lambda-calculus and provide an implementation in Haskell.
Explore related subjects
Keep this discovery
Deian Stefan, Alejandro Russo, John C. Mitchell, David Mazières. 2012-07-05. Flexible Dynamic Information Flow Control in the Presence of Exceptions. https://arxiv.org/abs/1207.1457
Cite the original work for its findings. Save a collection to share your selection of sources.