Paper 2014/943

HaTCh: A Formal Framework of Hardware Trojan Design and Detection

Syed Kamran Haider and Chenglu Jin and Masab Ahmad and Devu Manikantan Shila and Omer Khan and Marten van Dijk

Abstract

Electronic Design Automation (EDA) industry heavily reuses existing design blocks called IP cores. These IP cores are vulnerable to insertion of Hardware Trojans (HTs) at design time by third party IP core providers or by malicious insiders in the design team. State of the art research has shown that existing trojan detection techniques which claim to detect all publicly available HT benchmarks, can still be defeated by carefully designing new sophisticated trojans. Researchers have proposed techniques to detect these new trojans, however these techniques are known to be computationally infeasible. This state of affairs leads to two crucial observations. First, instead of guaranteeing a certain (low) false negative rate for a small constant set of publicly available benchmarks, a rigorous security framework of HTs should characterize which exponentially large class (exponential in number of wires in IP core) of HTs a tool can detect with negligible false negative rate. Second, an effective detection tool must be designed which is computationally feasible for this class of HTs which is orders of magnitude larger compared to the small subclass (e.g. TrustHub) considered in the current literature. To meet the above mentioned goals, we present HaTCh, the first rigorous framework of HT design and detection within the paradigm of pre-silicon logic testing based tools. We first introduce certain crucial properties of HTs which lead to the characterization of an exponentially large class of HTs that an adversary can (but is not limited to) design, for which we present a detection algorithm which detects any HT from this class with overwhelming probability $1-negl(\lambda)$. Given certain global characteristics regarding the stealthiness of a HT within this class, the computational complexity of our algorithm scales polynomially with the number of wires in the IP core, as opposed to the exponential (in number of IP core inputs) complexity of current state of the art detection schemes to detect such HTs. We have implemented this algorithm, compared it with existing countermeasures, and tested it on TrustHub HT benchmarks, previously proposed HTs which alleviate state of the art detection schemes, and also on a newly designed advanced HT. We argue that those HTs that fall outside the characterized class use HT design principles that allow HTs which can never be detected within the pre-silicon logic testing based paradigm.

Note: Included the Explicit vs. Implicit malicious behavior and the probability \alpha which caused several major changes.