CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives
复制标题
DOI：
10.1145/3591272
复制
发表时间：
2023-06
影响因子：
--
通讯作者：
Joel Kuepper;Andres Erbsen;Jason Gross;Owen Conoly;Chuyue Sun;Samuel Tian;David Wu;A. Chlipala;C. Chuengsatiansup;Daniel Genkin;Markus Wagner;Y. Yarom
中科院分区：
文献类型：
--
作者：
Joel Kuepper;Andres Erbsen;Jason Gross;Owen Conoly;Chuyue Sun;Samuel Tian;David Wu;A. Chlipala;C. Chuengsatiansup;Daniel Genkin;Markus Wagner;Y. Yarom
大多数软件领域依赖于编译器将高级代码翻译为多种不同的机器语言，其性能不会比开发人员有耐心直接用汇编语言编写的代码差太多。然而，密码学是一个例外，其中许多性能关键的例程直接在汇编中编写（有时通过元编程层）。过去的一些工作已经展示了如何对该程序集进行形式验证，而其他工作已经展示了如何自动生成C代码沿着形式证明，但与最知名的程序集相比，随之而来的性能损失。我们提出CryptOpt，第一个编译管道，专门高层次的加密功能程序到汇编代码显着快于GCC或Clang产生，机械化证明（在Coq），其最终定理语句提到很少超出输入功能程序和x86-64汇编的操作语义。在优化方面，我们通过汇编程序的空间应用随机搜索，并在目标CPU上重复进行自动基准测试。在形式验证方面，我们连接到菲亚特密码学框架（将功能程序转换为C类IR代码），并使用新的正式验证的程序等价性检查器对其进行扩展，将SMT求解器和符号执行引擎的已知功能的适度子集结合起来。整个原型是非常实用的，例如，为Curve 25519（TLS标准的一部分）和比特币椭圆曲线secp 256 k1生成新的已知最快的有限域算法实现，用于英特尔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.