摘要
硬件木马对原始电路的恶意篡改,已成为集成电路面临的核心安全威胁。为了保障集成电路的安全可信,研究人员提出了诸多硬件木马检测方法。其中,模型检测作为一种形式化验证方法,在设计阶段可有效检测出硬件木马。首先,阐述了模型检测的工作原理和应用流程;其次,介绍了基于模型检测的硬件木马检测技术的研究进展;最后,指出了当前该技术所面临的瓶颈,并讨论了潜在的研究方向。
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.
作者
张启智
赵毅强
高雅
马浩诚
ZHANG Qizhi;ZHAO Yiqiang;GAO Ya;MA Haocheng(School of MicroElectronics,Tianjin University,Tianjin 300110,China)
出处
《网络与信息安全学报》
2021年第2期57-63,共7页
Chinese Journal of Network and Information Security
基金
国家自然科学基金(61832018)。
关键词
硬件木马
模型检测
模型构建
属性声明
hardware Trojan
model checking
model establishing
property declaration
