Detecting Trojans in Unspecified Functionality by Solving Satisfiability Problems
Research Report Highlight
A new hardware Trojan detection methodology has been defined for Trojans modifying only unspecified functionality. Previous methodologies have been ineffective at identifying these Trojans. It monitors information leakage using boolean and SMT solvers.
For modern complex designs it is impossible to fully specify design behavior, and only feasible to verify functionally meaningful scenarios. Hardware Trojans modifying only unspecified functionality are not possible to detect using existing verification methodologies and Trojan detection strategies. In this report we provide a detection methodology for these Trojans by 1) precisely defining suspicious unspecified functionality in terms of information leakage, and 2) formulating detection as a satisfiability problem that can take advantage of the recent advances in both boolean and satisfiability modulo theory (SMT) solvers. We deviate from the original deliverable (metrics for evaluation of Trojan prevention/detection techniques) by giving the detection technique itself in this report and plan to address evaluation metrics in future reports.