VeriCHERI：在RTL层级对CHERI的详尽形式化安全验证
VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL
AI总结：
本文提出VeriCHERI，一种无需ISA规范的RTL层级安全验证方法，通过四个无界属性针对机密性和完整性目标，对CHERI硬件实现进行详尽的形式化安全验证。
摘要：
在计算系统中，保护内存中的数据免受攻击者侵害一直是一个令人关注的问题。CHERI是一种实现此类保护的有前景的方法，它通过在硬件中直接提供并强制执行细粒度的内存保护来实现。然而，为整个系统栈建立信任，需要对CHERI的硬件保护机制进行无遗漏的验证。现有的CHERI验证方法针对的是抽象ISA模型，而非底层的硬件实现。在先前的流程中，完全确保具体RTL实现具备CHERI的安全保证是一项挑战，且需要大量人工工作。本文提出了VeriCHERI，一种全新的安全验证方法。它在概念上与以往工作不同，因为它不需要任何ISA规范。我们不再检查是否符合黄金ISA模型，而是针对公认的机密性和完整性全局安全目标进行检查。为了完全覆盖这些目标，VeriCHERI仅使用四个无界属性，即可详尽地证明或证伪任何漏洞。我们在实现CHERI变体的基于RISC-V的处理器上，展示了VeriCHERI的有效性与可扩展性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
