Skip to main content

End to End Formal Verification of Processors with Fine-Grained Memory Protection

Conference: Verification Futures 2024 (click here to see full programme)
Speaker: Professor Tom Melham
Presentation Title: End to End Formal Verification of Processors with Fine-Grained Memory Protection

Capability Hardware Enhanced RISC Instructions (CHERI) extend conventional ISAs with capabilities that can enable fine-grained memory protection and scalable software compartmentalisation. This talk will discuss ongoing work at Oxford on the formal verification of a RISC-V processor with significant capability instruction extensions and so-called “compressed” capabilities. We use this case study both to drive research aiming at methodological innovation and to develop and exercise new tools for formal specification of instruction set architectures, aiming to make truly end-to-end verification against full, formal ISA specifications a reality.

Speaker Bio:

Tom Melham is a Professor of Computer Science at the University of Oxford and a Fellow of Balliol College, where he Tutor in Computation. Melham received his PhD from the University of Cambridge in 1990 for his foundational research in formal hardware verification and mechanized reasoning. In 1993 he joined the Computing Science Department at Glasgow University and was appointed to a Professorship of Computing Science at Glasgow in 1998, before moving to Oxford in 2002. Melham’s research interests include AI and technology in legal services and the justice system; testing and evaluation of AI-based systems; verification of quantum computation; applications of formal logic; mechanised reasoning; model checking and theorem proving; firmware verification; formal hardware verification; and programming language semantics.

He works closely with leading companies in EDA and semiconductors on advanced tools and methods for formal verification. Melham serves on the Board of Trustees of the Alan Turing Institute, the UK’s national institute for AI and data science. He is a chartered engineer and a Fellow of the British Computer Society and of the Royal Society of Edinburgh.

Key Points:
  • This work is the first ever formal verification with substantial coverage of a processor – the CHERIoT-ibex design from Microsoft – that includes compressed capabilities.
  • Our work caught around 30 bugs in the CherIoT-ibex design, all to do with the capability extensions added to the original ibex core. Four of these, if undetected, would have compromised its utility in preventing memory error exploits - so our verification has substantially increased confidence in the security guarantees provided by the processor.
  • We demonstrate several proof engineering innovations that allow us to aim for full, not bounded, proofs – against a comprehensive specification of the ISA in the Sail specification language.
  • Close Menu