HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)
- Marina Polubelova ,
- Karthikeyan Bhargavan ,
- Jonathan Protzenko ,
- Benjamin Beurdouche ,
- Aymeric Fromherz ,
- Natalia Kulatova ,
- Santiago Zanella-Béguelin
ACM Conference on Computer and Communications Security (CCS) |
Published by ACM | Organized by ACM
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 support 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 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 HACL* cryptographic library. Our vectorized code has already been incorporated into several software projects, including the Firefox web browser.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Permissions@acm.org. CCS ’20, November 9–13, 2020, Virtual Event, USA. © 2020 Association of Computing Machinery.
Publication Downloads
EverCrypt
June 26, 2019
EverCrypt is a high-performance, cross-platform, formally verified modern cryptographic provider distributed as a combined C/ASM library. EverCrypt packages cryptographic implementations from the HACL* and ValeCrypt projects, and automatically picks the fastest one available, depending on processor support and the target execution environment (multiplexing). Furthermore, EverCrypt offers an (agile) API that makes it simple to switch between algorithms (e.g., from SHA2 to SHA3). Code from EverCrypt has been integrated in Linux, Firefox, the Tezos blockchain, the Election Guard project, and many more.