Today, computer security is often based on mitigations that make exploitation cumbersome or unlikely. In other words, mitigation techniques provide no security guarantee, and time and time again mitigations have been circumvented.
To stop the ongoing exploit-mitigation arms-race, we need security enforcement mechanisms that can be proven impossible to circumvent. Unfortunately, mainstream computers have the necessary security primitives to support such enforcement mechanisms. Capability machines are computers that provide additional security primitives by replacing pointers with capabilities. Capabilities are unforgeable tokens of authority that must be used to access memory and other system resources.

In this dissertation, we present foundational research in the field of secure compilation that targets capability machines. In particular, we present novel and provably secure enforcement mechanisms for control-flow and encapsulation properties of high-level programming languages -- properties that all programmers rely on. The security proof demonstrates for the first time how state-of-the-art reasoning techniques for high-level programming languages can be used to reason about capability safety and secure compilation at the very lowest level. We also contribute new proof techniques for secure compilation proofs.

In Chapter 1, we introduce the concept of capabilities, show various instances of capabilities throughout computer science, and present and motivate the contents of this dissertation.

In Chapter 2, we present a formalisation of a capability machine with local capabilities and a calling convention that provably enforces well-bracketed control-flow (WBCF) and local-state encapsulation (LSE). We also present a notion of capability safety in terms of a logical relation. Using the logical relation, we prove correctness of program examples that interact with unknown code and rely on non-trivial control-flow for correctness. 

In Chapter 3, we present a formalisation of a capability machine with linear capabilities along with StkTokens: another calling convention provably enforcing WBCF and LSE.
Via a novel proof technique called fully-abstract overlay semantics, we prove that  StkTokens enforces these properties. The overlay semantics simplifies the full-abstraction proof significantly by retaining the language syntax and adding the desired property semantically.