Paper 2024/1070
Protecting cryptographic code against Spectre-RSB
Abstract
It is fundamental that executing cryptographic software must not leak secrets through side-channels. For software-visible side-channels, it was long believed that "constant-time" programming would be sufficient as a systematic countermeasure. However, this belief was shattered in 2018 by attacks exploiting speculative execution—so called Spectre attacks. Recent work shows that language support suffices to protect cryptographic code with minimal overhead against one class of such attacks, Spectre v1, but leaves an open question of whether this result can be extended to also cover other classes of Spectre attacks. In this paper, we answer this question in the affirmative: We design, validate, implement, and verify an approach to protect cryptographic implementations against all known classes of Spectre attacks—the main challenge in this endeavor is attacks exploiting the return stack buffer, which are known as Spectre-RSB. Our approach combines a new value-dependent information-flow type system that enforces speculative constant-time in an idealized model of transient execution and a compiler transformation that realizes this idealized model on the generated low-level code. Using the Coq proof assistant, we prove that the type system is sound with respect to the idealized semantics and that the compiler transformation preserves speculative constant-time. We implement our approach in the Jasmin framework for high-assurance cryptography and demonstrate that the overhead incurred by full Spectre protections is below 2% for most cryptographic primitives and reaches only about 5–7% for the more complex post-quantum key-encapsulation mechanism Kyber.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- High-assurance cryptoformal methodsimplementationSpectre
- Contact author(s)
-
santiago arranz-olmos @ mpi-sp org
gilles barthe @ mpi-sp org
c chuengsatiansup @ unimelb edu au
benjamin gregoire @ inria fr
vincent laporte @ inria fr
tiago oliveira @ sandboxquantum com
peter @ cryptojedi org
yuval yarom @ rub de
zhiyuanz5 @ student unimelb edu au - History
- 2024-07-02: approved
- 2024-07-01: received
- See all versions
- Short URL
- https://ia.cr/2024/1070
- License
-
CC0
BibTeX
@misc{cryptoeprint:2024/1070, author = {Santiago Arranz Olmos and Gilles Barthe and Chitchanok Chuengsatiansup and Benjamin Grégoire and Vincent Laporte and Tiago Oliveira and Peter Schwabe and Yuval Yarom and Zhiyuan Zhang}, title = {Protecting cryptographic code against Spectre-{RSB}}, howpublished = {Cryptology {ePrint} Archive, Paper 2024/1070}, year = {2024}, url = {https://eprint.iacr.org/2024/1070} }