【论文分享】A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level
本次分享的论文被收录于2021的DAC。
1. Contribution
文章提出了一种形式化验证方法，以检测硬件（HW）和SoC硬件/固件接口中的安全关键bug。文章还展示了一种组合方法，通过该方法发现的漏洞可以支持硬件级的设计修复，也支持软件级的设计修复。文章介绍了针对Pulpissimo的实验，在该平台上发现了几个安全关键漏洞，以及针对RocketChip的实验。
2. 扩展UPEC概念
UPEC确保了执行程序的非特权攻击者无法观察到机密数据。虽然UPEC包括了处理器内核中的所有信息泄漏场景，但现在SoCs具有许多外设和加速器，所以UPEC仍有问题。在复杂的SOC中，机密数据可以绕过主核，直接泄漏到内存或内存映射的未受保护区域。比如一个具有内存总线主接口的系统组件，它可以绕过内存保护，将机密数据复制到未受保护的内存空间或内存映射的未受保护区域。
因此，文章扩展了UPEC，不仅考虑了机密数据在程序的可见寄存器，还考虑了系统主要输出，包括机密数据直接传播到未受保护的内存区域（例如，通过DMA）的场景。每当机密数据传播到状态变量集，即架构状态变量、主要输出和未受保护的内存位置时，就会发出警报，这组状态变量称为可观察状态变量集。
文章还扩展了机密数据的可能位置集，包括系统的所有内存位置、所有主要输入以及受非特权用户程序保护的所有架构寄存器。UPEC不是静态地保护单个地址，而是为受保护的地址和相应的保护机制配置使用符号公式【Definition 1】，因此可以细化到其他具体实现。
比如：基于RISC-V ISA规范，文章开发了符合ISA的PMP配置（PMP寄存器内容）的符号描述，这些配置使用户级攻击者无法访问选定的内存位置（或内存映射设备寄存器）。
计算树逻辑性质如下：
作者在有界模型上运行UPEC SoC，如下图所示。文章没有显式枚举所有地址，而是将机密地址作为新的状态变量protected_addr引入计算模型。虽然此解决方案仍然隐式枚举所有地址，但它可利用文章提供的模型和SAT解算器特征之间的协同作用：在验证过程中，SAT解算器了解到，只有两个设计实例之间的差异才能导致安全警报。因此，它只考虑那些可能导致这种差异的地址。这大大降低了证明的复杂性。
下图显示了要证明的UPEC SoC属性。
3.COMPOSITIONAL HW/FW VERIFICATION
安全违规要么是由硬件错误引起的，这些错误可以直接在RTL模型中修复，要么是由HW/FW接口中的错误配置造成的。尽管这些违规行为也可以在RTL中解决，但是比起修改硬件，在FW中修复它们通常更方便。流程如下图所示。
FW的约束会转换为C语言断言，这些断言只依赖于程寄存器和地址，因此可以直接在FW中检查。这使得该流程与大多数FW开发和验证程序兼容。
4.实验
文章在Pulpissimo 和RocketChip 上证明了该方法的有效性。实验使用OneSpin 360 DV。
1. 文章在Pulpissimo发现的漏洞和修复如下图：
2. 文章发现Rocketchip的缓存控制器设计存在问题。
如果缓存未命中，缓存控制器将重新填充整个缓存行，而不检查相邻地址的PMP权限。如果相邻的位置不受保护，机密数据可以被复制到缓存中。虽然缓存中的机密数据在用户级别程序仍然无法访问，并且不违反机密性要求，但这可能会在某些情况下产生安全影响。
5.相关资料
https://github.com/kangoojim/symbolic-pmp
原文始发于微信公众号（COMPASS Lab）：【论文分享】A Formal Approach to Confidentiality Verification in SoCs
