Hardware Security Analysis Based On Information Flow Tracking

Digital hardware usually plays an important role in medical,financial,infrastructure and defense systems.With the globalization of information and supply chain,multiple countries and teams are involved in hardware design,and the safety of hardware design has been attracted widespread attention.Security vulnerabilities may be caused by insecure ports and hardware Trojans in hardware design.The possibility of accessing and tampering with security information are provided to attackers through these security vulnerabilities.Therefore,it is of important practical significance to research on the security analysis of hardware design.This thesis is based on the method of information flow tracking to detect whether the circuit has security threats.The main contents are described as follows:(1)The basic knowledge related to hardware security and information flow,including hardware security threats and protection technologies,classification of information flow and security strategies are introduced.At the same time,the security verification methods are illustrated.Also,the existing security verification methods and their respective advantages and disadvantages are summarized.(2)The hardware Trojan detection method based on information flow tracking is studied.According to the principle of information flow tracking,taint labels to the input and output ports should be added,and the shadow logic of the circuit should be expanded.After the netlist classification operation on the circuit which the shadow logic is added is performed,the formal verification tool is used to verify the equivalence of the circuit with the shadow logic,and then a value to the taint label of the input port according to the attribute of the input port is assigned.The value of the taint label on the output port is observd,and it can be judged whether the sensitive information in the circuit has been leaked or tampered.At the same time,according to the principle that the counterexamples are given by the formal verification tool when verification fails,the Trojan functional circuit starting logic including its location and value are detected for the circuit that is judged to be a security threat through formal verification.Finally,three experiments are done in this thesis,including comparision test of sample circuits with and without netlist classification,formal verification test of whether Trojan is involved in the sample circuits,as well as the test of location and value of the Trojan functional circuit starting logic.The effectiveness of the method is proved by these three experiments.(3)The complete trigger sequence detection method based on formal verification is studied.Based on the known Trojan functional circuit starting logic and its value,the counterexample given after the formal verification fails is used to reverse the trigger sequence of the original circuit.First,the Trojan functional circuit starting logic is used as the starting point of the backtracking,and the netlist classification operation is optimized to reduce the time complexity of reversing complex logic.Then the sequential logic is combined for each divided classification,so that it can be traced back to the input port of the circuit through formal verification.Finally,the integrity verification of the sequence obtained in each classification is detected to get a complete trigger sequence.The effectiveness of the netlist classification optimization operation is proved by some experiments,and the entire trigger sequence of the circuit is reversed in a short time for Trojan circuits with simple logic,also the time complexity is reduced as much as possible and the complete trigger sequence is reversed for processor circuits with complex circuit logic.