Abstract:
This paper presents an embedded security sublanguage for
enforcing
information-flow policies in the standard Haskell programming
language. The sublanguage provides useful information-flow
control
mechanisms including dynamic security lattices, run-time code
privileges and declassification, without modifying the base
language. This design avoids the redundant work of producing new
languages, lowers the threshold for adopting security-typed
languages, and also provides great flexibility and modularity for
using security-policy frameworks.
The embedded security sublanguage is designed using a standard
combinator interface called arrows.
Computations constructed
in the sublanguage have static and explicit control-flow
components,
making it possible to implement information-flow control using
static-analysis techniques at run
time, while providing strong
security guarantees. This paper presents a concrete Haskell
implementation and an example application demonstrating the
proposed
techniques.
Documentation:
Encoding Information Flow in Haskell,
by Peng Li and Steve Zdancewic.
in Proceedings of the 19th IEEE Computer
Security Foundation Workshop (CSFW), July 2006.
Source code:
The source code used in the paper can be browsed online here.