CHERIoT

Certification and basic information

The cheriot‑ibex core is a 32‑bit RISC‑V microcontroller unit that implements the CHERIoT 1.0 instruction-set architecture (ISA). It was certified by the CHERI Alliance on 26 March 2026 under programme version 1.0. The product is developed by Microsoft and is offered as IP in the form of a CPU core【255832263316341†L154-L166】. The core is not a derivative of any existing qualified product and is designed specifically to support CHERIoT【255832263316341†L154-L166】.

CHERIoT ISA and extensions

The Ibex core implements the stable CHERIoT 1.0 ISA, which targets embedded devices and is maintained by a coalition of vendors【255832263316341†L170-L174】. It supports a small number of RISC‑V extensions (such as C, M, D, Zb, Zicsr and Zifencei) to provide compressed instructions and other features【255832263316341†L187-L189】. The core does not support hybrid mode; it can be compiled in non‑CHERI mode for pure RISC‑V use, but that configuration is excluded from the certification【255832263316341†L191-L193】.

Formal verification and security

CHERIoT Ibex has been subjected to comprehensive formal verification. The University of Oxford’s group verified trace equivalence between the hardware implementation and the Sail specification【255832263316341†L195-L216】, while researchers at RPTU used the VeriCHERI framework to prove that the configuration with caches disabled does not violate CHERI’s security rules【255832263316341†L204-L219】. Combined, these results show that the core faithfully implements the CHERIoT ISA and maintains capability monotonicity—tags on capabilities can be cleared but not created arbitrarily【255832263316341†L240-L256】. Traditional design verification achieved 97 % RTL coverage【255832263316341†L222-L223】.

Memory operations and revocation

The hardware integrates a capability revoker within the load–store unit. It scans memory to clear tags on capabilities marked as revoked; software can control the range but not the operation itself【255832263316341†L240-L247】. Debug mode is isolated and controlled via an external debug unit; when enabled it bypasses CHERI checks, so production SoCs are expected to disable or restrict it【255832263316341†L227-L238】.

Overall, CHERIoT demonstrates how CHERI technology scales down to embedded systems, providing robust memory protection with formally proven security properties.