An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors
The work
| Authors | Mohammad Rahmani Fadiheh; Alex Wezel; Johannes Mueller; Joerg Bormann; Sayak Ray; Jason M. Fung; Subhasish Mitra; Dominik Stoffel; Wolfgang Kunz |
|---|---|
| Editors | |
| Type | article |
| Year | 2022 |
| Citekey | fadiheh2022exhaustive |
Where it appeared
| Published in | IEEE Transactions on Computers |
|---|
Identifiers
| arXiv | 2108.01979 from its landing_page_url |
|---|---|
| DOI | 10.1109/tc.2022.3152666 |
Access
| Landing page | https://arxiv.org/abs/2108.01979 |
|---|
Related
| Contains | fadiheh2018processor |
|---|---|
| Distinct from | fadiheh2018processor |
| Distinct from | fuchs2023architectural |
| Distinct from | randal2023transient |
| Distinct from | tan2025rtl |
| Distinct from | xu2025dejavuzz |
From bibtex.
Abstract
Hardware security issues have been emerging at an alarming rate in recent years. Transient execution attacks, in particular, pose a genuine threat to the security of modern computing systems. Despite recent advances, understanding the intricate implications of microarchitectural design decisions on processor security remains a great challenge and has caused a number of update cycles in the past. This paper addresses the need for a new approach to hardware sign-off verification which guarantees the security of processors at the Register Transfer Level. To this end, we introduce a formal definition of security with respect to transient execution attacks, formulated as a hardware property. We present a formal proof methodology based on Unique Program Execution Checking (UPEC) which can be used to systematically detect all vulnerabilities to transient execution attacks in RTL designs. UPEC does not exploit any a priori knowledge on known attacks and can therefore detect also vulnerabilities based on new, so far unknown, types of channels.
A copy is held
pdf, 1.5 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-17 18:32 UTC |
| Approved by | a person 2026-10-05 21:31 UTC |
Cite it as
@article{fadiheh2022exhaustive,
title = {An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors},
author = {Mohammad Rahmani Fadiheh and Alex Wezel and Johannes Mueller and Joerg Bormann and Sayak Ray and Jason M. Fung and Subhasish Mitra and Dominik Stoffel and Wolfgang Kunz},
year = {2022},
journal = {IEEE Transactions on Computers},
doi = {10.1109/tc.2022.3152666},
}
This record lives at https://refs.drheap.org/fadiheh2022exhaustive/ and will keep doing so.