Name
Abstract | ||
|---|---|---|
An application that fails to ensure information flow security may leak sensitive data such as passwords, credit card numbers, or medical records. News stories of such failures abound. Austin and Flanagan [2] introduce faceted values --- values that present different behavior according to the privilege of the observer --- as a dynamic approach to enforce information flow policies for an untyped, imperative $$\\lambda $$λ-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 and secure facet-aware socket-like communication. This library guarantees information flow security, independent of any vulnerabilities or bugs in application code. The library uses a control monad in the traditional way for encapsulating effects, but it also uniquely uses a second data monad to structure faceted values. To illustrate a non-trivial use of the library, we present a bi-monadic interpreter for a small language that illustrates the interplay of the control and data monads. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-662-49635-0_1 | POST |
Field | DocType | Volume |
Information flow (information theory),Programming language,Computer science,Covert channel,Imperative programming,Credit card,Theoretical computer science,Interpreter,Password,Haskell,Monad (functional programming) | Conference | 9635 |
ISSN | Citations | PageRank |
0302-9743 | 9 | 0.48 |
References | Authors | |
27 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thomas Schmitz | 1 | 15 | 0.88 |
| Dustin Rhodes | 2 | 15 | 1.54 |
| Thomas H. Austin | 3 | 307 | 15.96 |
| Kenneth Knowles | 4 | 55 | 3.33 |
| Cormac Flanagan | 5 | 2990 | 181.36 |