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.

翻译：我们正式核查RISC-V中物理内存保护(PMP)的开源硬件实施情况,这是用于关键安全系统(如关键石信任的执行环境)内存隔离的标准特征。PMP提供每个硬件-读机器-模式控制登记册,具体规定物理内存区域的访问权限。我们首先根据RISC-V ISA手册正式确定PMP规则的功能属性。然后,我们使用LIME工具将用Chisel拼写成UCLID5正式核查语言的PMP硬件模块的开源实施翻译为UCLID5的正式版本。我们把正式规格编码在UCLID5中,并核查硬件的功能正确性。这是核查Keystone框架的初步努力,在Keystone框架中,信任的计算基础依靠PMP提供完整性和保密性等安全保障。