Securing Cryptographic Software via Typed Assembly Language
Shixin Song, Tingzhen Dong, Kosi Nwabueze, Julian Zanders, Andres Erbsen, Adam Chlipala, Mengjia Yan
2025Year
Abstract
Authors of cryptographic software are well aware that their code should not leak secrets through its timing behavior, and, until 2018, they believed that following industry-standard constant-time coding guidelines was sufficient. However, the revelation of the Spectre family of speculative execution attacks injected new complexities.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext b4ad4776-4939-4fe1-b9a3-870a9be410fcBuilds on33
- Spectre Attacks: Exploiting Speculative ExecutionPaul Kocher, Jann Horn, Anders Fogh, Daniel Genkin et al.S&P 2019 · 2,435 citations
- DRAMA: Exploiting DRAM Addressing for Cross-CPU AttacksPeter Pessl, Daniel Gruss, Clémentine Maurice, Michael Schwarz et al.USENIX Security 2016 · 500 citations
- Leaky Cauldron on the Dark Land: Understanding Memory Side-Channel Hazards in SGXWenhao Wang, Guoxing Chen, Xiaorui Pan, Yinqian Zhang et al.CCS 2017 · 403 citations
- Translation Leak-aside Buffer: Defeating Cache Side-channel Protections with TLB AttacksBen Gras, Kaveh Razavi, Herbert Bos, Cristiano GiuffridaUSENIX Security 2018 · 357 citations
- ret2spec: Speculative Execution Using Return Stack BuffersGiorgi Maisuradze, Christian RossowCCS 2018 · 282 citations
Related papers
- Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants)Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire et al.ASPLOS 2025 · 1 citation
- Declassiflow: A Static Analysis for Modeling Non-Speculative Knowledge to Relax Speculative Execution Security MeasuresRutvik Choudhary, Alan Wang, Zirui Neil Zhao, Adam Morrison et al.CCS 2023 · 4 citations
- Spectre Declassified: Reading from the Right Place at the Wrong TimeBasavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi et al.S&P 2023
- Typing High-Speed Cryptography against Spectre v1Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte et al.S&P 2023
- Decompiling for Constant-Time AnalysisSantiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Youcef Bouzid et al.OOPSLA 2026 · 1 citation
