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.

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.