Arrows for secure information flow

11 years 6 months ago
Arrows for secure information flow
This paper presents an embedded security sublanguage for enforcing informationflow 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 all 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 formal proof that our embedded sublanguage provides noninterference, a concrete Haskel...
Peng Li, Steve Zdancewic
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where TCS
Authors Peng Li, Steve Zdancewic
Comments (0)