A Formal Verification Approach for Detecting Opcode Trojans

被引：0

作者：

Mathure, Nimish ^{[1
]}

Srinivasan, Sudarshan K. ^{[1
]}

Ponugoti, Kushal K. ^{[1
]}

Malik, Akansha ^{[1
]}

Quanbeck, Samuel ^{[1
]}

机构：

[1] North Dakota State Univ, Dept Elect & Comp Engn, Fargo, ND 58105 USA

来源：

2020 27TH IEEE INTERNATIONAL CONFERENCE ON ELECTRONICS, CIRCUITS AND SYSTEMS (ICECS) | 2020年

关键词：

Hardware Trojans; Opcode Trojans; Formal Verification;

D O I：

10.1109/icecs49266.2020.9294803

中图分类号：

TM [电工技术]; TN [电子技术、通信技术];

学科分类号：

0808 ; 0809 ;

摘要：

Hardware Trojans are malicious circuit modifications and are a rising threat to the integrated circuit supply chain. There are a number of trojans directed specifically at microprocessor designs. This paper examines the threat of invalid opcodes being used as trigger mechanism for trojans in microprocessors. We demonstrate the effect of such trojans and propose an automated formal verification methodology to detect such trojans. The methodology was tested on processor models based on MIPS and RISC-V architecture. Processor benchmark circuits with as many as 400,000 gates were verified using our approach.

引用

页数：4

共 13 条

[1] Formal Verification of Gate-Level Multiple Side Channel Parameters to Detect Hardware Trojans
Abbasi, Imran Hafeez
Lodhi, Faiq Khalid
Kamboh, Awais Mehmood
Hasan, Osman
[J]. FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS (FTSCS 2016), 2017, 694 : 75 - 92
[2] The hunt for the kill switch
Adee, Sally
[J]. IEEE SPECTRUM, 2008, 45 (05) : 34 - 39
[3] [Anonymous], 2005, Report of the Defense Science Board Task Force on Nuclear Weapon Effects: Test, Evaluation, and Simulation
[4] Hardware Trojan Attacks: Threat Analysis and Countermeasures
Bhunia, Swarup
Hsiao, Michael S.
Banga, Mainak
Narasimhan, Seetharam
[J]. PROCEEDINGS OF THE IEEE, 2014, 102 (08) : 1229 - 1247
[5] Burch J.R, 1994, LECT NOTES COMPUTER, V818
[6] Gruss D, 2015, PROCEEDINGS OF THE 24TH USENIX SECURITY SYMPOSIUM, P897
[7] Li Zhen, 2013, 2013 10th International Conference on Communications, Circuits and Systems (ICCCAS), P524, DOI 10.1109/ICCCAS.2013.6765398
[8] 2015 site condition monitoring and site check surveys of marine sedimentary and reef habitats in the Loch nam Madadh SAC, Loch nam Madadh SSSI and Loch an Duin SSSI
Moein, Samer
Gulliver, Thomas Aaron
Gebali, Fayez
Alkandari, Abdulrahman
[J]. IEEE ACCESS, 2016, 4 : 2721 - 2731
[9] Rathmair M, 2014, IEEE INT SYMP CIRC S, P169, DOI 10.1109/ISCAS.2014.6865092
[10] Reece T, 2013, 2013 IEEE INTERNATIONAL CONFERENCE ON TECHNOLOGIES FOR HOMELAND SECURITY (HST), P467, DOI 10.1109/THS.2013.6699049

← 1 2 →