使用 VST 对 liblzma 解码器组件的内存安全进行代理驱动验证

我们报告了 liblzma 解码器组件的内存安全验证、xz-utils 底层的压缩库：LZMA2 状态机、它控制的 LZMA1 解码器、外部解码路径和共享滑动窗口字典。使用经过验证的软件工具链 (VST) 构建，机器检查的主体定理建立了内存安全性和部分功能正确性。在 27 个已完成的 body 样张中，最大的一个是 lzma 解码，其 338 行源代码在预处理后扩展到 1,934 行 C；它的证明包括 183,268 行证明脚本，超过 775,768 行机械提取的目标陈述。验证暴露了原始 LZMA1 零输入处理中的未定义行为，其中范围解码器宏将零添加到空指针并减去两个空指针。与合成验证代码的类似工作不同，我们验证预先存在的、生产规模的 C.AI 代理完成证明目标并提出改进建议；人类编写和审查模型和规范，并批准语义更改； Rocq 内核检查证明项。在代理构建证明脚本时，主要的工程问题在于对产品 C 进行翻译和建模、构建用于驱动 Rocq 的强大工具，以及为证明代理提供反馈。 VST的断言逻辑表达了开发所需的每一个合约。我们描述了解决这些摩擦的管道、协调机制和验证工程技术。