Department of Computer Science and Technology

CHERI

CHERI Rigorous Engineering

CHERI uses a range of rigorous engineering techniques to speed development and increase assurance, in a hardware/software/semantics co-design process. We use formal models of the complete instruction-set architectures (ISA) at the heart of our design and engineering, both in lightweight ways that support and improve normal engineering practice - as documentation, in emulators used as a test oracle for hardware and for running software, and for test generation - and for formal verification. We formalise key intended security properties of the ISA specifications, and establish that these hold with mechanised proof. This is for the same complete ISA models (complete enough to boot operating systems), without idealisation.

Our work on CHERI C/C++, and on porting software to them, is also informed by and informs our Cerberus work on de facto and ISO C semantics.

All this is in collaboration with the REMS project.

ISA models

Our principal models, in our Sail instruction-set definition language, are:

From these, Sail generates sequential emulators, in C and OCaml, and theorem-prover definitions, in Coq, HOL4, and Isabelle, and SMT. The Sail instruction semantics is included, typeset automatically, in the CHERI ISA Specification.

The Sail CHERI-MIPS model is developed from an earlier model in Fox's L3 instruction-set definition language:

L3 also generates an emulator and Isabelle and HOL4 versions of the model.

We use the Sail (and L3) generated emulators as oracles to test CHERI hardware against, and to test and bring up CHERI software, the generated Isabelle definitions for formal mechanised proof of ISA security properties, and the generated SMT definitions for SMT checking of more specific properties.

Papers and documentation