Detecting Hardware Trojans in Unspecified Functionality
Verification is a bottleneck in the hardware design process, estimated to consume over 70% of hardware development resources. Developing pre-silicon verification infrastructure is crucial in order to catch functional bugs before tape-out and avoid silicon re-spin, however the process requires immense manual effort and is largely ad-hoc. Moreover, traditional verification techniques focus on increasing confidence that specified functionality is correct. Un-modeled behavior will not be verified by existing methods, meaning any security vulnerabilities in unspecified functionality will go unnoticed.
Security vulnerabilities include accidental bugs as well as malicious functionality (Hardware Trojans) inserted by an attacker with access to the design. Chip design mandates thousands of engineers and an entire ecosystem of design tools and fabrication services have access to the design, making Trojans a major concern for both the semiconductor industry and governments recognizing the dependence of critical infrastructure on off-the-shelf electronics. The focus of this project is on detecting Trojans inserted in the design pre-silicon (meaning no "golden" design model exists) whose behavior is embedded completely within unspecified functionality.
For example, consider a simple FIFO circuit shown in the figure below. The value of read_data is unspecified when the FIFO is not being read from, and an attacker can use this condition to leak information by inserting the circuitry shown in red. The number of cycles during which signals are "don’t care" in modern designs is large due to increasing design complexity. It is often impossible to enumerate what the desired value of every signal should be at every cycle and even more impractical to expend verification effort on "don’t care" functionality. This provides ample opportunity for Trojans to implement malicious behavior even when constrained to only modifying unspecified functionality.
Simple FIFO circuit showing a Trojan (in red) modifying unspecified functionality to leak information
Characterization of unspecified functionality is difficult because by definition unspecified functionality encompasses aspects of the design outside the focus of project engineers. We have developed attack scenarios for specific classes of unspecified functionality: RTL Don’t Cares (ITC 2015), vulnerable unspecified functionality in on-chip bus systems (DATE 2016 and TCAD 2016), and FPGA bitstreams (FPL 2016). Additionally, we have provided automated methods to generate assertions describing when signals are unspecified allowing characterization of unspecified functionality beyond the specific classes explored previously in our research (ICCAD 2015 and 2017).
After unspecified functionality is characterized, another major challenge is verifying unspecified functionality is Trojan-free. If a design could be fully specified and exhaustively verified no Trojans (or functional bugs) would exist. Achieving this is impossible for most designs, so our approach is to instead formulate design-independent properties in the form of satisfiability queries describing suspicious behavior of a signal when unspecified (ASP-DAC 2017 and ICCAD 2017). By formally verifying that the suspicious properties do not hold, Trojan detection without specification refinement or modification to the original design is possible using off-the-shelf SAT/SMT solvers and commercial equivalence checking tools.
Project Details: relationship between methods which characterize unspecified functionality and those which analyze the design to detect Trojans
N. Fern and K. -T. Cheng. "Mining Mutation Testing Simulation Traces for Security and Testbench Debugging", in International Conference on Computer Aided Design (ICCAD), 2017.
N. Fern, I. San, and K. -T. Cheng. "Detecting Hardware Trojans in Unspecified Functionality Through Solving Satisfiability Problems", in Asia South-Pacific Design Automation Conference (ASP-DAC), 2017.
N. Fern and K. -T. Cheng. "Verification and Trust for Unspecified IP Functionality" Hardware IP Security and Trust, Prabhat Mishra, Swarup Bhunia, and Mark Tehranipoor, Eds. Springer, 2017.
N. Fern, I. San, C. Koc, and K. -T. Cheng. "Hiding Hardware Trojan Communication Channels in Partially Specified SoC Bus Functionality", IEEE Transactions on Computer-Aided Design of Integrated Circuits and System (TCAD), 2016.
I. San, N. Fern, C. Koc, and K. -T. Cheng. "Trojans Modifying Soft-Processor Instruction Sequences Embedded in FPGA Bitstreams", in International Conference on Field-Programmable Logic and Applications (FPL), 2016.
N. Fern, Verification Techniques for Hardware Security, PhD thesis, University of California, Santa Barbara, June 2016.
N. Fern, I. San, C. Koc, and K. -T. Cheng. "Hardware Trojans in Incompletely Specified On-chip Bus Systems", in Design, Automation, Test in Europe (DATE), 2016.
N. Fern and K. -T. Cheng. "Detecting Hardware Trojans in Unspecified Functionality Using Mutation Testing", in International Conference on Computer Aided Design (ICCAD), 2015.
N. Fern, S. Kulkarni, and K. -T. Cheng. "Hardware Trojans Hidden in RTL Don’t Cares – Automated Insertion and Prevention Methodologies", in International Test Conference (ITC), 2015.