3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy
TL;DR
The paper addresses the challenge of deriving trustworthy, memory-safe binary format parsers from informal RFC descriptions. It introduces 3DGen, an AI-assisted workflow that translates informal inputs into the 3D DSL, supported by symbolic test generation (3dTestGen) and a verified C code pathway via EverParse. Through evaluation on 20 RFC-based network protocols, the approach demonstrates the potential to produce formally verified parsers and to reveal RFC ambiguities, while also highlighting limitations due to labeler inconsistencies and RFC wording. The work contributes an end-to-end architecture combining multi-agent AI, a compact DSL with formal semantics, symbolic test-generation, and differential testing to progressively refine intent into correct-by-construction code.
Abstract
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.