基于Yosys的硬件信息流安全验证与漏洞检测

作者：陈春雷; 王省欣; 谭静; 朱嘉诚; 胡伟

来源：计算机应用研究, 2021, 38(06): 1865-1869.

DOI：10.19734/j.issn.1001-3695.2020.05.0193

• 硬件安全
• 信息流安全
• 安全验证
• 漏洞检测
• Yosys

针对基于功能验证和侧信道分析的硬件安全漏洞检测方法的不足,提出了一种结合Yosys形式化验证能力和门级信息流追踪方法对集成电路设计进行安全验证和漏洞检测的方案。首先,使用Yosys对硬件电路设计进行逻辑综合,生成门级网表。其次,为电路设计中各信号的每个比特位添加污染标签,并采用二进制位粒度的污染标签传播策略为基本逻辑单元生成门级信息流模型,进而以此为基本单元构建整个电路的信息流模型。然后,描述电路设计中关键数据的机密性和完整性属性,并将其映射为Yosys可识别的安全约束。最后,结合Yosys和电路的信息流模型对电路设计的安全属性进行验证,安全验证中捕捉到违反安全属性的事件,即表明硬件设计中存在安全漏洞。实验表明,该方法能够准确检测到AES加密电路中植入的一种可满足性无关项木马。实验结果验证了该方法能够在不依赖功能验证和侧信道分析的前提下检测到安全漏洞,因而适用范围更广。

• 单位
  西北工业大学; 潍坊学院