Detecting Trojans in Unspecified Functionality by Solving Satisfiability Problems

  • Authors:
    Nicole Fern (UC/Santa Barbara), K.T. Tim Cheng (UC/Santa Barbara)
    Publication ID:
    P090753
    Publication Type:
    Deliverable Report
    Received Date:
    25-Apr-2017
    Last Edit Date:
    5-May-2017
    Research:
    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.

Abstract

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