CHERI Roadmap for Linux
- Allison Randal (Capabilities Limited)
- Hesham Almatary (Capabilities Limited)
- Kevin Brodsky (Arm Limited)
- Jessica Clarke (University of Cambridge)
- Brooks Davis (Capabilities Limited)
- Vincenzo Frascino (Arm Limited)
- Ben Laurie (Google)
- Alex Richardson (Google)
- Carl Shaw (Codasip)
- Robert N. M. Watson (Capabilities Limited and University of Cambridge)
This roadmap was developed by the CHERI Alliance Linux Strategy working group, outlining a path toward unified Linux support for CHERI hardware.
This is a living document; feedback and contributions are welcomed. Please see our GitHub Repository for source code and an issue tracker. There is a rendered version on the web, which is automatically updated when the git repository is committed to.
Introduction
CHERI is a hardware approach to memory safety that proposes an extension to established ISAs, such as Arm, RISC-V, and x86, that replaces simple (integer) pointers with a tagged capability data type, and adds capability-aware instructions to load, store, and manipulate the capability type. For existing software to benefit from the memory-safety and compartmentalization features of CHERI, it must be recompiled for this extended ISA, which may require porting to use pointer types appropriately.
For most applications, this is a minor adaptation task, although language runtimes can require more work. On the OS side, however, there is significant work required to enable support for capability-extended kernels, process environments, virtual machines, and so on. Extensive research and development activity has gone into porting a version of FreeBSD, called CheriBSD, to use CHERI’s features, and in particular explore and evaluate the sizeable design space of potential CHERI integrations with a general-purpose, MMU-based operating system. This work has been highly successful, with memory-safe ports of the FreeBSD kernel and userlevel, and over 10,000 open source packages using a CHERI-adapted LLVM toolchain.
With a clear set of abstractions now defined, and existing prototypes evaluated at scale, it is expected that future OS adaptations will be substantially less work. We hope that efforts, such as CHERI Linux, will be able to benefit from this research, allowing a more engineering-oriented approach in most cases. To date, the work on Linux has been less comprehensive, though the partial ports of the Linux kernel, Busybox, GCC and glibc, and Linux userspace packages have been sufficient to demonstrate feasibility.
We envision that future work would target CHERI support on Arm’s Morello prototype, CHERI-RISC-V-based platforms, and any future CHERI-enabled platforms (e.g., on x86 or possible future Arm implementations of CHERI), with the intention of reproducing the CheriBSD approach of implementing portable abstractions despite underlying architectural differences. We also believe that, generally, programming abstractions (and guarantees) for CHERI should be portable across operating systems, allowing application adaptation burden to be shared, and for CHERI Linux to benefit from existing work in this space. Inevitably there will be some differences around OS-specific APIs and features, but to the extent possible, this should be minimized.
Goals
The goal of this work is to develop a CHERI Linux adaptation that is at feature parity with CheriBSD, and of sufficiently high quality to both enable production use and support upstreaming to the Linux community. On the whole, this roadmap is drawn from the CheriBSD feature list, including mature entries (e.g., spatial memory safety for kernel and user space, and user space heap temporal safety), and also immature prototypes or prospective ones (such as co-process compartmentalization or kernel compartmentalization). The scope of this work will include both MMU-enabled and MMU-less instantiations of Linux. Both of these targets have already seen substantial interest (and work) in the CHERI community, and have use cases at their respective scales that will clearly benefit from CHERI protection. In the case of MMU-less Linux, CHERI can be used to provide the fine-grained security that MPUs cannot provide and which have often proved a barrier to its adoption.
This is a reasonable starting strategy, but it will likely evolve over time as we come to better understand CHERI integration into Linux. For example, we expect that there may be Linux features not present in FreeBSD that require more research-focused activities to address (such as eBPF) or even simply C stylistic differences (e.g., around the use of long) that change aspects of the work in important ways.
A longer term, but equally important, goal of the work is to engage with potential upstreaming to Linux and at least one major distribution – and to ensure that there is a useful consensus on both approach and implementation amongst the various interested parties and architectures. This will require bringing together a community of CHERI Linux collaborators, engaging with the broader Linux community, and working with potential adopters to steer technical direction. It will also require broadly available, accessible CHERI-based hardware.
In similar vein, we recommend continuing the current strategy of maximizing portability of CHERI protection, language integration, and APIs across architectures (e.g., Arm’s Morello, CHERI-RISC-V), toolchain (e.g., LLVM, GCC), and operating systems (e.g., FreeBSD, Linux). This has two strong benefits: Minimizing developer burden in adapting application-level code, and also ensuring that lessons learned in any of these can be broadly benefited from in all. This will also help reinforce the message to upstream communities that CHERI protection is a well defined, portable, and consistently implemented model, rather than the product of a fragmented community and therefore insufficiently mature to adopt.
To date, there have been a few different efforts to add CHERI support to Linux, with Arm’s Morello Linux prototype being the most mature and well supported. That implementation is focused on the Morello prototype architecture and microarchitecture, an MMU-enabled, high-performance design. In addition, Hesham Almatary at Capabilities Limited has developed a memory-safe variant of Linux targeted at MMU-less designs, based on CHERI-RISC-V. Finally, Huawei has also created a CHERI Linux prototype, focused on MMU-enabled CHERI-RISC-V, illustrating the feasibility of Linux on CHERI-RISC-V, but for technical and legal reasons it will not be a direct source for this work. It is our strong recommendation that Arm’s Morello Linux be the baseline for further work, used as a baseline against which further changes will be made (and, for existing work, merged).
One goal early in this work will be to develop a strategy for repositories and infrastructure to use in development work, as we migrate from a “Morello Linux” to a “CHERI Linux”. In doing so, it may be sensible to create a set of new “CHERI Linux” repositories where contributors from various organizations (academic, industrial, government) can collaborate in a vendor-neutral manner. A first engineering step, therefore, would be to bring in Arm’s work, as a collaborative activity, with suitable observation of, and management of, sensitivities about ownership, technical direction, and so on. There are other significant “people-focused” concerns about how to create a productive development community; however, the remainder of this document is focused on the technical roadmap rather than those topics, as we consider that roadmap to be a necessary input to joint planning required to create a broader plan.
The current major targets of this roadmap are in the areas of toolchain, emulation and crossbuild platforms, kernel support, and user space.
Toolchain
| Topic | Type | Description |
|---|---|---|
| LLVM / Clang | Engineering | The existing CHERI and Morello LLVM toolchains can already be used to [cross-]compile C/C++ Linux components. LLVM can be used to build Android’s bionic libc, musl libc, and newlib for bare-metal applications. Glibc is now working towards supporting LLVM as a first class citizen and an early version with CHERI support is available for RISC-V. At least the following work needs to take place: Upstream Morello LLVM support to baseline CHERI LLVM. Integrate CHERIoT support into baseline CHERI LLVM [not required for Linux, but an important engineering TODO for CHERI LLVM on the path to upstreaming to mainstream LLVM]. Transition from the SRI/Cambridge prototype CHERI-RISC-V ISA to the standardized CHERI-RISC-V ISA as it matures. Upstream CHERI LLVM support to baseline LLVM, optionally with Morello backend support [subject to Arm’s readiness for this]. |
| LLVM / Rust | Engineering | Rust is already present in the Linux kernel and although it only currently is available for x86_64, support is likely to spread to other architectures. Some user space applications on newer Linux distributions also require Rust. There are currently two independently developed CHERI Rust compilers available for Morello. The long term aim should be to get CHERI support upstreamed to the Rust community but again this requires updating the compiler to the latest upstream version. |
| GCC | Engineering | Arm has performed an initial prototype adaptation of GCC to support Morello, but it is of lower overall maturity – albeit promising in that it can already be used to compile glibc. Having more mature GCC support is an important milestone towards the adoption of CHERI in Linux distributions. Ideally Morello GCC would evolve into CHERI GCC over time. |
| CHERI GDB | Engineering | Minor extensions may be required to CHERI GDB to work with CHERI Linux, although it is already believed to work well on Morello Linux as the preferred debugger on that platform. Further adaptation will be required as library compartmentalisation is brought up – which should ideally be shared with GDB support for CheriBSD’s c18n feature. |
| Purecap LLVM | Engineering | At present, LLVM can cross-compile code using CHERI capabilities for all pointers ("purecap"), but it is not itself running using capabilities and instead relies on platforms' support for legacy ("hybrid/integer mode") binaries.The lack of a purecap LLVM JIT likely blocks porting of an appreciable amount of software and the lack of a libclang prevents its inclusion in development tools. (A purecap GCC is eventually also useful, but it is less used as a library). |
Emulation and crossbuild platforms
| Topic | Type | Description |
|---|---|---|
| QEMU system mode | Engineering | Today, Morello Linux runs on Morello hardware and Arm’s FVP emulator. Linux (both MMU- and MMU-less ) runs on QEMU for CHERI-RISC-V. CheriBSD’s Morello support is well tested and heavily used on QEMU for Morello, and is believed to be quite mature. As QEMU is widely available and used in the Linux community, ensuring that Morello Linux and, CHERI Linux (with both Morello and RISC-V support) works well on QEMU will ease integration into existing development environments and allow access to CHERI Linux’s Morello support for those unable to use FVP. QEMU will need to (in due course) be updated to the latest version to allow use of newer RISC-V extensions, such as vector support, that have gained CHERI support in the latest RISC-V International draft CHERI extension specification. As for LLVM, the aim should be to upstream CHERI support in QEMU to reduce future maintenance burden. |
| QEMU user mode | Engineering | This feature of QEMU is often used for the purposes of large-scale software cross building, so that host toolchain (e.g., make, compiler, linker) can run natively, while portions of a cross-built piece of software that depend on running on the target can be run in that way. User mode support integrates a rich understanding of not just the target architecture, but also OS system-call ABI, and so specific engineering work will be needed to enable pure-capability CHERI Linux processes under QEMU user mode. This work has been done for CheriBSD for Morello, but not yet CHERI-RISC-V, and will provide a reasonable template. General Linux user mode support is solid in upstream QEMU where FreeBSD support is largely a local addition. |
| bhyve hypervisor | Engineering | CheriBSD includes the bhyve hypervisor with support for virtualization on Arm’s Morello. It is capable of booting Morello Linux and provides a more performant development environment than QEMU. Debugging support currently lags behind QEMU and improvement would better support work on CHERI Linux. |
| CheriBSD Linux ABI | Engineering | During development of the current Arm Morello pure-capability usermode ABI, the CheriBSD team created a prototype adaptation of FreeBSD’s existing arm64 Linux process emulation updated for the new CHERI-enabled ABI. Continuing this work offers two important benefits: (1) Providing an independent second implementation of the ABI offering concrete feedback on the design and its implications with differing kernel designs, with practical validation, and (2) Providing early access to CHERI OS features unavailable via the Linux kernel during development – for example, being able to develop glibc support for heap temporal safety, and test Linux-compiled applications with it, before Linux kernel support is complete. |
Kernel support
| Topic | Type | Description |
|---|---|---|
| Hybrid kernel | Engineering | CheriBSD supports both hybrid (primarily integer-based pointers except where annotated to enable pure-capability userspace applications), and pure-capability kernels. In an ideal world, there would be no need for hybrid kernels, as adding qualifiers to pointers in system-call arguments, and implementing a translation layer between ABIs, is both disruptive and a noticeable development and maintenance burden. This is similar (but not identical) to the idea of supporting a 64-bit user space with a 32-bit kernel – possible, but ideally not required. The hybrid kernel is maintained in CheriBSD while evaluation continues as part of pure-capability kernel research, to permit side-by-side performance comparisons. Today, Morello Linux implements a hybrid kernel. As work on CHERI Linux continues, and the CheriBSD kernel research concludes, hopefully a conclusion will be drawn that hybrid support is not required, and this might be removed from the feature list. |
| Purecap kernel | Engineering | The Linux kernel can be compiled with LLVM and although a proof-of-concept MMU-enabled CHERI-RISC-V purecap kernel has been produced by Huawei, i however, it has not yet been fully ported to support CHERI’s memory-safety and compartmentalization features, and, it does not form a sound basis for further work. (see “Prior work on Linux adaptation” section below). A more robust proof-of-concept purecap port of MMU-less Linux is also available., and a more complete Linux kernel has previously been partially ported, but not yet been fully ported to support CHERI’s memory-safety and compartmentalization features. See “Prior work on Linux adaptation” section below for more details. Alfredo Mazzinghi’s PhD dissertation includes an initial analysis of areas of work required to replicate CheriBSD’s pure-capability kernel support in Linux. Note that work on kernel heap temporal safety is also planned for CheriBSD over the coming year – a feature that one would want to replicate in Linux. A practical approach would be to start with the Morello Linux kernel and use that as the starting point for a portable (including CHERI-RISC-V) work towards adding a clean CHERI-RISC-V purecap kernel implementation. |
| Kernel build utilities | Engineering | Changes to kernel types to support CHERI may lead to patch-checking tools such as smatch or sparse requiring modification. |
| Kernel compart-mentaliza-tion | Research | With a memory-safe kernel baseline, kernel compartmentalization is also an important (albeit currently very research-oriented) goal. An early prototype exists in CheriBSD on Morello, and the MMU-less Linux prototype includes linker-based compartmentalization that is able to sandbox simple kernel modules (e.g., device drivers). This is an area that is very much an active area of research, and so may not be an engineering goal for CHERI Linux in the short term – but its requirements should be taken into account when implementing, for example, kernel spatial and temporal safety. And, as the research prototypes and understanding evolve, it should be added to the engineering goals for CHERI Linux. |
| CheriABI | Engineering | Enables running spatially safe user space processes via capability-extended system calls, signal delivery, and so on. This is implemented in Morello Linux to a good level of technical maturity, and with care taken regarding ABI definition. Similar specification work needs to occur for CHERI-RISC-V, but can be built on the Morello definitions. |
| 64-bit compat | Engineering | Enables running 64-bit (legacy) processes on a capability-aware kernel. This is implemented in Morello Linux. |
| 32-bit compat | Engineering | Enables running 32-bit (legacy or x32) processes on a capability-aware kernel. The Morello ISA dropped armv7 support for simplicity and RISC-V designs do not typically support RV32 on an RV64 system due to a lack of legacy code, but an x32 approach might be viable (even critical for some vendors with pointer-heavy workloads or legacy binaries). This is a low priority and can wait for clear demand. |
| User space temporal safety | Research | A major recent feature of CHERI software-stack, heap temporal memory safety, requires kernel virtual-memory support to implement efficient capability revocation, used by user space heap allocators to prevent temporal heap aliasing enabled by use-after-reallocation vulnerabilities. There has not yet been a feasibility study for this feature in Linux. Further, temporal safety on CHERI remains an area of ongoing research, and it is reasonable to expect that thinking on this topic (as well as architectural support) will evolve considerably in coming years – both with respect to performance and the potential implications on system behavior (e.g., system-wide, not just process-local, impacts). |
| Co- processes | Research | This remains immature on CheriBSD, but continues to show promise in some applications. It mostly requires kernel changes in the current state, but runtimes may require significant changes as the ideas mature (e.g., consider a per-address space allocator and perhaps garbage collection). There has not yet been a feasibility study for this feature in Linux, and this is an active area of research for CHERI. |
| KVM | Engineering | The ability to boot capability-enabled guests using hardware-assisted virtualisation extensions. CheriBSD has working support for pure-capability guests in FreeBSD’s bhyve on Morello. Arm has in-progress work to bring up KVM support on Morello Linux, it is in early stages of development and currently supports only aarch64 guests not CHERI-enabled guests. It has been verified even if not extensively with LTP test suite. |
Bootloaders and firmware
| Topic | Type | Description |
|---|---|---|
| U-Boot | Engineering | U-Boot is a very common bootloader for Linux on embedded systems and is often seen as a critical component for Linux-based stacks on these devices. An early stage implementation of U-Boot with CHERI exists for RISC-V. |
| SBI | Engineering | The Supervisor Binary Interface (SBI) specification is RISC-V specific and is used to abstract hardware implementation from an OS or bare-metal application. It is implemented as part of bbl used by CheriBSD and in OpenSBI which is commonly used with the Linux kernel. Both implementations now support the latest CHERI-RISC-V draft specification but will need to track any further changes. |
| UEFI | Engineering | The Unified Extensible Firmware Interface (UEFI) is a specification that defines a software interface between an operating system and platform firmware and which is predominantly used for booting desktop and server systems. It has been adopted by Arm, RISC-V, Intel and AMD and so is an obvious target for CHERI support in these classes of systems. No work has been done to date to add CHERI support to UEFI loaders. |
User space support
| Topic | Type | Description |
|---|---|---|
| Dynamic linker c18n | Research | A significant focus of recent CHERI software research, this feature allows dynamically linked binaries and libraries to be placed in affordable sandboxes. It requires modest kernel changes combined with substantial run-time linker work, as well as testing and validation. There has not yet been a feasibility study for this feature in Linux. |
| glibc | Engineering | Similar to the Linux kernel, this will require substantial porting work to use CHERI’s features in the CheriABI process environment, as well as implement user space portions of temporal safety and library compartmentalisation. Ports of FreeBSD’s libc, bionic, musl, and newlib have demonstrated paths forward, and initial porting work of glibc on Morello has been performed. We need to come to consensus on the changes required, document them (e.g., produce an annotated POSIX spec), and bring these ideas to glibc. |
| Libraries + applications | Engineering | There is a significant overlap between Linux and FreeBSD in 10,000 open source packages that have already been ported to CheriBSD. Some of the fixes to these packages for CHERI are generally useful (good pointer hygiene) and have been contributed back upstream. The fixes that aren’t pushed upstream are maintained as forks, so the patchsets are available to be reused on the Linux packages of the same open source project. More porting work will be necessary for the subset of packages that are unique to Linux. The CheriBSD work has also been mostly focused on the desktop use case, so the server and embedded use cases will require expanding the set of packages ported to both CheriBSD and Linux. |
Linux distributions
| Topic | Type | Description |
|---|---|---|
| Desktop distribution | Engineering | In the longer-term, integrating the CHERI port into a popular mainstream desktop Linux distribution will encourage the adoption of CHERI and make it easier to migrate existing Linux workloads to CHERI. This will, however, likely require available hardware. However, porting a full Linux distro may depend on fully porting GCC and other languages and tools used within the distro’s build process, so it’s better to begin by targeting a simple Linux image such as an embedded distribution, and expand into a full Linux distribution later, once we have a more complete set of ported packages to work with. When working on a package repository for the selected Linux distribution, additional changes will have to be made to the distribution’s user space configuration to allow a user to install and run pre-compiled hybrid/integer mode and pure-capability third-party programs. For example, CheriBSD maintains separate local base directory hierarchies for separate ABIs to avoid conflicts between files from packages of different ABIs. The distribution package manager may need modification to make it aware of the different ABI use for installation and dependency tracking. |
| Server distribution | Research | Although similar in many ways to the desktop distribution, there are some technologies that may require special attention. In the kernel, XDP requires CHERI support in eBPF. eBPF is also supported now in some SmartNICs and ideally these should also contain CHERI processors to maintain security across the system. Remote Direct Memory Access (RDMA) is an increasingly popular technology that will need careful analysis regarding the impact on CHERI tagging. DPDK may also need to be supported. Hardening Linux containers with CHERI would be highly beneficial for servers, although a CHERI-enabled Go language will be required to build Docker or Podman. Servers will also require hypervisor and KVM support. This has an early implementation in Morello, but has not yet been considered for RISC-V. |
| Embedded distribution | Engineering | Yocto is becoming the most common method of building Linux distributions and is supported by many major silicon vendors including NVidia and Xilinx/AMD. It supports building a huge number of Linux packages and CHERI support can be added through additional build layers that augment existing build instructions. Yocto layers that add CHERI toolchains and a basic user space exist for both Morello and CHERI-RISC-V. |
Testing
| Topic | Type | Description |
|---|---|---|
| Linux Test Project | Engineering | This code may require adaptation to CHERI C, and may also require adaptation to OS-related changes in a CHERI-enabled environment. Ideally these will be run and pass well for both hybrid and CHERI-enabled ABIs. |
| cheribsdtest | Engineering | Port over / adapt the CheriBSD test suite, which confirms properties such as suitable bounds setting during process setup, VM interactions with tagged memory, aspects of system-call argument handling, and various other properties we would like to hold true. This might become a cheritest (again) rather than being a cheribsdtest so as to maintain a common test suite over time? |
Prior work on Linux adaptation
Morello Linux contains a hybrid Linux kernel (not purecap) which supports running and building simple user space applications in purecap mode using a new CHERI-aware ABI called PCuABI. Two software stacks are supported; BusyBox and Debian. However, Debian still runs in vanilla AArch64 mode, but new simple programs can be built in purecap mode:
- ARM, Morello Linux, https://www.morello-project.org/
- Morello pure capability kernel user Linux ABI specification
- Linaro, Porting Linux tools into Morello Architecture, 2021
Many (but not all) Linux-based user space environments depend on GCC for compilation. Arm has developed an initial Morello GCC adaptation believed to be sufficient to compile glibc. However, in their Morello Linux work, they have been using musl in order to bootstrap a user environment even without GCC support. It is not clear how mature the GCC work is, and unlike Morello LLVM, ongoing development and maintenance plans are unclear. Unless a pure LLVM-based compilation of a complete glibc-based Linux distribution can be achieved in the medium term, pushing forward Morello GCC support (and generalizing it to be CHERI GCC support) will be important:
- Jonathan Corbet, Supporting CHERI capabilities in GCC and glibc, LWN, 2022
- Adhemerval Zanella, Building GLIBC with LLVM: The How and Why, Linaro, April 2023
- Linaro, Active development branch for work-in-progress building glibc with LLVM, 2024
The MMU-less CHERI-RISC-V Linux port is entirely purecap; both the kernel and userspace. The userspace stack includes a simple CHERI-aware run-time linker, uclibc-ng, and BusyBox, all built in purecap mode. It does support an initial implementation of the CompartOS compartmentalisation model which could isolate device drivers built as kernel modules, and user ELF programs built in FDPIC ELF format. This builds with the CHERI-LLVM toolchain without the use of GCC:
- Hesham Almatary, Alfredo Mazzinghi, Robert N. M. Watson, Case Study: Securing MMU-less Linux Using CHERI, In SE 2024 - Companion, February 2024, pages 69-92
- Hesham Almatary, CHERI compartmentalisation for embedded systems, Technical Report UCAM-CL-TR-976, University of Cambridge Computer Laboratory, November 2022
There is also work by Huawei on a CHERI-enabled Linux, which they have recently published a workshop paper on. For both serious policy and technical reasons, this is not a suitable input to the CHERI Linux project beyond a simple proof-of-concept demonstration. In particular, it appears that there is frequent rederivation of capabilities from integer pointers without suitable boundsetting throughout the kernel and userspace, such as capability derivation and bounding for mmap being performed within the userspace wrapper, effectively leading to referential and spatial safety protections being ineffectual. However, we include these references for awareness purposes:
- Huawei, Linux kernel on CHERI RISC-V, https://github.com/cheri-linux
- Kui Wang, Dmitry Kasatkin, Vincent Ahlrichs, Lukas Auer, Konrad Hohentanner, Julian Horsch, and Jan-Erik Ekberg, Cherifying Linux: A Practical View on using CHERI, In EuroSec '24: Proceedings of the 17th European Workshop on Systems Security, April 2024, Pages 15–21
Technical reports
- Kernel memory safety: Alfredo Mazzinghi, CHERI Memory Safety in the CheriBSD kernel, PhD Draft, 2024. (available by request – future paper submission is anticipated)
- CHERI C/C++ programming languages: Robert N. M. Watson, Alexander Richardson, Brooks Davis, John Baldwin, David Chisnall, Jessica Clarke, Nathaniel Filardo, Simon W. Moore, Edward Napierala, Peter Sewell, and Peter G. Neumann. CHERI C/C++ Programming Guide, Technical Report UCAM-CL-TR-947, Computer Laboratory, June 2020.
- Morello prototype disclaimers: Robert N. M. Watson, Graeme Barnes, Jessica Clarke, Richard Grisenthwaite, Peter Sewell, Simon W. Moore, and Jonathan Woodruff. Arm Morello Programme: Architectural security goals and known limitations, Technical Report UCAM-CL-TR-982, Computer Laboratory, July 2023.
- Morello performance: Robert N. M. Watson, Jessica Clarke, Peter Sewell, Jonathan Woodruff, Simon W. Moore, Graeme Barnes, Richard Grisenthwaite, Kathryn Stacer, Silviu Baranga, Alexander Richardson. Early performance results from the prototype Morello microarchitecture, Technical Report UCAM-CL-TR-986, Computer Laboratory, September 2023.
Selected CHERI research papers
There are also in-flight efforts, of varying degrees of completion, to write papers on: the pure-capability kernel, library compartmentalization, and an experiences piece on memory-safe C/C++ at scale. There are also a number of papers on CHERI specific microarchitecture
- Current (load-barrier) heap temporal safety. Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Jessica Clarke, Peter Rugg, Brooks Davis, Mark Johnston, Robert Norton-Wright, David Chisnall, Simon W. Moore, Peter G. Neumann, and Robert N. M. Watson. Cornucopia Reloaded: Load Barriers for CHERI Heap Temporal Safety. Proceedings of ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'24). San Diego, CA, USA, April 27 - May 1, 2024.
- CHERI C formal semantics. Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alex Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, and Peter Sewell. Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour. In Proceedings of 2019 Architectural Support for Programming Languages and Operating Systems (ASPLOS’24), San Diego, CA, USA, April 27- May 1, 2024.
- Morello platform. Richard Grisenthwaite, Graeme Barnes, Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Jonathan Woodruff. The Arm Morello Evaluation Platform—Validating CHERI-Based Security in a High-Performance System, IEEE Micro, vol. 43, no. 3, pp. 50-57, May-June 2023, doi: 10.1109/MM.2023.3264676.
- Earlier (store-barrier) temporal safety. Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz Napierala, Alexander Richardson, John Baldwin, David Chisnall, Jessica Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, Timothy M. Jones, Simon W. Moore, Peter G. Neumann, and Robert N. M. Watson. Cornucopia: Temporal Safety for CHERI Heaps. In Proceedings of the 41st IEEE Symposium on Security and Privacy (Oakland 2020). San Jose, CA, USA, May 18-20, 2020.
- Spatially safe POSIX userlevel. 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