-
题名基于Yosys的硬件信息流安全验证与漏洞检测
被引量：4
- 1
-
-
作者
陈春雷
王省欣
谭静
朱嘉诚
胡伟
-
机构
潍坊学院计算机工程学院
西北工业大学网络空间安全学院
-
出处
《计算机应用研究》
CSCD
北大核心
2021年第6期1865-1869,共5页
-
基金
国家自然科学基金资助项目(61672433)。
-
文摘
针对基于功能验证和侧信道分析的硬件安全漏洞检测方法的不足,提出了一种结合Yosys形式化验证能力和门级信息流追踪方法对集成电路设计进行安全验证和漏洞检测的方案。首先,使用Yosys对硬件电路设计进行逻辑综合,生成门级网表。其次,为电路设计中各信号的每个比特位添加污染标签,并采用二进制位粒度的污染标签传播策略为基本逻辑单元生成门级信息流模型,进而以此为基本单元构建整个电路的信息流模型。然后,描述电路设计中关键数据的机密性和完整性属性,并将其映射为Yosys可识别的安全约束。最后,结合Yosys和电路的信息流模型对电路设计的安全属性进行验证,安全验证中捕捉到违反安全属性的事件,即表明硬件设计中存在安全漏洞。实验表明,该方法能够准确检测到AES加密电路中植入的一种可满足性无关项木马。实验结果验证了该方法能够在不依赖功能验证和侧信道分析的前提下检测到安全漏洞,因而适用范围更广。
-
关键词
硬件安全
信息流安全
安全验证
漏洞检测
yosys
-
Keywords
hardware security
information flow security
security verification
vulnerability detection
yosys
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
