Robust Constant-Time Cryptography
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan
摘要
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.
问问这篇 Paper
问问你的智能体。
Lune 读过与它相关的顶会 Paper,每个回答都会注明依据哪几篇。
引用它的顶会 Paper2
- Avoiding Instruction-Centric Microarchitectural Timing Channels Via Binary-Code TransformationsMichael Flanders, Reshabh K. Sharma, Alexandra E. Michael, Dan Grossman 等ASPLOS 2024 · 被引用 4 次
- dfence: Fine-Grained Speculation Barriers for Efficient and Effective Hardware-Software Protection in the Spectre EraDavide Davoli, Marton Bognar, Lesly-Ann Daniel, Benjamin Gregoire 等CCS 2026 · 被引用 1 次
相关 Paper
- Enforcing Fine-grained Constant-time PoliciesBasavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte 等CCS 2022 · 被引用 11 次
- Constant-time foundations for the new spectre eraSunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen 等PLDI 2020 · 被引用 90 次
- Formal verification of a constant-time preserving C compilerGilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin 等POPL 2020 · 被引用 77 次
- Typing High-Speed Cryptography against Spectre v1Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte 等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 等S&P 2022 · 被引用 61 次
