Unspecified design functionality can be modified by Hardware Trojans to leak information. Existing methods capable of detecting these Trojans require that unspecified functionality already be characterized, and suggest a manual ad-hoc process to enumerate “don't care” conditions potentially containing security vulnerabilities. Prior work has shown the potential of mutation testing to uncover testbench holes and highlight unspecified functionality, but requires tedious manual analysis of undetected faults to gain useful insight. This work provides the missing link required to fully automate characterization of unspecified functionality and can formally prove the absence of Trojans. Our approach is to mine simulation traces generated during mutation testing to produce assertions characterizing verification holes or unspecified functionality. These assertions can be fed directly to Trojan detection methods making securing unspecified functionality a completely automated process. Our trace mining technique is able to identify unspecified Wishbone bus functionality in a Trojan-free UART core and verify the functionality is benign, while flagging the same functionality in a Trojan-infected version of the design.
展开▼
