HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms)
| Autor: | Santiago Zanella-Béguelin, Natalia Kulatova, Benjamin Beurdouche, Marina Polubelova, Jonathan Protzenko, Aymeric Fromherz, Karthikeyan Bhargavan |
|---|---|
| Přispěvatelé: | Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Microsoft Research, Carnegie Mellon University [Pittsburgh] (CMU), Programming securely with cryptography (PROSECCO ) |
| Jazyk: | angličtina |
| Předmět: |
Cryptographic primitive
business.industry Computer science Hash function 020207 software engineering Cryptography 02 engineering and technology Parallel computing Encryption [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Software 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing SIMD business Implementation Formal verification ComputingMilieux_MISCELLANEOUS |
| Zdroj: | Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, Nov 2020, Virtual Event, United States CCS |
| DOI: | 10.1145/3372297.3423352 |
| Popis: | 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 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 HACL* crypto library. Our vectorized code has already been incorporated into several software projects, including the Firefox web browser. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|