Encoding Information Flow in Haskell

Encoding Information Flow in Haskell by Peng Li and Steve Zdancewic.

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 secirity 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 sstandard 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.

Very interesting use of arrows. EDSL in Haskell with privilege informations encoded in the type, & more; fun!

[Edit: corrected link]

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I assume you mean...

Li and Zdancewic also did

Li and Zdancewic also did the Language-Based Approach to Unifying Events and Threads, which I couldn't fully wrap my head around. Should give it one more try, though.