  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.
