Das Paper "CryptOpt: Verified Compilation with Randomized Program - Search for Cryptographic Primitives" von Yuval Yarom und weiteren internationalen Kolleg*innen hat einen Human-Competitive “Humies” Gold Award auf der diesjährigen Genetic and Evolutionary Computation Conference (GECCO 2023) gewonnen. Die Konferenz hat vom 15. bis 19. Juli in Lissabon stattgefunden und wird durchgeführt von der Special Interest Group on Genetic and Evolutionary Computation (SIGEVO) der Association for Computing Machinery (ACM). Auf der seit 1999 jährlich stattfindenden Konferenz werden die neuesten Ergebnisse im Forschungsgebiet „evolutionary computation“ präsentiert. Sie gilt als größte und führende Konferenz in dem Bereich. Der "Humies"-Wettbewerb zeichnet seit 2004 auf der GECCO Beiträge aus, die durch eine Form genetischer und evolutionärer Berechnungen Ergebnisse hervorbringen, die mit menschlichen Ergebnissen konkurrieren. Yarom ist seit April neu ernannter Professor für Computer Security am HGI und ist PI im Exzellenzcluster CASA.
Zum vollständigen Paper gelangen Sie über diesen -> Link.
Über das Paper
"CryptOpt: Verified Compilation with Randomized Program - Search for Cryptographic Primitives"
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner , Yuval Yarom
Abstract: Most software domains rely on compilers to translate high-level code to multiple different machine languages, with performance not too much worse than what developers would have the patience to write directly in assembly language. However, cryptography has been an exception, where many performance-critical routines have been written directly in assembly (sometimes through metaprogramming layers). Some past work has shown how to do formal verification of that assembly, and other work has shown how to generate C code automatically along with formal proof, but with consequent performance penalties vs. the best-known assembly. 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 for the relatively new Intel i9 12G, of finite-field arithmetic for both Curve25519 (part of the TLS standard) and the Bitcoin elliptic curve secp256k1.
Allgemeiner Hinweis: Mit einer möglichen Nennung von geschlechtszuweisenden Attributen implizieren wir alle, die sich diesem Geschlecht zugehörig fühlen, unabhängig vom biologischen Geschlecht.
