A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators
The work
| Authors | Anna Lena Duque Antón; Johannes Müller; Lucas Deutschmann; Mohammad Rahmani Fadiheh; Dominik Stoffel; Wolfgang Kunz |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2024 |
| Citekey | anton2024goldenfree |
Where it appeared
| Published in | Design, Automation and Test in Europe Conference (DATE '24) |
|---|
Identifiers
| arXiv | 2312.06515 from its landing_page_url |
|---|
Access
| Landing page | https://arxiv.org/abs/2312.06515 |
|---|
Related
| Distinct from | bhunia2014hardware |
|---|---|
| Distinct from | bloem2018formal |
| Distinct from | ganesan2021effective |
| Distinct from | gupta2022securing |
| Distinct from | lyu2026rtl2lean |
| Distinct from | sarma2026controllerdatapath |
| Distinct from | thornton2026version |
| Distinct from | trippel2021fuzzing |
| Distinct from | yin2025boole |
From bibtex.
Abstract
The threat of hardware Trojans (HTs) in security-critical IPs like cryptographic accelerators poses severe security risks. The HT detection methods available today mostly rely on golden models and detailed circuit specifications. Often they are specific to certain HT payload types, making pre-silicon verification difficult and leading to security gaps. We propose a novel formal verification method for HT detection in non-interfering accelerators at the Register Transfer Level (RTL), employing standard formal property checking. Our method guarantees the exhaustive detection of any sequential HT independently of its payload behavior, including physical side channels. It does not require a golden model or a functional specification of the design. The experimental results demonstrate efficient and effective detection of all sequential HTs in accelerators available on Trust-Hub, including those with complex triggers and payloads.
A copy is held
pdf, 389.7 kB. 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-17 03:33 UTC |
| Approved by | a person 2026-09-17 17:01 UTC |
Filed under
Cite it as
@inproceedings{anton2024goldenfree,
title = {A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators},
author = {Anna Lena Duque Antón and Johannes Müller and Lucas Deutschmann and Mohammad Rahmani Fadiheh and Dominik Stoffel and Wolfgang Kunz},
year = {2024},
booktitle = {Design, Automation and Test in Europe Conference (DATE '24)},
}
This record lives at https://refs.drheap.org/anton2024goldenfree/ and will keep doing so.