Research On High-level Trust Model Based Trojan Detection Key Techniques

Hardware Trojans are malicious modifications made to the circuits during the design or manufacturing process of the integrated circuits(ICs).Once the chip is manufactured,the hardware Trojan will exist in the circuit for a long time.Hardware Trojans can perform harmful functionalities,including information leakage,functional manipulation,performance degradation,etc.Due to the variety of hardware Trojans,there is no universal hardware Trojan detection technology that can guarantee the security of ICs.This paper first analyzes the security threats in the life cycle of ICs and analyzes the stages where Trojans can be inserted: in the pre-silicon stage,the hardware Trojan is mainly hidden in the third-party IP cores,while in the post-silicon stage,the hardware Trojan is mainly implanted by modifying the circuit layout design during the chip manufacturing process.In addition,this paper systematically studies the characteristics of different hardware Trojans,points out the shortcomings of existing Trojan detection methods and proposes a solution to solve the key problems in Trojan detection methodologies by constructing a high-level security model.The formal model is validated to focus on detecting hardware Trojans hidden in third-party IP cores.A high-level electromagnetic radiation model is leveraged to construct the spectral fingerprint,and the hardware Trojan that is implanted in the manufacturing process can be detected by the side-channel detection methods.In the pre-silicon stage,this paper focuses on the research of formal hardware verification based on the RTL code.Based on the comparison results of equivalent checking,theorem proving and model checking,a complete formal model modeling theory based on a finite state machine(FSM)is proposed.Based on the FSM extraction tool of Boolean satisfiability calculation(3-SAT solver),a Python script-based translation tool is developed to perform the automatic modeling from FSM to a formal model.The semantics and common attributes of Query security attribute description language based on the computational logic tree are analyzed.A security attribute description method for hardware Trojan detection is proposed,including various security attributes such as information flow control(determination,invariance)and access authority determination.A multi-IP So C system based on AMBA AXI4-Lite bus is built,and experiments are carried out for the single IP-level information leakage hardware Trojan and the systemlevel denial-of-service hardware Trojan.The detection of hardware Trojan malicious behaviors and the accurate positioning of hardware Trojan code are realized,which verifies the applicability of the formal hardware Trojan detection technology proposed in this paper.In the post-silicon stage,this paper proposes a method of utilizing the high-level security model to enhance the side-channel hardware Trojan detection methods.Considering the driven capabilities and logic states of the basic logic units in the circuits,a Hamming weight electromagnetic radiation model is established.Based on the spectrum factor analysis,the electromagnetic spectrum fingerprint which can be used for hardware Trojan detection post-silicon is formed to solve the problem of the non-golden chip of the side-channel Trojan detection approaches.The influence of non-ideal factors such as noise and process deviation on the electromagnetic spectrum fingerprint are studied,and the simulation verification under ±5% process deviation is completed.The overall correlation between the simulation model and the measured test is over98%.Finally,on the Xilinx FPGA detection platform,11 hardware Trojan circuits are designed based on the AES circuit,and the Euclidean distance discrimination algorithm with reference and the neural network adaptive detection algorithm are utilized to achieve a minimum ratio of 0.2% detection rate.