Constructing formal verification models for hardware Trojans

被引：0

作者：

Shen L. ^{[1
,2
]}

Mu D. ^{[3
]}

Cao G. ^{[4
,5
]}

Xie G. ^{[2
]}

Shu F. ^{[2
]}

机构：

[1] School of Automation, Northwestern Polytechnical University, Xi'an

[2] School of Computer Information and Engineering, Changzhou Institute of Technology, Changzhou

[3] School of Cybersecurity, Northwestern Polytechnical University, Xi'an

[4] School of Management, Northwestern Polytechnical University, Xi'an

[5] School of Economics and Management, Changzhou Institute of Technology, Changzhou

来源：

Xi'an Dianzi Keji Daxue Xuebao/Journal of Xidian University | 2021年 / 48卷 / 03期

关键词：

Formal verification; Hardware security; Hardware Trojan; Model checking; Security verification;

D O I：

10.19665/j.issn1001-2400.2021.03.019

中图分类号：

学科分类号：

摘要：

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. © 2021, The Editorial Board of Journal of Xidian University. All right reserved.

引用

页码：146 / 154

页数：8

共 15 条

[1]

LI H, LIU Q, Zhang J., A Survey of Hardware Trojan Threat and Defense, Integration the VLSI Journal, 55, pp. 426-437, (2016)

[2]

JIN Y, GUO X, DUTTA R G, Et al., Data Secrecy Protection through Information Flow Tracking in Proof-carrying Hardware IP Part I: Framework Fundamentals, IEEE Transactions on Information Forensics and Security, 12, 10, pp. 2416-2429, (2017)

[3]

BIDMESHKI M M, GUO X L, DUTTA R G, Et al., Data Secrecy Protection through Information Flow Tracking in Proof-carrying Hardware IP Part II: Framework Automation, IEEE Transactions on Information Forensics and Security, 12, 10, pp. 2430-2443, (2017)

[4]

GUO X, DUTTA R G, MISHRA P, Et al., Automatic RTL-to-formal Code Converter for IP Security Formal Verification, Proceedings of the 2016 17th International Workshop on Microprocessor and SOC Test and Verification, pp. 35-38, (2017)

[5]

GUO X, DUTTA R G, MISHAR P, Et al., Automatic Code Converter Enhanced PCH Framework for SoC Trust Verification, IEEE Transactions on Very Large Scale Integration Systems, 25, 12, pp. 3390-3400, (2017)

[6]

QIN Maoyuan, MU Dejun, HU Wei, Et al., Fine-granularity Gate Level Formal Verification Method for Hardware Security, Journal of Xidian University, 45, 5, pp. 143-148, (2018)

[7]

DING Ming, ZHANG Shuling, ZHANG Chen, Et al., Method for the Verification of Safety Requirements of Avionics Systems, Journal of Xidian University, 46, 3, pp. 66-73, (2019)

[8]

MUKHERJEE R, KROENING D, MELHAM T., Hardware Verification Using Software Analyzers, Proceedings of the 2015 IEEE Computer Society Annual Symposium on VLSI, pp. 7-12, (2015)

[9]

IRFAN A, CIMATTI A, GRIGGIO A, Et al., Verilog2SMV: aTool for Word-level Verification, Proceedings of the 2016 Design, Automation and Test in Europe Conference and Exhibition, pp. 1156-1159, (2016)

[10]

WORF C., Yosys Open SYnthesis Suite

← 1 2 →