| Title | Securing Concurrent Lazy Programs Against Information Leakage |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Vassena, M., Breitner, J., Russo, A. |
| Conference Name | 2017 IEEE 30th Computer Security Foundations Symposium (CSF) |
| Keywords | Agda proof assistant, composability, Concurrency, concurrency control, concurrent lazy programs security, covert channel, Cyber-physical systems, data privacy, data structures, functional languages, Functional programming, Haskell, Haskell libraries, IFC libraries, IFC tools, information leakage, information-flow control tools, Lattices, lazy calculus, lazy evaluation, lazy languages, lazyDup, Libraries, Message systems, Metrics, noninterference, program diagnostics, pubcrawl, resilience, Resiliency, security, security library MAC, security of data, Sensitivity, software libraries, software tools, theorem proving, Timing, Writing |
| Abstract | Many state-of-the-art information-flow control (IFC) tools are implemented as Haskell libraries. A distinctive feature of this language is lazy evaluation. In his influencal paper on why functional programming matters, John Hughes proclaims:,,Lazy evaluation is perhaps the most powerful tool for modularization in the functional programmer's repertoire.,,Unfortunately, lazy evaluation makes IFC libraries vulnerable to leaks via the internal timing covert channel. The problem arises due to sharing, the distinguishing feature of lazy evaluation, which ensures that results of evaluated terms are stored for subsequent re-utilization. In this sense, the evaluation of a term in a high context represents a side-effect that eludes the security mechanisms of the libraries. A naive approach to prevent that consists in forcing the evaluation of terms before entering a high context. However, this is not always possible in lazy languages, where terms often denote infinite data structures. Instead, we propose a new language primitive, lazyDup, which duplicates terms lazily. By using lazyDup to duplicate terms manipulated in high contexts, we make the security library MAC robust against internal timing leaks via lazy evaluation. We show that well-typed programs satisfy progress-sensitive non-interference in our lazy calculus with non-strict references. Our security guarantees are supported by mechanized proofs in the Agda proof assistant. |
| DOI | 10.1109/CSF.2017.39 |
| Citation Key | vassena_securing_2017 |
Securing Concurrent Lazy Programs Against Information Leakage