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

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

Research output: Contribution to journalArticlepeer-review


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× - 10× speedup in analysis time compared to the state-of-the-art model checking-based techniques.

Original languageEnglish (US)
Pages (from-to)1167-1180
Number of pages14
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Issue number4
StatePublished - Apr 1 2022


  • Analytical models
  • Formal Verification
  • Gate-level modeling.
  • Hardware
  • Hardware Trojans
  • Integrated circuit modeling
  • Logic gates
  • Model Checking
  • Security
  • Security Vulnerabilities
  • Sequential circuits
  • Trojan horses
  • Hardware trojans (HTs)
  • Security vulnerabilities
  • Gate-level modeling
  • Model checking
  • Formal verification

ASJC Scopus subject areas

  • Software
  • Electrical and Electronic Engineering
  • Computer Graphics and Computer-Aided Design


Dive into the research topics of 'ForASec: Formal Analysis of Hardware Trojan-Based Security Vulnerabilities in Sequential Circuits'. Together they form a unique fingerprint.

Cite this