Department of Computer Science and Technology

CHERI

The Digital Security by Design (DSbD) Initiative

On 22 January 2019, the UK government announced that the UK Industrial Strategy Challenge Fund (ISCF) will support the integration of new fundamental hardware security through a £70M investment, to be matched by a further £117M from industry including from Microsoft and Google.

The ISCF Digital Security by Design challenge aims to radically update the foundation of our insecure digital computing infrastructure, by demonstrating that mainstream processor technology (e.g. from Arm) and software can be updated to include new security technologies based on the CHERI Architecture, along with accompanying innovations across system software, runtime environments, formal verification, and tools from the UK research base and businesses. The programme will create a hardware platform prototype in which a mainstream processor technology will be updated to include CHERI-like security technologies, along with formal modeling and verification of the architecture. The programme will fund work through the Innovate UK, EPSRC, and ESRC, and will support industrial transition and academic research around the prototype.

On 26 September 2019, UKRI announced a £8M funding call for research into CHERI as part of Digital Security by Design. As part of the program, Arm will produce a demonstrator CPU, SoC, and board based on experimental integration of CHERI into the ARMv8-A ISA. The boards will be available for industrial and academic research from 2021. Speakers at the Digital Security by Design Collaborators' Workshop in London included Robert Watson (University of Cambridge), Richard Grisenthwaite (Arm), and Manuel Costa (Microsoft). Slides and videos from the workshop are now online.

On 17 October 2019, Arm announced the Morello board, an experimental CPU, SoC, and board integrating CHERI support into an ARMv8-A baseline system. Our own Morello blog post on the Cambridge Security Research Group blog provides further background on the programme, as well as links to workshop slides and videos regarding CHERI and Morello. Our page on Morello provides more detail on the forthcoming board. The Department of Computer Science and Technology also has a blog post on DSbD and Morello.

This webpage supports the DSbD programme by providing supporting information on the CHERI architecture, software stack, and formal models; it will be updated frequently over the coming months as further information becomes available. The CHERI research team is eager to collaborate with academia and industry in exploring new potential applications and many unexplored research areas for CHERI (e.g., in hypervisors, in language runtimes, with higher-level programming languages, in formal verification, and so on).

The CHERI architecture

PIs: Robert N. M. Watson (University of Cambridge), Simon W. Moore (University of Cambridge), Peter Sewell (University of Cambridge), and Peter Neumann (SRI International)

Mainstream computer systems are chronically insecure. One of the main reasons for this is that conventional hardware architectures and C/C++ language abstractions provide only coarse-grained memory protection, which turns many coding errors into exploitable security vulnerabilities. CHERI is an ongoing research project, from 2010 to date, that revises the hardware/software architectural interface with hardware support for capabilities that can be used for fine-grained memory protection and/or scalable software compartmentalisation. CHERI aims to provide practically deployable performance and compatibility for software, as well as being microarchitecturally viable for mainstream architectures and microarchitectures.

CHERI is a hardware/software/semantics co-design project, combining hardware implementation, adaption of mainstream software stacks, and formal semantics and proof. The CHERI ideas have been developed first as a modification to 64-bit MIPS and now also for 32/64-bit RISC-V and 64-bit ARMv8-A. We have prototyped a complete software stack for CHERI by adapting widely used open-source software such as Clang/LLVM, FreeBSD, FreeRTOS, and applications such as WebKit, OpenSSH, and PostgreSQL. We have formally modeled the architecture and constructed a number of proofs about its security, as well as used these models for microarchitectural validation in our prototypes. These models also have the potential to support further activities such as formal proofs about software and microarchitecture.

We have published a number of technical reports and papers on the CHERI approach, including on the instruction set and its design, how efficient microarchitecture can support the CHERI model, and how software systems can be adapted to utilize CHERI's architectural features.

Digital Security by Design slides and videos

UKRI has now posted slides and videos from the 26 September 2019 Digital Security by Design Challenge Collaborators' Workshop::

  • Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter G. Neumann. CHERI: Capability Hardware Enhanced RISC Instructions, ISCF Digital Security by Design Challenge Collaborators' Workshop, London, UK, 26 September 2019. (Slides) (Video)
  • Richard Grisenthwaite (Arm). Digital Security by Design, ISCF Digital Security by Design Challenge Collaborators' Workshop, London, UK, 26 September 2019. (Slides) (Video)
  • Manuel Costa (Microsoft). Hardware Memory Safety: Challenges and Opportunities, ISCF Digital Security by Design Challenge Collaborators' Workshop, London, UK, 26 September 2019. (Slides) (Video)

Reports on the CHERI architecture

An Introduction to CHERI is a high-level description of our architectural, microarchitectural, formal methods, software model, and software prototyping approaches, as well as a guide to further reading on CHERI:

  • Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter G. Neumann. An Introduction to CHERI, Technical Report UCAM-CL-TR-941, Computer Laboratory, September 2019.

The authoritative reference to the CHERI Instruction-Set Architecture (ISA) is the ISA specification. This report is updated intermittently to reflect ongoing research into the CHERI approach; the current version, released in June 2019, is 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, Hongyan Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7), Technical Report UCAM-CL-TR-927, Computer Laboratory, June 2019.

Formal modeling and verification has been an essential part of both the practical day-to-day aspects of developing CHERI, as well as an essential longer-term argument for its security and maintainability. We describe this work in a tech report released in September 2019:

We have also recently released a technical report exploring the impact of Spectre-style attacks on systems implementing the CHERI architecture:

Announcements about DSbD and the Morello board

We have gathered a number of links to announcements and blog posts about DSbD and Arm's forthcoming Morello board here:

Reference CHERI software stack

As part of the DARPA-supported work to develop the CHERI Architecture, we have adapted a complete open-source software stack including compiler and toolchain (based on Clang/LLVM), general-purpose and embedded operating systems (based on FreeBSD and FreeRTOS), and application suite to the architecture (including software such as OpenSSH, PostgreSQL, and WebKit). This stack is "architecture neutral" in that it can support CHERI extensions on multiple architectures, including the original 64-bit MIPS CHERI and also more recent work on 32-bit and 64-bit RISC-V CHERI. With our industry partners, we anticipate providing a complete adaptation of this infrastructure to the hardware platform prototype.

We are currently preparing further technical reports for release in the autumn of 2019 in order to support the DSbD programme:

  • A new version of the CHERI Programmer's Guide technical report, last released in September 2015. The new version will take into account compiler and operating-system research since that date, as well as updates to our corresponding software prototypes. We anticipate this report being released in October 2019.

More information will be available soon.

Research papers on the CHERI Architecture

Over the past ten years, we have published numerous papers elaborating and exploring the CHERI protection model and its application to architecture, microarchitecture, and software, as well as formal modeling and verification of that architecture. A complete publications list can be found on the CHERI Publications Page. Recent publications of particular note include:

  • 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. Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. In Proceedings of the 41st IEEE Symposium on Security and Privacy (SP), May 2020.
  • 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. CHERI Concentrate: Practical Compressed Capabilities. In IEEE Transactions on Computers, 10.1109/TC.2019.2914037, IEEE, 2019.
  • Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, Jessica 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. CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment. In Proceedings of 2019 Architectural Support for Programming Languages and Operating Systems (ASPLOS’19). Providence, RI, USA, April 13-17, 2019
  • Alexandre Joannou, Jonathan Woodruff, Robert Kovacsics, Simon W. Moore, Alex Bradbury, Hongyan Xia, Robert N. M. Watson, David Chisnall, Michael Roe, Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter G. Neumann, Alfredo Mazzinghi, Alex Richardson, Stacey Son, and A. Theodore Markettos. Efficient Tagged Memory. Proceedings of the 2017 IEEE 35th International Conference on Computer Design (ICCD). Boston, MA, USA, November 5-8, 2017.
  • Robert N. M. Watson, Peter G. Neumann, and Simon W. Moore. Balancing Disruption and Deployability in the CHERI Instruction-Set Architecture (ISA), New Solutions for Cybersecurity, Shrobe H., Shrier D., Pentland A. eds., MIT Press/Connection Science: Cambridge MA. (to appear, fall 2017)
  • Robert N.M. Watson, Robert M. Norton, Jonathan Woodruff, Simon W. Moore, Peter G. Neumann, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Michael Roe, Nirav H. Dave, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Ed Maste, Steven J. Murdoch, Colin Rothwell, Stacey D. Son, and Munraj Vadera. Fast Protection-Domain Crossing in the CHERI Capability-System Architecture. IEEE Micro vol. 36 no. 5, p. 38-49, Sept.-Oct., 2016