Skip to Main content Skip to Navigation
New interface
Conference papers

High-Assurance Cryptography in the Spectre Era

Abstract : High-assurance cryptography leverages methods from program verification and cryptography engineering to deliver efficient cryptographic software with machine-checked proofs of memory safety, functional correctness, provable security, and absence of timing leaks. Traditionally, these guarantees are established under a sequential execution semantics. However, this semantics is not aligned with the behavior of modern processors that make use of speculative execution to improve performance. This mismatch, combined with the high-profile Spectre-style attacks that exploit speculative execution, naturally casts doubts on the robustness of high-assurance cryptography guarantees. In this paper, we dispel these doubts by showing that the benefits of high-assurance cryptography extend to speculative execution, costing only a modest performance overhead. We build atop the Jasmin verification framework an end-to-end approach for proving properties of cryptographic software under speculative execution, and validate our approach experimentally with efficient, functionally correct assembly implementations of ChaCha20 and Poly1305, which are secure against both traditional timing and speculative execution attacks.
Document type :
Conference papers
Complete list of metadata
Contributor : Tamara Rezk Connect in order to contact the contributor
Submitted on : Wednesday, September 22, 2021 - 8:38:35 PM
Last modification on : Wednesday, November 30, 2022 - 11:22:07 AM
Long-term archiving on: : Thursday, December 23, 2021 - 7:23:18 PM


Files produced by the author(s)




Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, et al.. High-Assurance Cryptography in the Spectre Era. S&P 2021 - IEEE Symposium of Security and Privacy, May 2021, Virtual, France. ⟨10.1109/SP40001.2021.00046⟩. ⟨hal-03352062⟩



Record views


Files downloads