Symbolic execution based test-patterns generation algorithm for hardware Trojan detection. Issue 78 (September 2018)

• Record Type: Journal Article
• Authors: Shen, Lixiang; Mu, Dejun; Cao, Guo; Qin, Maoyuan; Blackstone, Jeremy; Kastner, Ryan
• Is Part Of: Computers & security. Issue 78(2018)
• Page Start: 267
• Page End: 280
• Publication Date: 2018-09
• Subjects: Hardware Trojan -- Symbolic execution -- Satisfiability modulo theory -- Metamorphic testing -- Control flow graph; Computer security -- Periodicals; Electronic data processing departments -- Security measures -- Periodicals; 005.805
• DOI: 10.1016/j.cose.2018.07.006
• Languages: English
• ISSNs: 0167-4048

Abstract

Abstract: Hardware Trojan detection is a very difficult challenge. However, the combination of symbolic execution and metamorphic testing is useful for detecting hardware Trojans in Verilog code. In this paper, symbolic execution and metamorphic testing were combined to detect internal conditionally triggered hardware Trojans in the register-transfer level design. First, control flow graphs of Verilog code were generated. Next, parallel symbolic execution and satisfiability modulo theories solver generated test patterns. Finally, metamorphic testing detected the hardware Trojans. The work used Trust-Hub benchmarks in experiments.