Secure Computation Laboratory

HaTCh: A Formal Framework for Hardware Trojans Design and Detection

Electronic Design Automation (EDA) industry heavily reuses third party IP cores which are vulnerable to insertion of Hardware Trojans (HTs) at design time by third party IP core providers. Recent works have shown that existing HT detection techniques, which claim to detect all publicly available HT benchmarks, can still be defeated by carefully designing new sophisticated HTs. In this work, we first discover certain crucial properties of HTs which lead to the definition of an exponentially large class of Deterministic Hardware Trojans that an adversary can design. Based on these design principles, we then introduce HaTCh, the first rigorous algorithm of HT detection within the paradigm of pre-silicon logic testing based tools. HaTCh detects any HT from a huge class of deterministic HTs which is orders of magnitude larger than the small subclass (e.g. TrustHub) considered in the current literature. We prove that HaTCh offers negligible false negative rate and controllable false positive rate for the class of HTs under consideration. Given certain global characteristics regarding the stealthiness of the HT within this class, the computational complexity of HaTCh for practical HTs scales polynomially with the number of wires in the IP core.