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.

翻译：保护内存中的数据免受攻击者侵害仍然是计算系统中的一个持续关注点。CHERI是一种通过在硬件中直接提供并强制执行细粒度内存保护来实现此类防护的有前景的方法。然而，要建立对整个系统栈的信任，需要对CHERI基于硬件的保护机制进行无间隙的验证。现有的CHERI验证方法针对的是抽象的指令集架构（ISA）模型，而非底层的硬件实现。在先前的工作流程中，要完全确保具体RTL实现满足CHERI的安全保证是一项挑战，并且需要大量人工投入。本文提出了VeriCHERI，一种新颖的安全验证方法。它在概念上不同于以往的工作，因为它不需要任何ISA规范。我们不是检查与一个黄金ISA模型的符合性，而是根据已确立的全局安全目标——机密性和完整性——进行检查。为了全面覆盖这些目标，VeriCHERI仅使用四条无界属性来穷尽式地证明或证伪任何漏洞。我们在一个实现了CHERI变体的RISC-V处理器上展示了VeriCHERI的有效性和可扩展性。