Ensuring Secure RTL Circuit Design

Modern digital chip designers face increased security challenges when using third-party intellectual property (3PIP) in their designs. Using formal verification techniques, vulnerabilities in the register transfer language (RTL), such as, code bugs or hardware (HW) Trojans can be detected before the chip is delivered to the end-user, or even thwarted, after the chip has been shipped. This document presents several motivational problems with their respective solution which are reinforced by supporting data. In the first solution, formal verification is used to detect RTL vulnerabilities in a self-locking lock bit and security critical identification (ID) register of a hypothetical 3PIP. In the second solution, formal verification is used in a specific manner to verify components and paths against the circuit specification to detect RTL vulnerabilities. The third solution detects RTL vulnerabilities when the circuit under test is black boxed, such as, due to encryption. The fourth solution gives a system integrator the option to use HW wrappers to enforce security properties and prevent malicious events during run-time. The results of the first solution show that 21 of 28 HW Trojan vulnerabilities where detected in the self-locking lock bit with a security critical ID register circuit. Results of the second solution demonstrate that a single HW Trojan vulnerability can be detected using formal proofs which use taint propagation properties as well as linear time properties. Results for the third solution show the feasibility of detecting a HW Trojan vulnerability in a black boxed single in-line 8-bit CPU. Finally, results for the fourth solution show that 28 different HW Trojans can be thwarted by using a HW wrapper to enforce a specific security property of the self-locking lock bit and security critical ID register circuit.