CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Securing Concurrent Lazy Programs Against Information Leakage

Marco Vassena (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Joachim Breitner ; Alejandro Russo (Institutionen för Data- och informationsteknik, Informationssäkerhet (Chalmers))
30th IEEE Computer Security Foundations Symposium, CSF 2017; Santa Barbara; United States; 21 August 2017 through 25 August 2017 (1940-1434). p. 37-52. (2017)
[Konferensbidrag, refereegranskat]

Many state-of-the-art information-flow control (IFC) tools are implemented as Haskell libraries. In this language, lazy evaluation is a distinctive feature appreciated by developers. 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 naïve 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. We make the security library MAC robust against internal timing leaks via lazy evaluation, by using lazyDup to duplicate terms manipulated in high contexts, as they are evaluated. 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.

Nyckelord: Covert Channel, Haskell, Lazy Evaluation, Noninterference

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2017-05-10. Senast ändrad 2017-12-18.
CPL Pubid: 249245


Läs direkt!

Länk till annan sajt (kan kräva inloggning)