CHERIoT Ibex Certification Record

This is the public certification record for the product and version named below. It preserves the scope and principal answers published when the certification was granted.

Product information

• Certification date: 26 March 2026
• Certification programme version: 1.0
• Organisation: Microsoft
• Organisation type: commercial company
• Product: cheriot-ibex
• Product type: processor intellectual property — CPU
• Reference: cheriot-ibex
• Version: 1.0
• Derivative of a qualified product: no
• Product source: Microsoft CHERIoT Ibex repository

cheriot-ibex is a 32-bit RISC-V microcontroller core implementing the CHERIoT 1.0 instruction-set architecture.

Architecture and scope

The certified configuration implements CHERIoT 1.0, with the C, M, D, Zb, Zicsr, and Zifencei RISC-V extensions described in the submitted record. The core does not provide a hybrid execution mode. It can be built as a conventional RISC-V core without CHERI, but that non-CHERI configuration is expressly outside this certification.

The CHERIoT 1.0 architecture specification and its public Sail model define the reference architecture used by the implementation.

Verification evidence

The applicant reported two complementary forms of formal verification:

• trace equivalence between the core and the Sail specification, described in the published preprint;
• VeriCHERI analysis of the RTL security properties, described in VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL.

The record states that the cache-disabled configuration was verified against direct and indirect data flows that would violate CHERI rules. With caches enabled, timing channels can affect confidentiality, while the verified integrity properties remain. Conventional design verification included randomised and coverage-based testing, with reported RTL coverage of 97 per cent.

Memory access and debug

Debug mode places the core under the control of an external debug unit and omits CHERI checks. Software running normally on the core cannot enter this mode; it is reached through the external debug mechanism, commonly JTAG. The certification record expects a production system-on-chip either to disable that path or to provide an appropriately restricted debug environment.

The hardware revoker can scan revocable memory and clear tags from capabilities that refer to deallocated objects. It does not use a capability operand for the scan, but its hardware operation is limited to clearing relevant tags. This mechanism forms part of CHERIoT’s temporal memory-safety model.

Capability tags

The submitted record identifies no operation that can set a tag on an arbitrary value. The system begins with root capabilities and derives later capabilities from them. Operations may clear tags but cannot turn an arbitrary integer into a valid capability.

The core supports memory interfaces that carry capability data and tags in either a single wider transaction or two narrower transactions. The record explains the atomicity and integration conditions for both forms, including additional care where direct-memory-access hardware shares memory. These conditions apply to the surrounding system-on-chip rather than to the processor core alone.

Temporal memory safety

CHERIoT combines the architectural capability model with a hardware revoker and software allocation model designed to invalidate capabilities to deallocated objects. Certification applies to the core mechanisms described in the record. Whether a complete device achieves the intended property also depends on its memory system, integration, runtime, and configuration.

Certification boundary

The certification covers cheriot-ibex version 1.0 in its CHERIoT configuration. It does not certify a complete chip, board, operating system, application, debug policy, or production device built around the core.