Formal Modelling and Proof in the CHERI Design and Implementation Process

Explore the rigorous engineering methods applied to develop a security-enhanced processor architecture in this IEEE conference talk. Delve into the use of formal models for the complete instruction-set architecture (ISA) in the design and engineering process of CHERI, a hardware capability-based architecture supporting fine-grained memory protection and scalable secure compartmentalization. Learn about the formalization of key security properties and their verification through mechanized proof. Discover how these methods have been integral to CHERI's development, enabling rapid experimentation and increasing confidence in the design. Gain insights into the potential adoption of CHERI in mass-market commercial processors and its implications for addressing memory safety issues in computing.

Microsoft: 70% of patched vulnerabilities are memory safety issues
Two fundamental problems
Rigorous engineering for hardware security
CHERI: hardware support for capabilities
Versions of CHERI
Fine-grained memory protection
Capability manipulations
Scalable software compartmentalisation
Protection domain transitions
A prose architecture description
A formal architecture model
The formal specification of Cload
Prose security properties
Formal security properties
Mapping instructions to abstract actions
Property about storing data
Monotonicity of reachable capabilities
Memory isolation between compartments
Conclusion