Professor Robert N. M. Watson (Cambridge), Professor Simon W. Moore (Cambridge), Professor Peter Sewell (Cambridge), Dr Jonathan Woodruff (Cambridge), Brooks Davis (SRI), and Dr Peter G. Neumann (SRI)
After over a decade of research creating the CHERI protection model, hardware, software, and formal models and proofs, developed over three DARPA research programmes, we are at a truly exciting moment. Today, Arm announced first availability of its experimental CHERI-enabled Morello processor, System-on-Chip, and development board – an industrial quality and industrial scale demonstrator of CHERI merged into a high-performance processor design. Not only does Morello fully incorporate the features described in our CHERI ISAv8 specification to provide fine-grained memory protection and scalable software compartmentalisation, but it also implements an Instruction-Set Architecture (ISA) with formally verified security properties. The Arm Morello Program is supported by the £187M UKRI Digital Security by Design (DSbD) research programme, a UK government and industry-funded effort to transition CHERI towards mainstream use.
CHERI and Morello
The University of Cambridge and SRI International began work on the CHERI architectural protection model in 2010 as part of DARPA’s CRASH programme, with support exceeding $30M from DARPA across two further research programmes, MRC and SSITH, with additional support from EPSRC, ERC, Arm, Google, and HP. CHERI implements architectural capabilities that directly enable software security features such as fine-grained memory protection and scalable software compartmentalisation — both important software vulnerability mitigation techniques that are not well supported on current processor architectures. Hardware-supported capabilities are an old idea in computer science, and of particular historic interest at Cambridge where the CAP Computer was prototyped – but in 2010, their application to contemporary processor architectures and software stacks was open territory for new blue-sky research.
By the end of the CRASH programme in 2015, we had successfully developed an early FPGA-based prototype beginning to demonstrate the promise of such an idea, focused on providing a platform able to efficiently run memory-safe C/C++ and open the door to new, more secure software architectures based on high-performance compartmentalisation. However, many open questions remained – not least, whether there were potential successful integrations with industrial-scale processor designs, efficient microarchitectural implementations of capabilities and memory tagging, viable compiler and OS techniques that could use them, and clear and valuable applications large-scale software corpora.
Arm joined the collaboration in 2014, and it has been an exciting and at times intense journey as we worked side-by-side to address many challenging obstacles. Until the start of the pandemic in March 2020, we had Arm engineers working side-by-side with us at the William Gates Building at the University of Cambridge, as well as industrial collaborators from companies such as Google and Microsoft working together to address a long series of hardware, software, and formal methodology challenges in adopting and using the technology – those collaborations now continue online. During our collaboration, we developed new architectural approaches (e.g., compressed capabilities and CHERI temporal safety), microarchitectural techniques (e.g., tag controllers and caches), new operating system approaches (e.g., memory-safe UNIX process environment), new language and compiler techniques (e.g., memory-safe C compilation and linkage), and formal approaches (including proofs about ISA-based malicious code containment). Each one of these concepts has been utilised in creating the prototype architecture used in Morello, its hardware, and its software stack. You can learn more about these and other aspects of CHERI by reading our Introduction to CHERI technical report.
A key tenet of our collaboration has been an open approach to prevent intellectual property impediments to use of the “capability essential IP” necessary to implement CHERI in other Instruction-Set Architectures. Further details can be found in our recent Capability Essential IP technical report declaring those concepts.
Arm’s engineers took as their starting point the existing Arm Neoverse N1 design, which is used in Arm-based servers at major cloud providers. The result was a new, experimental chip and board, Morello, which will now become a development, evaluation, and demonstration platform for dozens of UK-based companies and universities participating in Digital Security by Design. Many further boards have been ordered by international research labs and governments eager to explore the technology. Collectively, we aim to develop new software models enabled by CHERI, and to evaluate its impacts on security, compatibility, and performance, building on already substantial work exploring these concerns across open-source operating systems and applications.
Rich research agendas (e.g., as written about today by Microsoft) and demonstrators (e.g., THG and Manchester University’s Soteria demonstrator) will explore a huge range of application workloads and approaches to utilising CHERI’s protections across various operating systems, programming languages, and applications. What does all of that software have in common? A long history of security vulnerabilities that demand disruptive change able to dramatically reduce them, and that is able confine successful attacks. Recent studies at the Microsoft Security Response Center (MSRC), exploring past Microsoft security vulnerabilities, and Capabilities Limited, looking at the open-source desktop software ecosystem, have estimated that CHERI can deterministically mitigate, respectively, in excess of 67% and 74% of past vulnerabilities. However, these security claims, and implied requirements for low performance overheads, require experimental validation that now possible with Arm’s Morello prototype.
What Morello has already demonstrated
We are hitting the ground running: Within weeks of first preproduction chips arriving at Arm’s facilities in Cambridge, England, our full CHERI prototype software stack was running on early development boards. This includes Cambridge and SRI’s memory-safe CheriBSD UNIX kernel (a CHERI-enabled version of the open-source FreeBSD kernel), memory-safe CheriABI UNIX userspace including programs such as OpenSSH, and CHERI-adapted applications such as Apple’s WebKit including its JavaScriptCore (JSC) just-in-time (JIT) compiler adapted to target Morello (developed in collaboration with Arm), as well Arm’s own work on the Android operating system. With multiple boards now at our own lab in Cambridge, we are starting on early performance evaluation of CHERI’s spatial and temporal memory-safety features, bringing up GPU device drivers required to support a rich user-facing application ecosystem, and preparing to support a growing research ecosystem as further Morello boards are received by research partners around the world.
It is worth reflecting on what has been achieved. We have now experimentally validated a number of key hypotheses developed during our early work in DARPA’s CRASH programme:
Architecture: That an architectural capability-system model can be successfully atom smashed with a contemporary, MMU-enabled ISA such as Armv8-A.
Formal methods: That it is possible to formally model and verify the security of that architecture specification, with machine-checked mathematical proof about its full 60,000 line definition, showing it ensures goals such as malicious code confinement, as well as to automatically generate hardware test suites from the same models.
Microarchitecture: That an architectural capability-system model can be implemented in a high-performance, industrial quality multicore superscalar processor implementation, including microarchitecture such as CHERI’s compressed capabilities and a tag controller/cache model. Morello is based on Arm’s widely used Neoverse N1 microarchitecture – very much the “real thing” – and achieves 2.5Ghz, its target clock frequency.
Memory-safe C/C++: That it is possible to support memory-safe variants of C and C++ (“CHERI C/C++”) using that architecture, through recompilation using industrial compiler toolchains such as LLVM, providing strong and deterministic spatial and referential memory safety for a large corpus of off-the-shelf C/C++ software with minimal modification.
Memory-safe UNIX: That it is possible to compile and run a memory-safe version of a fully fledged UNIX operating system kernel and userspace with minor adaptions.
These results are, to say the least, surprising – none were foregone conclusions, and it’s only in the final stages of the Morello implementation process that we have confidence that they are indeed true.
Our next directions at Cambridge and SRI
We are now turning our attention to a series of escalating experiments over the coming months and years, as prototype silicon becomes more widely available:
Software performance: That, across a rich variety of software components and workloads (SPEC, web browsers, language runtimes, OS kernels, …) we can achieve acceptable performance-security trade-offs for spatial and temporal safety.
Microarchitectural choices: Exploring the cost and performance of various microarchitectural designs and parameter choices with respect to tagging, capability compression, branch prediction, and so on. Exploring how CHERI scales to exascale systems. Ensuring that emerging threats like speculative execution attacks are mitigated
Compartmentalisation: That CHERI compartmentalisation achieves the greater than an order-of-magnitude improvements compared to MMU separation seen in FPGA-based experiments, as well as compartment scalability, and that multiple viable software models can be implemented conveniently and efficiently over CHERI primitives.
Source-level compatibility and quality: That the compatibility objectives permitting widespread deployment across current C and C++ software can be met across a large code corpus, and with sufficient quality of implementation to support Morello consumers.
Security evaluation: That further evaluation including formal analysis, analytic studies, and practical penetration testing, show that CHERI fulfils the promises of fine-grained memory protection and scalable compartmentalisation.
All of this work is dependent on a heavy software-engineering agenda to explore these ideas through hands-on experimentation with real-world, large-scale software stacks. We look forward to the coming years as we get to work with collaborators on these and many other topics.
Acknowledgements
CHERI and Morello are the result of hundreds of staff years of effort across Cambridge, SRI, Arm, Microsoft, Google, and others. From the PhD students and postdocs exploring novel approaches to microarchitecture, compilers, and operating systems, to the research software engineers, consultants, and industrial collaborators who led research development efforts essential to the transition of this work, as well as the amazing team at Arm working on Morello architecture, hardware, and software, this truly has been a vast collective effort.
We are especially wish to thank our current and past collaborators at Cambridge and SRI, with whom it has been an honour to work for over a decade, including: Hesham Almatary, Jonathan Anderson, Alasdair Armstrong, Peter Blandford-Baker, John Baldwin, Hadrien Barrel, Thomas Bauereiss, Ruslan Bukin, Brian Campbell, David Chisnall, Jessica Clarke, Nirav Dave, Lawrence Esswood, Nathaniel W. Filardo, Franz Fuchs, Dapeng Gao, Khilan Gudka, Brett Gutstein, Alexandre Joannou, Mark Johnston, Robert Kovacsics, Ben Laurie, A. Theo Markettos, J. Edward Maste, Alfredo Mazzinghi, Alan Mujumdar, Prashanth Mundkur, Steven J. Murdoch, Edward Napierala, Kyndylan Nienhuis, George Neville-Neil, Robert Norton-Wright, Philip Paeps, Lucian Paul-Trifu, Allison Randal, Ivan Ribeiro, Alex Richardson, Michael Roe, Colin Rothwell, Peter Rugg, Hassen Saidi, Peter Sewell, Thomas Sewell, Stacey Son, Ian Stark, Domagoj Stolfa, Andrew Turner, Munraj Vadera, Konrad Witaszczyk, Hongyan Xia, and Bjoern A. Zeeb. We are very pleased that so many of the students and postdocs who have moved on from Cambridge to industry continue to actively collaborate with us on CHERI at companies such as Google and Microsoft.
Our eight-year collaboration with Arm has been incredibly rewarding, and we wish to thank Graeme Barnes, Richard Grisenthwaite, Lee Smith, Hugo Vincent, Lee Eisen, Kevin Brodsky, Ruben Ayrapetyan, Silviu Baranga, Karthik Muthusamy, Mark Nicholson, Mark Inskip, and countless others with whom it has been a great pleasure to work with, and to learn so much from. Our expanding collaboration with Microsoft has also been extremely productive, and we particularly wish to thank Manuel Costa, Saar Amar, and Nicolas Joly.
Finally, we are grateful to Howie Shrobe, MIT professor and past DARPA CRASH and MRC program manager, who offered both technical insight and support throughout this work. We are also grateful to Robert Laddaga, Stu Wagner, and Jonathan Smith, who succeeded Howie in overseeing the CRASH program, John Launchbury (DARPA I2O office director), Dale Waters (DARPA AEO office director), Linton Salmon (DARPA SSITH program manager), Keith Rebello (DARPA SSITH program manager), Daniel Adams and Laurisa Goergen (DARPA I2O SETAs supporting the CRASH and MRC programs), Marnie Dunsmore and John Marsh (DARPA MTO SETAs supporting the SSITH program), John Goodacre (UKRI), and Georgios Papadakis (UKRI).
This is excellent. The work will lead to secure software. But even before the CAP development at Cambridge, Professor Sir Maurice Wilkes inspired, and advised Plessey’s development of the PP250. This industrial strength multi-processor, defined a capability-based secure instruction set. The work deserves more study in the development of Capability based, secure computer science.
This work is brilliant… but I must say that having worked at Plessey on the CORAL compiler for PP250 this same level of security was inherent in the architecture so much more elegantly. It’s 50 years ago but my take away from that time was that the “Enter Capability” concept captured it all. It’s not well described in the literature but to my mind it’s the core essence of how PP250 encapsulated fault tolerance and hence security.
3 generations of pp250 took it from a room full of equipment to a 19 ” rack to a pcb. Its secure, proven in commercial and military service, but never put on a chip!
Blows my mind that we want to spend a fortune reinventing something when we already have a proven solution that was never hacked.
I assume people are still aware of the independence of logic design / physical implementation and the importance of hardware protection of software.
As one of the worlds experts in computer security i am surprised that Ptarmigan was taken out of service and replaced by an insecure system without consulting the developers. Has COVID infected everyone?
after the Harold Wilson pay freeze/brain drain, we all had to work overseas but we stay in touch.
From: ex pp250/Ptarmigan Development manager, and QMC Physics. retired.