Author:

Keywords:

G0G0519N#56397259

Abstract:

Our modern society increasingly relies upon computing devices for its proper functioning. With their increased presence, the number of interactions between different software components also increases. To secure this interaction and contain the impact of bug exploits (both malicious and accidental in nature), some form of security primitive to enforce the interface between different components is required. In this dissertation, we study hardware capabilities as a possible solution to this problem. Capabilities are hardware-enforced, bounds-checked pointers that carry permissions. They are an assembly-level hardware primitive that allows for fine-grained spatial protection within components, and lightweight compartmentalization between components. They have been researched since the 60s, but have recently seen renewed interest thanks to the CHERI project at the University of Cambridge. Given their low-level and flexible nature, writing correct and secure capability-manipulating programs is difficult. To remedy this problem, this thesis studies methods to reason formally about the security offered by capabilities. We capture these guarantees in a form of general security contract for a capability machine, which we call a universal contract. This universal contract describes how capabilities limit the power of arbitrary, untrusted code. Thus, it enables us to verify whether concrete application code satisfies certain properties of interest, even in the presence of arbitrary untrusted code. The first contributions of this thesis illustrate this approach in various settings. We introduce formal, mechanized models of different capability machines that leverage intra-language universal contracts to reason about concrete assembly code. The first model, Cerise, illustrates how one can reason about the spatial protection and compartmentalization provided by a vanilla capability machine. To illustrate the model, we verify a counter that depends on encapsulation of private state and a heap-based calling convention that uses dynamic memory allocation. We also verify an example of dynamic sealing, illustrating that hardware capabilities are sufficiently powerful to implement design patterns from the object capability literature at the assembly level. Next, support for effects in the form of Memory-Mapped I/O (MMIO) is added to the Cerise model. Compartmentalization offered by capabilities is used to build lightweight, nestable security wrappers around I/O devices. The wrappers enable layered enforcement of full-system safety properties on MMIO traces admitted by the capability machine. Interestingly, different layers of wrappers can be verified under different attacker models, and the results obtained by verifying layers closer to the hardware can be reused when verifying higher layers. This nesting and the ensuing opportunities for verification are difficult to achieve efficiently on commodity hardware. To illustrate the model, we verify two examples in a three-layer system of wrappers, where each layer reuses results from the previous one and considers a more refined attacker model. The last instance of universal contracts we focus on is in efficiently supporting a form of enclaved execution on top of capability hardware; a combination that had not been achieved before. Enclaved execution is a popular mechanism for dynamically creating Trusted Execution Environments (TEEs) called enclaves. Enclaves are isolated execution contexts that protect integrity and confidentiality of software inside the enclave (even against compromised system software) and that support attestation. We demonstrate a novel, bottom-up design for flexible enclaves on top of a capability machine and present three different implementations of the design, providing preliminary performance benchmarks. Pinpointing the correct formal treatment of enclaved execution as a universal contract is ongoing work. Reasoning about code at the assembly level is hard and error-prone. As a final contribution, we therefore shift our focus from intra-language assembly-level reasoning to reasoning about secure compilation to capability architectures. The standard criterion of full abstraction is used to instantiate secure compilation, and a compiler from separation-logic-verified C-like code to C-like code with support for so-called linear capabilities (a non-duplicable type of capability) is proven fully abstract. The intuition behind the compiler is that the linear separation logic resources can be reified and represented by linear capabilities at the target level. The full abstraction proof roughly implies that attacks that are possible on the target-level capability architecture must have already been possible at the verified source level, i.e. the compiler did not create additional security issues not present at the source level. In the long run, the hope is to support a form of gradual verification, where security-critical parts of C codebases can be verified and compiled with this compiler, in such a way that security guarantees are upheld in the presence of buggy or untrusted code.