Hardware Trojans detection through automatic properties extraction and formal verification

Xiaojie DAI; Mengni CHENG; Jiacheng ZHU; Yu TAI

doi:10.1051/jnwpu/20254340813

All issues

Volume 43 / No 4 (August 2025)

JNWPU, 43 4 (2025) 813-820

Full HTML

Open Access

Issue		JNWPU Volume 43, Number 4, August 2025


Page(s)		813 - 820
DOI		https://doi.org/10.1051/jnwpu/20254340813
Published online		08 October 2025

JNWPU 2025, 43(4): 813–820

Hardware Trojans detection through automatic properties extraction and formal verification

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

Xiaojie DAI (戴晓洁), Mengni CHENG (程梦妮), Jiacheng ZHU (朱嘉诚) and Yu TAI (邰瑜)

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系列部分测试基准实验结果表明: 所提方法成功自动提取了与低活跃度信号相关的定常属性, 并有效地检测出了硬件木马。所提方法为大规模集成电路设计中的硬件木马检测提供了一种快速准确的解决方案。

Key words: hardware design / property extraction / formal verification / hardware Trojans detection

关键字 : 硬件设计 / 属性提取 / 形式化验证 / 硬件木马检测

This is an Open Access article distributed under the terms of the Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

随着半导体供应链的全球化, 为节约开发成本和时间, 现代计算系统通常集成了来自不同安全等级供应商的电路设计, 特别是来自不可信第三方的知识产权(intellectual property, IP)核, 这些互联互通的计算资源的硬件组件构成了一个混合信任的硬件电路计算环境。硬件木马是硬件电路在设计和生产过程中可能发生的恶意设计修改, 会导致电路功能异常、制造后门允许远程操控和破坏等问题[1]。例如, 2012年在军用级FPGA的ProASIC3芯片中发现了未记录的硬件木马[2], 该木马通过提取密钥, 使攻击者能够修改芯片的配置, 从而完全控制芯片。与芯片设计制造流程相对应, 硬件木马检测技术可以分为硅前检测和硅后检测。随着集成电路集成度的不断提高以及设计规模的不断增大, 硬件设计硅后检测也越来越艰难, 一方面设计验证需要的代价太大; 另一方面测试和验证方法的局限性导致其覆盖率难以保证。因此系统中往往存在未被发现的漏洞, 只有在造成重大损失后才会被发现, 带来了巨大的安全风险。因此在硅前设计阶段对硬件设计进行安全性检测是十分必要的[3]。2016年美国国家自然科学基金委(national science foundation, NSF)形式化安全方法研讨会报告指出：形式化验证是计算机系统达到安全和保密需求的唯一可靠途径，其中可验证的底层硬件安全机制是软件安全的基础[4]。因此, 如何应用形式化的方法快速准确地定位到硬件木马是一个值得深入研究的课题。

近年发展起来的基于属性检查的形式化验证是一种静态的硬件设计验证方式, 旨在通过工具从逻辑上检查设计文件是否满足某种属性, 相对于逻辑仿真验证硬件设计, 形式化验证可以极大缩短验证时间[5]。基于信息流追踪[6–7]的形式化验证方法可以检测出违反机密性、安全性以及隔离特性等安全属性的恶意逻辑, 为硬件设计脆弱性检测提供了一种新的思路。Guo等[8]研究了硬件信任评估中常用的两大类形式化方法: 定理证明和等价验证, 并从形式化视角概述了符号代数在等价验证中的使用。进一步, 该团队提出了一种新的分层形式化验证框架用于硅前阶段的电路信任评估[9], 通过形式化验证8051微处理器上的内存完整性属性证明所提出框架的适用性。Farzana等[10]描述了一种属性驱动的形式化方法用于设计安全的SoC, 并证明了该方法在不同威胁模型下的有效性, 将形式化方法融入SoC设计流程, 从设计端增强安全性。

很多学者重点研究了集成电路设计的属性自动提取, 并利用属性进行形式化验证。Vasudevan等[11]通过Goldmine工具静态分析与决策树自动提取断言语句, 利用一种形式化引擎验证断言语句的有效性。Danese等[12]提出了一种数据挖掘与覆盖率分析相结合的方法, 提取形式如G(φ→ψ)的时序断言。Ghasempouri等[13]提出了基于度量标准评估规范的列联表相关性及“兴趣性”挖掘技术, 能够对获得的断言进行排序。Malburg等[14]阐述了一种通过图的构建来遍历动态依赖图从而推断时序属性的方法。这些研究在安全属性方面有所欠缺。Garcia等[15]通过对硬件规范的挖掘来自动生成硬件设计属性, 该属性可以与基于断言的验证技术一起使用, 但仅限于在单个执行跟踪上评估的属性[16], 无法显示信息流从特定源流向特定接收器。Smith等[17]利用函数语言开展安全属性自动提取, 然而该方法无法在时序上对安全属性进行挖掘, 若对该方法进行时间属性的扩展会导致性能低下。Bauer等[18]建立了基于LTL(linear temporal logic)三值语义的属性提取框架, 时刻监视硬件设计行为来提取一个不确定的结果, 无法对确定的属性进行提取。工具方面, IODINE结合静态分析与动态跟踪方法来自动查找例如信号互斥或One-hot编码行为的作为属性实例[19]。Zhang等[20]采用机器学习方法自动提取硬件设计的关键安全属性, 包含通过对已知漏洞进行训练获取未知漏洞和通过已知安全属性的训练提取更多的属性。Isadora工具能够完成由跟踪属性到信息流安全属性的提取。与在多个跟踪轨迹定义的行为规范不同, 规范挖掘是在执行单个跟踪定义的行为模式中进行发掘, 所以只适用于对跟踪属性的提取。Deutschbein等[21]在工具设计中加入了信息流跟踪逻辑, 把安全规范应用到工具结构中, 能够提取信息流信息。然而这些工具仍处于研究阶段, 距离应用还存在一定差距, 自动提取出的属性大多无法兼备硬件设计的功能与安全性, 仍需要人工书写验证属性, 当系统规模大或结构复杂时, 属性的定义和验证会变得更为复杂, 无法保证属性的完备性。

硬件木马检测技术代表性的方法有逻辑测试、形式验证、代码分析和机器学习方法[22]。由于芯片结构日益复杂, 获取“黄金模型(经验证没有硬件木马植入的电路)”已经非常困难, 需要黄金模型的方式具有很大的局限性[23]。在大规模系统上应用神经网络进行分析可能会面临计算资源和时间的挑战。通过手动的代码分析、逻辑验证等硬件木马检测方式非常耗时。因此，如何自动提取硬件电路设计属性中与木马相关的属性, 并根据形式化验证结果来判别是否存在木马, 对大规模电路设计的硬件木马检测具有实用意义。

1 硬件木马检测方法

本文提出了一种基于属性自动提取与形式化验证的硬件木马检测方法。首先利用仿真工具获得硬件设计电路中每个信号的仿真轨迹数据; 接着对轨迹数据采用遍历查找算法找出符合特性的属性信号, 实现集成电路定常属性的自动提取; 然后进一步缩小需要提取属性的设计规模, 方便电路设计及检测人员进行人工分析, 通过人工分析对查找到的属性信号进行判别, 将有效属性作为形式化验证的电路验证语句; 同时采用形式化验证工具对检测出的有效属性进行验证, 根据验证结果定位属性关联的设计语句, 可以检测硬件木马, 并获取木马触发条件。硬件木马检测过程如图 1所示。

图1

硬件木马检测过程

2 属性自动提取方法

2.1 数字电路低翻转信号特性

数字电路可以分为组合逻辑和时序逻辑2种, 组合逻辑由逻辑门组成, 其输出仅取决于当前的输入。时序逻辑包括时钟和存储元件, 具有时序性, 任意时刻的输出信号不仅取决于当时的输入信号, 而且还取决于电路原来的状态。低触发信号是指在数字电路仿真信号观测值中存在明显断崖式概率分布的信号集合, 以单比特信号为例，它的取值为低(高)的概率无限接近于零，而取值为高(低)的概率接近于1，即低触发信号的取值状态极少或者永不产生跳变, 当信号发生跳变时, 它的熵值会增加, 即信号翻转时会以某种方式传递更多的信息。例如在硬件设计源代码中嵌入一个恶意逻辑, 当明文输入为特定值时, 该逻辑可以泄露密钥到输出端口, 该特定值出现概率极低, 在有限的测试周期中很难测到其跳变情况。

2.2 定常属性

集成电路属性是集成电路设计行为的形式化或有关设计规范的约束。定常属性是对始终成立的硬件设计不变行为进行建模, 例如, 安全策略通常希望加密算法核完成加密的时间或者功率恒定, 以防止信息从时间或能量侧信道泄露。硬件电路设计在不同输入条件下表现出的行为应该不变, 检测人员可以将集成电路设计的不变特性形式化表述为定常属性。常量值和常量时间都属于定常属性。

2.3 定常属性的提取算法

利用定常属性的不变特性, 可以将其看做极低概率发生变化的事件, 对电路设计中仿真获得的所有信号进行遍历, 对其中不发生翻转的信号进行标记, 由于仿真受限于时间和规模, 短时间不发生变化的信号长时间可能发生变化, 但长时间不发生变化的信号在短时间内一定不会发生变化, 据此可以得出, 从仿真数据里得到的不翻转信号一定包含了电路设计的定常属性。

基于上面判断, 可以通过遍历查找电路轨迹里的不翻转信号来挖掘定常属性, 算法具体描述为: 首先判断字符串的起始位是否为地址符‘/’, 末尾的信号值不能为不定态‘x’或者高阻态‘z’, 如果满足上述条件则将该信号加入到数据链表中, 否则继续判断下一条字符串, 直到整个仿真信号集都被加入到数据链表之中。接下来判断数据链表之中的每个信号是否有过翻转行为。

创建一个指向链表头部的指针cur, 令其指向第一个信号节点, 创建另一个同样指向链表头部的指针pre, 在cur指针指向每一个信号的过程中, pre指针不断往后搜索。当出现cur指针与pre指针所指向的节点处信号名称相同的情况时, 搜索中止并判断2个节点的信号值是否相等, 如果不相等则将该节点的翻转标志位sig赋值为1, 表示该信号在仿真过程中至少经过了1次翻转。对于每一个链表中的信号都重复上述过程, 通过遍历链表来查看每一个信号值在仿真过程中是否发生翻转。最后在标记阶段完成后, 搜索整个链表提取出节点标志位sig为0的信号及其取值作为低翻转信号集。提取算法如下所示。

算法1 低翻转信号提取算法

1: 输入: AES-T1000仿真数据集

2: 输出: 低翻转信号集合

3: define biaoji: //翻转标记函数

4: while cur is not None do//当前节点不为空

5: while pre is not None do//下一节点不为空

6: if cur!=pre do//如果信号数值不等

7: cur.sig←1//设置翻转位为1

8: pre←pre.next//分析下一节点

9: cur←cur.next//分析下一节点

10: define tiqu(self, difan): //低翻转信号提取函数

11: while cur is not None do//当前节点不为空

12: if cur.sig==0 do//如果该节点标志位为0

13: difan← cur//将该信号加入到低翻转信号数组中

14: cur ← cur.next//分析下一节点

3 形式化验证方法

形式化验证技术是一种基于数理逻辑论证方法检验系统是否满足给定安全规范的方法[24]。该方法采用规范化的语法语义去定义系统以及系统应该满足的属性, 再进行人工或自动化的推理论证, 最终可以给出系统关于给定属性的安全性或正确性结论。与软件测试这种保障软件安全的方法不同, 形式化验证是用推理论证的方法“证明”软件不存在某种安全漏洞, 而不是采用用例覆盖的方法去“检测”漏洞的存在性, 因此形式化方法可以从根本上保证系统的安全性。在建立形式化规范与系统模型后, 需要采用形式化验证器进行辅助验证, 如交互式定理证明器、行为监测引擎等。

Yosys是基于Verilog RTL的开源逻辑综合和验证工具, 可以处理任何可综合的Verilog设计[24–26], 可以将Verilog设计通过逻辑综合转换为门级网表, 并集成了SAT验证工具, 用于实现功能和安全属性的形式化验证。

图 2为典型属性形式化验证流程。首先使用属性描述语言以断言的形式描述需验证的属性, 可以将断言语句直接嵌入原始逻辑中, 然后将属性中的断言语句转换为证明约束, 使用形式化求解器在证明约束下验证集成电路设计是否满足断言。若不满足断言则验证失败, 提供一个反例, 可用于违反策略的逻辑复现; 若满足断言, 则验证成功。

图2

形式化验证流程图

4 实验结果及分析

4.1 仿真测试环境

实验环境配置如表 1所示。实验中各个模块程序主要采用Python编写, 实验采用开源电路综合优化工具软件Yosys, 安装在虚拟机的Ubuntu 18.04.1操作系统中, 内置SAT求解器用于测试基准形式化安全验证。测试数据由ModelSim SE-64 10.4生成。

表1

实验环境配置

4.2 定常属性提取和分析

通过ModelSim对AES-T1000基准进行轨迹仿真, 获得包含时钟信号、复位信号、明密文和密钥信号在内的信号数据集作为输入信号数据, 部分仿真波形如图 3所示。

在Visual Studio Code软件中执行算法1所示的算法过程, 从6万条AES-T1000仿真轨迹数据中提取到的6条低翻转信号集如表 2所示。

对实验提取出的6个低翻转信号进行分析: 信号Capacitance是信号load在TOP级模块实例化中的别名, 所以两者等价即信号值相等, 本实验中一直为0表示木马在仿真周期内未被触发。表 2中后3个信号是木马触发信号Tj_Trig在不同级别模块中的展示, 可视为同一信号, 表示木马未被触发。从而得到该硬件电路的定常属性为: 断言木马触发信号Tj_Trig始终保持为0, 断言木马的负载输出信号Capacitance与信号load始终保持为0, 可通过属性描述语言表达如下:

1: set rst: =0

2: assert Tj_Trig==0

图3

AES-T1000仿真波形(部分)

表2

低翻转信号集

4.3 收敛速度仿真

从算法过程分析, 低翻转信号个数应该是随仿真时间收敛的, 为了观察具体规律, 本文分别选择AES-T1000基准和RSA-T300基准设计内的2个模块进行仿真。

AES-T1000设计中TOP模块是顶层模块, TSC模块是该设计中木马的负载模块, 仿真结果如图 4所示, 可以看到2个模块的低翻转信号个数分别从451和279逐渐收敛到个位数, 在仿真初期收敛速度较快, 随着仿真时间的增加收敛速度明显放缓。TOP模块的低翻转信号提取结果最终收敛为木马触发信号Tj_Trig, TSC模块最终收敛为木马的负载信号load和触发信号Tj_Trig。

在RSA-T300设计中, 选择RSACypher和Modmult模块进行分析, 仿真结果如图 5所示, 可以看到RSACypher模块在仿真时间超过600个时钟周期后, 低翻转信号个数从147收敛为38。在检查低翻转信号集合与原始设计后, 38个信号中7个为使能信号TjEnable, 30个为木马触发计数信号TrojanCounter, 1个eqOp信号为触发信号。Modmult模块在经过200个时钟周期的仿真后, 低翻转信号个数快速下降到5并保持不变。检查这5个信号的原始设计, 发现这5个信号均为第33位信号, 该设计为32位密码核, 第33位信号始终未使用, 所以未发生反转。

从图 4~5仿真结果可以看出硬件设计内的低翻转信号个数整体上具有随时间逐渐收敛的趋势, 一般在仿真初期收敛速度较快, 随着仿真时间的增加收敛速度明显放缓。

图4

AES-T1000低翻转信号个数随仿真时间变化情况(单个周期为10 ns)

图5

RSA-T300低翻转信号个数随仿真时间变化情况(单个周期为10 ns)

4.4 形式化验证结果及分析

本文中主要通过Verilog断言语句以及形式化验证工具Yosys对集成电路属性进行形式化验证。验证前使用Yosys工具将包含Tj_Trig信号的Trojan_Trigger模块RTL级代码转换为门级, 生成门级网表文件GATELEVEL.v。具体脚本指令如下:

1: read_verilog Trojan_Trigger.v

2: hierarchy-check

3: proc; opt; fsm; memory; opt

4: write_verilog GATELEVEL.v

仿真需要证明在不复位的前提下, 低翻转信号Tj_Trig是否始终保持为0。具体安全约束脚本指令如下, 第一条指令读入设计文件, 第二条指令调用SAT工具并设置约束:

1: read_verilog GATELEVEL.v

2: sat-prove Tj_Trig 1′b0-set \rst 0

验证结束, SAT求解器形式化验证失败并给出一个反例(如图 6~7所示), AES-T1000返回的信号表明, 当满足state为特定值时, 低翻转信号Tj_Trig的逻辑值将会翻转为逻辑1。RSA-T300返回的信号表明, 只有第二位为1, 其他位均为0时, 木马触发, 与RSA-T300测试向量中木马设计触发条件完全一致。

通过观察图 6~7中的反例可以看出: 当输入明文为特定值时, Tj_Trig信号会跳变为逻辑1, 在原始代码中进行追溯可以发现该信号为木马触发信号, 当信号逻辑为1时会触发负载以泄露密钥; 当计数器触发条件时, 即TrojanCounter第二位为1时, 木马被触发。实验结果表明, 本方法可以精确捕捉、定位与木马相关的触发信号或相关单元。

现有FANCI、VeriTrust和GLIFT 3种当前广泛使用的安全验证方法需要设计者重新建模, 设计验证框架, 个别验证规模有限。表 3总结了4种方法针对Trust-Hub数据集部分木马测试基准的检测结果, 本文方法从信息流的角度研究集成电路安全验证与木马检测方法, 在门级网表的基础上描述信息流和标签的传播, 无需设计者引入新的模型或框架, 同样能够达到木马检测效果, 相比GLIFT在适用范围方面具有一定优势, 可以实现对多种功能不同的硬件设计的木马检测。

图6

AES-T1000属性形式化验证结果

图7

RSA-T300属性形式化验证结果

表3

硬件木马检测结果对比

5 结论

本文提出了一种基于属性自动提取与形式化验证的硬件木马检测方法, 以低翻转信号特性为基础开展定常功能属性的自动提取, 提取仿真轨迹中始终不变的信号, 将其作为定常属性, 采用Yosys验证工具读取集成电路RTL级代码设计, 通过将自动提取出的定常属性转化为相应约束的方式, 利用布尔可满足性分析的方法, 对其进行形式化验证, 如果验证失败, 可以返回1个反例, 对反例进行分析可以发现是硬件木马触发条件。本文方法能够帮助测试人员缩小需要提取属性的规模, 快速识别、定位集成电路设计中的木马。

References

FENG Yan, CHEN Lan. Hardware trojan detection based on path feature and support vector machine[J]. Journal of Electronics & Information Technology, 2023, 45(6): 1921–1932 (in Chinese) [Google Scholar]
TAMZIDUL H, JONATHAN C, PRABUDDHA C, et al. Hardware IP trust validation: learn (the untrustworthy), and verify[C]//IEEE International Test Conference, New York, 2018: 1–10 [Google Scholar]
CHEN Xingren, XIONG Yan, HUANG Wenchao, et al. A multi-view hardware Trojan detection method based on static analysis[J]. Netinfo Security, 2023, 23(10): 48–57 (in Chinese) [Google Scholar]
CHONG S, GUTTMAN J, DATTA A, et al. Report on the NSF workshop on formal methodsforsecurity[EB/OL]. (2016-08-03)[2024-07-25]. [Article] [Google Scholar]
MOEBIUS N, STENZEL K, REIF W. Formal verification of application-specific security properties in a model-driven approach[C]//International Symposium on Engineering Secure Software and Systems, Berlin, 2010: 166–181 [Google Scholar]
HU W, ARDESHIRICHAM A, KASTNER R. Hardware information flow tracking[J]. ACM Computing Surveys, 2021, 54(4): 1–39 [Google Scholar]
ARDESHIRICHAM A, HU W, MARXEN J, et al. Register transfer level information flow tracking for provably secure hardware design[C]//Design, Automation & Test in Europe Conference & Exhibition, 2017: 1691–1696 [Google Scholar]
GUO X, DUTTA R G, JIN Y, et al. Pre-silicon security verification and validation: a formal perspective[C]//2015 52nd ACM/EDAC/IEEE Design Automation Conference, San Francisco, 2015: 1–6 [Google Scholar]
GUO X, DUTTA R G, JIN Y. Hierarchy-preserving formal verification methods for pre-silicon security assurance[C]//2015 16th International Workshop on Microprocessor and SoC Test and Verification, Austin, 2015: 48–53 [Google Scholar]
FARZANA N, RAHMAN F, TEHRANIPOOR M, et al. SoC security verification using property checking[C]//2019 IEEE International Test Conference, Washington, 2019: 1–10 [Google Scholar]
VASUDEVAN S, SHERIDAN D, PATEL S, et al. Goldmine: automatic assertion generation using data mining and static analysis[C]//2010 Design, Automation & Test in Europe Conference & Exhibition, 2010: 626–629 [Google Scholar]
DANESE A, RIVA N D, PRAVADELLI G. A-team: automatic template-based assertion miner[C]//Proceedings of the 54th Annual Design Automation Conference, 2017: 1–6 [Google Scholar]
GHASEMPOURI T, PRAVADELLI G. On the estimation of assertion interestingness[C]//2015 IFIP/IEEE International Conference on Very Large Scale Integration, 2015: 325–330 [Google Scholar]
MALBURG J, FLENKER T, FEY G. Property mining using dynamic dependency graphs[C]//2017 22nd Asia and South Pacific Design Automation Conference, 2017: 244–250 [Google Scholar]
GARCIA F, OSWALD D, KASPER T, et al. Lock it and still lose it: on the(in)security of automotive remote keyless entry systems[C]//Proceedings of the 25th USENIX Security Symposium, 2016: 929–944 [Google Scholar]
KOZYRI E, CHONG S, MYERS A C. Expressing information flow properties[J]. Foundations and Trends in Privacy and Security, 2022, 3(1): 1–102. [Article] [Google Scholar]
SMITH C, FERNS G, ALBARGHOUTHI A. Discovering relational specifications[C]//Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017: 616–626 [Google Scholar]
BAUER A, LEUCKER M, SCHALLHART C. Monitoring of real-time properties[C]//Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 2006 [Google Scholar]
HANGAL S, NARAYANAN S, CHANDRA N, et al. IODINE: a tool to automatically infer dynamic invariants for hardware designs[C]//2005 42nd ACM/IEEE Design Automation Conference, Anaheim, 2005: 775–778 [Google Scholar]
ZHANG R, STANLEY N, GRIGGS C, et al. Identifying security critical properties for the dynamic verification of a processor[J]. ACM SIGARCH Computer Architecture News, 2017, 45(1): 541–554. [Article] [Google Scholar]
DEUTSCHBEIN C, MEZA A, RESTUCCIA F, et al. Toward hardware security property generation at scale[J]. IEEE Security & Privacy, 2022, 20(3): 43–51 [Google Scholar]
HUANG Zhao, WANG Quan, YANG Pengfei. Hardware Trojan: research progress and new trends on key problems[J]. Chinese Journal of Computers, 2019, 42(5): 993–1017 (in Chinese) [Google Scholar]
SHI Jiangyi, WEN Cong, LIU Hongjin, et al. Hardware Trojan detection for gate-level netlists based on graph neural network[J]. Journal of Electronics & Information Technology, 2023, 45(9): 3253–3262 (in Chinese) [Google Scholar]
SRI D B, RAJAKUMAR K, MADHUSOODHANAN P, et al. A holistic approach to CPU verification using formal techniques[C]//2022 IEEE Women in Technology Conference, 2022: 1–5 [Google Scholar]
SHAH D, HUNG E, WOLF C, et al. Yosys+nextpnr: an open source framework from verilog to bitstream for commercial fpgas[C]//2019 IEEE 27th Annual International Symposium on Field-Programmable Custom Computing Machines, 2019: 1–4 [Google Scholar]
CHEN Chunlei, WANG Xingxin, TAN Jing, et al. Hardware information flow security verification and vulnerability detection using Yosys[J]. Application Research of Computers, 2021, 38(6): 1865–1869 (in Chinese) [Google Scholar]

All Tables

实验环境配置

低翻转信号集

硬件木马检测结果对比

All Figures

	图1 硬件木马检测过程
In the text

	图2 形式化验证流程图
In the text

	图3 AES-T1000仿真波形(部分)
In the text

	图4 AES-T1000低翻转信号个数随仿真时间变化情况(单个周期为10 ns)
In the text

	图5 RSA-T300低翻转信号个数随仿真时间变化情况(单个周期为10 ns)
In the text

	图6 AES-T1000属性形式化验证结果
In the text

	图7 RSA-T300属性形式化验证结果
In the text

Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.

Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.

Initial download of the metrics may take a while.

[1] FENG Yan, CHEN Lan. Hardware trojan detection based on path feature and support vector machine[J]. Journal of Electronics & Information Technology, 2023, 45(6): 1921–1932 (in Chinese) [Google Scholar]

[2] TAMZIDUL H, JONATHAN C, PRABUDDHA C, et al. Hardware IP trust validation: learn (the untrustworthy), and verify[C]//IEEE International Test Conference, New York, 2018: 1–10 [Google Scholar]

[3] CHEN Xingren, XIONG Yan, HUANG Wenchao, et al. A multi-view hardware Trojan detection method based on static analysis[J]. Netinfo Security, 2023, 23(10): 48–57 (in Chinese) [Google Scholar]

[4] CHONG S, GUTTMAN J, DATTA A, et al. Report on the NSF workshop on formal methodsforsecurity[EB/OL]. (2016-08-03)[2024-07-25]. [Article] [Google Scholar]

[5] MOEBIUS N, STENZEL K, REIF W. Formal verification of application-specific security properties in a model-driven approach[C]//International Symposium on Engineering Secure Software and Systems, Berlin, 2010: 166–181 [Google Scholar]

[6] HU W, ARDESHIRICHAM A, KASTNER R. Hardware information flow tracking[J]. ACM Computing Surveys, 2021, 54(4): 1–39 [Google Scholar]

[7] ARDESHIRICHAM A, HU W, MARXEN J, et al. Register transfer level information flow tracking for provably secure hardware design[C]//Design, Automation & Test in Europe Conference & Exhibition, 2017: 1691–1696 [Google Scholar]

[8] GUO X, DUTTA R G, JIN Y, et al. Pre-silicon security verification and validation: a formal perspective[C]//2015 52nd ACM/EDAC/IEEE Design Automation Conference, San Francisco, 2015: 1–6 [Google Scholar]

[9] GUO X, DUTTA R G, JIN Y. Hierarchy-preserving formal verification methods for pre-silicon security assurance[C]//2015 16th International Workshop on Microprocessor and SoC Test and Verification, Austin, 2015: 48–53 [Google Scholar]

[10] FARZANA N, RAHMAN F, TEHRANIPOOR M, et al. SoC security verification using property checking[C]//2019 IEEE International Test Conference, Washington, 2019: 1–10 [Google Scholar]

[11] VASUDEVAN S, SHERIDAN D, PATEL S, et al. Goldmine: automatic assertion generation using data mining and static analysis[C]//2010 Design, Automation & Test in Europe Conference & Exhibition, 2010: 626–629 [Google Scholar]

[12] DANESE A, RIVA N D, PRAVADELLI G. A-team: automatic template-based assertion miner[C]//Proceedings of the 54th Annual Design Automation Conference, 2017: 1–6 [Google Scholar]

[13] GHASEMPOURI T, PRAVADELLI G. On the estimation of assertion interestingness[C]//2015 IFIP/IEEE International Conference on Very Large Scale Integration, 2015: 325–330 [Google Scholar]

[14] MALBURG J, FLENKER T, FEY G. Property mining using dynamic dependency graphs[C]//2017 22nd Asia and South Pacific Design Automation Conference, 2017: 244–250 [Google Scholar]

[15] GARCIA F, OSWALD D, KASPER T, et al. Lock it and still lose it: on the(in)security of automotive remote keyless entry systems[C]//Proceedings of the 25th USENIX Security Symposium, 2016: 929–944 [Google Scholar]

[16] KOZYRI E, CHONG S, MYERS A C. Expressing information flow properties[J]. Foundations and Trends in Privacy and Security, 2022, 3(1): 1–102. [Article] [Google Scholar]

[17] SMITH C, FERNS G, ALBARGHOUTHI A. Discovering relational specifications[C]//Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017: 616–626 [Google Scholar]

[18] BAUER A, LEUCKER M, SCHALLHART C. Monitoring of real-time properties[C]//Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 2006 [Google Scholar]

[19] HANGAL S, NARAYANAN S, CHANDRA N, et al. IODINE: a tool to automatically infer dynamic invariants for hardware designs[C]//2005 42nd ACM/IEEE Design Automation Conference, Anaheim, 2005: 775–778 [Google Scholar]

[20] ZHANG R, STANLEY N, GRIGGS C, et al. Identifying security critical properties for the dynamic verification of a processor[J]. ACM SIGARCH Computer Architecture News, 2017, 45(1): 541–554. [Article] [Google Scholar]

[21] DEUTSCHBEIN C, MEZA A, RESTUCCIA F, et al. Toward hardware security property generation at scale[J]. IEEE Security & Privacy, 2022, 20(3): 43–51 [Google Scholar]

[22] HUANG Zhao, WANG Quan, YANG Pengfei. Hardware Trojan: research progress and new trends on key problems[J]. Chinese Journal of Computers, 2019, 42(5): 993–1017 (in Chinese) [Google Scholar]

[23] SHI Jiangyi, WEN Cong, LIU Hongjin, et al. Hardware Trojan detection for gate-level netlists based on graph neural network[J]. Journal of Electronics & Information Technology, 2023, 45(9): 3253–3262 (in Chinese) [Google Scholar]

[24] SRI D B, RAJAKUMAR K, MADHUSOODHANAN P, et al. A holistic approach to CPU verification using formal techniques[C]//2022 IEEE Women in Technology Conference, 2022: 1–5 [Google Scholar]

[25] SHAH D, HUNG E, WOLF C, et al. Yosys+nextpnr: an open source framework from verilog to bitstream for commercial fpgas[C]//2019 IEEE 27th Annual International Symposium on Field-Programmable Custom Computing Machines, 2019: 1–4 [Google Scholar]

[26] CHEN Chunlei, WANG Xingxin, TAN Jing, et al. Hardware information flow security verification and vulnerability detection using Yosys[J]. Application Research of Computers, 2021, 38(6): 1865–1869 (in Chinese) [Google Scholar]