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

Imran Hafeez Abbassi, Faiq Khalid, Osman Hasan, Awais Mehmood Kamboh, Muhammad Shafique

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)32240-32257
Number of pages18
JournalIEEE Access
StatePublished - Jun 11 2018


  • dynamic power
  • formal verification
  • Gate level modeling
  • hardware Trojan
  • leakage power
  • model checking
  • nuXmv model checker
  • path delay

ASJC Scopus subject areas

  • General Computer Science
  • General Materials Science
  • General Engineering


Dive into the research topics of 'McSeVIC: A model checking based framework for security vulnerability analysis of integrated circuits'. Together they form a unique fingerprint.

Cite this