Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor

Abstract

This paper reports the first comprehensive formal verification of observational correctness for the CHERIoT-Ibex processor, a RISC-V core implementing the security-focused CHERI architecture with complex, internally compressed capabilities. Utilizing the Sail ISA specification as the definitive reference model, the methodology establishes that the processor's stream of memory interactions is functionally identical to the specification. This achievement provides comprehensive, microarchitecture-independent assurance of the functional correctness and liveness of this security-critical hardware design.

Report

Key Highlights

• First Comprehensive Formal Verification: This is the initial comprehensive formal verification of a capability-extended RISC-V processor that incorporates internally 'compressed' capabilities.
• Target: The verification focuses on the CHERIoT-Ibex processor, which integrates the CHERI architecture extensions.
• Observational Correctness: The primary property verified is 'observational correctness,' proving that the hardware's observable interactions with memory perfectly match the definitive ISA specification.
• Golden Reference Model: The ISA description written in the Sail specification language serves as the reference model for RTL correctness.
• Liveness Established: In addition to functional correctness, the verification successfully established the liveness property of the processor.

Technical Details

• Processor Architecture: CHERIoT-Ibex, a RISC-V Instruction Set Architecture (ISA) equipped with CHERI architectural extensions.
• CHERI Mechanism: CHERI enhances memory protection and software compartmentalization by replacing conventional integer pointers with hardware-enforced 'capabilities,' which are memory addresses bound to permissions.
• Capability Encoding: The processor utilizes 'internally compressed' capabilities, described as a concise encoding that shares characteristics with floating-point number representations, adding significant complexity to the verification task.
• Specification Language: The formal and definitive reference model for the ISA is written in the Sail ISA specification language.
• Verification Flow: A prototype flow was utilized to translate the Sail specification into SystemVerilog, making the abstract ISA description accessible to conventional formal verification tools.
• Verification Goal: To prove that the processor, when started in the same initial state as the Sail model, generates an identical stream of interactions with memory.

Implications

• Enhanced Security Assurance: Providing comprehensive formal verification for a processor utilizing CHERI—a critical memory safety and security architecture—significantly increases trust in the hardware implementation, essential for secure embedded and compartmentalized systems.
• Validation of CHERI Implementation: Successfully verifying the functional correctness of a complex feature like internally compressed capabilities demonstrates the feasibility and robustness of implementing advanced security features within the RISC-V ecosystem.
• Methodology Advancement: The development and successful application of a prototype flow translating Sail to SystemVerilog establishes a powerful methodology. This bridges the gap between high-level, executable ISA specifications and the formal verification of low-level RTL, potentially becoming a standard practice for verifying complex RISC-V extensions.
• Foundational Trust for RISC-V: By proving abstract, microarchitecture-independent functional correctness, this work strengthens the foundation of the RISC-V ecosystem, especially as it moves toward adopting security extensions like CHERI in commercial and safety-critical domains.