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

MAC, A Verified Information-Flow Control Library

Marco Vassena (Institutionen för Data- och informationsteknik, Informationssäkerhet (Chalmers))
Gothenburg : Chalmers University of Technology, 2017.
[Licentiatavhandling]

Information Flow Control (IFC) is a language-based security mechanism that tracks where data flows within a program and prevents leakage of sensitive data. IFC has been embedded in pure functional languages such as Haskell, in the form of a library, thus reducing the implementation and maintenance effort and fostering a secure-by-construction programming-model. MAC is a state-of- the-art IFC Haskell library that detects leaks statically and that supports many advanced programming features, such as exceptions, mutable references and concurrency. While MAC is an elegant functional pearl and is implemented concisely in less than 200 lines of code, it does not provide any formal security guarantee.

This thesis presents the first full-fledged verified formal model of MAC, which guarantees that any program written against the library’s API satisfies non-interference by construction. In particular, the contributions of this work improve MAC in three areas: formal verification techniques, expressivity and protection against covert channels. Firstly, the thesis enriches term erasure with two-steps erasure, a novel flexible technique, which has been used to reason systematically about the security implications of advanced programming features and that greatly simplifies the non-interference proof. Secondly, this work gives a functor algebraic structure to labeled values, an abstract data type which protects values with explicit labels, thus enabling flexible manipulation of labeled data through classic functional programming patterns. Thirdly, the thesis closes the sharing-based internal-timing covert channel, which exploits the sharing feature of lazy evaluation to leak data, by affecting the timing behavior of threads racing to gain access to some shared resource. We design an unsharing primitive that disables sharing by lazily duplicating thunks and we apply it to restrict sharing, when needed for security reasons.

All the results presented in this thesis have been corroborated with extensive mechanized proofs, developed in the Agda proof assistant.

Nyckelord: Agda, NonInterference, Information-Flow Control, Haskell, Functional Programming



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2017-05-11. Senast ändrad 2017-06-02.
CPL Pubid: 249247

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

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


Institutioner (Chalmers)

Institutionen för Data- och informationsteknik, Informationssäkerhet (Chalmers)

Ämnesområden

Informations- och kommunikationsteknik
Datavetenskap (datalogi)

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:


Flexible manipulation of labeled values for information-flow control libraries


On formalizing information-flow control libraries


Securing Concurrent Lazy Programs Against Information Leakage


Examination

Datum: 2017-06-09
Tid: 13:15
Lokal: Lecture hall EC, EDIT building, Johanneberg Campus, Rännvägen 6B
Opponent: Prof. David Pichardie, Department of Computer Science, ENS Rennes, France