ForASec: Formal Analysis of Hardware Trojan-Based Security Vulnerabilities in Sequential Circuits
The work
| Authors | Faiq Khalid; Imran Hafeez Abbassi; Semeen Rehman; Awais Mehmood Kamboh; Osman Hasan; Muhammad Shafique |
|---|---|
| Editors | |
| Type | article |
| Year | 2022 |
| Citekey | khalid2022forasec |
Where it appeared
| Published in | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |
|---|---|
| Volume | 41 |
| Issue | 4 |
| Pages | 1167--1180 |
Identifiers
| arXiv | 1812.05446 from its landing_page_url |
|---|---|
| DOI | 10.1109/tcad.2021.3061524 |
Access
| Landing page | https://arxiv.org/abs/1812.05446 |
|---|
Related
| Distinct from | abbasi2013formal |
|---|---|
| Distinct from | iman2025special |
| Distinct from | parrot2023design |
| Distinct from | tollec2024faultresistant |
From bibtex.
Abstract
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.
A copy is held
pdf, 2.1 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-18 03:14 UTC |
| Approved by | a person 2026-10-05 21:13 UTC |
Filed under
Cite it as
@article{khalid2022forasec,
title = {ForASec: Formal Analysis of Hardware Trojan-Based Security Vulnerabilities in Sequential Circuits},
author = {Faiq Khalid and Imran Hafeez Abbassi and Semeen Rehman and Awais Mehmood Kamboh and Osman Hasan and Muhammad Shafique},
year = {2022},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
volume = {41},
number = {4},
pages = {1167--1180},
doi = {10.1109/tcad.2021.3061524},
}
This record lives at https://refs.drheap.org/khalid2022forasec/ and will keep doing so.