UC Santa Barbara

Verification for hardware security has become increasingly important in recent years as our infrastructure is heavily dependent on electronic systems. Traditional verification methods and metrics attempt to answer the question: does my design correctly perform the intended specified functionality? The question this dissertation addresses is: does my design perform malicious functionality in addition to the intended functionality? Malicious functionality inserted into a chip is called a Hardware Trojan.

This work is devoted to developing both new threat models and detection methodologies for a less studied but extremely stealthy class of Trojan: Trojans which do not rely on rare triggering conditions to stay hidden, but instead only alter the logic functions of design signals which have unspecified behavior, meaning the Trojan never violates the design specification.

The main contributions of this work are 1) precise definitions for dangerous unspecified functionality in terms of information leakage and several methods to identify such functionality, 2) satisfiability-based formal methods to test potentially dangerous unspecified functionality for the existence of Trojans, and 3) numerous examples of how the proposed Trojans can completely undermine system security if inserted in on-chip bus systems, communication controllers, and encryption IP.