Skip to main content
Article
Typed Faceted Values for Secure Information Flow in Haskell
Technical Report UCSC-SOE-14-07 (2014)
  • Thomas H. Austin, University of California, Santa Cruz
  • Kenneth Knowles, University of California, Santa Cruz
  • Cormac Flanagan, University of California, Santa Cruz
Abstract
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.
Keywords
  • Computer Science,
  • Haskell,
  • Secured information,
  • Faceted values,
  • programming
Disciplines
Publication Date
July 14, 2014
Publisher Statement
SJSU users: use the following link to login and access the article via SJSU databases
Citation Information
Thomas H. Austin, Kenneth Knowles and Cormac Flanagan. "Typed Faceted Values for Secure Information Flow in Haskell" Technical Report UCSC-SOE-14-07 (2014)
Available at: http://works.bepress.com/thomas_austin/14/