《计算机应用研究》|Application Research of Computers

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

Hardware information flow security verification and vulnerability detection using yosys

免费全文下载 (已被下载 次)  
获取PDF全文
作者 陈春雷,王省欣,谭静,朱嘉诚,胡伟
机构 潍坊学院 计算机工程学院;西北工业大学 网络空间安全学院
统计 摘要被查看 次,已被下载
摘要 针对基于功能验证和侧信道分析的硬件安全漏洞检测方法的不足,提出了一种结合Yosys形式化验证能力和门级信息流追踪方法对集成电路设计进行安全验证和漏洞检测的方案。首先,使用Yosys对硬件电路设计进行逻辑综合,生成门级网表。其次,为电路设计中各信号的每个比特位添加污染标签,并采用二进制位粒度的污染标签传播策略为基本逻辑单元生成门级信息流模型,进而以此为基本单元构建整个电路的信息流模型。然后,描述电路设计中关键数据的机密性和完整性属性,并将其映射为Yosys可识别的安全约束。最后,结合Yosys和电路的信息流模型对电路设计的安全属性进行验证,安全验证中捕捉到违反安全属性的事件,即表明硬件设计中存在安全漏洞。实验表明,所提出的方法能够准确检测到AES加密电路中植入的一种可满足性无关项木马。实验结果验证了本方法能够在不依赖功能验证和侧信道分析的前提下检测到安全漏洞、因而适用范围更广。
关键词 硬件安全;信息流安全;安全验证;漏洞检测;Yosys
基金项目 国家自然科学基金资助项目(61672433)
本文URL http://www.arocmag.com/article/02-2021-05-039.html
收稿日期
修回日期
页码 -
中图分类号 TP309
文献标志码