VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL

TL;DR

VeriCHERI presents a spec-free, RTL-level formal verification flow for CHERI that directly targets global confidentiality and integrity objectives rather than ISA specifications. By deriving unbounded properties from a general security objective and using interval-based checks with a CHERI-specific UPEC adaptation, it detects both functional and timing-related vulnerabilities, including Meltdown-style leaks. The approach is demonstrated on the CHERIoT Ibex core, where it uncovered several issues and a Meltdown-style timing vulnerability that was mitigated, illustrating scalability and practical impact. Invariants such as weak capability monotonicity and representability invariants provide reusable verification IPs, suggesting VeriCHERI can complement existing functional verification to deliver stronger trust in CHERI hardware implementations.

Abstract

Protecting data in memory from attackers continues to be a concern in computing systems. CHERI is a promising approach to achieve such protection, by providing and enforcing fine-grained memory protection directly in the hardware. Creating trust for the entire system stack, however, 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 paper presents VeriCHERI, a novel approach to security verification. It is conceptionally 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 demonstrate the effectiveness and scalability of VeriCHERI on a RISC-V based processor implementing a CHERI variant.

Figures (4)

• Figure 1: 1-safety non-interference interval properties
• Figure 2: Interval property for monotonicity
• Figure 3: UPEC property for CHERI
• Figure 4: VeriCHERI Verification Flow