Security Path Checking Of A Circuit With Model Checking Technology

With the rapid development of information technology,digital system and the integrated circuit has become a part of our lives unwittingly.The IP core from third party is widely used in the integrated circuits,which makes the internal information system and the data among the various systems be a potential interaction of security threats.The integrated circuit with high requirements for data confidentiality and integrity is required to confirm to modify permissions and access permissions of the critical data inside of the systems.It is necessary to ensure that critical data cannot be leak or modified without permissions.This thesis marks the data flow inside a circuit,tracks its direction without modifying or damaging the original function,and adopts model checking technology to perform the security path checking.As a verification method based on Finite State Machine,the model detection technology can automatically verify whether the circuit system or the software design can satisfy the desired attributes.This thesis analyzes the basic theory and principles of the model detection method,and explains Kripke structure,CTL*,CTL and LTL temporal logic.The characteristics of the model detection can be used to verify the security path of the tinted circuit,but its application is inseparable from the effective model checker.In this thesis,NuSMV is selected as the model checking tool,which can describe complex finite state systems in a clear and concise way.Based on the security path verification method of tint tracking,this thesis tracks the direction of data flow by marking that in gate-level Verilog,thereby forming a traceable IP core code.In terms of data flow marking and tracking methods,this thesis also introduces various simple logic gates and flip-flops in detail,as well as the methods to add tint-tracking labels and its internal algorithms.Finally,this thesis designs and implements an innovative tool chain,and introduces its main algorithm,the data structure and conversion program.This tool chain can automatically convert the gate-level Verilog into marked NuSMV code,and generate IP core verification code,thus providing a great convenience for security path verification of a specific circuit.