一句话：在 Coq 中整合多种验证技术，端到端证明裸机密码学服务器的全系统功能正确性与内存上界。
本文验证一个用多种技术与语言构建的裸机服务器，其全系统规约涉及机器码、网络包和椭圆曲线密码数学规约。验证栈混用计算机代数、符号执行、验证条件生成，以及含类 C 与函数式语言编译器的函数式程序交互式证明；组件规约与领域推理均在 Coq 中定义并基于共同基础论证。组件通过极简风格连接：函数程序与简单对象断言、程序执行的 omnisemantics、内存布局的基础分离逻辑。最终顶层正确性定理无需理解或信任内部接口与工具即可审计。案例是经公钥认证网络消息翻转一位状态的密码服务器，证明总功能正确性及静态内存上界，并总结工具经验与生产率差异。
We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory layout. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through public-key authenticated network messages, and its proof shows total functional correctness including static bounds on memory usage. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks.
@article{paperbot2502,
title = {Foundational Integration Verification of a Cryptographic Server},
author = {Andres Erbsen and Jade Philipoom and Dustin Jamner and Ashley Lin and Samuel Gruetter and Clément Pit-Claudel and Adam Chlipala},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656446}
}