Typed Faceted Values for Secure Information Flow in Haskell
Thomas H. Austin, Kenneth Knowles, Cormac Flanagan · 2014
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 facetaware socket-like communication, and robust declassification.