Despite decades of research, the computer industry still struggles to build secure systems. The majority of security vulnerabilities are caused by a combination of two fundamental problems. First, mainstream engineering methods are not suited to find small bugs in corner cases. Second, mainstream hardware architectures and C/C++ language abstractions provide only coarse-grained memory protection, which lets these small bugs escalate to serious security vulnerabilities. CHERI, the context of our work, is an ongoing research project that addresses the second problem with hardware support for fine-grained memory protection and scalable software compartmentalisation. CHERI achieves this by extending commodity hardware architectures with a capability system, in which all memory accesses must be authorised by a capability. Capabilities are unforgeable tokens that contain address bounds and permissions, determining the memory region and the types of accesses they can authorise. They can be passed around and manipulated only in specific ways. CHERI has been initially developed as CHERI-MIPS, with later work on CHERI-RISC-V.

In this thesis, we address the first problem in the context of CHERI: we formally state and prove security properties for the CHERI-MIPS architecture. Our first set of security properties forms a new abstraction layer of CHERI-MIPS, explaining execution steps in terms of nine abstract actions, one for each kind of memory access, capability manipulation, and security domain transition. We use this abstraction to reason about arbitrary code: we characterise which capabilities can be accessed or constructed by potentially compromised or malicious code and which memory locations it can overwrite until it transitions to another security domain. We use this to prove the correctness of a simple compartmentalisation scenario, in which CHERI’s capability system is used to isolate a component from the rest of the system. Our results are based on a full, non-idealised, sequential specification of CHERI-MIPS, which is complete enough to boot an operating system. The challenges of proving our properties include the size of the architecture, its easy-to-miss corner cases, and the fact that the architecture keeps evolving.

As a step towards CHERI’s industrial adoption, the Morello program is developing the eponymous prototype CHERI extension of the Armv8-A architecture, along with a processor implementation, development board, and software. Building on our work, the formal verification of architectural security properties is an important part of this program.