RTL Verification for Secure Speculation Using Contract Shadow Logic
Modern out-of-order processors face speculative execution attacks. Despite various proposed software and hardware mitigations to prevent such attacks, new attacks keep arising from unknown vulnerabilities. Thus, a formal and rigorous evaluation of the ability of hardware designs to deal with speculative execution attacks is urgently desired.
Authors
- Yuheng Yang (ORCID: https://orcid.org/0000-0001-8695-5139)
- Thomas Bourgeat (ORCID: https://orcid.org/0000-0002-8468-8409)
- Mengjia Yan (ORCID: https://orcid.org/0000-0002-6206-9674)
- Qinhan Tan (ORCID: https://orcid.org/0000-0003-2475-3675)
- Sharad Malik (ORCID: https://orcid.org/0000-0002-0837-5443)
Institutions
- Princeton University (US)
- École Polytechnique Fédérale de Lausanne (CH)
- Massachusetts Institute of Technology (US)
Publication Details
- Published
- 2025-02-06
- DOI
- https://doi.org/10.1145/3669940.3707243
- Citations
- 3
- Primary Topic
- Security and Verification in Computing
- Type
- article
- Field-Weighted Citation Impact
- 7.44