Hardware Trojans detection through automatic properties extraction and formal verification

基于属性自动提取与形式化验证的硬件木马检测方法

School of Cybersecurity, Northwestern Polytechnical University, Xi'an 710072, China

Received: 26 August 2024

Abstract

To address the difficulties in obtaining golden reference models and the low accuracy when conducting pre-silicon hardware Trojans detection on a large-scale integrated circuit design, a formal detection method to quickly and accurately locate hardware Trojans is proposed in this paper. The hopping signals within each clock cycle are used as the object of analysis in integrated circuit functional traces, in which the candidate set of these signals is obtained by a traversal matching approach. The properties of the candidate set are excavated by utilizing the low flip signal feature to realize the automatic extraction of the hardware design functional properties. According to the counterexamples given by the verification results, the hardware Trojans related design can be quickly located through analysis and formal verification. The experimental results of some Trust-Hub AES benchmarks show that the proposed method can automatically extract the constant properties related to low-activity signals and successfully detect hardware Trojans. This study provides a fast and accurate solution of hardware Trojans detection on a large-scale integrated circuit design.

摘要

在大规模集成电路设计领域, 硅前硬件木马检测面临两大挑战: 缺乏黄金模型和检测准确率不足。研究旨在提出一种新的方法以提高集成电路设计中硬件木马的检测速度和准确性。该方法采用形式化分析, 将集成电路功能轨迹中每个时钟周期内信号的跳变作为分析焦点, 通过遍历匹配技术构建了候选信号集, 并利用低翻转信号的特性进行属性挖掘, 以实现硬件设计功能属性的自动提取。此外, 通过分析和形式化验证来执行硬件木马检测, 并利用验证结果中的反例来快速定位相关设计中的硬件木马。对Trust-Hub数据集的AES系列部分测试基准实验结果表明: 所提方法成功自动提取了与低活跃度信号相关的定常属性, 并有效地检测出了硬件木马。所提方法为大规模集成电路设计中的硬件木马检测提供了一种快速准确的解决方案。