PhD and Postdoc Research
My research interests include hardware verification and security. I graduated from UC Santa Barbara with a PhD in Computer Engineering in June of 2016 under the advisement of Professor Tim Cheng working in the SoC Design and Test Lab. My thesis focused on identifying and verifying unspecified design functionality susceptible to malicious manipulation. After graduation I continued my research in hardware security as a post-doc at UC Santa Barbara and visiting Scholar at Hong Kong University of Science and Technology.
Detecting Hardware Trojans in Unspecified Functionality
Hardware is the root of trust in electronic systems. Hardware can both be exploited to mount powerful attacks on a system (ex. Rowhammer) and designed to provide extra security not possible with only software defenses (ex. Data Execution Prevention). Because hardware design mandates thousands of engineers and an entire ecosystem of design tools and fabrication services, many people have access to the design and the opportunity to insert malicious functionality known as Hardware Trojans. This project develops HDL-level analysis methods to verify the absence of Trojans and accidental security holes in unspecified functionality by:
Characterizing unspecified functionality, and
Verifying unspecified functionality is Trojan-free.
Hardware Design Lifecycle: this project focuses on Trojans inserted in the HDL design meaning no “golden model” is available for verification.
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
This project develops methods to:
Characterize unspecified functionality, and
Verify unspecified functionality is Trojan-free.
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, “Evaluating Assertion Set Completeness to Expose Hardware Trojans and Verification Blindspots”, in Design, Automation and Test in Europe (DATE) Conference, 2019.
N. Fern and K.-T. Cheng, “Pre-silicon Formal Verification of JTAG Instruction Opcodes for Security”, International Test Conference (ITC), 2018.
N. Fern and K-T. Cheng. “Mining Mutation Testing Simulation Traces for Security and Testbench Debugging“, 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“, Asia South-Pacific Design Automation Conference (ASP-DAC), 2017.
N. Fern and K-T. Cheng. “Verification and Trust for Unspecified IP Functionality” in 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“, 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”, Design, Automation, Test in Europe (DATE), 2016.
N. Fern and K-T. Cheng. “Detecting Hardware Trojans in Unspecified Functionality Using Mutation Testing”, 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”, International Test Conference (ITC), 2015.