CHERI is an instruction set architecture based on providing hardware support for capabilities. In particular, CHERI separates protection checks from virtual memory.
The basic CHERI design in woodruff:isca:2014 tackled spatial safety but left a hole wrt temporal safety. That is, capabilities could be used to protect a region of memory but there was no way to revoke a capability. This was addressed in later papers.
Notes related to CHERI architecture
Capabilities, CHERI-Flute, Instruction set architecture, Sail ISA specification language
Papers related to CHERI architecture
- ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS [armstrong:popl19:2019]
- The state of Sail [armstrong:spisa:2019]
- Verified security for the Morello capability-enhanced prototype Arm architecture [bauereiss:ucam:2021]
- End-to-end formal verification of a RISC-V processor extended with capability pointers [gao:fmcad:2021]
- Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process [nienhuis:secpriv:2020]
- Reasoning about a machine with local capabilities [skorstengaard:esop:2018]
- StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities [skorstengaard:popl:2019]
- CHERI: A hybrid capability-system architecture for scalable software compartmentalization [watson:sandp:2015]
- The CHERI capability model: Revisiting RISC in an age of risk [woodruff:isca:2014]
- CHERI concentrate: Practical compressed capabilities [woodruff:tocs:2019]