摘要
针对硬件安全验证的效率受形式化验证模型构建方式影响的问题,提出了一种面向硬件木马检测的自动构造形式化验证模型的方法。该方法首先遍历寄存器传输级设计的控制流图,提取出赋值语句的路径条件及其对应赋值表达式,构成Kripke结构中状态转移的约束关系;然后将Verilog语法的约束关系转换成模型检测器的语法,从而生成形式化验证模型;最后利用模型检测器对所构造的模型进行验证,当模型违反设定的安全验证属性时,检测到其中的硬件木马。利用Trust-HUB硬件木马测试基准的实验结果表明,该方法生成的形式化验证模型,能够有效检测寄存器传输级硬件设计中的木马。
The effectiveness of hardware security verification is affected by the way of constructing formal verification models.To solve this problem,this paper proposes a method which can automatically construct formal verification models for hardware Trojans detection.First,the method traverses the control flow graphs of the register transfer level design to extract the path conditions of assignment statements and the corresponding expressions.The constraint relations of the Kripke’state transition are generated based on the path conditions and the expressions.Second,the constraint relations of the Verilog grammar are transformed to the grammar of the model checker and generate the formal verification models.Finally,a model checker verifies the models and detects the hardware Trojans when a predefined specification is verified as false.In experiments,the hardware Trojans in the Trust-HUB benchmarks are detected,which shows that the models constructed by our method can effectively detect hardware Trojans in register transfer level design.
作者
沈利香
慕德俊
曹国
谢光前
束方勇
SHEN Lixiang;MU Dejun;CAO Guo;XIE Guangqian;SHU Fangyong(School of Automation,Northwestern Polytechnical University,Xi’an 710072,China;School of Computer Information and Engineering,Changzhou Institute of Technology,Changzhou 213032,China;School of Cybersecurity,Northwestern Polytechnical University,Xi’an 710072,China;School of Management,Northwestern Polytechnical University,Xi’an 710072,China;School of Economics and Management,Changzhou Institute of Technology,Changzhou 213032,China)
出处
《西安电子科技大学学报》
EI
CAS
CSCD
北大核心
2021年第3期146-154,共9页
Journal of Xidian University
基金
国家自然科学基金(61672433)
国家密码发展基金(MMJJ20170210)
陕西省重点研发项目(2018KW-005)
江苏省社会科学基金(16GLB014)
江苏省高校自然科学基金(18KJB520004)。
关键词
形式化验证
模型检测
硬件安全
硬件木马
安全验证
formal verification
model checking
hardware security
hardware Trojan
security verification