基于模型检测的硬件木马检测技术研究

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

Abstract

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.

Key words: hardware Trojan, model checking, model establishing, property declaration

CLC Number:

TN407

Qizhi ZHANG, Yiqiang ZHAO, Ya GAO, Haocheng MA. Survey on model checking based hardware Trojan detection technology[J]. Chinese Journal of Network and Information Security, 2021, 7(2): 57-63.

Figures/Tables 3

References 32

[1]	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.
[2]	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.
[3]	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.
[4]	CLARKE E M , GRUMBERGO , PELED D ,et al. Model checking[M]. Cambridge: MIT press, 1999.
[5]	BARTOLETTI M , DEGANO P , FERRARI G L ,et al. Model checking usage policies[C]// Trustworthy Global Computing. 2009: 19-35.
[6]	ALESSANDRO C , EDMUND C , FAUSTO G ,et al. NUSMV:a new symbolic model checker[J]. STTT 2, 2000: 410-425
[7]	MCMILLAN K L . Symbolic model checking:an approach to the state explosion problem[M]. Kluwer Academic, 1993.
[8]	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.
[9]	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.
[10]	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.
[11]	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.
[12]	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.
[13]	PAKONEN A , BUZHINSKY I . Verification of fault tolerant safety I＆C systems using model checking[C]// International Conference on Industrial Technology. 2019.
[14]	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.
[15]	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.
[16]	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.
[17]	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.
[18]	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.
[19]	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.
[20]	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.
[21]	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.
[22]	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.
[23]	RATHMAIR M , SCHUPFER F , KRIEG C . Applied formal methods for hardware Trojan detection[C]// IEEE International Symposium on Circuits ＆ Systems. 2014: 169-172.
[24]	ZHANG Y , YU L , LI H ,et al. Small Trojan testing using bounded model checking[C]// IEEE International Test Conference. 2018.
[25]	ZHAO J F , . Case study:discovering hardware Trojans based on model checking[C]// The 8th International Conference. 2018: 64-68.
[26]	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.
[27]	高洪博 . 指令诱发型硬件木马检测技术研究[D]. 郑州:信息工程大学, 2013.
	GAO H B . Research on detection techniques of instruction-triggered hardware Trojan horse[D]. Zhengzhou:Information Engineering University, 2013.
[28]	GAO H , LI Q , ZHU Y ,et al. Code-controlled hardware Trojan horse[C]// International Conference on Information Computing ＆Applications. 2012: 171-178.
[29]	HE J J , GUO X , MEADE T ,et al. SoC interconnection protection through formal verification[J]. Integration, 2019,64: 143-151.
[30]	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.
[31]	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.
[32]	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.

Metrics

Recommended 0

No Suggested Reading articles found!

Survey on model checking based hardware Trojan detection technology

RichHTML

PDF下载

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 3

References 32

Related Articles 5

Metrics

Recommended 0

[1]	Lingjuan WU, Jiacheng ZHU, Shibo TANG, Jing TAN, Wei HU. Design and detection of hardware Trojan based on satisfiability don't cares [J]. Chinese Journal of Network and Information Security, 2021, 7(2): 35-42.
[2]	Yongkang TANG, Xing HU, Ting SU, Shaoqing LI. Research on electromagnetic radiation based side-channel analysis method for hardware Trojan detection [J]. Chinese Journal of Network and Information Security, 2021, 7(2): 43-56.
[3]	Kan WANG,Hao CHEN,Xu-guang GUAN,Yong GU. Research on hardware Trojan defense [J]. Chinese Journal of Network and Information Security, 2017, 3(9): 1-12.
[4]	Qiang XU,Xing-hao JIANG,Li-hong YAO,Zhi-qiang ZHANG,Cheng ZHANG. Overview of the detection and prevention study of hardware Trojans [J]. Chinese Journal of Network and Information Security, 2017, 3(4): 1-13.
[5]	Cong-hua ZHOU,Wei-he CHEN,Zhi-feng LIU. Formal specification and security verification of usage control model based on PAT [J]. Chinese Journal of Network and Information Security, 2016, 2(3): 52-67.