Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor
Louis-Emile Ploix, Alasdair Armstrong, Tom Melham, Ray Lin, Haolong Wang, Anastasia Courtney
TL;DR
This work tackles the challenge of formally verifying a CHERI-extended RISC-V core with compressed capabilities against a Sail specification, establishing observational correctness for the processor’s memory interactions. It introduces a Sail-to-SystemVerilog flow and a pipeline follower that synchronizes Sail evaluation with a pipelined ISA implementation, supported by a global data-type invariant to enable unbounded proofs via $k$-induction. The verification uncovers roughly 30 design bugs, including critical monotonicity violations, and demonstrates practical impact by enabling high-assurance CHERI hardware implementations such as CHERIoT-Ibex in embedded contexts. Positioned among prior CHERI verification efforts, this methodology offers a repeatable, scalable pathway for proving hard security properties in CHERI-enabled processors and informs both core verification and broader CHERI hardware development.
Abstract
The CHERI architecture equips conventional RISC ISAs with significant architectural extensions that provide a hardware-enforced mechanism for memory protection and software compartmentalisation. Architectural capabilities replace conventional integer pointers with memory addresses bound to permissions constraining their use. We present the first comprehensive formal verification of a capability extended RISC-V processor with internally 'compressed' capabilities - a concise encoding of capabilities with some resemblance to floating point number representations. The reference model for RTL correctness is a minor variant of the full and definitive ISA description written in the Sail ISA specification language. This is made accessible to formal verification tools by a prototype flow for translation of Sail into SystemVerilog. Our verification demonstrates a methodology for establishing that the processor always produces a stream of interactions with memory that is identical to that specified in Sail, when started in the same initial state. We additionally establish liveness. This abstract, microarchitecture-independent observational correctness property provides a comprehensive and clear assurance of functional correctness for the CHERIoT-Ibex processor's observable interactions with memory.