Survey on model checking based hardware Trojan detection technology

Qizhi ZHANG; Yiqiang ZHAO; Ya GAO; Haocheng MA

doi:10.11959/j.issn.2096-109x.2021029

您当前的位置：

首页 >

文章列表页 >

Survey on model checking based hardware Trojan detection technology

Topic: Integrated Circuit Hardware Security | 更新时间：2024-06-03

- Survey on model checking based hardware Trojan detection technology
- Chinese Journal of Network and Information Security Vol. 7, Issue 2, Pages: 57-63(2021)
- 作者机构：
- 作者简介：
- 基金信息：
- DOI：10.11959/j.issn.2096-109x.2021029
  CLC： TN407
- Online First：2021-04，
  
  Published：15 April 2021
- 稿件说明：
移动端阅览
Qizhi ZHANG, Yiqiang ZHAO, Ya GAO, et al. Survey on model checking based hardware Trojan detection technology[J]. Chinese Journal of Network and Information Security, 2021, 7(2): 57-63.
DOI：

Qizhi ZHANG, Yiqiang ZHAO, Ya GAO, et al. Survey on model checking based hardware Trojan detection technology[J]. Chinese Journal of Network and Information Security, 2021, 7(2): 57-63. DOI： 10.11959/j.issn.2096-109x.2021029.

摘要

硬件木马对原始电路的恶意篡改，已成为集成电路面临的核心安全威胁。为了保障集成电路的安全可信，研究人员提出了诸多硬件木马检测方法。其中，模型检测作为一种形式化验证方法，在设计阶段可有效检测出硬件木马。首先，阐述了模型检测的工作原理和应用流程；其次，介绍了基于模型检测的硬件木马检测技术的研究进展；最后，指出了当前该技术所面临的瓶颈，并讨论了潜在的研究方向。

Abstract

Hardware Trojan is malicious tampering to the original circuit

which has become the most important security threat of integrated circuit.In order to ensure the safety and reliability of ICs

many hardware Trojan detection methods are proposed.As one of the formal verification methods

model checking can effectively detect the hardware Trojan in the design phase.Firstly

the working principle and process of model checking were described.Secondly

the research progress of hardware Trojan detection technology based on model checking was introduced.Finally

the bottlenecks faced by the current technology were pointed out and the potential research direction was discussed.

关键词

Keywords

references

AGRAWAL D , BAKTIR S , KARAKOYUNLU D , et al . Trojan detection using IC fingerprinting [C ] // IEEE Symposium on Security and Privacy (SP '07) , 2007 : 296 - 310 .

FLOTTES M , DUPUIS S , BA P , et al . On the limitations of logic testing for detecting hardware Trojans Horsesv [C ] // 10th International Conference on Design ＆ Technology of Integrated Systems in Nanoscale Era (DTIS),Naples . 2015 : 1 - 5 .

HELY D , MARTIN J , DARIO G , et al . Experiences in side channel and testing based hardware Trojan detection [C ] // IEEE 31st VLSI Test Symposium (VTS) . 2013 : 1 - 4 .

CLARKE E M , GRUMBERGO , PELED D , et al . Model checking [M ] . Cambridge : MIT press , 1999 .

BARTOLETTI M , DEGANO P , FERRARI G L , et al . Model checking usage policies [C ] // Trustworthy Global Computing . 2009 : 19 - 35 .

ALESSANDRO C , EDMUND C , FAUSTO G , et al . NUSMV:a new symbolic model checker [J ] . STTT 2 , 2000 : 410 - 425

MCMILLAN K L . Symbolic model checking:an approach to the state explosion problem [M ] . Kluwer Academic , 1993 .

SZWED P , . Efficiency of formal verification of ArchiMate business processes with NuSMV model checker [C ] // Federated Conference on Computer Science and Information Systems (FedCSIS),Lodz . 2015 : 427 - 1436 .

XU N , MA Z , JIANG J , et al . Model checking instance based on NuSMV [C ] // IEEE SmartWorld,Ubiquitous Intelligence ＆ Computing,Advanced ＆ Trusted Computing,Scalable Computing ＆Communications,Cloud ＆ Big Data Computing,Internet of People and Smart City Innovation (SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI) . 2018 : 2052 - 2056 .

SEBASTIANI R , ROVERI Marco , PISTORE M , et al . NuSMV2:an open source tool for symbolic model checking [C ] // International Conference on Computer Aided Verification . 2002 .

HASAN SR , KAMHOUA CA , KWIAT KA , et al . Translating circuit behavior manifestations of hardware Trojans using model checkers into run-time Trojan detection monitors [C ] // IEEE Asian Hardware-Oriented Security and Trust (AsianHOST) . 2016 : 1 - 6 .

DESAI K , STEVENS K.S , O'LEARY J , et al . Symbolic verification of timed asynchronous hardware protocols [C ] // IEEE Computer Society Annual Symposium on VLSI (ISVLSI) . 2013 : 47 - 152 .

PAKONEN A , BUZHINSKY I . Verification of fault tolerant safety I＆C systems using model checking [C ] // International Conference on Industrial Technology . 2019 .

BEHRMANN G , DAVID A , LARSEN K G . A Tutorial on UPPAAL [C ] // Proc of Int school on Formal Methods for the Design of Computer Communication ＆ Software Systems . 2004 : 200 - 236 .

AAAMIR N , FAROOQUE A , AMJAD A , et al . Comparison of model checking tools using timed automata - PRISM and UPPAAL [C ] // IEEE International Conference on Computer and Communication Engineering Technology (CCET) . 2018 : 248 - 253 .

YAN X , LI Y , LI X . Real-time simulation of automotive systems based on UPPAAL [C ] // Proceedings of 2017 IEEE 8th International Conference on Software Engineering and Service Science . 2017 : 193 - 196 .

CHAUDHTY Y.A.K , HAMMED M . Formal verification of cloud based distributed System using UPPAAL [C ] // International Conference on Innovation and Intelligence for Informatics,Computing,and Technologies (3ICT) . 2019 : 1 - 4 .

YAN X , WANG L , CHE X , et al . Source code testing for automotive software based on UPPAAL model [C ] // IEEE International Conference on Software Engineering ＆ Service Science , 2014 : 95 - 98 .

LI H , LIU Q , ZHANG J , et al . A Survey of hardware Trojan detection,diagnosis and prevention [C ] // IEEE International Conference on Computer-aided Design ＆ Computer Graphics . 2016 .

HASAN S.R , KAMHOUA C.A , KWIAT K.A , et al . A novel framework to introduce hardware Trojan monitors using model checking based counterexamples:inspired by game theory [C ] // 2018 IEEE 61st International Midwest Symposium on Circuits and Systems (MWSCAS) . 2018 : 853 - 856 .

LODHI F K , ABBASI I H , KAMBOH A M , et al . Formal verification of gate-level multiple side channel parameters to detect hardware Trojans [C ] // Communications in Computer and Information Science . 2016 .

HAFEEZ A I , FAIQ K , OSMAN H , et al . McSeVIC:a model checking based framework for security vulnerability analysis of integrated circuits [J ] . IEEE Access ， 2018 ， 6 ： 1 .

RATHMAIR M , SCHUPFER F , KRIEG C . Applied formal methods for hardware Trojan detection [C ] // IEEE International Symposium on Circuits ＆ Systems . 2014 : 169 - 172 .

ZHANG Y , YU L , LI H , et al . Small Trojan testing using bounded model checking [C ] // IEEE International Test Conference . 2018 .

ZHAO J F , . Case study:discovering hardware Trojans based on model checking [C ] // The 8th International Conference . 2018 : 64 - 68 .

KRIEG C , RATHMAIR M , SCHUPFER F . A process for the detection of design-level hardware Trojans using verification methods [C ] // High Performance Computing ＆ Communications,IEEE Intl Symp on Cyberspace Safety ＆ Security,IEEE Intl Conf on Embedded Software ＆ Syst . 2015 .

高洪博 . 指令诱发型硬件木马检测技术研究 [D ] . 郑州:信息工程大学 , 2013 .

GAO H B . Research on detection techniques of instruction-triggered hardware Trojan horse [D ] . Zhengzhou:Information Engineering University , 2013 .

GAO H , LI Q , ZHU Y , et al . Code-controlled hardware Trojan horse [C ] // International Conference on Information Computing ＆Applications . 2012 : 171 - 178 .

HE J J , GUO X , MEADE T , et al . SoC interconnection protection through formal verification [J ] . Integration , 2019 , 64 : 143 - 151 .

RAJENDRAN J , DHANDAYUTHAPANY A M , VEDULA V , et al . Formal security verification of third party intellectual property cores for information leakage [C ] // IEEE International Conference on VLSI Design ＆ International Conference on Embedded Systems . 2016 : 547 - 552 .

CLARKE E M , KLIEBER W , MILO N , et al . Model checking and the state explosion problem [J ] . Lecture Notes in Computer Science , 2011 : 1 - 30 .

CRUZ J , FARAHMANDI F , AHMED A , et al . Hardware Trojan detection using ATPG and model checking [C ] // International Conference on Vlsi Design ＆ International Conference on Embedded Systems . 2018 : 91 - 96 .

Views

276

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Survey on generalized safety and security technology for system on wafer

Modeling and security analysis of hardware trojan attack based on GSCPN

Design and detection of hardware Trojan based on satisfiability don't cares

Research on hardware Trojan defense

Formal specification and security verification of usage control model based on PAT

Related Author

MEI Bo

CAO Zhipeng

SHEN Jianliang

GUO Wei

LI Peijie

ZHANG Wenbo

LI Peijie

CAO Zhipeng

Related Institution

Information Engineering University

School of Cybersecurity, Northwestern Polytechnical University

College of Informatics, Huazhong Agricultural University

⁰