VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL

Protecting data in memory from attackers continues to be a concern in computer systems. CHERI is a promising approach to achieve such protection, by providing and enforcing fine-grained memory protection directly in the hardware. However, establishing trust for the entire system stack requires a gap-free verification of CHERI's hardware-based protection mechanisms. Existing verification methods for CHERI target the abstract ISA model rather than the underlying hardware implementation. Fully ensuring the CHERI security guarantees for a concrete RTL implementation is a challenge in previous flows and demands high manual efforts. In this talk, we present VeriCHERI, a novel approach to security verification. It is conceptually different from previous works in that it does not require any ISA specification. Instead of checking compliance with a golden ISA model, we check against well-established global security objectives of confidentiality and integrity. Fully covering these objectives, VeriCHERI uses as few as four unbounded properties to exhaustively prove or disprove any vulnerability. We present a case study on a RISC-V-based processor implementing a CHERI variant that demonstrates the effectiveness and scalability of VeriCHERI. The verification approach uncovered several security-critical bugs, including a timing side channel that allows an attacker to probe arbitrary memory words.

Johannes Müller received his Dipl.-Ing. degree in Electrical and Computer Engineering from the University of Kaiserslautern in 2018. He is currently a Ph.D. candidate and researcher in the Electronic Design Automation group at RPTU Kaiserslautern-Landau, working under supervision of Prof. Wolfgang Kunz and Prof. Dominik Stoffel. His research interests include formal security verification, access control mechanisms and timing side channels. He co-authored the DAC '22 best paper award winning work on verification of data-independent timing. For his work on SoC-wide security verification, he received the Intel Hardware Security Academic Award 2022.