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 paper, 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 distributed HT-based security analysis of complex sequential circuits. We analyze multiple ISCAS89 and trust-hub benchmarks for different ASIC technologies, i.e., 65nm, 45nm, and 22nm, 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 6x to 10x speedup in analysis time compared to state-of-the-art model checking-based techniques.

Original languageEnglish (US)
Pages (from-to)1167-1180
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

ASJC Scopus subject areas

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


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