Analyzing threats & detecting trojans using formal analysis in a semiconductor IP

It is a well-known fact that a substantial part of the effort in the development of a semiconductor IP goes into verification. Since the cost of incomplete or incorrect implementation increases exponentially in the later stages of semiconductor supply chain, it is critical to identify a wide range of test cases that could prove the design achieves the functional specifications, in early stages of the project. This problem is compounded for security as identifying verification scenarios for security specification and design decisions is complicated. The problem is further compounded by the fact that the third-party IPs are generally developed following standard specification of certain technologies without much knowledge of the environment or the application where its used. Such third-party IPs also carry the risk of trojans installed into them through supply chain. In this paper we discuss how threat modelling can be used to identify potential threats in the IP and derive verifications scenarios, that verify mitigations, to address those threats. We then describe how these verification scenarios aid in identifying potential trojans in the design using formal methods based verification.