A Formal Approach to Identifying Hardware Trojans in Cryptographic Hardware
A Formal Approach to Identifying Hardware Trojans in Cryptographic Hardware
复制标题
识别加密硬件中硬件木马的正式方法
DOI：
10.1109/ismvl51352.2021.00034
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Homma Naofumi
中科院分区：
文献类型：
--
作者：
Ito Akira;Ueno Rei;Homma Naofumi
针对高级加密标准（AES）和椭圆曲线密码体制，提出了一种基于伽罗瓦域算法的检测和识别嵌入到密码硬件数据路径中的硬件木马的形式化方法。为了检测HT，我们的方法首先执行作为伽罗瓦域多项式（或加密硬件的参考电路）和多项式表示门级网表的输入输出关系的规范之间的等价性检查。我们的方法利用零抑制二元决策图进行有效的验证。一旦HT被发现，所提出的方法，然后检测HT的触发条件使用零抑制的二元决策图的特性。它还确定了HT定位使用一种新的计算机代数方法。我们的实验结果表明，所提出的方法可以验证网表，并确定HT触发条件和位置的233位乘法器通常用于椭圆曲线密码在1.8秒内。此外，我们表明，如果给定的参考电路，所提出的方法可以检测到一个现实的HT插入到整个高级加密标准的硬件，包括控制逻辑，在大约三秒钟。
This paper presents a new formal method for detecting and identifying hardware Trojans (HTs) inserted into the datapath of cryptographic hardware based on Galois-field arithmetic such as for the Advanced Encryption Standard and elliptic curve cryptography. To detect HTs, our method first performs equivalence checking between the specifications given as Galois-field polynomials (or the reference circuit of cryptographic hardware) and polynomials representing the input-output relations of a gate-level netlist. Our method exploits zero-suppressed binary decision diagrams for efficient verification. Once an HT is found, the proposed method then detects the trigger condition of the HT using the characteristics of zero-suppressed binary decision diagrams. It also identifies the HT localization using a novel computer algebra method. Our experimental results show that the proposed method can verify netlists and identify HT trigger conditions and locations on a 233-bit multiplier commonly used in elliptic curve cryptography within 1.8 seconds. In addition, we show that if the reference circuit is given, the proposed method can detect a realistic HT inserted into the entire Advanced Encryption Standard hardware, including control logic, in approximately three seconds.