Detecting Hardware Trojans in Unspecified Functionality Through Solving Satisfiability Problems

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


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. We pro- pose 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. The formulated detection procedure can be applied to a gate-level design using commercial equivalence checking tools, or directly to the Verilog/VHDL code by reasoning about the satisfiability of SMT expressions built from traversing the data-flow graph. We demonstrate the effectiveness of our approach on an adder coprocessor and a UART communication controller infected with Trojans which process information leaked from the on-chip bus during idle cycles using signals with only partially specified behavior.

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