论文标题
验证RISC-V物理记忆保护
Verifying RISC-V Physical Memory Protection
论文作者
论文摘要
我们正式验证RISC-V中物理内存保护（PMP）的开源硬件实现，这是用于在安全关键系统（例如Keystone Trust的执行环境）中用于内存隔离的标准功能。 PMP提供了每个硬件 - 线程机器模式控制寄存器，以指定物理内存区域的访问特权。我们首先根据RISC-V ISA手册正式化PMP规则的功能属性。然后，我们使用石灰工具将用凿子编写的PMP硬件模块的开源实现转换为UCLID5正式验证语言。我们在UCLID5中编码形式规范，并验证硬件的功能正确性。这是验证Keystone框架的最初努力，在该框架中，受信任的计算基础（TCB）依靠PMP提供安全保证，例如完整性和机密性。
We formally verify an open-source hardware implementation of physical memory protection (PMP) in RISC-V, which is a standard feature used for memory isolation in security critical systems such as the Keystone trusted execution environment. PMP provides per-hardware-thread machine-mode control registers that specify the access privileges for physical memory regions. We first formalize the functional property of the PMP rules based on the RISC-V ISA manual. Then, we use the LIME tool to translate an open-source implementation of the PMP hardware module written in Chisel to the UCLID5 formal verification language. We encode the formal specification in UCLID5 and verify the functional correctness of the hardware. This is an initial effort towards verifying the Keystone framework, where the trusted computing base (TCB) relies on PMP to provide security guarantees such as integrity and confidentiality.
