Thomas H. Austin, Kenneth Knowles, Cormac Flanagan
07/14/2014 09:28 AM
Computer Science
When an application fails to ensure information flow security, it may leak sensitive data such as passwords, credit card numbers, or medical records. News stories of such failures abound. Austin and Flanagan [2012] introduce faceted values – values that present different behavior according to the privileges of the observer – as a dynamic approach to enforcing information flow policies for an untyped, imperative λ-calculus.
We implement faceted values as a Haskell library, elucidating their relationship to types and monadic imperative programming. In contrast to previous work, our approach does not require modification to the language runtime. In addition to pure faceted values, our library supports faceted mutable reference cells, secure facet- aware socket-like communication, and robust declassification.
