Analyzing Threats and Detecting Trojans Through Formal Analysis in a Semiconductor 3PIP

It is a well-known fact that a substantial part of the effort in the development of a semiconductor Intellectual Property (IP) goes into verification. Since the cost of incomplete or incorrect implementation increases exponentially in the later stages of the semiconductor supply chain, it is critical to identify, in early stages of development, a wide range of test cases that provides the assurance that the design achieves the functional specifications. This challenge is compounded for security as identifying verification scenarios for security specification and design decisions is complicated and often not approached methodically. The problem is further compounded by the fact that third-party IPs (3PIP) are generally developed following a standard specification of the relevant technology without complete knowledge of the environment or the application of the 3PIP. 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 methodically identify verification scenarios in the 3PIP that when used in conjunction with formal methods can confirm the effectiveness of the mitigations and detect any trojans or other unexpected ways to bypass security measures.