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.

Anna Duque Antón received her Dipl.-Ing. degree in Electrical and Computer Engineering from the University of Kaiserslautern in 2019. She is currently a Ph.D. candidate at the Electronic Design Automation group at the same university, working under supervision of Prof. Kunz and Prof. Stoffel. Her research interests include formal security verification, access control mechanisms and hardware trojan detection. For her work on SoC-wide security verification, she received the Intel Hardware Security Academic Award 2022.