西安电子科技大学学报 ›› 2021, Vol. 48 ›› Issue (3): 146-153.doi: 10.19665/j.issn1001-2400.2021.03.019

• 网络空间安全 • 上一篇    下一篇

针对硬件木马的形式化验证模型构造方法

沈利香1,2(),慕德俊3,曹国4,5,谢光前2,束方勇2   

  1. 1.西北工业大学 自动化学院,陕西 西安 710072
    2.常州工学院 计算机信息工程学院,江苏 常州 213032
    3.西北工业大学 网络空间安全学院,陕西 西安 710072
    4.西北工业大学 管理学院,陕西 西安 710072
    5.常州工学院 经济与管理学院,江苏 常州 213032
  • 收稿日期:2019-11-11 出版日期:2021-06-20 发布日期:2021-07-05
  • 作者简介:沈利香(1977—),女,副教授,西北工业大学博士研究生,E-mail:2016100110@nwpu.edu.cn
  • 基金资助:
    国家自然科学基金(61672433);国家密码发展基金(MMJJ20170210);陕西省重点研发项目(2018KW-005);江苏省社会科学基金(16GLB014);江苏省高校自然科学基金(18KJB520004)

Constructing formal verification models for hardware Trojans

SHEN Lixiang1,2(),MU Dejun3,CAO Guo4,5,XIE Guangqian2,SHU Fangyong2   

  1. 1. School of Automation,Northwestern Polytechnical University,Xi’an 710072,China
    2. School of Computer Information and Engineering,Changzhou Institute of Technology,Changzhou 213032,China
    3. School of Cybersecurity,Northwestern Polytechnical University,Xi’an 710072,China
    4. School of Management,Northwestern Polytechnical University,Xi’an 710072,China
    5. School of Economics and Management,Changzhou Institute of Technology,Changzhou 213032,China
  • Received:2019-11-11 Online:2021-06-20 Published:2021-07-05

摘要:

针对硬件安全验证的效率受形式化验证模型构建方式影响的问题,提出了一种面向硬件木马检测的自动构造形式化验证模型的方法。该方法首先遍历寄存器传输级设计的控制流图,提取出赋值语句的路径条件及其对应赋值表达式,构成Kripke结构中状态转移的约束关系;然后将Verilog语法的约束关系转换成模型检测器的语法,从而生成形式化验证模型;最后利用模型检测器对所构造的模型进行验证,当模型违反设定的安全验证属性时,检测到其中的硬件木马。利用Trust-HUB硬件木马测试基准的实验结果表明,该方法生成的形式化验证模型,能够有效检测寄存器传输级硬件设计中的木马。

关键词: 形式化验证, 模型检测, 硬件安全, 硬件木马, 安全验证

Abstract:

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.

Key words: formal verification, model checking, hardware security, hardware Trojan, security verification

中图分类号: 

  • TP393.083