Oxford researchers lead significant advance in processor verification for CHERIoT-Ibex

Professor Tom Melham and undergraduate student Louis-Emile Ploix have played a key role in a groundbreaking formal verification effort that enhances the quality and reliability of the CHERIoT-Ibex processor.  

This work, conducted in collaboration with the University of Cambridge, lowRISC CIC, and Microsoft, marks a major advancement in ensuring the correctness of the CHERIoT-Ibex RISC-V processor design through rigorous mathematical proofs. 

Formal verification is a critical step in processor design, ensuring that a processor behaves exactly as intended under all possible conditions. Traditional methods, such as simulation-based testing, can only check a limited number of scenarios, potentially leaving undetected errors. However, formal verification mathematically proves that a processor's design is correct across all possible executions, significantly improving confidence in its reliability. 

At the heart of this achievement is a formal verification framework developed by Professor Tom Melham and Louis-Emile Ploix, alongside Alasdair Armstrong from the University of Cambridge. Their framework establishes observational equivalence - a method that ensures the CHERIoT-Ibex hardware behaves identically to its formal specification, known as the RISC-V International Sail specification. This is done using unbounded proofs, meaning the verification holds true for all possible executions, not just a subset of test cases. 

Oxford’s contribution is particularly significant in developing and applying new formal methods to verify the CHERIoT-Ibex processor. Using Cadence Jasper™ verification tools and Sail support, the team has automated the generation of a SystemVerilog reference model from the Sail specification. This rigorous verification process ensures that the security mechanisms in CHERIoT-Ibex, which protect against memory vulnerabilities and enable secure compartmentalisation, are implemented correctly. 

‘The CHERIoT-Ibex project has been an ideal challenge for our formal verification research at Oxford, which aims at both scientific innovation and strong real-world impact. We are delighted that our work has significantly helped to increase confidence in the commercial-grade quality of Microsoft’s CHERIoT-Ibex core.’ - Professor Tom Melham and lead verification engineer Louis-Emile Ploix. 

This achievement highlights the growing role of open-source collaboration in advancing processor verification. lowRISC, a not-for-profit organisation focused on open-source silicon development, has integrated this formal verification framework into the CHERIoT-Ibex repository. This means that companies and researchers worldwide can benefit from the verification efforts, ensuring that high-quality, secure, and reliable processors are accessible to a broad range of developers. 

For industry, this applied verification research means reduced risk of design flaws, improved security, and faster time-to-market for new processors. As modern processors grow in complexity, formal verification is becoming an essential tool for ensuring their correctness before fabrication. The Oxford-led research sets a precedent for future RISC-V verification projects, offering a robust methodology that others can adopt. Beyond CHERIoT-Ibex, lowRISC has also applied this formal verification framework to its regular Ibex processor, widely used in the OpenTitan® root of trust.  

The early, foundational work at Oxford on the formal verification of CHERIoT-Ibex was started as a third-year undergraduate project by alumnus Ray Lin, and its continuation by Louis-Emile Ploix and other members of the team was funded by Digital Security by Design and UKRI as part of the SCorCH project.  

By integrating formal verification into the design process, this research ensures that next-generation processors like CHERIoT-Ibex meet the highest standards of security and reliability, reinforcing Oxford’s leadership in advancing verification technologies for modern computing.