McSeVIC: A model checking based framework for security vulnerability analysis of integrated circuits

The rising trend of globalization in the integrated circuits' design process has increased their vulnerabilities against malicious intrusions. The security vulnerability analysis using conventional design time simulations is computationally intensive and incomplete by nature. Formal verification has the potential to overcome these limitations of simulation techniques; however, the existing state-of-the-art formal verification techniques cannot be used as such to analyze the effects of hardware Trojans (HTs) that may impact the performance of the circuit without altering its functionality. In this paper, we propose a novel model checking-based formal framework for a priori assessment of circuit vulnerabilities against both the functional and parametric HTs at the early stages of the design. This framework is characterized by the gate-level side channel parameters, i.e., dynamic power, leakage power, and propagation delay, to examine the impacts of malicious circuitry insertion. An algorithm based on the temporal logic properties is proposed, which computes the bounds for the side channel parameters to define the expected secure regions of circuit operation. Moreover, we propose a second algorithm for formally analyzing the security vulnerabilities in the circuit by introducing partitions, which significantly reduces the size of state space. We evaluate the masking effects on the intrusions while considering 3-sigma variation in the process. We demonstrate the effectiveness of our proposed approach by analyzing the security vulnerabilities on a set of ISCAS85 and 74× benchmarks.