- author = "Joel Kuepper",
- title = "Enhancing State-of-the-Art Techniques Generating Low-Level Code for Cryptographic Arithmetic",
- school = "School of Computer and Mathematical Sciences, Faculty of Sciences, Engineering, and Technology, The University of Adelaide",
- year = "2024",
- address = "Australia",
- month = sep,
- keywords = "genetic algorithms, genetic programming, Genetic Improvement, Bitcoin Core (LLVM), JSON CryptOpt",
-
URL = "
https://yuval.yarom.org/pdfs/Kuepper24.pdf",
- size = "221 pages",
-
abstract = "Fast cryptography is a crucial enabler for modern
communication over the Internet. It provides
authenticity, confidentiality, integrity, and
non-repudiation in the vast majority of web traffic to
date. Its ubiquitous deployment makes correctness and
high speed of paramount importance.
The status quo for achieving high speed in cryptography is that implementations are written manually in assembly languages and hand-optimised by domain experts. While achieving high speeds, this process is tedious and error-prone. Prior work has shown how those hand-written implementations can be formally verified, and other work has shown how to optimise existing implementations. However, both approaches require significant manual effort.
This thesis presents CryptOpt, an optimising code generator that uses Genetic Improvement to automatically generate those high-speed assembly implementations. While doing so, the emitted code preserves enough structure to enable mechanised correctness validation.
CryptOpt uses a random local search heuristic. It starts by implementing the target function correctly. It then randomly mutates this implementation to generate a different implementation that is semantically equivalent. CryptOpt then runs both implementations on the target hardware and keeps the more performant one. By repeating those steps iteratively, the performance of the code is gradually improved. The main benefit of this technique is that the microarchitecture can be treated as an opaque unit, as opposed to the need for manual micro-architecture modeling in other approaches.
CryptOpt seamlessly integrates into Fiat Cryptography, a framework that follows a correct-by-construction approach for the automatic generation of cryptographic code. Before this thesis, Fiat Cryptography bottomed out at higher-level languages like C or Rust. Now, the formal correctness guarantees are extended to the assembly level.
The resulting optimised implementations are up to 2.96 times faster than what off-the-shelf compilers produce. For Curve25519 (part of the TLS standard) and the Bitcoin elliptic curve, the newly generated code is as fast as hand-written implementations on average, and can outperform on latest microarchitectures. The CryptOpt-generated code for Curve-25519 is integrated into BoringSSL, the cryptographic library that powers Google Chrome and Microsoft Edge",
-
notes = "29 Oct 2024
https://yuval.yarom.org/news.php
Supervisors: Yuval Yarom, Chitchanok Chuengsatiansup, Markus Wagners",
