£190m programme will create new CHERI-ARM CPU

A team of researchers at the Department of Computer Science and Technology are working with Arm and others to radically update the foundation of today's insecure digital computing infrastructure, funded by a new £190m UKRI Digital Security by Design (DSbD) programme. The UKRI will provide £70m funding and this is expected to be matched by up to £117 million from industry, from companies including Google and Microsoft.

Mainstream computer systems are chronically insecure. Conventional hardware instruction sets and the C/C++ programming languages, dating back to the 1970s, provide only coarse-grained memory protection. This turns many coding errors into exploitable security vulnerabilities.

CHERI is an ongoing research project that revises the hardware/software architectural interface with hardware support for capabilities that can be used for fine-grained memory protection and scalable software compartmentalisation.

The team at the University of Cambridge: Simon Moore, Robert N. M. Watson and Peter Sewell (left to right)

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 mainstream processor technology in all mobile phones and tablets is based on the Arm architecture. The Digital Security by Design programme will explore ideas for updating the Arm processor technology to include new security technologies based on CHERI. This aims to demonstrate that many of the security attacks that plague modern systems can be prevented.

Arm, funded by the programme, will create a hardware platform prototype called "Morello", in which a mainstream high-performance processor and software stack is enhanced with CHERI security technologies. The programme will fund additional work around CHERI experimentation and prototyping through open calls from Innovate UK, EPSRC, and ESRC, and will support industrial transition and academic research around the prototype.

An early experimental FPGA-based CHERI tablet

As part of Digital Security by Design, in a £2.7m Innovate UK grant, the University of Cambridge team (with colleagues at the University of Edinburgh, Arm, and Linaro) will develop formal models and machine-checked mathematical proofs to confirm that the new design does provide the intended security properties.

The team will validate and evaluate design choices in Morello by adapting the experimental CHERI software stack, which includes CHERI versions of the open-source FreeBSD operating system and applications such as WebKit, to the platform. This is the first time that formal proof will have been applied to the security of a mainstream architecture, or that real-world C/C++-language software will have protected at scale with an industrial-scale capability processor.

Ben Laurie, Director of Security at Google Research, said: "The CHERI architecture's support for fine-grain memory protection and scalable compartmentalization promises to revolutionise our ability to protect personal data and provide strong defences against malware on mobile devices and in the cloud. Arm's prototype CPU and board are vital next steps in enabling deployment of CHERI technology."

The UK Government will work with Arm as part of a broader Government plan to improve digital security and protect British businesses and data.

“Achieving truly robust security for a world of a trillion connected devices requires a radical shift in how technology companies approach cyber-threats. Research into new ways of building inherently more cyber-resilient chip platforms is critical,” said Richard Grisenthwaite, senior vice president, chief architect and fellow, Arm.

“We look forward to continuing to collaborate with the University of Cambridge as we develop our prototype hardware, the Morello Board, as a real-world test platform for prototype architecture using the CHERI protection model. It will enable industry and academic partners to assess the security benefits of foundational new technologies we’re making significant investments in.”

Digital Security by Design should enable mass-market adoption of CHERI, taking it from academic prototypes to industrial systems, and improving the security of the devices we all depend on.

CHERI has been developed over a 10-year research project, led by Principal Investigators Robert N. M. Watson, Simon Moore, and Peter Sewell at the University of Cambridge Department of Computer Science and Technology, and by Peter G. Neumann at SRI International. It has been funded largely by DARPA (in the CRASH, MRC, and SSITH programmes), with additional support from the EPSRC REMS Programme Grant, the European Research Council, Arm, and Google.

The views, opinions and/or findings expressed are those of the author and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.