隨著數位積體電路的複雜性不斷增加，第三方矽智財電路（IP）的利用已廣泛應用於現代電子系統中，然而惡意電路或稱作硬體木馬可能被植入到第三方IP中。在這項研究中，我們提出了一個基於正規驗證的硬體木馬檢測方法來檢測處理器內核中的硬體木馬。該方法生成一組正規特性，可以驗證處理器中不同類型的指令和不同的執行狀況，例如分支、例外處理和中斷。我們還展示了生成的正規特性能夠檢測具有各種觸發條件和惡意行為的硬體木馬，並提出幾種驗證技術來減少驗證負擔。我們設計了6個具有不同觸發條件和惡意行為的硬體木馬，並使用一個開源RISC-V處理器作為主電路來評估我們提出的方法。實驗結果顯示該方法能夠檢測出全部6種硬體木馬，且無漏報和誤報。

With the growing complexity of digital integrated circuits (ICs), the utilization of third-party intellectual properties (IPs) has been widely used in modern electronic systems. However the malicious circuits, or hardware Trojans (HTs), can be inserted into the third-party IPs. In this work we propose a hardware Trojan detection method based on formal verification to detect HTs in processor cores. The method generates a set of formal properties that can verify different types of instructions and different scenarios in a processor, such as branches, exceptions, and interrupts. We also show that the generated formal properties can detect HTs with various trigger conditions and malicious behaviors. Several verification techniques have also been proposed to reduce the verification burdens. We design 6 HTs with different trigger conditions and malicious behaviors and use an open-source RISC-V processor as the host circuit to evaluate our proposed method. Experimental results show that the proposed method can detect all the 6 hardware Trojans without false negatives and false positives.

[1] H. Salmani, “COTD: Reference-Free Hardware Trojan Detection and Recovery Based on Controllability and Observability in Gate-Level Netlist,” IEEE Trans. Inf. Forensics Security, vol. 12, no. 2, pp. 338-350, Feb. 2017.
[2] H. Salmani, M. Tehranipoor and J. Plusquellic, “A Novel Technique for Improving Hardware Trojan Detection and Reducing Trojan Activation Time,” IEEE Trans. Very Large Scale Integr. Syst., vol. 20, no. 1, pp. 112-125, Jan. 2012.
[3] B. Zhou, W. Zhang, S. Thambipillai, J. Teo, K. Jin, V. Chaturvedi and T. Luo, “Cost-efficient Acceleration of Hardware Trojan Detection Through Fan-Out Cone Analysis and Weighted Random Pattern Technique,” IEEE Trans. Comput.-Aided Design of Integr. Circuits and Syst., vol. 35, no. 5, pp. 792-805, May 2016.
[4] X. Zhang and M. Tehranipoor, “Case study: Detecting hardware Trojans in third-party digital IP cores,” in Proc. IEEE Int. Symp. Hardware-Oriented Security and Trust, San Diego, CA, USA, 2011, pp. 67-70.
[5] S. Dupuis, M. -L. Flottes, G. Di Natale and B. Rouzeyre, “Protection Against Hardware Trojans With Logic Testing: Proposed Solutions and Challenges Ahead,” IEEE Design & Test, vol. 35, no. 2, pp. 73-90, April 2018.
[6] A. Waksman, M. Suozzo, and S. Sethumadhavan, “FANCI: Identification of stealthy malicious logic using Boolean functional Analysis,” in Proc. ACM Conf. Computer and Communication Security, 2013, pp. 697-708.
[7] H. Salmani and M. Tehranipoor, “Analyzing circuit vulnerability to hardware Trojan insertion at the behavioral level,” in Proc. IEEE Int. Symp. Defect and Fault Tolerance in VLSI and Nanotechnology Systems (DFTS), New York, NY, USA, 2013, pp. 190-195.
[8] K. Hasegawa, M. Oya, M. Yanagisawa and N. Togawa, “Hardware Trojans classification for gate-level netlists based on machine learning,” in Proc. IEEE 22nd Int. Symp. On-Line Testing and Robust System Design (IOLTS), Sant Feliu de Guixols, Spain, 2016, pp. 203-206.
[9] T. Kurihara and N. Togawa, “Hardware-Trojan Classification based on the Structure of Trigger Circuits Utilizing Random Forests,” in Proc. IEEE 27th Int. Symp. On-Line Testing and Robust System Design (IOLTS), Torino, Italy, 2021, pp. 1-4.
[10] Syntacore. (2018). [Online]. Available: https://github.com/syntacore/scr1
[11] M. Kuo, C. Hu and K. Lee, “Time-Related Hardware Trojan Attacks on Processor Cores,” in Proc. IEEE Int. Test Conf., Tokyo, Japan, 2019, pp. 43-48.
[12] C. Duran, H. Morales, C. Rojas, A. Ruospo, E. Sanchez and E. Roa, “Simulation and Formal: The Best of Both Domains for Instruction Set Verification of RISC-V Based Processors,” in Proc. IEEE Int. Symp. Circuits and Systems (ISCAS), Seville, Spain, 2020, pp. 1-4.
[13] RISC-V Formal Verification Framework. (2019). [Online]. Available: https://github.com/SymbioticEDA/riscv-formal
[14] L. Weingarten, A. Mahzoon, M. Goli and R. Drechsler, “Polynomial Formal Verification of a Processor: A RISC-V Case Study,” in Proc. 24th Int. Symp. Quality Electronic Design (ISQED), San Francisco, CA, USA, 2023, pp. 1-7.
[15] A. Munir, M. Magdy, S. Ahmed, S. Nasr, S. El-Ashry and A. Shalaby, “Fast Reliable Verification Methodology for RISC-V Without a Reference Model,” in Proc. 19th Int. Workshop Microprocessor and SOC Test and Verification (MTV), Austin, TX, USA, 2018, pp. 12-17.
[16] K. Devarajegowda et al., “Gap-free Processor Verification by S2QED and Property Generation,” in Proc. Design, Automation & Test in Europe Conf. & Exhibition (DATE), Grenoble, France, 2020, pp. 526-531.
[17] K. Devarajegowda, E. Kaja, S. Prebeck and W. Ecker, “ISA Modeling with Trace Notation for Context Free Property Generation,” in Proc. 58th ACM/IEEE Design Automation Conf. (DAC), San Francisco, CA, USA, 2021, pp. 619-624.
[18] J. Rajendran, A. M. Dhandayuthapany, V. Vedula and R. Karri, “Formal Security Verification of Third Party Intellectual Property Cores for Information Leakage,” in Proc. 29th Int. Conf. VLSI Design and Proc. 15th Int. Conf. Embedded Systems (VLSID), Kolkata, India, 2016, pp. 547-552.
[19] J. Rajendran, V. Vedula and R. Karri, “Detecting malicious modifications of data in third-party intellectual property cores,” in Proc. 52nd ACM/EDAC/IEEE Design Automation Conf. (DAC), San Francisco, CA, USA, 2015, pp. 1-6.
[20] N. Fern, S. Kulkarni and K. -T. T. Cheng, “Hardware Trojans hidden in RTL don't cares — Automated insertion and prevention methodologies,” in Proc. IEEE Int. Test Conf. (ITC), Anaheim, CA, USA, 2015, pp. 1-8.
[21] J. Portillo, E. John and S. Narasimhan, “Building trust in 3PIP using asset-based security property verification,” in Proc. IEEE 34th VLSI Test Symp. (VTS), Las Vegas, NV, USA, 2016, pp. 1-6.
[22] N. Fern, I. San and K. -T. T. Cheng, “Detecting hardware Trojans in unspecified functionality through solving satisfiability problems,” in Proc. 22nd Asia and South Pacific Design Automation Conf. (ASP-DAC), Chiba, Japan, 2017, pp. 598-504.
[23] N. Mathure, S. K. Srinivasan, K. K. Ponugoti, A. Malik and S. Quanbeck, “A Formal Verification Approach for Detecting Opcode Trojans,” in Proc. 27th IEEE Int. Conf. Electronics, Circuits and Systems (ICECS), Glasgow, UK, 2020, pp. 1-4.
[24] K. K. Ponugoti, S. K. Srinivasan and N. Mathure, “Formal Verification Approach to Detect Always-On Denial of Service Trojans in Pipelined Circuits,” in Proc. 28th IEEE Int. Conf. Electronics, Circuits, and Systems (ICECS), Dubai, United Arab Emirates, 2021, pp. 1-6.
[25] S. Yao, X. Chen, J. Zhang, Q. Liu, J. Wang, Q. Xu, Y. Wang, and H. Yang, “FASTrust: Feature analysis for third-party IP trust verification,” in Proc. IEEE Int. Test Conf. (ITC), Anaheim, CA, USA, 2015, pp. 1-10.
[26] JasperGold RTL Apps. [Online]. Available: https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification/jasper-gold-verification-platform.html