Verification for hardware security has become increasingly important in recent years as our infrastructure is heavily dependent on electronic systems. Security vulnerabilities in hardware can arise from both the specification and implementation. If a weak cryptographic algorithm or flawed access control scheme is implemented, the system will be insecure. Additionally, the implementation itself can also be susceptible to side channel, fault, and scan-chain attacks, contain Hardware Trojans, or simply not conform to the specification.
Identification of security weaknesses in both specification and implementation is further complicated by the fact that a specification usually only defines a small fraction of design behavior. For example, a serial multiplier requires several intermediate cycles before the final result is computed. There are many multiplier implementations that perform completely different computations during intermediate cycles, yet produce identical final values.
Functional verification only targets functionality outlined in the specification, however, unspecified functionality presents an attacker with an enormous opportunity to implement malicious functionality in the form of very stealthy Hardware Trojans.
Design, manufacturing, testing, and deployment of silicon chips is a global effort involving multiple companies and countries. If a single contributor in this process decides it advantageous to insert malicious functionality into the chip, referred to as Hardware Trojans, the consequences can be disastrous. Detection is challenging because Hardware Trojans can be inserted during any phase of the chip design lifecycle: as malicious 3rd party IP, modifications to the netlist or layout, or mask alterations during fabrication to name a few.
There are also many categories of Hardware Trojans. Some Trojans leak secret information through power or timing side-channels, while others cause denial of service attacks, or affect circuit functionality. This project is focused on digital Trojans, which alter circuit functionality in a stealthy way, but can still be detected in the functional domain.
Each stage relies on prior stages to specify correct design behavior, and also refines the specification. For example, the design specification is used to develop RTL code and the test plan for verifying the RTL, while the RTL code is designated as a reference implementation when performing equivalence checking with a gate-level netlist. Rarely is design behavior completely specified. At the RT-level, the presence of don't cares allows for multiple correct gate-level implementations, and this flexibility allows for operations such as state re-encoding, re-timing and logic minimization.
This freedom and flexibility provides opportunity for area/timing/power optimization, but also provides an attacker with an opportunity to insert malicious functionality into the design which still conforms to the design specification. Traditional verification and testing techniques are primarily concerned with testing that the RTL or silicon conforms to the specification with the goal being to reveal accidental logic errors and manufacturing defects.
The figure above outlines the problem this project addresses. Ambiguities in the specification allow for multiple valid implementations, some of which contain Hardware Trojans adhering to a given threat model (shown in red). New methodologies are needed to identify portions of the design specification which need to be refined in order to ensure that implementations containing Trojans no longer conform to the revised specification. Since for most complex designs it is impossible to completely specify design behavior, new threat models which accurately capture Trojan functionality must be defined and targeted.