Joint work with Kyndylan Nienhuis, Alexandre Joannou, Anthony Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell

Memory safety bugs are still a major source of security vulnerabilities. CHERI aims to address this by extending commodity instruction set architectures with hardware support for capabilities, enabling fine-grained memory protection and scalable software compartmentalisation while maintaining performance. CHERI was initially developed as a MIPS extension, but work on versions for RISC-V and ARM is underway.

The integration of such a security mechanism into hardware architectures requires high confidence in its correctness: one bug in the mechanism or its interaction with other architecture features can lead to security vulnerabilities in all implementations of the architecture. This makes machine-checked statements and proofs of the intended security properties essential.

In this talk, we discuss our formal models of production-scale ISAs with CHERI extensions, as well as our formalisation of key security properties of those ISAs. In particular, these properties establish bounds on which capabilities arbitrary code can construct from an initial set of capabilities. As a use case of the capability mechanism, we discuss the isolation of a software compartment. The properties and the isolation scenario have been formalised and verified using the interactive theorem prover Isabelle/HOL w.r.t. a model of the complete CHERI-MIPS ISA. Work on verifying the properties for prototypes of CHERI-RISC-V and CHERI-ARM is ongoing.