- author = "Joel Kuepper and Andres Erbsen and Jason Gross and Owen Conoly and Chuyue Sun and Samuel Tian and David Wu and Adam Chlipala and Chitchanok Chuengsatiansup and Daniel Genkin and Markus Wagner and Yuval Yarom",
- title = "{CryptOpt}: Verified Compilation with Randomized Program Search for Cryptographic Primitives",
- booktitle = "44th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2023",
- year = "2023",
- editor = "Nate Foster",
- pages = "article no. 158",
- address = "Orlando, Florida",
- month = "17-21 " # jun,
- publisher = "Association for Computing Machinery",
- note = "{Gold winner 2023 HUMIES, PLDI Distinguished Paper}",
- keywords = "genetic algorithms, genetic programming, Genetic Improvement, SBSE, elliptic-curve cryptography, search-based software engineering, assembly, Software and its engineering, Source code generation, Security and privacy, Public key (asymmetric) techniques, Logic and verification, General and reference, Performance Measurement, Theory of computation, Cryptographic primitives",
-
URL = "
https://pldi23.sigplan.org/details/pldi-2023-pldi/53/CryptOpt-Verified-Compilation-with-Randomized-Program-Search-for-Cryptographic-Primi",
-
URL = "https://arxiv.org/abs/2211.10665",
-
URL = "https://human-competitive.org/sites/default/files/humies_3.txt",
-
URL = "
https://human-competitive.org/sites/default/files/pldi23main-p326-final.pdf",
-
URL = "https://doi.org/10.1145/3591272",
-
DOI = "
doi:10.1145/3591272",
- size = "25 pages",
- abstract = "We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic functional programs into assembly code significantly faster than what GCC or Clang produce, with mechanized proof (in Coq) whose final theorem statement mentions little beyond the input functional program and the operational semantics of x86-64 assembly. On the optimization side, we apply randomized search through the space of assembly programs, with repeated automatic benchmarking on target CPUs. On the formal-verification side, we connect to the Fiat Cryptography framework (which translates functional programs into C-like IR code) and extend it with a new formally verified program-equivalence checker, incorporating a modest subset of known features of SMT solvers and symbolic-execution engines. The overall prototype is quite practical, e.g. producing new fastest-known implementations of finite-field arithmetic for both Curve25519 (part of the TLS standard) and the Bitcoin elliptic curve secp256k1 for the Intel 12 and 13 generations.",
-
notes = "See also \cite{Chuengsatiansup:2022:GI}
Mon 19 Jun 2023 09:40 - 10:00 at Royal - PLDI: Welcome & Opening Session Chair(s): Nate Foster
University of Adelaide, Australia",
