一句话：在 F* 的 Low* 工具链中提出语言技术，使高层模块化验证代码可特化并编译为零开销 C 代码。
该工作关注大规模低层高效安全代码验证中的结构、架构与工程问题：如何在高抽象层模块化编写并验证代码，同时控制编译过程并生成可集成到主流软件的低开销 C 代码。作者在 F* 证明助手的浅嵌入 Low* 工具链中设计并实现了一组语言级技术，支持模块化验证、代码特化与零成本抽象。评估表明，这些技术对 HACL 库扩展到超过 10 万行已验证源码、提升证明工程师生产力至关重要。最后以流式 API 为案例，通用地刻画其语义并复用到十余个场景，其中六个进入 Python 参考实现，替代了曾含 CVE 的 C 代码。
For all the successes in verifying low-level, efficient, security-critical code, little has been said or studied about the structure, architecture and engineering of such large-scale proof developments. We present the design, implementation and evaluation of a set of language-based techniques that allow the programmer to modularly write and verify code at a high level of abstraction, while retaining control over the compilation process and producing high-quality, zero-overhead, low-level code suitable for integration into mainstream software. We implement our techniques within the F proof assistant, and specifically its shallowly-embedded Low toolchain that compiles to C. Through our evaluation, we establish that our techniques were critical in scaling the popular HACL library past 100,000 lines of verified source code, and brought about significant gains in proof engineer productivity. The exposition of our methodology converges on one final, novel case study: the streaming API, a finicky API that has historically caused many bugs in high-profile software. Using our approach, we manage to capture the streaming semantics in a generic way, and apply it “for free” to over a dozen use-cases. Six of those have made it into the reference implementation of the Python programming language, replacing the previous CVE-ridden code.
@article{paperbot1918,
title = {Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification},
author = {Son Ho and Aymeric Fromherz and Jonathan Protzenko},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607844}
}