Paper 2024/1070

Protecting cryptographic code against Spectre-RSB

Santiago Arranz Olmos, Max Planck Institute for Security and Privacy
Gilles Barthe, Max Planck Institute for Security and Privacy, IMDEA Software
Chitchanok Chuengsatiansup, University of Melbourne
Benjamin Grégoire, Research Centre Inria Sophia Antipolis
Vincent Laporte, Centre Inria de l'Université de Lorraine
Tiago Oliveira, SandboxAQ
Peter Schwabe, Max Planck Institute for Security and Privacy, Radboud University Nijmegen
Yuval Yarom, Ruhr University Bochum
Zhiyuan Zhang, University of Melbourne
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
No rights reserved
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}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.