ForASec: Formal Analysis of Security Vulnerabilities in Sequential Circuits
This addresses the problem of efficient and comprehensive security analysis for integrated circuit designers, though it is incremental as it builds on existing model checking methods.
The paper tackles the computationally intensive and incomplete security vulnerability analysis of sequential circuits by proposing a novel model checking-based methodology that partitions the state-space for distributed analysis, achieving approximately 11x to 16x speedup compared to state-of-the-art techniques.
Security vulnerability analysis of Integrated Circuits using conventional design-time validation and verification techniques (like simulations, emulations, etc.) is generally a computationally intensive task and incomplete by nature, especially under limited resources and time constraints. To overcome this limitation, we propose a novel methodology based on model checking to formally analyze security vulnerabilities in sequential circuits while considering side-channel parameters like propagation delay, switching power, and leakage power. In particular, we present a novel algorithm to efficiently partition the state-space into corresponding smaller state-spaces to enable distributed security analysis of complex sequential circuits and thereby mitigating the associated state-space explosion due to their feedback loops. We analyze multiple ISCAS89 and trust-hub benchmarks to demonstrate the efficacy of our framework in identifying security vulnerabilities. The experimental results show that ForASec successfully performs the complete analysis of the given complex and large sequential circuits, and provides approximately 11x to 16x speedup in analysis time compared to state-of-the-art model checking-based techniques. Moreover, it also identifies the number of gates required by an HT that can go undetected for a given design and variability conditions.