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

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

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

您当前的位置：

首页 >

文章列表页 >

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

专题：集成电路硬件安全 | 更新时间：2024-06-03

- 基于模型检测的硬件木马检测技术研究
- Survey on model checking based hardware Trojan detection technology
- 网络与信息安全学报 2021年7卷第2期页码：57-63
- 作者机构：
- 作者简介：
  
  [ "张启智（1998- ），男，山东菏泽人，天津大学博士生，主要研究方向为集成电路设计与硬件形式化验证。" ]
  [ "赵毅强（1964- ），男，河北辛集人，博士，天津大学教授、博士生导师，主要研究方向为集成电路安全、混合信号集成电路设计、光电检测与成像系统设计、传感器系统设计。" ]
  [ "高雅（1998- ），女，辽宁东港人，天津大学硕士生，主要研究方向为数字电路安全。" ]
  [ "马浩诚（1996- ），男，河北沧州人，天津大学博士生，主要研究方向为集成电路设计与硬件安全。" ]
- 基金信息：
  
  国家自然科学基金重点项目;The Key Program of National Natural Science Foundation of China(61832018)
- DOI：10.11959/j.issn.2096-109x.2021029
  中图分类号： TN407
- 网络首发：2021-04，
  
  纸质出版：2021-04-15
- 稿件说明：
移动端阅览
张启智, 赵毅强, 高雅, 等. 基于模型检测的硬件木马检测技术研究[J]. 网络与信息安全学报, 2021,7(2):57-63.

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.
张启智, 赵毅强, 高雅, 等. 基于模型检测的硬件木马检测技术研究[J]. 网络与信息安全学报, 2021,7(2):57-63. DOI： 10.11959/j.issn.2096-109x.2021029.

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 .

浏览量

276

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

晶上系统广义功能安全技术研究综述

基于GSCPN的硬件木马攻击建模与安全性分析

基于可满足性无关项的硬件木马设计与检测

硬件木马防护技术研究

基于PAT的使用控制模型的形式化规约与安全性分析