Detecting Trojans in Unspecified Functionality by Solving Satisfiability Problems

  • Authors:
    Nicole Fern (UC/Santa Barbara), K.T. Tim Cheng (UC/Santa Barbara)
    Publication ID:
    Publication Type:
    Deliverable Report
    Received Date:
    Last Edit Date:
    2634.001 (University of California/Santa Barbara)

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.

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450

Important Information for the SRC website. This site uses cookies to store information on your computer. By continuing to use our site, you consent to our cookies. If you are not happy with the use of these cookies, please review our Cookie Policy to learn how they can be disabled. By disabling cookies, some features of the site will not work.