Accelerating hardware security verification and vulnerability detection through state space reduction. Issue 103 (April 2021)

• Record Type: Journal Article
• Authors: Shen, Lixiang; Mu, Dejun; Cao, Guo; Qin, Maoyuan; Zhu, Jiacheng; Hu, Wei
• Is Part Of: Computers & security. Issue 103(2021)
• Publication Date: 2021-04
• Subjects: Hardware security -- Security verification -- Model checking -- State space reduction -- Hardware Trojan; Computer security -- Periodicals; Electronic data processing departments -- Security measures -- Periodicals; 005.805
• DOI: 10.1016/j.cose.2020.102167
• Languages: English
• ISSNs: 0167-4048

Abstract

Abstract: Model checking is an effective technique for formal verification of hardware security properties in order to detect security vulnerabilities. However, a major challenge lies in state space explosion. In this work, we propose methods to accelerate hardware security verification and vulnerability detection through state space reduction. Specifically, we reduce state space of formal model by performing value reduction and transition relation reduction. The control flow and data dependent graphs control the process of value reduction and transition relation reduction. In addition, we provide an approach that allows the automated mining of security properties from register-transfer-level hardware designs. Experimental results using Trust-HUB benchmarks have demonstrated that our proposed methods can significantly reduce the complexity of the formal model and thus the formal security verification time for hardware Trojan detection.