基于VST的Agent驱动liblzma解码器组件内存安全验证
Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST
- GenProof
- IMDEA Software Institute（IMDEA软件研究所）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
该研究基于VST，通过AI智能体辅助验证了liblzma生产级C解码器组件的内存安全，发现了其中的未定义行为，并解决了智能体驱动形式化验证的相关工程问题。
AI中文摘要：
我们报告了对liblzma解码器组件的内存安全验证，liblzma是xz-utils底层的压缩库，涉及LZMA2状态机、其控制的LZMA1解码器、外部解码路径以及共享滑动窗口字典。该验证基于Verified Software Toolchain（VST），通过机器检查的主体定理确立了内存安全性和部分功能正确性。在27个已完成的主体证明中，最大的证明覆盖了lzma_decode函数，其338行源代码在预处理后扩展为1934行C代码；该证明包含183268行证明脚本，对应775768行机械提取的目标语句。验证还发现了原始LZMA1零输入处理中的未定义行为，即范围解码器宏将零添加到空指针并对两个空指针执行减法操作。与其他合成验证代码的类似工作不同，我们验证的是已有的生产级C代码：AI智能体完成证明目标并提出改进方案；人类编写和审查模型与规范，并批准语义变更；Rocq内核检查证明项。在智能体构建证明脚本的过程中，主要工程问题在于转换和建模生产级C代码、构建用于驱动Rocq的健壮测试框架，以及为证明智能体提供反馈。VST的断言逻辑表达了开发所需的所有契约，我们描述了解决这些摩擦的流程、协调机制和证明工程技术。
英文摘要：
We report on the verification of memory safety for decoder components of liblzma, the compression library underlying xz-utils: the LZMA2 state machine, the LZMA1 decoder it controls, the outer decoding path, and the shared sliding-window dictionary. Built with the Verified Software Toolchain (VST), machine-checked body theorems establish memory safety and partial functional correctness. Across 27 completed body proofs, the largest covers lzma decode, whose 338 source lines expand to 1,934 lines of C after preprocessing; its proof comprises 183,268 lines of proof script over 775,768 lines of mechanically extracted goal statements. The verification exposed undefined behavior in raw LZMA1 zero-input handling, where range-decoder macros add zero to a null pointer and subtract two null pointers. Unlike similar work that synthesizes verified code, we verify pre-existing, production-scale C. AI agents complete proof goals and propose refinements; humans write and review models and specifications, and approve semantic changes; the Rocq kernel checks the proof terms. With agents constructing the proof scripts, the main engineering problems lay in translating and modeling production C, building a robust harness for driving Rocq, and providing feedback for proving agents. VST's assertion logic expressed every contract required by the development. We describe the pipeline, coordination mechanisms, and proof-engineering techniques that resolved these frictions.
