一句话：首个将高层密码函数式程序编译为汇编的流水线，通过随机搜索与 Coq 机器化证明，生成比 GCC/Clang 更快的代码。
密码学中许多性能关键例程长期以手写汇编实现，已有工作或对汇编做形式验证，或自动生成带证明的 C 代码，但性能不如最佳手工汇编。本文提出 CryptOpt，一个将高层密码函数式程序特化为汇编代码的编译流水线。优化侧，它在汇编程序空间中进行随机搜索，并在目标 CPU 上反复自动基准测试以挑选最优实现；验证侧，它接入 Fiat Cryptography 框架（该框架把函数式程序翻译为类 C 的 IR），并新增一个经形式验证的程序等价检查器，内嵌 SMT 求解器与符号执行引擎的部分机制。最终机器化证明（Coq）的定理只涉及输入函数式程序与 x86-64 汇编的操作语义。原型系统实用性强，为 TLS 标准中的 Curve25519 与比特币椭圆曲线 secp256k1 在 Intel 第 12、13 代处理器上生成了新的最快已知有限域算术实现。
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 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.
@article{paperbot1998,
title = {CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives},
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},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591272}
}