一句话：提出 3DGen，用 AI 智能体将 RFC 与示例转成 3D 规约，并综合出可证明正确的 C 解析器。
解析攻击者控制的输入是软件安全漏洞的主要来源之一，尤其是程序员将 RFC 中的非形式格式描述转录为低层、内存不安全语言中的高效解析逻辑时。本文提出 3DGen，利用 AI 智能体将自然语言文档（如 RFC）和示例输入等混合非形式输入转换为 3D 格式规约。为帮助人类理解和信任生成的规约，3DGen 还用符号方法合成测试输入，并借助外部 oracle 验证，从而区分多个看似合理的候选解。通过反复精炼，3DGen 产生符合测试套件的 3D 规约，并生成安全、高效且可证明正确的 C 解析代码。作者在 20 个互联网标准格式上评估了 3DGen，表明 AI 智能体能够在非平凡规模上生成经过形式验证的 C 代码；其关键使能因素是使用领域特定语言将 AI 输出限制在可自动符号分析的类别内。
Improper parsing of attacker-controlled input is a leading source of software security vulnerabilities, especially when programmers transcribe informal format descriptions in RFCs into efficient parsing logic in low-level, memory unsafe languages. Several researchers have proposed formal specification languages for data formats from which efficient code can be extracted. However, distilling informal requirements into formal specifications is challenging and, despite their benefits, new, formal languages are hard for people to learn and use. In this work, we present 3DGen, a framework that makes use of AI agents to transform mixed informal input, including natural language documents (i.e., RFCs) and example inputs into format specifications in a language called 3D. To support humans in understanding and trusting the generated specifications, 3DGen uses symbolic methods to also synthesize test inputs that can be validated against an external oracle. Symbolic test generation also helps in distinguishing multiple plausible solutions. Through a process of repeated refinement, 3DGen produces a 3D specification that conforms to a test suite, and which yields safe, efficient, provably correct, parsing code in C. We have evaluated 3DGen on 20 Internet standard formats, demonstrating the potential for AI-agents to produce formally verified$C$code at a non-trivial scale. A key enabler is the use of a domain-specific language to limit AI outputs to a class for which automated. symbolic analysis is tractable.
DOI 原文 ·
@inproceedings{paperbot8874,
title = {3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers},
author = {Sarah Fakhoury and Markus Kuppe and Shuvendu K. Lahiri and Tahina Ramananandro and Nikhil Swamy},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00173}
}