Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor
The work
| Authors | Louis-Emile Ploix; Alasdair Armstrong; Tom Melham; Ray Lin; Haolong Wang; Anastasia Courtney |
|---|---|
| Editors | |
| Type | misc |
| Year | 2025 |
| Citekey | ploix2025comprehensive |
Identifiers
| arXiv | 2502.04738 from its landing_page_url |
|---|
Access
| Landing page | https://arxiv.org/abs/2502.04738 |
|---|---|
| Free full text | https://arxiv.org/pdf/2502.04738 |
Related
| Distinct from | baty2024formal |
|---|---|
| Distinct from | bloem2018formal |
| Distinct from | bouzafour2018modelchecking |
| Distinct from | burch1994automatic |
| Distinct from | dumitrescu2003construction |
| Distinct from | huang2018instructionlevel |
| Distinct from | jules2025herve |
| Distinct from | kan2026interaction |
| Distinct from | kocher1996timing |
| Distinct from | melham1988using |
| Distinct from | tan2023security |
| Distinct from | toma2006verification |
From bibtex.
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.
A copy is held
pdf, 1.1 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-16 19:53 UTC |
| Approved by | a person 2026-09-16 20:46 UTC |
Cite it as
@misc{ploix2025comprehensive,
title = {Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor},
author = {Louis-Emile Ploix and Alasdair Armstrong and Tom Melham and Ray Lin and Haolong Wang and Anastasia Courtney},
year = {2025},
}
This record lives at https://refs.drheap.org/ploix2025comprehensive/ and will keep doing so.