Category Archives: CHERI

Morello chip on board

Formal CHERI: rigorous engineering and design-time proof of full-scale architecture security properties

Memory safety bugs continue to be a major source of security vulnerabilities, with their root causes ingrained in the industry:

  • the C and C++ systems programming languages that do not enforce memory protection, and the huge legacy codebase written in them that we depend on;
  • the legacy design choices of hardware that provides only coarse-grain protection mechanisms, based on virtual memory; and
  • test-and-debug development methods, in which only a tiny fraction of all possible execution paths can be checked, leaving ample unexplored corners for exploitable bugs.

Over the last twelve years, the CHERI project has been working on addressing the first two of these problems by extending conventional hardware Instruction-Set Architectures (ISAs) with new architectural features to enable fine-grained memory protection and highly scalable software compartmentalisation, prototyped first as CHERI-MIPS and CHERI-RISC-V architecture designs and FPGA implementations, with an extensive software stack ported to run above them.

The academic experimental results are very promising, but achieving widespread adoption of CHERI needs an industry-scale evaluation of a high-performance silicon processor implementation and software stack. To that end, Arm have developed Morello, a CHERI-enabled prototype architecture (extending Armv8.2-A), processor (adapting the high-performance Neoverse N1 design), system-on-chip (SoC), and development board, within the UKRI Digital Security by Design (DSbD) Programme (see our earlier blog post on Morello). Morello is now being evaluated in a range of academic and industry projects.

Morello desktopMorello chip on board

However, how do we ensure that such a new architecture actually provides the security guarantees it aims to provide? This is crucial: any security flaw in the architecture will be present in any conforming hardware implementation, quite likely impossible to fix or work around after deployment.

In this blog post, we describe how we used rigorous engineering methods to provide high assurance of key security properties of CHERI architectures, with machine-checked mathematical proof, as well as to complement and support traditional design and development workflows, e.g. by automatically generating test suites. This is addressing the third problem, showing that, by judicious use of rigorous semantics at design time, we can do much better than test-and-debug development.
Continue reading Formal CHERI: rigorous engineering and design-time proof of full-scale architecture security properties

Arm releases experimental CHERI-enabled Morello board as part of £187M UKRI Digital Security by Design programme

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.

Continue reading Arm releases experimental CHERI-enabled Morello board as part of £187M UKRI Digital Security by Design programme

Report: Assessing the Viability of an Open-Source CHERI Desktop Software Ecosystem

CHERI (Capability Hardware Enhanced RISC Instructions) is an architectural extension to processor Instruction-Set Architectures (ISAs) adding efficient support for fine-grained C/C++-language memory protection as well as scalable software compartmentalisation. Developed over the last 11 years at SRI International and the University of Cambridge, CHERI is now the subject of a £187M UK Industrial Strategy Challenge Fund (ISCF) transition initiative, which is developing the experimental CHERI-enabled Arm Morello processor (shipping in 2022). In early 2021, UKRI funded a pilot study at Capabilities Limited (a Lab spinout led by Ben Laurie and I) to explore potential uses of CHERI and Morello as the foundation for a more secure desktop computer system. CHERI use case studies to date have focused on server and mobile scenarios, but desktop system security is essential as well, as it is frequently targeted in malware attacks (including ransomware) that also depend on plentiful software vulnerabilities. For this project, we were joined by Alex Richardson (previously a Senior Research Software Engineer at Cambridge, and now at Google), who led much of the development work described here.

In September 2021, we released our final report, Assessing the Viability of an Open-Source CHERI Desktop Software Ecosystem, which describes our three-staff-month effort to deploy CHERI within a substantive slice of an open-source desktop environment based on X11, Qt (and supporting libraries), and KDE. We adapted the software stack to run with memory-safe CHERI C/C++, performed a set of software compartmentalisation white boarding experiments, and concluded with a detailed 5-year retrospective vulnerability analysis to explore how memory safety and compartmentalisation would have affected past critical security vulnerabilities for a subset of that.

A key metric for us was ‘vulnerability mitigation’: 73.8% of past security advisories and patches (and a somewhat higher proportion of CVEs) would have been substantially mitigated by deploying CHERI. This number is not dissimilar to the Microsoft Security Response Center (MSRC)’s estimate that CHERI would have deterministically mitigated at least 67% of Microsoft’s 2019 critical memory-safety security vulnerabilities, although there were important differences in methodology (e.g., we also considered the impact of compartmentalisation on non-memory-safety vulnerabilities). One challenge in this area of the work was in establish de facto threat models for various open-source packages, as few open source vendors provide concrete definition of which bugs might (or might) constitute vulnerabilities. We had to reconstruct a threat model for each project in order to assess whether we could consider a vulnerability mitigated or not.

At low levels of the stack (e.g., 90% of X11 vulnerabilities, and 100% of vulnerabilities in supporting libraries such as giflib), vulnerabilities were almost entirely memory-safety issues, with very high mitigation rates using CHERI C/C++. At higher levels of the stack improved software compartmentalisation (e.g., enabling more fine-grained sandboxing at acceptable overheads) impacted many KDE-level vulnerabilities (e.g., 82% of Qt security notices, and 43% of KDE security advisories). Of particular interest to us was the extent to which it was important to deploy both CHERI-based protection techniques: while memory protection prevents arbitrary code execution in the vast majority of affected cases, the potential outcome of software crashing then required better compartmentalisation (e.g., of image-processing libraries) to mitigate potential denial of service. Of course, some vulnerabilities, especially at higher levels of the stack, were out of scope for our architectural approach — e.g., if an application fails to encrypt an email despite the user indicating via the UI that they require encryption, we have little to say about it.

Compatibility is also an important consideration in contemplating CHERI deployment: We estimated that we had to modify 0.026% LoC relative a 6-million line C and C++ source code base to run the stack with CHERI C/C++ memory safety. This figure compares favourably with %LoC modification requirements we have published relating to operating-system changes (e.g., in our 2019 paper on CheriABI), and a number of factors contribute to that. Not least, we have substantially improved the compatibility properties of CHERI C/C++ over the last few years through improved language and compiler support — for example, our compiler can now better resolve provenance ambiguity for intptr_t expressions through static analysis (CHERI requires that all pointers have a single source of provenance), rather than requiring source-level annotation. Another is that these higher-level application layers typically had less use of assembly code, fewer custom memory allocators and linkers, and, more generally, less architectural awareness. Along the way we also made minor improvements to CHERI LLVM’s reporting of specific types of potential compatibility problems that might require changes, as well as introducing a new CHERI LLVM sanitiser to assist with potential problems requiring dynamic detection.

The study is subject to various limitations (explored in detail in the report), not least that we worked with a subset of a much larger stack due to the three-month project length, and that our ability to assess whether the stack was working properly was limited by the available test suites and our ability to exercise applications ourselves. Further, with the Arm Morello board becoming available next year, we have not yet been able to assess the performance impact of these changes, which are another key consideration in considering deployment of CHERI in this environment. All of our results should be reproducible using the open-source QEMU-CHERI emulator and cheribuild build system. We look forward to continuing this work once shipping Arm hardware is available in the spring!

CHERI Software Release for Summer 2021

The CHERI project at SRI International and the University of Cambridge are pleased to announce our second CHERI reference software-stack release. The release supports the CHERI-RISC-V and Arm Morello architectures. A complete set of development tools, including compiler, OS, debugger, and emulator are included in the release.

For this second release, the software has been packaged to be used in an easily accessible Docker image, hosted on Docker Hub. The focus of the release has been on CheriBSD, with the merging of pure capability kernels and Morello support to the development mainline. There are also many continued improvements to tooling, including updates to cheribuild (our unified build system), the CHERI Clang/LLVM compiler suite, the CHERI-extended GNU Debugger (gdb), and the QEMU full-system emulator (which now supports both the CHERI-RISC-V and Morello architectures).

The CHERI protection model provides architectural primitives to protect computer systems from widely-exploited security vulnerabilities. CHERI revises the hardware/software architectural interface with hardware support for capabilities that can be used for fine-grained memory protection and scalable software compartmentalization. Supported by DARPA (the US
Defense Advanced Research Projects agency) as well as UKRI (UK Research and Innovation) and its Digital Security by Design (DSbD) program, CHERI is the work of a large research team at the University of Cambridge, SRI International, Arm and many industrial and academic collaborators throughout the world.

The release along with full release notes are now available on line at https://cheri-dist.cl.cam.ac.uk/