Hardware Trojan Detection in Behavioral Intellectual Properties (IP's) Using Property Checking Techniques

This work introduces a fully automatic method to detect the presence of HW Trojans in third party behavioral IPs (3PBIPs) using formal verification methods. In particular, property checking at the behavioral level. Some state of the art High-Level Synthesis (HLS) tools now also include advanced formal verification tools. This work leverages these tools to detect the malicious alteration of 3PIPs when no golden reference IP is available. This work has also been extended to detect HW Trojans built into encrypted 3PBIPs by performing High-Level Synthesis on these IPs and re-constructing the C code in order to perform the verification on them. We present three case studies of two of the most typical HW Trojans with different trigger and payload mechanisms. The first leads to the malfunction of the IP, the second leaks information while the third leads to the denial of service. In all three cases, our proposed method was able to detect the HW Trojan in a fully automatic way.