3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers

TL;DR

3DGen leverages AI and symbolic methods to automatically generate provably correct binary format parsers from informal specifications, improving security and reliability in data parsing.

Contribution

The paper introduces 3DGen, a novel framework that uses AI to transform informal format descriptions into formal, verifiable parser specifications with symbolic test generation.

Findings

Successfully applied to 20 Internet formats

Generated safe, efficient C parsers with formal correctness guarantees

Demonstrated scalability of AI-assisted formal parser synthesis

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.