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^{th}$ and $13^{th}$ generations.

翻译：摘要：大多数软件领域依赖编译器将高级代码翻译为多种不同的机器语言，其性能与开发者愿意直接编写汇编语言的耐心水平相比不会差太多。然而，密码学是一个例外，其许多性能关键型例程直接以汇编语言编写（有时通过元编程层）。过去的一些工作展示了如何对该汇编代码进行形式化验证，另一些工作则展示了如何自动生成C代码及其形式化证明，但会引入与已知最优汇编代码相比的性能损失。我们提出CryptOpt，这是首个专用编译流水线，能将高级密码学函数式程序编译为显著优于GCC或Clang生成的汇编代码，并提供机械化证明（基于Coq），其最终定理陈述几乎仅涉及输入函数式程序和x86-64汇编的操作语义。在优化方面，我们通过对汇编程序空间进行随机化搜索，并在目标CPU上重复自动基准测试。在形式化验证方面，我们连接了Fiat Cryptography框架（该框架将函数式程序翻译为类C的IR代码），并扩展了一个新的经形式化验证的程序等价检查器，该检查器整合了SMT求解器和符号执行引擎的已知功能的适度子集。整体原型非常实用，例如为Curve25519（TLS标准的一部分）和比特币椭圆曲线secp256k1生成了已知最快的有限域算术实现，适用于Intel第12代和第13代处理器。