Security Analysis And Backdoor Vulnerability Detection Of The Soft-core IP

With continuous improvement of the information terminal intelligent degree,the size of the chips and functional requirements are getting higher and higher,So C becomes the mainstream of integrated circuit design.Considering the cost and efficiency and the need to seize the market quickly,So C design tends to be intellectual property gradually.With high flexibility and portability,IP soft cores which have nothing to do with manufacturing process are widely used in So C design.But many IP soft cores are provided by third-party vendors,their security is not guaranteed,So the security of IP soft cores must be tested.Once the trojan codes in the IP soft cores are used in the chips,it will form hardware trojans in the chips.Hardware trojans are malicious additions or tampering of the circuits collectively during the integrated circuit design or manufacturing process.Hardware trojans can be triggered under specific conditions and cause the chips failure or leak secret information.Hardware trojans bring serious risks and hazards to information security and national security.The corresponding hardware trojan detection technology has become a hot research field of hardware security.In this paper,two IP soft cores detection methods are proposed.One is the use of self-developed software to analyze the circuit structure and internal signals of IP soft cores which can significantly reduce the detection range of the trojan circuit.The other is the use of theorem proving device Coq which utilizes mathematical proof to prove the safety of IP soft cores.The main work is as follows:(1)Introducing the basic concept of hardware trojans and the corresponding detection methods.Then DES and AES encryption algorithms are studied.(2)According to the characteristics of trojans’ concealment,We propose to analyze the circuit structure and internal signals of IP soft cores to detect hardware trojans.Then JAVA language is used to develop a dedicated hardware trojan detection software.The common structural modules in the circuit,such as accumulators,state machines,pseudo-random sequence and linear shift register,are modeled to establish the software trojan library.And then using the software analyzes the code structure,combings the signal flow in the modules and detects security of the signal transmission.All of these are used to determine whether the signals have been tampered with.(3)In order to further analyze the security and backdoor vulnerability of IP soft cores,The theorem proving program Coq which utilizes mathematical proof is used to prove the security of IP soft cores.This paper specifies the conversion rules from RTL codes to Coq codes,and constructs the corresponding circuit models of combinatorial logic,timing logic and so on,and the RTL codes of DES and AES are transformed according to the rules defined.IP users can convert verilog codes into Coq codes with the same original circuit structure according to conversion rules.In the Coq codes,signals of the circuit are attached to a secret attribute,and the secret level would be defined according to the specific structure of the circuit.The additional secret attribute is an important basis for detecting whether there is a backdoor vulnerability in IP soft cores.(4)The security theorems of the secret information in DES and AES are defined by Coq language,then the security theorems are proved by using the converted Coq codes.Experimental results show that Coq can detect the backdoor vulnerability and hardware trojans in IP soft cores.