一句话：在 F* 中嵌入 x64 汇编子集，借助依赖类型检查器运行经验证的 VC 生成器，实现汇编与 C 互操作的高效验证。
高性能密码库常混合高级语言与汇编代码，要形式验证这类混合程序的正确性与安全性颇具挑战。本文在 F* 中嵌入 x64 汇编的一个子集，支持验证汇编代码及其与 F* 生成的 C 代码的互操作。关键思想是利用依赖类型系统的类型检查器，在类型检查期间运行一个经过验证的验证条件生成器，从而定制发送给 SMT 求解器的验证条件。作者结合 proof-by-reflection 风格与 SMT 求解，提升了汇编代码正确性证明的自动化程度，并完成了 AES-GCM 优化实现的首次正确性证明；该密码例程被 90% 的安全互联网流量使用。
High-performance cryptographic libraries often mix code written in a high-level language with code written in assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding of a subset of x64 assembly language in F* that allows efficient verification of both assembly and its interoperation with C code generated from F*. The key idea is to use the computational power of a dependent type system's type checker to run a verified verification-condition generator during type checking. This allows the embedding to customize the verification condition sent by the type checker to an SMT solver. By combining our proof-by-reflection style with SMT solving, we demonstrate improved automation for proving the correctness of assembly-language code. This approach has allowed us to complete the first-ever proof of correctness of an optimized implementation of AES-GCM, a cryptographic routine used by 90% of secure Internet traffic.
@article{paperbot626,
title = {A verified, efficient embedding of a verifiable assembly language},
author = {Aymeric Fromherz and Nick Giannarakis and Chris Hawblitzel and Bryan Parno and Aseem Rastogi and Nikhil Swamy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290376}
}