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

Hardware information flow security verification and vulnerability detection using Yosys

作　　者：陈春雷 王省欣 谭静 朱嘉诚 胡伟[2] Chen Chunlei;Wang Xingxin;Tan Jing;Zhu Jiacheng;Hu Wei(School of Computer Engineering,Weifang University,Weifang Shandong 261061,China;School of Cybersecurity,Northwestern Polytechnical University,Xi’an 710072,China)

机构地区：[1]潍坊学院计算机工程学院,山东潍坊261061 [2]西北工业大学网络空间安全学院,西安710072

出　　处：《计算机应用研究》2021年第6期1865-1869,共5页Application Research of Computers

基　　金：国家自然科学基金资助项目(61672433)。

摘　　要：针对基于功能验证和侧信道分析的硬件安全漏洞检测方法的不足,提出了一种结合Yosys形式化验证能力和门级信息流追踪方法对集成电路设计进行安全验证和漏洞检测的方案。首先,使用Yosys对硬件电路设计进行逻辑综合,生成门级网表。其次,为电路设计中各信号的每个比特位添加污染标签,并采用二进制位粒度的污染标签传播策略为基本逻辑单元生成门级信息流模型,进而以此为基本单元构建整个电路的信息流模型。然后,描述电路设计中关键数据的机密性和完整性属性,并将其映射为Yosys可识别的安全约束。最后,结合Yosys和电路的信息流模型对电路设计的安全属性进行验证,安全验证中捕捉到违反安全属性的事件,即表明硬件设计中存在安全漏洞。实验表明,该方法能够准确检测到AES加密电路中植入的一种可满足性无关项木马。实验结果验证了该方法能够在不依赖功能验证和侧信道分析的前提下检测到安全漏洞,因而适用范围更广。Functionality-validation and side-channel-analysis methods are facing significant limitations in the context of hardware security vulnerability detection.In view of these limitations,this paper integrated Yosys-based formal validation and gate-level information flow tracking to propose a security-validation and vulnerability-detection method.The proposed method consisted of four steps.The first step synthesized the Verilog design of a circuit to generate gate-level netlist through Yosys.The second step endowed each bit of the circuit signals with a one-bit taint label,and thus generated gate-level information flow models of basic logic units based on this bitwise-granularity taint label propagation policy.The gate-level models established the foundation of building the information flow for the entire circuit.The third step described confidentiality and integrity of the key data,and subsequently mapped confidentiality and integrity into Yosys-recognizable security constraints.The fourth step validated the security properties of the circuit by Yosys and the information flow model.Violation of security properties means security flaws in the circuit.Experiments show that the proposed method can detect a satisfiability Don’t-Care Trojan implanted into an AES encryption circuit.The experimental results validate that the proposed method is more widely applicable due to no reliance on functionality-validation or side-channel analysis.

关 键 词：硬件安全 信息流安全 安全验证 漏洞检测 Yosys 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]