Curated research library
Find CHERI research by the question you need to answer. Each entry explains why the paper is useful, identifies its system or method and links to the primary publication.
New to the literature?
The CHERI architecture has changed materially over time. Foundational papers explain the design ideas, while newer papers better represent current architectures and software experience. Do not treat publication count as evidence; match architecture, ABI, implementation, workload and threat model.
Theme 01
Use these works to understand the capability model, deployment trade-offs and experience taking CHERI into a high-performance Arm platform.
Introduces the hybrid capability-system architecture and its case for scalable protection-domain crossing. Use it for foundational design rationale; check newer specifications for current instruction behavior.
Explains the compressed capability representation used to make bounds and permissions practical within a fixed-width capability. Important when reasoning about representable bounds and allocation alignment.
Describes the high-performance Morello processor, SoC and board used for industrial-scale experimentation. Use it to understand the platform, not as evidence of current commercial Arm product support.
Theme 02
These papers connect architectural capabilities to a process ABI, compiler semantics and a complete operating-system environment.
Shows how all userspace pointers can be capabilities and how the kernel can interact with process memory through explicitly delegated authority. A central paper for understanding pure-capability CheriBSD.
Provides a mechanised account of CHERI C pointer behavior, provenance and undefined behavior. Use it when compiler or language claims require more than an informal programming guide.
Connects the mature CHERI protection model with Morello and CHERIoT experience. Useful for a compact, current explanation before reading narrower evaluations.
Theme 03
Use these papers for low-cost embedded systems and for extending compartmentalisation beyond the main CPU.
Presents the CHERIoT hardware-software design for small embedded systems, including fine-grained compartments and temporal-safety mechanisms within constrained resources.
Examines an RTOS built around small mutually distrusting compartments, sealed objects and explicit authority. Useful for system structure, recovery and supply-chain isolation questions.
Studies capability checking across heterogeneous accelerators. Use it when the trust boundary crosses CPU, accelerator and shared-memory interfaces.
Explores moving low-level GPU driver work out of a privileged kernel context and using CHERI compartments to control authority efficiently.
Theme 04
These works explain how executable ISA models and mechanised proofs inform CHERI design and implementation confidence.
Shows how formal models were used as architecture definitions, executable references and proof foundations in the CHERI design cycle.
Develops and proves security properties for the Morello capability architecture model. Use it to understand design-time architectural assurance and the precise assumptions behind the proof.
Theme 05
Bounds stop out-of-range access; temporal safety addresses capabilities that outlive the allocation they once referred to.
Characterises pointer-revocation strategies and their performance implications. Useful for understanding why temporal safety needs explicit system mechanisms beyond spatial bounds.
Introduces a heap temporal-safety approach using CHERI capabilities. Read it with the later Reloaded paper to understand both the original design and subsequent improvements.
Refines the earlier Cornucopia approach with load barriers. Use the methods and benchmark section when comparing performance and allocator integration.
Using the library
This is a curated entry point, not a complete bibliography. The University of Cambridge CHERI publications catalogue remains the maintained primary index.