Paper 2022/1270

Typing High-Speed Cryptography against Spectre v1

Basavesh Ammanaghatta Shivakumar, Max Planck Institute for Security and Privacy
Gilles Barthe, Max Planck Institute for Security and Privacy, IMDEA Software
Benjamin Grégoire, Inria Sophia Antipolis - Méditerranée
Vincent Laporte, Inria Nancy - Grand Est, Université de Lorraine
Tiago Oliveira, Max Planck Institute for Security and Privacy
Swarn Priya, Inria Sophia Antipolis - Méditerranée
Peter Schwabe, Max Planck Institute for Security and Privacy, Radboud University
Lucas Tabary-Maujean, École Normale Supérieure Paris-Saclay
Abstract

The current gold standard of cryptographic software is to write efficient libraries with systematic protections against timing attacks. In order to meet this goal, cryptographic engineers increasingly use high-assurance cryptography tools. These tools guide programmers and provide rigorous guarantees that can be verified independently by library users. However, high-assurance tools reason about overly simple execution models that elide micro-architectural leakage. Thus, implementations validated by high-assurance cryptography tools remain potentially vulnerable to micro-architectural attacks such as Spectre or Meltdown. Moreover, proposed countermeasures are not used in practice due to performance overhead. We propose, analyze, implement and evaluate an approach for writing efficient cryptographic implementations that are protected against Spectre v1 attacks. Our approach ensures speculative constant-time, an information flow property which guarantees that programs are protected against Spectre v1. Speculative constant-time is enforced by means of a (value-dependent) information flow type system. The type system tracks security levels depending on whether execution is misspeculating. We implement our approach in the Jasmin framework for high assurance cryptography, and use it for protecting all implementations of an experimental cryptographic library that includes highly optimized implementations of symmetric primitives, of elliptic-curve cryptography, and of Kyber, a lattice-based KEM recently selected by NIST for standardization. The performance impact of our protections is very low; for example, less than 1% for Kyber and essentially zero for X25519.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint.
Keywords
High-assurance crypto formal methods implementation
Contact author(s)
basavesh shivakumar @ mpi-sp org
gilles barthe @ mpi-sp org
benjamin gregoire @ inria fr
Vincent Laporte @ inria fr
tfaoliveira @ gmail com
swarn priya @ inria fr
peter @ cryptojedi org
lucas tabary @ ens-paris-saclay fr
History
2022-09-26: approved
2022-09-25: received
See all versions
Short URL
https://ia.cr/2022/1270
License
No rights reserved
CC0

BibTeX

@misc{cryptoeprint:2022/1270,
      author = {Basavesh Ammanaghatta Shivakumar and Gilles Barthe and Benjamin Grégoire and Vincent Laporte and Tiago Oliveira and Swarn Priya and Peter Schwabe and Lucas Tabary-Maujean},
      title = {Typing High-Speed Cryptography against Spectre v1},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1270},
      year = {2022},
      note = {\url{https://eprint.iacr.org/2022/1270}},
      url = {https://eprint.iacr.org/2022/1270}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.