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

  • Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, 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. In Security and Privacy 2020. [ bib | project page | pdf | abstract ]
  • An Introduction to CHERI. Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter Neumann. Technical Report UCAM-CL-TR-941, University of Cambridge, Computer Laboratory, September 2019. [ bib | project page | pdf | abstract ]
  • Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. Kyndylan Nienhuis, Alexandre Joannou, Anthony Fox, Michael Roe, Thomas Bauereiss, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. Technical Report UCAM-CL-TR-940, University of Cambridge, Computer Laboratory, September 2019. [ bib | pdf | abstract ]
  • Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7). Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Nathaniel Wesley Filardo, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton, Alex Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia. Technical Report UCAM-CL-TR-927, University of Cambridge, Computer Laboratory, June 2019. 496pp. [ bib | pdf | abstract ]
  • CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment. Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and Jonathan Woodruff. In ASPLOS 2019, Best paper award. [ bib | DOI | project page | pdf | http | abstract ]
  • CHERI Concentrate: Practical Compressed Capabilities. Jonathan Woodruff, Alexandre Joannou, Hongyan Xia, Anthony Fox, Robert Norton, Thomas Bauereiss, David Chisnall, Brooks Davis, Khilan Gudka, Nathaniel W. Filardo, A. Theodore Markettos, Michael Roe, Peter G. Neumann, Robert N. M. Watson, and Simon W. Moore. IEEE Transactions on Computers, 2019. [ bib | DOI | pdf | abstract ]
  • CheriABI: Enforcing valid pointer provenance and minimizing pointer privilege in the POSIX C run-time environment. Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and Jonathan Woodruff. Technical Report UCAM-CL-TR-932, University of Cambridge, Computer Laboratory, January 2019. [ bib | project page | pdf | abstract ]
  • ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 71. [ bib | DOI | supplementary material | project page | pdf | abstract ]
  • Exploring C Semantics and Pointer Provenance. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311. [ bib | DOI | supplementary material | project page | pdf | abstract ]
  • Extracting Behaviour from an Executable Instruction Set Model. Brian Campbell and Ian Stark. In FMCAD 2016, Full proceedings http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf. [ bib | pdf | abstract ]
  • Into the depths of C: elaborating the de facto standards. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N.M. Watson, and Peter Sewell. In PLDI 2016, PLDI 2016 Distinguished Paper award. [ bib | DOI | project page | pdf | http | abstract ]