Department of Computer Science and Technology

CHERI

Capability Hardware Enhanced RISC Instructions (CHERI)


June 2019: Learn about the CHERI architecture! We have now posted CHERI ISAv7. This new version of the ISA elaborates CHERI-RISC-V, adopts the CHERI Concentrate compression model, adds support for side-channel resistance, and makes a variety of other changes to improve performance and functionality. This is the first version of our specification that directly incorporates formal description of the ISA.
April 2019: We are pleased to announce that our ASPLOS 2019 paper on CHERI and OS design, CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment, on the general-purpose OS design implications of CHERI when used for ubiquitous memory safety, has won an ASPLOS Best Paper award.
August 2018: The New Scientist has published an article, Uncrackable computer chips stop malicious bugs attacking your computer, covering CHERI and other projects relating to security-focused computer architectures.
Learn more about fundamental research into security and the hardware-software interview by watching Robert Watson's August 2012 ACM Queue interview.

This project is an outgrowth of our earlier Capsicum project, which explored hybrid capability models in the context of UNIX operating system design. While a successful project, we identified a number of limitations to current CPU designs that made application compartmentalisation tricky, despite enhanced operating system support. CHERI is a hardware-software interface research project seeking to revise ISA design in order to better support software compartmentalisation. CHERI transposes the Capsicum hybrid capability model into the CPU architecture space, allowing fine-grained compartmentalisation within process address spaces – while continuing to support current software designs.

Prototype CHERI-MIPS processor on FPGA

We have developed a prototype of the CHERI ISA using the Bluespec Extensible RISC Implementation (BERI), a 64-bit MIPS FPGA soft core implemented in the Bluespec HDL. The FreeBSD operating system has also been ported to CHERI in order to allow us to compare, side-by-side, traditional software compartmentalisation approaches (based on a translation look-aside buffer (TLB)), with those supported by a capability coprocessor. We run lightly modified commodity software stacks (see below) on this prototype, allowing us to validate our hybrid design, evaluating compatibility, performance, and security implications of our changes to hardware and software.

Prototype CHERI software stack

We have developed a significant CHERI prototype software stack to explore and evaluate the implications of CHERI on compatibility, performance, and security for off-the-shelf C/C++ software stacks. This includes adapted versions of the Clang/LLVM compiler suite, FreeBSD and FreeRTOS operating systems, and numerous userspace libraries and applications, including WebKit, to run on the CHERI Architecture.

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. The ISA model for CHERI-MIPS, in Sail, is available. 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.

Qemu-CHERI

We have also developed a Qemu CHERI-MIPS implementation, which provides an ISA-level emulation of our CHERI extensions to the 64-bit MIPS ISA. While not micro-architecturally realistic, this emulation can be useful for software development, especially in the absence of an FPGA or access to Bluespec. It is faster than the Sail-generated C emulator, but less directly based on the Sail CHERI-MIPS ISA specification.

Media

  • Robert N. M. Watson, the New Scientist's 11 August 2018 issue contains an article, Uncrackable computer chips stop malicious bugs attacking your computer, describes ongoing research involving architectural security, including CHERI. Link.
  • Robert N. M. Watson, the Economist's June 2014 Technology Quarterly explores how compartmentalised software designs can mitigate vulnerabilities such as Heartbleed could impact privacy in Big Data systems. Link.
  • Peter G. Neumann, the San Jose Mercury News's Bruce Newman talks with Peter Neumann about cybersecurity. Link.
  • Robert N. M. Watson, IEEE Spectrum Techwise Conversation podcast interview, recorded 26 December 2012, explores the argument for clean-slate design and the nature of current attacker-defender asymmetry. Link.
  • Robert N. M. Watson, Queue Portrait: Robert Watson recorded in August 2012, explores research into the hardware-software interface. Link.