ForASec: Formal Analysis of Security Vulnerabilities in Sequential Circuits

TL;DR

This paper introduces ForASec, a formal model checking framework that efficiently detects security vulnerabilities in complex sequential circuits by partitioning state-space, significantly improving analysis speed and detection capabilities.

Contribution

The paper presents a novel partitioning algorithm for distributed security analysis of sequential circuits, enabling scalable and complete vulnerability detection.

Findings

Achieves 11x to 16x speedup over existing methods

Successfully analyzes large benchmarks like ISCAS89 and trust-hub

Identifies undetectable gates under variability conditions

Abstract

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.