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

Sarah FakhouryMarkus KuppeShuvendu LahiriTahina RamananandroNikhil Swamy

article2025International Conference on Software Engineering13 citations

Presents 3DGen, an automated framework that pairs AI agents with symbolic test generation to translate informal RFC specifications into provably correct, memory-safe C binary parsers.

Listen

Incorrect parsing of binary network inputs is a leading source of severe software security vulnerabilities. Manually converting ambiguous, natural language specifications from Request for Comments (RFC) documents into low-level, memory-unsafe languages like C is notoriously error-prone, leaving systems exposed to exploits for decades. Formal domain-specific languages (DSLs) like 3D offer provable correctness and memory safety via code generators like EverParse, but authoring these specifications by hand requires steep learning curves and substantial engineering effort.

The article introduces 3DGen, an automated framework designed to evaluate whether artificial intelligence agents can reliably translate natural language RFC documents into formal 3D specifications, which then automatically compile into verified, secure C code.

The framework combines a multi-agent system powered by GPT-4 with automated formal methods. The agents—split into planning, domain expertise, and 3D programming roles—interactively draft candidate specifications. To validate these candidates, the framework introduces 3DTestGen, a symbolic test generator that produces test cases and performs differential testing. The overall approach was evaluated across 20 standardized Internet protocols, using Wireshark as an initial external oracle to label valid and invalid network packets.

The evaluation revealed several critical findings. First, while 3DGen initially achieved a 45% pass rate (9 of 20 protocols) against standard Wireshark labeling, investigation showed that all 11 failing cases were due to Wireshark being overly permissive and ignoring RFC-mandated constraints. Once labels were corrected to match RFC standards, 3DGen achieved a 100% success rate across all 20 protocols. Second, when comparing generated specifications to existing expert-written specifications across 7 protocols, 3DGen matched equivalent behavior and uncovered three human errors in existing specifications for UDP, ICMP, and VXLAN. Third, symbolic differential analysis successfully distinguished subtle semantic divergences among candidate specifications, proving its value in grouping equivalent programs and surfacing missing constraints.

These findings demonstrate that targeting an analyzable domain-specific language rather than prompting an AI model for raw C code drastically mitigates software security risks. This intermediate representation allows symbolic tools to systematically check AI outputs, eliminate undefined behaviors, and generate provably secure C parsers at scale. Furthermore, the framework serves as an auditing mechanism to expose discrepancies in legacy tools and human-authored specifications.

Organizations developing security-critical software should consider adopting DSL-based AI pipelines with symbolic validation loops rather than directly deploying AI-generated imperative code. Before strong autonomous adoption, development teams should maintain human review over synthesized tests and conduct user studies to determine how seamlessly non-expert engineers can operate the intent-refinement loop.

The study's primary limitation is the framework's dependency on the quality and strictness of the labeling oracle, as shown by Wireshark's permissiveness and occasional under-constrained test sets. Users should exercise caution to ensure test suites are comprehensive, but confidence remains high that candidate specifications passing well-aligned symbolic test suites will compile into provably memory-safe and correct parsing code.

Microsoft formal specification formal specification language internet provably correct binary format parsers binary format program synthesis

arXiv: 2404.10362

Paper: Teaching Large Language Models to Self-Debug, Xinyun Chen et al. (2023). Introduces foundational techniques for iterative LLM self-debugging and refinement against execution feedback, which underpin the repeated repair cycles in 3DGen.
Paper: Grammar-Constrained Decoding for Structured NLP Tasks without Finetuning, Saibo Geng et al. (2023). Demonstrates grammar-constrained decoding to force neural models to adhere strictly to formal syntax, providing context for restricting LLM generation to formal domain-specific languages.
Paper: Instruction Tuning for Secure Code Generation, Jingxuan He et al. (2024). Explores tuning language models to prevent memory and security vulnerabilities during code generation, addressing the core security motivation of safe parser synthesis.
Paper: CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis, Erik Nijkamp et al. (2022). Establishes multi-turn conversational program synthesis frameworks that decompose complex specification translation tasks into iterative sub-goals.
Paper: Competition-level code generation with AlphaCode, Yujia Li et al. (2022). Pioneers the methodology of generating candidate programs at scale and pruning them via automated test execution and behavioral clustering.

Paper: VeruSAGE: A Study of Agent-Based Verification for Rust Systems, Chenyuan Yang et al. (2025). Extends the concept of AI-assisted formal systems verification by evaluating multi-agent LLM frameworks on end-to-end correctness proofs for real-world systems code.
Paper: LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks, Po-Nien Kung et al. (2026). Applies agentic informal-to-formal decomposition and compiler-in-the-loop validation to construct mechanically verified mathematical proofs.
Paper: RustAssistant: Using LLMs to Fix Compilation Errors in Rust Code, Pantazis Deligiannis et al. (2025). Investigates interactive LLM repair guided by compiler and static analysis diagnostics to resolve complex memory safety constraints in systems software.
Paper: AgentDoG: A Diagnostic Guardrail Framework for AI Agent Safety and Security, Dongrui Liu et al. (2026). Develops diagnostic guardrails and execution path attribution to monitor and secure autonomous multi-step AI agent workflows.

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

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.

Topics

formal specification formal specification language internet parsing algorithm software test generations software vulnerabilities

Keywords

provably correct binary format parsers binary format program synthesis natural language specifications parser combinators symbolic test-case generation formal specifications code generation protocol specification formal semantics

I Introduction
I-A 3dGen: A Framework for AI-assisted DSL Programming
II Problem Formulation
III The 3dGen Approach
III-A 3DGen: An Abstract Algorithm
III-B Agent Based Implementation
III-C 3dTestGen: Symbolic Test Case Generation
IV Experimental Setup
IV-A Network Protocols
IV-B Generating Specifications with 3dGen
IV-C Generating a Labeled Test Set for each Protocol
IV-D Handwritten 3D Specifications
V Results
V-A Capabilities of 3dGen
V-A1 Labeler and RFC disagreement
V-A2 Agent Mistakes
V-B Distinguishing Candidates with Differential Testing
V-C 3dGen vs. Human Written Specs
VI Related Work
VII Conclusion
References
-A Branch coverage with 3DTestGen
-B Comparing code produced by 3DGen to Handwritten Specifications
-C Syntactic Characteristics of code produced by 3dGen

Knowls

Knowl 1 — 3DGen Iterative Intent-Refinement Algorithm for Format Specifications
algorithm
The 3DGen algorithm synthesizes formally verified binary format specifications written in the 3D domain-specific language (DSL) from informal natural language standards (e.g., RFCs) and input examples. The algorithm operates by iteratively proposing candidate specifications via a large language model (LLM), verifying their syntax and types, generating symbolic test inputs via an SMT-based test generator (3DTestGen), classifying tests using an external oracle or packet dissector, and pruning inconsistent candidates.
Input: RFC document $RFC$ , packet labeling function $LblImpl$ , seed positive packet set $I^+_0$ , seed negative packet set $I^-_0$
Output: A set of valid 3D specifications $CandProgs$ , augmented test sets $I^+, I^-$
$(I^+, I^-) \leftarrow (I^+_0, I^-_0)$
$st \leftarrow \{ 3DDoc, RFC, I^+, I^- \}$
$CandProgs \leftarrow \emptyset$
for each refinement iteration do
    choose non-deterministically:
        branch 1 (Candidate Generation):
             $p \leftarrow \text{QUERYLLM}(st)$
             $se \leftarrow \text{3DSYNCHK}(p)$
            if $se \neq \text{SUCCESS}$ then
                 $st \leftarrow st \cup \{(p, se)\}$
            else
                 $CandProgs \leftarrow CandProgs \cup \{p\}$
            end if
        branch 2 (Symbolic Test Augmentation):
             $I' \leftarrow \text{3DTESTGEN}(CandProgs, I^+ \cup I^-)$
             $(I^+, I^-) \leftarrow (I^+, I^-) \cup \text{LABELINPUTS}(I', LblImpl)$
    for each $q \in CandProgs$ do
        for all $i \in I^+ \cup I^-$ do
            if $(i \in I^+ \land \neg \text{3DEXEC}(q, i)) \lor (i \in I^- \land \text{3DEXEC}(q, i))$ then
                 $st \leftarrow st \cup \{(q, i)\}$
                 $CandProgs \leftarrow CandProgs \setminus \{q\}$
                break
            end if
        end for
    end for
end for
return $CandProgs, I^+, I^-$
The algorithm utilizes four primary components:
- $\text{3DSYNCHK}(p)$ : checks whether candidate specification $p$ conforms to the syntax and static type constraints of the 3D language, returning error message $se$ .
- $\text{3DEXEC}(p, i)$ : compiles $p$ to C code using the EverParse verified toolchain and executes it on packet $i$ , returning $\text{true}$ if accepted and $\text{false}$ otherwise.
- $\text{3DDoc}$ : complete reference manual and syntax examples for the 3D language.
- $\text{3DTESTGEN}(CandProgs, I^+ \cup I^-)$ : a symbolic execution engine that produces concrete packets exercising branches in candidate specifications.
Upon convergence, any specification in $CandProgs$ satisfies $\forall i^+ \in I^+, \text{3DEXEC}(p, i^+) = \text{true}$ and $\forall i^- \in I^-, \text{3DEXEC}(p, i^-) = \text{false}$ .
Knowl 2 — 3DGen Multi-Agent Architecture for Specification Generation
model/method
3DGen implements its LLM query and specification repair mechanism as a multi-agent system built on the AutoGen framework. Rather than passing all informal context, language manuals, and test failures into a monolithic LLM prompt, 3DGen decomposes the reasoning and synthesis process across three specialized agents interacting in a group chat:
1. Planner Agent: Serves as the group chat manager and workflow orchestrator. It receives the meta-task prompt, manages conversation flow, executes verification tools (the syntax/type checker $\text{3DSYNCHK}$ and the execution checker $\text{3DEXEC}$ ), and posts error diagnostics back to the group.
2. 3D Developer Agent: Responsible for generating and repairing 3D specification code. It has access to the 3D language manual (consisting of approximately 2,000 lines of documentation and 20 examples), syntactical guidelines, and specific code repair prompts.
3. Domain Expert Agent: Reads the domain specification (e.g., protocol RFC documents and packet format descriptions) and provides targeted requirements to the 3D Developer Agent while critiquing proposed specifications against the domain requirements.
The conversation flow operates iteratively: the Domain Expert conveys format requirements from the RFC, the Developer produces 3D code, the Planner invokes $\text{3DSYNCHK}$ and $\text{3DEXEC}$ , and failure outputs are fed back to the Developer for repair until candidate specifications pass all tests or a maximum iteration threshold (e.g., 15 refinement iterations) is reached.
Knowl 3 — First-Order SMT-LIB Specialization for 3D Parser Combinators in 3DTestGen
model/method
In the EverParse framework, 3D specification semantics are modeled in $\text{F}^\star$ as higher-order parser combinators with signatures of the form: $\text{parser } t : (\text{input}: \text{seq byte}) \rightarrow \text{option } (t \times \mathbb{N})$ where applying a parser to an input byte sequence returns either $\text{None}$ (parse failure) or $\text{Some}(v, n)$ indicating parsed value $v$ of type $t$ and consumed byte count $n$ .

Because SMT-LIB version 2 (SMT2) solvers (such as Z3) do not natively support higher-order functions like parse_pair and parse_refine, 3DTestGen implements an AST transformation that inlines and specializes higher-order combinators into first-order state-transforming functions. The parser operates over an uninterpreted function representing the input byte array:
```
(declare-fun Input (Int) Int)
(assert (forall ((i Int)) (and (<= 0 (Input i)) (< (Input i) 256))))
```
Parser execution is modeled as transitioning an algebraic State datatype that tracks:
- remaining-input-size: remaining unparsed bytes in the input stream,
- current-pos: zero-based read offset in Input,
- has-failed: boolean flag indicating whether parsing has failed,
- return-value: integer or structured value produced by the parser.
A primitive parser (e.g., parse-uint8) advances current-pos, decrements remaining-input-size, and extracts Input(current-pos) if remaining-input-size > 0 and has-failed is false; otherwise, it transitions to a fail state. Compound parsers are encoded as sequences of let-bound state transitions.
Knowl 4 — Branch Coverage via Symbolic Branch-Trace Tagging in 3DTestGen
model/method
To generate diverse test inputs that systematically exercise different specification paths rather than repeatedly hitting trivial parse paths, 3DTestGen instruments the SMT2 encoding with branch tags.

The SMT encoding declares an uninterpreted function branch-trace: Int -> Int and adds a branch-index counter to the parser's symbolic State. Each conditional branch in the specification AST (specifically value constraints and union casetype discriminators) is augmented with an assertion tying the branch decision to the corresponding position in branch-trace:
```
(if (and (> (return-value s1) 42)
         (= 0 (branch-trace (branch-index s1))))
    (parse-uint8 (incr-branch-index s1))
    (if (and (not (> (return-value s1) 42))
             (= 1 (branch-trace (branch-index s1))))
        ...))
```
To generate a test suite that achieves branch coverage up to a specified depth $D$ :
1. 3DTestGen initializes branch-index to 0 in init.
2. It asserts (>= (branch-index (parse-message init)) D) or fixes specific prefixes of branch-trace.
3. By enumerating binary/n-ary branch assignments across branch-trace in a depth-first search manner and invoking Z3 on each path condition, 3DTestGen synthesizes concrete sequences of input bytes that force the parser along every satisfiable execution path.
Knowl 5 — SMT-Based Symbolic Differential Testing and Semantic Equivalence Verification
model/method
Given two 3D format specifications $p_1$ and $p_2$ , 3DTestGen determines whether they are semantically equivalent or synthesizes differentiating inputs using SMT queries over unbounded packet sizes.

To check if $p_1$ implies $p_2$ , 3DTestGen queries Z3 for a model satisfying the existential predicate: $\exists \text{Input}.\; \text{3DEXEC}(p_1, \text{Input}) \land \neg \text{3DEXEC}(p_2, \text{Input})$

Outcomes of the query:
- SAT: Z3 outputs a concrete byte sequence that is accepted by $p_1$ but rejected by $p_2$ , providing a witness differentiating test case.
- UNSAT: No byte sequence can be accepted by $p_1$ and rejected by $p_2$ , proving that the language accepted by $p_1$ is a subset of $p_2$ (i.e., $L(p_1) \subseteq L(p_2)$ ).
- UNKNOWN: Z3 times out or cannot decide the formula.
Two candidate specifications $p_1$ and $p_2$ are proven semantically equivalent ( $L(p_1) = L(p_2)$ ) if and only if Z3 returns $\text{UNSAT}$ for both directions:
1. $p_1 \land \neg p_2 \implies \text{UNSAT}$
2. $p_2 \land \neg p_1 \implies \text{UNSAT}$

Knowl 6 — 3DGen Protocol Specification Synthesis Performance Across 20 RFCs

empirical result

3DGen was evaluated on 20 IETF standard network protocols using GPT-4-32k (temperature 1.0, maximum 15 refinement iterations per attempt, 5 runs per protocol).

Protocol	Accepted (x/5)	Avg. Syntax Refinements	Avg. Packet Refinements
UDP	5	0.3	0
ICMP	0 (1*)	7.5	6
VXLAN	0 (2*)	7.6	7.4
IPV6	0 (1*)	7.8	2.0
IPV4	2	4.0	11.0
Ethernet	0 (1*)	11.4	4.6
TCP	0 (2*)	10.2	2.5
GRE	0 (1*)	10.4	4.6
DHCP	2	8.2	0
DCCP	1	14.25	0.75
TPKT	0 (1*)	5.0	6.6
ARP	3	4.8	1.8
NTP	3	7.4	3.0
NBNS	1	4.6	4.0
IGMP	5	3.8	0
NSH	1	11.0	2.0
TFTP	0 (1*)	11.0	1.0
RTP	0 (1*)	3.0	12.0
PPP	0 (1*)	7.6	5.0
OSPFv3	0 (1*)	13.6	2.0
Total	pass@5: 45%	*pass@5: 100%**

On the initial test suite labeled by Wireshark's dissector, 3DGen achieved a $\text{pass@5}$ rate of $45\%$ (9/20 protocols). In the remaining 11 cases, failures occurred because 3DGen generated specifications strictly adhering to RFC constraints which Wireshark's dissectors did not enforce (labeling invalid packets as valid). When test labels were adjusted to strictly conform to the RFC text (marked with *), 3DGen generated compliant specifications for $100\%$ (20/20) of protocols.

Knowl 7 — Discrepancies Between RFC Format Constraints and Wireshark Dissector Validations

data/table

In 11 of the 20 evaluated network protocols, 3DGen synthesized specifications enforcing constraints documented in RFC standards that are ignored or accepted permissively by Wireshark dissectors:

Protocol	Detected RFC vs. Wireshark Disagreement	Wireshark Message
ICMP	Header length constraints	None
Ethernet	Ethertype payload length	None
VXLAN	Reserved bits must be 0	None
	I flag must be 1	None
	Header must be 8 bytes	None
IPV6	Payload Length exceeds framing length	Warning
GRE	Reserved0 must be zero	None
	Version number must be zero	None
TFTP	Opcode fields must be between 0–5	None
TCP	Window fields must not be zero	Warning
	ACK number must be consistent with ACK flag	Warning
TPKT	Version field must be 3	None
	Reserved field must be 8 bits	None
PPP	Code field must be between 1–11	None
	Length field must be 1 octet, at least size 4	None
	Data must be constrained by Length	None
RTP	Version must be 2	None
OSPF	Version field must not be 3	None
	Reserved field must be 0	None
	Header length must be 16 bytes	None

Wireshark allows these violations either because dissectors accommodate multi-RFC protocol families (e.g., GRE allowing version 1 for PPTP), diagnostic workflows allow malformed packets, or cross-layer encapsulation validation is missing.

Knowl 8 — Bugs Uncovered in Expert-Written EverParse Specifications via 3DGen Differential Testing

empirical result

3DTestGen's symbolic differential testing was used to compare 3DGen-generated specifications against existing human-written specifications in the EverParse repository across 7 protocols. The analysis proved semantic equivalence in 2 cases and uncovered human specification bugs in 3 protocols:

Protocol	Equivalent?	Root Cause Divergence	After H.S. Fix
UDP	No	Handwritten spec missing constraint on Length field	$\checkmark$
ICMP	No	Handwritten spec UNUSED_BYTES field was 32 bits instead of 32 bytes	$\checkmark$
VXLAN	No	Handwritten spec VXLanID field was two bytes too short	$\checkmark$
IPV6	$\checkmark$	None	n/a
IPV4	No	Generated spec missing value constraints on IHL, TotalLength	n/a
Ethernet	$\checkmark$	None	n/a
TCP	No	Generated spec missing constraints on options payload	n/a

For UDP, ICMP, and VXLAN, differential testing proved that the AI-generated specifications correctly captured the RFC requirements where human experts had introduced errors. Following corrections to the handwritten specifications, 3DTestGen proved formal equivalence (marked $\checkmark$ ), and patches were merged into the upstream EverParse repository. For IPv4 and TCP, the generated specifications were underconstrained due to non-exhaustive test suites, but supplying tests synthesized from the constraints enabled 3DGen to produce equivalent specifications.

Knowl 9 — Semantic Divergence and Differential Pruning of Multiple Generated Candidate Specifications

empirical result

When 3DGen generates multiple candidate specifications that all pass the provided test suite, 3DTestGen's differential testing isolates semantic differences between candidates to assist user disambiguation:

Protocol	# Candidates	# Distinct	Divergent Fields
UDP	5	2	Optional Data[:consume-all] field
IPV4	2	2	Additional constraints on Flag values
VXLAN	2	1	None (Semantically Equivalent)
DHCP	2	2	options field length, constraints on Flags
ARP	3	2	Incorrect additional remainder[:consume-all] field
NTP	3	3	Additional constraints on LeapIndicator, Status, Type
IGMP	5	3	Optional OtherFields[:consume-all]
TCP	2	2	Constraints on Options field

In 7 out of 8 protocols yielding multiple candidates, at least two candidates were semantically distinct. For ARP and IPv4, one candidate was strictly more constrained than the other (the set of valid packets accepted by candidate $A$ was a strict subset of candidate $B$ ). In both cases, the stricter candidate correctly matched the RFC, indicating that preference for stricter candidates serves as an effective pruning heuristic.

Knowl 10 — Syntactic Metrics and DSL Compactness of Generated 3D Specifications

data/table

A structural comparison between 3D DSL specifications synthesized by 3DGen, handwritten specifications (H.S.), and the corresponding verified C parser code produced by EverParse highlights the compactness of the DSL:

Protocol	LOC (C)	LOC (3D)	Fields	Constraints	Casetypes	Structs	Bitfields	Consume-all
UDP (3DGen / H.S.)	158 / 158	7 / 8	4 / 4	1 / 1	0 / 0	1 / 1	0 / 0	0 / 0
ICMPv4 (3DGen / H.S.)	1208 / 2119	99 / 164	72 / 61	11 / 6	1 / 1	12 / 13	0 / 0	2 / 1
VXLAN (3DGen / H.S.)	296 / 266	16 / 10	10 / 7	7 / 6	0 / 0	3 / 1	5 / 3	0 / 0
IPV6 (3DGen / H.S.)	341 / 427	10 / 16	7 / 7	1 / 1	0 / 0	1 / 1	2 / 3	0 / 0
IPV4 (3DGen / H.S.)	544 / 534	30 / 35	25 / 15	5 / 5	0 / 0	3 / 2	15 / 6	0 / 0
TCP (3DGen / H.S.)	615 / 1445	45 / 161	27 / 64	3 / 17	1 / 1	5 / 8	8 / 21	1 / 1
Ethernet (3DGen / H.S.)	352 / 353	25 / 26	13 / 11	0 / 0	1 / 1	4 / 3	3 / 0	0 / 0
Mean (All 20 Protocols)	—	26.2	15.7	3.4	0.30	2.75	3.35	0.71
Mean (7 Protocol Subset)	499.7	33.1	22.5	4.0	0.42	4.14	4.71	0.42
Mean (7 Protocol H.S.)	757.4	60.0	24.1	5.1	0.42	4.14	4.71	0.28

The declarative 3D specifications range from 6 to 99 lines of code across all 20 protocols, while the generated memory-safe, verified C code is several times larger (up to 1,208 LOC for ICMPv4), incorporating automated buffer-bound verification and error-handling logic.

Coverage note — No substantial contributed material was omitted from the extraction.

References

1.J. Bangert and N. Zeldovich, ‘‘Nail: A practical tool for parsing and generating data formats,’’ in 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). Broomfield, CO: USENIX Association, Oct. 2014, pp. 615–628. [Online]. Available: https://www.usenix.org/conference/osdi14/technical-sessions/presentation/bangert
2.T. Ramananandro, A. Delignat-Lavaud, C. Fournet, N. Swamy, T. Chajed, N. Kobeissi, and J. Protzenko, ‘‘Everparse: Verified secure zero-copy parsers for authenticated message formats,’’ in Proceedings of the 28th USENIX Conference on Security Symposium, ser. SEC’19. USA: USENIX Association, 2019, p. 1465–1482.
3.N. Swamy, T. Ramananandro, A. Rastogi, I. Spiridonova, H. Ni, D. Malloy, J. Vazquez, M. Tang, O. Cardona, and A. Gupta, ‘‘Hardening attack surfaces with formally proven binary format parsers,’’ in Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’22), June 13–17, 2022, San Diego, CA, USA, 2022. [Online]. Available: https://www.fstar-lang.org/papers/EverParse3D.pdf
4.OpenAI, ‘‘Gpt-4 technical report,’’ 2023.
5.J. Protzenko, J.-K. Zinzindohoue, A. Rastogi, T. Ramananandro, P. Wang, S. Zanella-Beguelin, A. Delignat-Lavaud, C. Hritcu, K. Bhargavan, C. Fournet, and N. Swamy, ‘‘Verified low-level programming embedded in F*,’’ PACMPL, vol. 1, no. ICFP, pp. 17:1–17:29, Sep. 2017. [Online]. Available: http://arxiv.org/abs/1703.00053
6.S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao, ‘‘React: Synergizing reasoning and acting in language models,’’ arXiv preprint arXiv:2210.03629, 2022.
7.Y. Gao, Y. Xiong, X. Gao, K. Jia, J. Pan, Y. Bi, Y. Dai, J. Sun, and H. Wang, ‘‘Retrieval-augmented generation for large language models: A survey,’’ arXiv preprint arXiv:2312.10997, 2023.
8.Z. Xi, W. Chen, X. Guo, W. He, Y. Ding, B. Hong, M. Zhang, J. Wang, S. Jin, E. Zhou et al., ‘‘The rise and potential of large language model based agents: A survey,’’ arXiv preprint arXiv:2309.07864, 2023.
9.L. Wang, C. Ma, X. Feng, Z. Zhang, H. Yang, J. Zhang, Z. Chen, J. Tang, X. Chen, Y. Lin et al., ‘‘A survey on large language model based autonomous agents,’’ arXiv preprint arXiv:2308.11432, 2023.
10.Y. Du, S. Li, A. Torralba, J. B. Tenenbaum, and I. Mordatch, ‘‘Improving factuality and reasoning in language models through multiagent debate,’’ arXiv preprint arXiv:2305.14325, 2023.
11.C. Qian, X. Cong, C. Yang, W. Chen, Y. Su, J. Xu, Z. Liu, and M. Sun, ‘‘Communicative agents for software development,’’ arXiv preprint arXiv:2307.07924, 2023.
12.Q. Wu, G. Bansal, J. Zhang, Y. Wu, S. Zhang, E. Zhu, B. Li, L. Jiang, X. Zhang, and C. Wang, ‘‘Autogen: Enabling next-gen llm applications via multi-agent conversation framework,’’ arXiv preprint arXiv:2308.08155, 2023.
13.C. Barrett, P. Fontaine, and C. Tinelli, ‘‘The Satisfiability Modulo Theories Library (SMT-LIB),’’ https://smtlib.cs.uiowa.edu/, 2016.
14.L. De Moura and N. Bjrner, ‘‘Z3: An efficient smt solver,’’ in Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14. Springer, 2008, pp. 337–340.
15.M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. d. O. Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman et al., ‘‘Evaluating large language models trained on code,’’ arXiv preprint arXiv:2107.03374, 2021.
16.J. Austin, A. Odena, M. Nye, M. Bosma, H. Michalewski, D. Dohan, E. Jiang, C. Cai, M. Terry, Q. Le et al., ‘‘Program synthesis with large language models,’’ arXiv preprint arXiv:2108.07732, 2021.
17.H. Pearce, B. Ahmad, B. Tan, B. Dolan-Gavitt, and R. Karri, ‘‘Asleep at the keyboard? assessing the security of github copilot’s code contri-butions,’’ in 2022 IEEE Symposium on Security and Privacy (SP), 2022, pp. 754–768.
18.Y. Li, D. Choi, J. Chung, N. Kushman, J. Schrittwieser, R. Leblond, T. Eccles, J. Keeling, F. Gimeno, A. D. Lago, T. Hubert, P. Choy, C. d. M. d’Autume, I. Babuschkin, X. Chen, P.-S. Huang, J. Welbl, S. Gowal, A. Cherepanov, J. Molloy, D. J. Mankowitz, E. S. Robson, P. Kohli, N. de Freitas, K. Kavukcuoglu, and O. Vinyals, ‘‘Competition-level code generation with alphacode,’’ 2022. [Online]. Available: https://arxiv.org/abs/2203.07814
19.B. Chen, F. Zhang, A. Nguyen, D. Zan, Z. Lin, J.-G. Lou, and W. Chen, ‘‘Codet: Code generation with generated tests,’’ 2022. [Online]. Available: https://arxiv.org/abs/2207.10397
20.Z. Manna and R. Waldinger, ‘‘A deductive approach to program synthesis,’’ ACM Trans. Program. Lang. Syst., vol. 2, no. 1, p. 90–121, jan 1980. [Online]. Available: https://doi.org/10.1145/357084.357090
21.S. Gulwani, O. Polozov, and R. Singh, ‘‘Program synthesis,’’ Found. Trends Program. Lang., vol. 4, no. 1-2, pp. 1–119, 2017. [Online]. Available: https://doi.org/10.1561/2500000010
22.R. Alur, R. Bodk, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa, ‘‘Syntax-guided synthesis,’’ in Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, 2013, pp. 1–8. [Online]. Available: https://ieeexplore.ieee.org/document/6679385/
23.A. Gandhi, T. Q. Nguyen, H. Jiao, R. Steen, and A. Bhatawdekar, ‘‘Natural language commanding via program synthesis,’’ 2023.
24.S. K. Lahiri, S. Fakhoury, A. Naik, G. Sakkas, S. Chakraborty, M. Musuvathi, P. Choudhury, C. von Veh, J. P. Inala, C. Wang, and J. Gao, ‘‘Interactive code generation via test-driven user-intent formalization,’’ CoRR, vol. abs/2208.05950, 2023. [Online]. Available: https://doi.org/10.48550/arXiv.2208.05950
25.M. Endres, S. Fakhoury, S. Chakraborty, and S. K. Lahiri, ‘‘Formalizing natural language intent into program specifications via large language models,’’ CoRR, vol. abs/2310.01831, 2023. [Online]. Available: https://doi.org/10.48550/arXiv.2310.01831
26.M. Md Rakib Hossain Misu, C. V. Lopes, I. Ma, and J. Noble, ‘‘Towards ai-assisted synthesis of verified dafny methods,’’ 2024.
27.J. Yen, T. Levai, Q. Ye, X. Ren, R. Govindan, and B. Raghavan, ‘‘Semi-automated protocol disambiguation and code generation,’’ in Proceedings of the 2021 ACM SIGCOMM 2021 Conference, ser. SIGCOMM ’21. New York, NY, USA: Association for Computing Machinery, 2021, p. 272–286. [Online]. Available: https://doi.org/10.1145/3452296.3472910

Citation

MLA

Fakhoury, S., et al. “3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers”. arXiv, 2024, http://arxiv.org/abs/2404.10362v2.

APA

Fakhoury, S., Kuppe, M., Lahiri, S. K., Ramananandro, T., & Swamy, N. (2024). 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers. arXiv. http://arxiv.org/abs/2404.10362v2

Chicago

Fakhoury, S., M. Kuppe, S. K. Lahiri, T. Ramananandro, and N. Swamy. 2024. “3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers”. arXiv. http://arxiv.org/abs/2404.10362v2.

Harvard

Fakhoury, S. et al. (2024) “3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers”, arXiv [Preprint]. Available at: http://arxiv.org/abs/2404.10362v2.

Vancouver

1. Fakhoury S, Kuppe M, Lahiri SK, Ramananandro T, Swamy N (2024) 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers. arXiv

BibTeX

@article{fakhoury20243dgen,
  title = {3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers},
  author = {Fakhoury, Sarah and Kuppe, Markus and Lahiri, Shuvendu K. and Ramananandro, Tahina and Swamy, Nikhil},
  year = {2024},
  journal = {arXiv},
  url = {http://arxiv.org/abs/2404.10362v2},
  eprint = {2404.10362}
}

Metadata:arXiv

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF

License: https://creativecommons.org/licenses/by/4.0/

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

Abstract

Topics

Keywords

Table of Contents

Knowls

Knowl 1 — 3DGen Iterative Intent-Refinement Algorithm for Format Specifications

Knowl 2 — 3DGen Multi-Agent Architecture for Specification Generation

Knowl 3 — First-Order SMT-LIB Specialization for 3D Parser Combinators in 3DTestGen

Knowl 4 — Branch Coverage via Symbolic Branch-Trace Tagging in 3DTestGen

Knowl 5 — SMT-Based Symbolic Differential Testing and Semantic Equivalence Verification

Knowl 6 — 3DGen Protocol Specification Synthesis Performance Across 20 RFCs

Knowl 7 — Discrepancies Between RFC Format Constraints and Wireshark Dissector Validations

Knowl 8 — Bugs Uncovered in Expert-Written EverParse Specifications via 3DGen Differential Testing

Knowl 9 — Semantic Divergence and Differential Pruning of Multiple Generated Candidate Specifications

Knowl 10 — Syntactic Metrics and DSL Compactness of Generated 3D Specifications

References

Citation

BibTeX

Access the Paper