During the EDA process, a design may be tampered directly by dishonest engineers (or “industry spy”), or may be tampered indirectly through the use of malicious modules from a third party Intellectual Property (3PIP) block vendor. During integration and fabrication, the chips may also be tampered by untrusted system integrator or even foundry. Particularly for high-end commercial or classified military chips, Hardware Trojan (HT) Detect-Locate-and-Mask (DL&M) is crucially necessary so as to make sure a design is produced exactly as the original specification (golden). Our objectives are (1) to detect any functionality difference which might be caused by bugs or HTs, (2) to locate/output the difference circuitry to correct the bugs or to investigate the tampering intention or purpose, and (3) to “kill” (mask) the HTs by restoring the chip's functionality back to golden with a minimum circuitry change. Besides blocking the plotted damage in an early stage and pointing the spy source by revealing the HT intention, the masking circuit revision must also be minimized to avoid affecting the chip performance (timing) too much. In this paper, we propose a scheme that integrates reverse engineering, formal verification, functional ECO, and logic rewiring to detect, locate and mask Hardware Trojans with minimized cost. This formal verification based scheme can guarantee catching 100% of the hidden combinational circuit HTs and can handle multiple HTs (no number limit) automatically in one run. Some techniques within our scheme won the first places of the CAD Contests at ICCAD 2012, 2013, and 2014 [1-3].
展开▼
