Design for Assurance: Employing Functional Verification Tools for Thwarting Hardware Trojan Threat in 3PIPs

Third-party intellectual property cores are essential building blocks of modern digital hardware. However, they usually come from vendors of different trust levels and may contain undocumented design functionality. Distinguishing such stealthy malicious design modifications remains a significant research challenge. State-of-the-art hardware Trojan detection methods usually require expert knowledge, sophisticated tools or large volumes of training samples. In this work, we make a step towards design for assurance by developing a Trojan detection method targeting look-up-table (LUT) netlists, which exploits the rich explicit structural and behavior characteristics embedded in the initialization vectors of LUTs to pinpoint Trojans. The proposed method automatically extracts a small set of high-quality Trojan related properties and detects Trojans through formal verification of the extracted properties, eliminating the limitation of manual property specification while covering a much wider range of Trojan designs. We further present a defense solution to mitigate the identified Trojans through lightweight design reconfiguration to neutralize the Trojan payload. The proposed method can be seamlessly integrated into the standard EDA flow to enable security to be evaluated along with functional correctness and performance budgets. Experimental results have demonstrated that our method can detect and mitigate <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">Trust-Hub</i>, <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ATTRITION</i> as well as satisfiability don't care Trojans.