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.

This talk presents 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.