Selection And Combinable Proof Of IP Core Security Path

As modern semiconductor chips become larger and more complex in scale and design,a large number of IP cores are used in chips in order to shorten the development cycle and reduce the design cost.However,these IP cores are often provided by third parties,whose security cannot be guaranteed.Malicious manufacturers may implant backdoors or hardware trojans in the IP cores,resulting in serious threats to the information security of the entire chip and system.Therefore,reliable verification methods are required to detect the security of the third-party IP cores.This paper proposes a verification method based on the formal verification,for the third-party IP soft core's RTL information flow security inspection.Describe the security properties of IP core based on the demand of the security of IP core,making accord with normative description of formal verification methods.It can automatically verify IP core's security properties without affecting the normal function of IP core.This paper analyzes the basic theory of IP core security path verification,and introduces the environment and methods required for IP core security path verification.The proposed code smudge marking and tracking method of IP core can more intuitively observe the information flow trend in the IP core through the register-level smudge marking bit,so as to analyze the large and complex data paths in the IP core,and to build a good verification environment with the description of security properties.The existing verification methods cannot both advantages of efficiency and accuracy.In the numerous data paths,there are some we don't care about and the others we care about.It will waste a lot of time and cost if we choose to verify all of them.This paper introduces in detail how to select critical security path and cut off paths which have nothing to do with security demand to improve the efficiency an accuracy of verification.At the same time,the traditional verification method cannot directly detect the ultra-long paths that may be cascaded and complex.The combinability proof method of the ultra-long path proposed in this paper skillfully converts it into the combinability proof of several short paths,which reduces the difficulty of verification.An automated tool chain is proposed at the end of the paper with a detailed presentation of the overall scheme and tool chain functions.For the implementation of the security path verification,we take a test of IP cores which contain hardware Trojan or back-doors,including encryption IP cores(AES,3DES),communication IP cores(RS232),bus IP cores(CAN)and so on.Finally we detect the information security problem of IP core successfully.And compared with the tradional method,we improve the detection efficency and accuracy.It shows that the verification method proposed in this paper has a very important reference value for the security detection of the third-party IP core.