On the Foundations of Practical Language-Based Security

Sammanfattning: Language-based information flow control (IFC) promises to provide programming languages and tools that make it easy for developers to write secure code. Traditionally, research in this field aims to build a variant on a programming language or system that lets developers write code that gives them strong guarantees beyond the potential memory- and type-safety guarantees of modern languages. However, two developments in the field challenge this paradigm. Firstly, backwards-compatible security enforcement without false alarms promises to retrofit security enforcement on code that was not written with the enforcement mechanism in mind. This has the potential to greatly increase the applicability of IFC enforcement to legacy and mobile code from untrusted sources. Secondly, library-based security, a technique by which IFC researchers provide a software library in an established language whose programming interface gives the same guarantees as a stand-alone IFC tool for developers to use promises to do away with specialized IFC languages. This technique also has the potential to increase the applicability of IFC enforcement as developers no longer need to adopt a whole new language to get security guarantees. This thesis makes contributions to both these recent developments that come in two parts; the first part concerns enforcing secure information flow without introducing false alarms while the second part concerns the correctness of using libraries instead of fullyfledged IFC programming languages to write secure code. The first part of the thesis makes the following contributions: 1. It unifies the existing literature, in the form of Secure Multi-Execution and Multiple Facets, on security enforcement without false alarms by introducing Faceted Secure Multi-Execution. 2. It explores the unique optimisation challenges that appear in this setting. Specifically, mixing multi-execution and facets means that unnecessarily large faceted trees give rise to unnecessary executions in multi-execution and vice verse. This thesis proposes optimisation strategies that can overcome this hurdle. 3. It proves an exponential lower bound on black-box false-alarm-free enforcement and new possibility results for false-alarm-free enforcement of a variant of the noninterference security condition known as termination insensitive noninterference. 4. It classifies the special cases of enforcement that is not subject to the aforementioned exponential lower bound. Specifically, this thesis shows how and why the choice of security lattice makes the difference between exponential, polynomial, and constant overheads in multi-execution. In short, the first part of the thesis unifies the existing literature on false-alarm-free IFC enforcement and presents a number of results on the performance of enforcement mechanisms of this kind. The second part of the thesis meanwhile makes the following contributions: 1. It reduces the trusted computing base of security libraries by showing how to implement secure effects on top of an already secure core without incurring any new proof obligations. 2. It shows how to simplify DCC, the core language in the literature, without losing expressiveness. 3. It proves that noninterference can be derived in a simple and straightforward way from parametricity for both static and dynamic security libraries. This in turn reduces the conceptual gap between the kind of security libraries that are written today and the proofs one can write to prove that the libraries ensure noninterference. In short, the second part of the thesis provides a new direction for thinking about the correctness of security libraries by both reducing the amount of trusted code and by introducing improved means of proving that a security library guarantees noninterference.