Paper 2020/572

HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms)

Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, and Santiago Zanella-Béguelin

Abstract

We present a new methodology for building formally verified cryptographic libraries that are optimized for multiple architectures. In particular, we show how to write and verify generic crypto code in the F* programming language that exploits single-instruction multiple data (SIMD) parallelism. We show how this code can be compiled to platforms that supports vector instructions, including ARM Neon and Intel AVX, AVX2, and AVX512. We apply our methodology to obtain verified vectorized implementations on all these platforms for the Chacha20 encryption algorithm, the Poly1305 one-time MAC, and the SHA-2 and Blake2 families of hash algorithms. A distinctive feature of our approach is that we aggressively share code and verification effort between scalar and vectorized code, between vectorized code for different platforms, and between implementations of different cryptographic primitives. By doing so, we significantly reduce the manual effort needed to add new implementations to our verified library. In this paper, we describe our methodology and verification results, evaluate the performance of our code, and describe its integration into the larger HACL⋆ crypto library. Our vectorized code has already been incorporated into several software projects, including the Firefox web browser.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint. MINOR revision.
Keywords
Formal VerificationHigh Assurance Cryptography
Contact author(s)
karthikeyan bhargavan @ inria fr
History
2020-10-26: last of 2 revisions
2020-05-16: received
See all versions
Short URL
https://ia.cr/2020/572
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2020/572,
      author = {Marina Polubelova and Karthikeyan Bhargavan and Jonathan Protzenko and Benjamin Beurdouche and Aymeric Fromherz and Natalia Kulatova and Santiago Zanella-Béguelin},
      title = {HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms)},
      howpublished = {Cryptology ePrint Archive, Paper 2020/572},
      year = {2020},
      note = {\url{https://eprint.iacr.org/2020/572}},
      url = {https://eprint.iacr.org/2020/572}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.