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

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

网络与信息安全学报 ›› 2021, Vol. 7 ›› Issue (2): 57-63.doi: 10.11959/j.issn.2096-109x.2021029

• 专题：集成电路硬件安全 • 上一篇下一篇

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

张启智, 赵毅强, 高雅, 马浩诚

天津大学微电子学院，天津 300110

修回日期:2021-01-21 出版日期:2021-04-15 发布日期:2021-04-01
作者简介:张启智（1998- ），男，山东菏泽人，天津大学博士生，主要研究方向为集成电路设计与硬件形式化验证。
赵毅强（1964- ），男，河北辛集人，博士，天津大学教授、博士生导师，主要研究方向为集成电路安全、混合信号集成电路设计、光电检测与成像系统设计、传感器系统设计。
高雅（1998- ），女，辽宁东港人，天津大学硕士生，主要研究方向为数字电路安全。
马浩诚（1996- ），男，河北沧州人，天津大学博士生，主要研究方向为集成电路设计与硬件安全。
基金资助:
国家自然科学基金(61832018)

Survey on model checking based hardware Trojan detection technology

Qizhi ZHANG, Yiqiang ZHAO, Ya GAO, Haocheng MA

School of MicroElectronics, Tianjin University, Tianjin 300110, China

Revised:2021-01-21 Online:2021-04-15 Published:2021-04-01
Supported by:
The National Natural Science Foundation of China(61832018)

摘要/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

中图分类号:

TN407

张启智, 赵毅强, 高雅, 马浩诚. 基于模型检测的硬件木马检测技术研究[J]. 网络与信息安全学报, 2021, 7(2): 57-63.

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.

图/表 3

参考文献 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.

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

Survey on model checking based hardware Trojan detection technology

在线阅读

pdf下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 3

参考文献 32

相关文章 5

Metrics

推荐阅读 0

[1]	武玲娟, 朱嘉诚, 唐时博, 谭静, 胡伟. 基于可满足性无关项的硬件木马设计与检测[J]. 网络与信息安全学报, 2021, 7(2): 35-42.
[2]	唐永康, 胡星, 苏颋, 李少青. 用于硬件木马检测的电磁辐射分析方法研究[J]. 网络与信息安全学报, 2021, 7(2): 43-56.
[3]	王侃,陈浩,管旭光,顾勇. 硬件木马防护技术研究[J]. 网络与信息安全学报, 2017, 3(9): 1-12.
[4]	许强,蒋兴浩,姚立红,张志强,张诚. 硬件木马检测与防范研究综述[J]. 网络与信息安全学报, 2017, 3(4): 1-13.
[5]	周从华,陈伟鹤,刘志锋. 基于PAT的使用控制模型的形式化规约与安全性分析[J]. 网络与信息安全学报, 2016, 2(3): 52-67.