ForASec: Formal Analysis of Hardware Trojan-Based Security Vulnerabilities in Sequential Circuits

In this article, we propose a novel model checking-based methodology that analyzes the hardware trojan (HT)-based security vulnerabilities in sequential circuits with 100% coverage while addressing the state-space explosion issue and completeness issue. In this work, the state-space explosion issue is addressed by efficiently partitioning the larger state space into corresponding smaller state spaces to enable the distributed HT-based security analysis of complex sequential circuits. We analyze multiple ISCAS89 and trust-hub benchmarks for different ASIC technologies, i.e., 65, 45, and 22 nm, to demonstrate the efficacy of our framework in identifying HT-based security vulnerabilities. The experimental results show that ForASec successfully performs the complete analysis of the given complex and large sequential circuits, and provides approximately 6 x-10 x speedup in analysis time compared to the state-of-the-art model checking-based techniques.