Runtime enforcement mechanisms are an important and well-employed method for ensuring an execution only exhibits acceptable behavior, as dictated by a security policy. Wherever interaction occurs between two or more parties that do not completely trust each other, it is most often the case that a runtime enforcement mechanism is between them in some form, monitoring the exchange. Considering the ubiquity of such scenarios in the computing world, there has been an increased effort to build formal models of runtime monitors that closely capture their capabilities so that their effectiveness can be analysed more precisely. While models have grown more faithful to their real-life counterparts, is- sues concerning complexity and manageability (a common concern for software engineers) of centralized policies remains to be fully addressed. The goal of this thesis is to provide a principled approach to policy construction that is modular, intuitive, and backed by formal methods. This thesis introduces a class of policy combinators adequate for use with runtime en- forcement policies and analyses a particular instance of them called Static Committee Com- binators (SCCs). SCCs present a model of policy composition where combinators act as committees that vote on events passing through the monitor. They were conceptualized in collaboration with Jay Ligatti and Daniel Lomsak. The general class of combinators are called Static Decision Combinators (SDCs), which share key features with SCCs such as allowing combinators to respond with alternative events when polled, in addition to re- sponding with grants or denials. SDCs treat the base-level policies they compose as black boxes, which helps decouple the system of combinators from the underlying policy model. The base policies could be modelled by automata but the combinators would not maintain their own state, being "static". This allows them to be easily defined and understood using truth tables, as well as analysed using logic tools. In addition to an analysis of SDCs and SCCs, we provide useful examples and a reusable combinator library.

Over the last years, security-kernels have played a promising role in reshaping the landscape of platform security on embedded devices. Security-kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms on a small TCB, which enforces isolation between components. The reduced TCB  minimizes the system attack surface and facilitates the use of formal methods to ensure the kernel functional correctness and security. In this thesis, we explore various aspects of building a provably secure separation kernel using virtualization technology. We show how the memory management subsystem can be virtualized to enforce isolation of system components. Virtualization is done using direct-paging that enables a guest software to manage its own memory configuration. We demonstrate the soundness of our approach by verifying that the high-level model of the system fulfills the desired security properties. Through refinement, we then propagate these properties (semi-)automatically to the machine-code of the virtualization mechanism. Further, we show how a runtime monitor can be securely deployed alongside a Linux guest on a hypervisor to prevent code injection attacks targeting Linux. The monitor takes advantage of the provided separation to protect itself and to retain a complete view of the guest. Separating components using a low-level software cannot by itself guarantee the system security. Indeed, current processors architecture involves features that can be utilized to violate the isolation of components. We present a new low-noise attack vector constructed by measuring caches effects which is capable of breaching isolation of components and invalidates the verification of a software that has been verified on a memory coherent model. To restore isolation, we provide several countermeasures and propose a methodology to repair the verification by including data-caches in the statement of the top-level security properties of the system. / <p>QC 20170831</p> / PROSPER / HASPOC