Paper 2020/1104

High-Assurance Cryptography Software in the Spectre Era

Gilles Barthe, Sunjay Cauligi, Benjamin Gregoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, and Peter Schwabe


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.

Available format(s)
Publication info
Published elsewhere. Proceedings of the IEEE Symposium on Security and Privacy, 2021
high-assurance cryptographyverificationside-channel resistancespeculative execution
Contact author(s)
kevliao @ mit edu
2021-01-15: revised
2020-09-15: received
See all versions
Short URL
Creative Commons Attribution


      author = {Gilles Barthe and Sunjay Cauligi and Benjamin Gregoire and Adrien Koutsos and Kevin Liao and Tiago Oliveira and Swarn Priya and Tamara Rezk and Peter Schwabe},
      title = {High-Assurance Cryptography Software in the Spectre Era},
      howpublished = {Cryptology ePrint Archive, Paper 2020/1104},
      year = {2020},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.