【论文分享】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