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

doi:10.1109/TCAD.2021.3061524

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

Electrical Engineering

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English (US)
Pages (from-to)	1167-1180
Number of pages	14
Journal	IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Volume	41
Issue number	4
DOIs	https://doi.org/10.1109/TCAD.2021.3061524
State	Published - Apr 1 2022

Keywords

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

Access to Document

10.1109/TCAD.2021.3061524

Cite this

@article{642523352c61497bad64c4ad8b5d648e,

title = "ForASec: Formal Analysis of Hardware Trojan-Based Security Vulnerabilities in Sequential Circuits",

abstract = "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.",

keywords = "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",

author = "Faiq Khalid and Abbassi, {Imran Hafeez} and Semeen Rehman and Kamboh, {Awais Mehmood} and Osman Hasan and Muhammad Shafique",

note = "Publisher Copyright: {\textcopyright} 1982-2012 IEEE.",

year = "2022",

month = apr,

day = "1",

doi = "10.1109/TCAD.2021.3061524",

language = "English (US)",

volume = "41",

pages = "1167--1180",

journal = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",

issn = "0278-0070",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

number = "4",

}

TY - JOUR

T1 - ForASec

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

AU - Khalid, Faiq

AU - Abbassi, Imran Hafeez

AU - Rehman, Semeen

AU - Kamboh, Awais Mehmood

AU - Hasan, Osman

AU - Shafique, Muhammad

PY - 2022/4/1

Y1 - 2022/4/1

N2 - 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.

AB - 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.

KW - Analytical models

KW - Formal Verification

KW - Gate-level modeling.

KW - Hardware

KW - Hardware Trojans

KW - Integrated circuit modeling

KW - Logic gates

KW - Model Checking

KW - Security

KW - Security Vulnerabilities

KW - Sequential circuits

KW - Trojan horses

KW - Hardware trojans (HTs)

KW - Security vulnerabilities

KW - Gate-level modeling

KW - Model checking

KW - Formal verification

UR - http://www.scopus.com/inward/record.url?scp=85104613203&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85104613203&partnerID=8YFLogxK

U2 - 10.1109/TCAD.2021.3061524

DO - 10.1109/TCAD.2021.3061524

M3 - Article

AN - SCOPUS:85104613203

SN - 0278-0070

VL - 41

SP - 1167

EP - 1180

JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

IS - 4

ER -

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

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this