Robust Constant-Time Cryptography
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan
Abstract
Cryptographic library developers take care to ensure their library does not leak secrets even when there are (inevitably) exploitable vulnerabilities in the applications the library is linked against. To do so, they choose some class of application vulnerabilities to defend against and hardcode protections against those vulnerabilities in the library code. A single set of choices is a poor fit for all contexts: a chosen protection could impose unnecessary overheads in contexts where those attacks are impossible, and an ignored protection could render the library insecure in contexts where the attack is feasible. We introduce RoboCop , a new methodology and toolchain for building secure and efficient applications from cryptographic libraries, via four contributions. First, we present an operational semantics that describes the behavior of a (cryptographic) library executing in the context of a potentially vulnerable application so that we can precisely specify what different attackers can observe. Second, we use our semantics to define a novel security property, Robust Constant Time (RCT), that defines when a cryptographic library is secure in the context of a vulnerable application. Crucially, our definition is parameterized by an attacker model, allowing us to factor out the classes of attackers that a library may wish to secure against. This refactoring yields our third contribution: a compiler that can synthesize bespoke cryptographic libraries with security tailored to the specific application context against which the library will be linked, guaranteeing that the library is RCT in that context. Finally, we present an empirical evaluation that shows the RoboCop compiler can automatically generate code to efficiently protect a wide range (over 500) of cryptographic library primitives against three classes of attacks: read gadgets (due to application memory safety vulnerabilities), speculative read gadgets (due to application speculative execution vulnerabilities), and concurrent observations (due to application threads), with performance overhead generally under 2% for protections from read gadgets and under 4% for protections from speculative read gadgets, thus freeing library developers from making one-size-fits-all choices between security and performance.
Ask about this paper
Ask your agent about it.
Lune has read the top-tier papers around this one, so every answer names the papers it rests on.
Your agent calls
Lunesearch_papers
Free to start. No credit card required.
Terminal
Install the CLIlune papers get 6dc34d8a-b894-4afc-a2bd-7850ab194720Cited by top-tier papers2
- Avoiding Instruction-Centric Microarchitectural Timing Channels Via Binary-Code TransformationsMichael Flanders, Reshabh K. Sharma, Alexandra E. Michael, Dan Grossman et al.ASPLOS 2024 · 4 citations
- dfence: Fine-Grained Speculation Barriers for Efficient and Effective Hardware-Software Protection in the Spectre EraDavide Davoli, Marton Bognar, Lesly-Ann Daniel, Benjamin Gregoire et al.CCS 2026 · 1 citation
Related papers
- Enforcing Fine-grained Constant-time PoliciesBasavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte et al.CCS 2022 · 11 citations
- Constant-time foundations for the new spectre eraSunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen et al.PLDI 2020 · 90 citations
- Formal verification of a constant-time preserving C compilerGilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin et al.POPL 2020 · 77 citations
- Typing High-Speed Cryptography against Spectre v1Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte et al.S&P 2023
- "They're not that hard to mitigate": What Cryptographic Library Developers Think About Timing AttacksJan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt et al.S&P 2022 · 61 citations
