VeriCHERI：针对 CHERI RTL 层面的彻底形式安全验证

保护计算系统中内存数据的安全性持续是一项关注点。CHERI 作为一种实现此类保护的有前景的方案，通过在硬件中提供和执行细粒度的内存保护机制。然而，要为整个系统堆栈建立信任，需对 CHERI 的硬件基础保护机制进行无缝隙的验证。现有 CHERI 验证方法针对的是抽象的 ISA 模型，而非底层硬件实现。 fully 确保针对具体 RTL 实现的 CHERI 安全保证，以前工作中的一个挑战，要求大量手动工作。本文提出了 VeriCHERI，一种新的安全验证方法。其概念上与前述工作不同，无需任何 ISA 规范。不同于检查是否符合给定的 ISA 模型，VeriCHERI 针对保密性和完整性等既定的全局安全目标进行验证。通过完全覆盖这些目标，VeriCHERI 只需四个无界属性即可穷尽性地证明或反证是否存在任何漏洞。我们在基于 RISC-V 的处理器上实现 CHERI 变体，展示了 VeriCHERI 的有效性和可扩展性。