验证 RISC-V 物理内存保护
密码学与安全
2022-11-07 v1
摘要
我们正式验证了 RISC-V 中物理内存保护（PMP）的一个开源硬件实现，PMP 是用于 Keystone 可信执行环境等安全关键系统中内存隔离的标准特性。PMP 提供每硬件线程的机器模式控制寄存器，用于指定物理内存区域的访问权限。我们首先基于 RISC-V ISA 手册形式化了 PMP 规则的功能属性。然后，我们使用 LIME 工具将用 Chisel 编写的开源 PMP 硬件模块实现翻译为 UCLID5 形式化验证语言。我们在 UCLID5 中对形式化规范进行编码，并验证该硬件的功能正确性。这是验证 Keystone 框架的初步工作，其可信计算基（TCB）依赖 PMP 提供完整性与机密性等安全保证。
引用
@article{arxiv.2211.02179,
title = {Verifying RISC-V Physical Memory Protection},
author = {Kevin Cheang and Cameron Rasmussen and Dayeol Lee and David W. Kohlbrenner and Krste Asanović and Sanjit A. Seshia},
journal= {arXiv preprint arXiv:2211.02179},
year = {2022}
}
备注
SECRISC-V 2019 Workshop