Pre-silicon Formal Verification of JTAG Instruction Opcodes for Security

摘要

Widely implemented standards such as IEEE 1149.1 (JTAG) and 1687 (iJTAG) are essential in providing improved chip and board testability, but it has been demonstrated that undocumented or poorly obfuscated scan and debug instructions can be exploited by hackers to undermine system security. Prior work proposes adding authentication or encryption to JTAG to improve security, but these methods can only protect functionality known to the design and test team. Out-of-spec JTAG functionality can be inserted accidentally or with malicious intent (e.g., hardware Trojans). Our proposed technique can detect anomalous JTAG instructions not present in the specification using commercial formal equivalence checking tools. We demonstrate the effectiveness of our technique by characterizing the entire JTAG instruction set space for the OpenSPARC T2 benchmark in a completely automated manner. In the original design our technique formally proves all undefined opcodes map to the benign bypass instruction and provides the size and location within the design hierarchy of all data registers. In a modified version of the design our technique correctly detects several undefined opcodes that are used to access the L2 cache, as well as extra out-of-spec elements in a data register selected by an existing instruction.