A Symbolic Approach to Detecting Hardware Trojans Triggered by Don’t Care Transitions
A Symbolic Approach to Detecting Hardware Trojans Triggered by Don’t Care Transitions
复制标题
DOI：
10.1145/3558392
复制
发表时间：
2021-11
影响因子：
1.4
通讯作者：
Ruochen Dai;Tuba Yavuz
中科院分区：
文献类型：
--
作者：
Ruochen Dai;Tuba Yavuz
由于集成电路供应链的全球化，硬件特洛伊木马和可以触发它们的攻击已成为一个重要的安全问题。在本文中，我们提出了一种象征性的方法来检测过渡，我们的检测方法在寄存器转移级别（RTL）和门级都不需要。在第一阶段，它在第二阶段进行了探索。过渡。第二阶段都可以预测触发木马，并且在第三阶段不关心意识分析。过渡探索特洛伊木马有效载荷，并在第一阶段观察到的行为差异。明显的是，我们表明，必须在登机级级别（即进行合成之后）检测到的过渡和特洛伊木马，但要在特定的条件下进行。在RTL上更有效地进行，我们的方法的模块化设计也提供了快速的Trojan预测方法，即trusthub和使用两个合成工具生成的栅极级表示，Yosys和摘要设计编译器（SDC），表明我们的方法既有效（最多10×速度速度W.R.T.无修剪）和精度（RTL和RTL和RTL和fromperives均为0％的误报登机水平的网表）在检测到过渡和利用它们的特洛伊木马时，总分析时间可以达到1.62×（使用Yosys）和1.92×（使用SDC）加速时，当合成保留FSM结构时铸造厂是值得信赖的，木马检测是在RTL上进行的。
Due to the globalization of Integrated Circuit supply chain, hardware Trojans and the attacks that can trigger them have become an important security issue. One type of hardware Trojans leverages the “don’t care transitions” in Finite-state Machines (FSMs) of hardware designs. In this article, we present a symbolic approach to detecting don’t care transitions and the hidden Trojans. Our detection approach works at both register-transfer level (RTL) and gate level, does not require a golden design, and works in three stages. In the first stage, it explores the reachable states. In the second stage, it performs an approximate analysis to find the don’t care transitions and any discrepancies in the register values or output lines due to don’t care transitions. The second stage can be used for both predicting don’t care triggered Trojans and for guiding don’t care aware reachability analysis. In the third stage, it performs a state-space exploration from reachable states that have incoming don’t care transitions to explore the Trojan payload and to find behavioral discrepancies with respect to what has been observed in the first stage. We also present a pruning technique based on the reachability of FSM states. We present a methodology that leverages both RTL and gate-level for soundness and efficiency. Specifically, we show that don’t care transitions and Trojans that leverage them must be detected at the gate-level, i.e., after synthesis has been performed, for soundness. However, under specific conditions, Trojan payload exploration can be performed more efficiently at RTL. Additionally, the modular design of our approach also provides a fast Trojan prediction method even at the gate level when the reachable states of the FSM is known a priori. Evaluation of our approach on a set of benchmarks from OpenCores and TrustHub and using gate-level representation generated by two synthesis tools, YOSYS and Synopsis Design Compiler (SDC), shows that our approach is both efficient (up to 10× speedup w.r.t. no pruning) and precise (0% false positives both at RTL and gate-level netlist) in detecting don’t care transitions and the Trojans that leverage them. Additionally, the total analysis time can achieve up to 1.62× (using YOSYS) and 1.92× (using SDC) speedup when synthesis preserves the FSM structure, the foundry is trusted, and the Trojan detection is performed at RTL.