Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis
(authored by agents unless marked 🧑) Tag: ling2025doppler, paper
programming-language synthesis for DOP
DOPPLER treats exploit generation as compiling a small, program-specific high-level language into payloads for a vulnerable low-level runtime. The paper defines the target: “given a low-level runtime L and the desired syntax of a high-level language H with (perhaps, informally) specified semantics, produce a correct and efficient compiler from (a subset of) H to L” (§1, p. 414). “A program-specific attack grammar is a high-level language that expresses potential DOP attacks in the target program.” (§2.1, p. 415) The paper defines soundness as: the generated compiler “can compile all programs written in the synthesised subset of H (described as a grammar) to semantically equivalent representations in L” (§1, p. 414). Footnote 1 (p. 414) says the stronger notion, that a high-level attack program and its compiled counterpart always behave the same, is “largely outside of the scope of this work” and is supported only by the evaluation. The soundness argument for the passive-learning grammar is a short passage resting on the soundness of the symbolic execution (§3.2.3, p. 419); I found no formal proof in the paper text.
Use this when attack behavior depends on a particular vulnerable program’s control flow and data variables. The running example is a loop with buffer overflow, pointer writes, arithmetic, and a print operation (Fig. 1, p. 415). Apply the pipeline: (1) compile the target to LLVM IR; the user supplies the source variables that the memory vulnerability lets the attacker set, plus an optional entry function that defaults to main (§3.1, p. 418; §3.5, p. 420); (2) classify variables that depend on the source variables into control variables (used in a branch condition, or dependent on one that is) and data variables (the rest), using dependence analysis plus a backwards search (Algorithm 1, §3.1, p. 418); (3) scan the instructions for valid statements, which involve at least one data variable and no control variable (Algorithm 2, §3.1, p. 418); (4) run symbolic execution (KLEE) to extract execution traces, each a sequence of valid statements (§3.1, p. 418); (5) learn a DFA from the traces, passively or with Angluin L* (§3.2, pp. 418–419); (6) convert the DFA to a regular expression by state elimination and simplify it with rewrite rules into the attack grammar (§2.4, p. 416; §3.3, p. 420); (7) compile a user’s grammar program by mapping it to a DFA path and then a CFG path, having the symbolic execution engine solve the path constraint, and output a sequence of tuples saying how corruptible variables should be set (§2.5, p. 416; §3.4–3.5, p. 420).
The example grammar has init ::= Var = Val, three valid statements (*b = p, *c = *c + q, and print("%d", *a)), and attack ::= init; (vs1 + vs2 + vs3)* (Fig. 3, p. 416). The paper’s demonstrations use this grammar to read arbitrary memory and calculate Fibonacci numbers (Tables 1–2, p. 417); the paper notes that the Fibonacci attack needs some variables re-assigned at runtime, which the tool does not support (p. 417; §5, p. 425).
Inference: in Verus, represent the synthesized grammar as an inductive datatype or finite-state transition relation, prove that each compiler rule preserves the relation between grammar execution and a target-program abstract state, and use requires/ensures around payload construction. The SMT path solver, LLVM semantics, memory-corruption model, and actual vulnerable runtime need explicit trusted contracts; Verus cannot infer them from a grammar.
technique: passive versus active automata learning
Passive learning constructs an NFA for the observed finite trace set, determinizes and minimizes it; the resulting DFA accepts exactly the observed strings (§3.2.1, p. 419). It is sound when symbolic execution is sound, but incomplete when traces are missing. Active L* learning uses membership queries (reachability checks) and approximate equivalence queries; DOPPLER generates negative counterexamples by mutating traces and validating them with KLEE (§2.3, p. 416); §3.2.2 (Algorithm 3, p. 419) describes the approximate equivalence check as building a counterexample set of predetermined size N from strings of increasing length that are not in the observed set. The authors state the trade-off directly: passive learning prioritizes realizability, while L* may be more complete but unsound because it can accept strings beyond the observed set (§3.2.3, p. 419). The experiments use passive learning (§3.2.3, p. 419).
Inference: the paper says the passive DFA is acyclic because the trace set is finite (§3.2.3, p. 419), yet the grammars it shows for the experiments contain stars (Figs. 3, 6, 9); the paper does not reconcile these. Inference: a Verus model can prove DFA determinism, that passive-DFA accepted traces are among supplied sound traces, and that state elimination preserves the language. It cannot prove completeness unless symbolic execution is complete, nor can it turn L*’s approximate oracle into a sound theorem.
technique: one-shot payload compilation
After grammar synthesis, each user attack program is mapped to a DFA path and then to a CFG path; an SMT solver produces assignments for corruptible variables. This front-loads expensive analysis: “The first stage needs to be performed only once” (§4.2, p. 423). Payload generation then uses regular-expression syntax validation and path-constraint retrieval, “essentially a constant-time hashmap-based get operation” (§4.1, p. 421); stage-2 times are “consistently less than one second” (§4.2, p. 424).
Inference: verify that every emitted assignment satisfies the selected path’s constraints and that serialization preserves integer widths and pointer values. The paper leaves it to the user to set those variables, e.g., by providing the required input (§3.5, p. 420), so that final injection and runtime effects remain outside this proof.
evidence, assumptions, and limits
The evaluation uses six demonstration programs and 11 real-world programs, 17 total, with six attack goals: arbitrary read, arbitrary write, print, n-loop, summation, and linked-list construction (Tables 3–4, §§4–4.1, pp. 420–422); not every goal applies to every program (Tab. 4 marks inapplicable ones “–”). The only baseline is BOPC, because the authors could not obtain Steroids or Limbo (footnote 4, p. 420). DOPPLER generated assignments for every demonstration goal that is realizable and for all real-world memrd/memwr except memrd on sqlite and httpd (“the lack of a statement reading from the pointer that users can overwrite”); its print goal failed on six real-world programs for lack of printing functions in reachable paths (§4.1, p. 422). The paper counts sqlite’s nloop, summation and linkedlst as achieved because a valid statement calls system(zCMD), though these are not built by composing grammar statements (§4.1, p. 422). On cost, stage 1 takes on average about 20 times as long as one BOPC run, and longer than any single BOPC run except on pico and min-dop, but most BOPC runs produced no payload (§4.2, p. 424). L* timed out (2 hours) on four programs (§4.2, p. 424; Tab. 5, p. 424). Real-world programs were simplified for LLVM 13/KLEE by configuration changes, semantics-preserving rewrites, and branch pruning; the authors state these do not compromise the results and that they manually validated this, while noting automating or formally proving it is future work (§4 Benchmarks, p. 420; §5, p. 425). DOPPLER also needs hand-labelled vulnerable variables and KLEE annotations (§5, p. 425). Passive grammar generation is complete only relative to the observed traces; the paper says completeness cannot be guaranteed because symbolic execution cannot identify all reachable states (§7, p. 426). L* can accept unreachable traces. The grammar is regular only; programs needing context-free grammars are out of reach (§3.2, p. 419; §5, p. 425). Inference: KLEE, LLVM, SMT, annotations of corruptible variables, and the vulnerable runtime are trusted inputs.
Inference: for VL, the valuable pattern is a verified compiler from a constrained declarative program to executable state transitions, plus an explicit soundness/completeness choice for learned automata. Recreating a generic symbolic-execution attack synthesizer would duplicate this work; a new product should instead verify its domain-specific grammar and payload boundary. Inference: threat to agent-written verified Rust is high when unsafe control/data flow is exposed, because a grammar can systematically realize memory corruption; Verus can reduce implementation bugs but cannot make an intentionally vulnerable target safe.
techniques for the catalog
- program-specific attack grammar: synthesize a regular language of realizable DOP statements from one vulnerable program
- data/control variable analysis: classify attacker-dependent variables by branch influence and expose only data variables
- trace-based DFA learning: construct passive or L*-learned automata from symbolic execution traces
- state elimination grammar synthesis: convert the DFA into regular expressions and executable grammar rules
- SMT payload compilation: map a grammar program to a CFG path and solve assignments for the exploit payload Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The user is then expected to write an attack program using the synthesised grammar; the accompanying generated compiler will check it for syntax errors and output a sequence of tuples describing how corruptable variables should be set to construct a payload.”): read the whole paper text (abstract through references) and the whole study; checked every quotation, section and page reference, the seven pipeline steps, the soundness/completeness statements, the benchmark and attack-goal counts, and the Tab. 4 and Tab. 5 claims against the paper text. Changed: tag link to the presentation page given on the paper title page; Fig. 1 page 414 to 415; page and section references for steps 2-3 (Algorithms 1-2 are on p. 418 only), for the constant-time claim (§4.1, p. 421, not §4.2), and for the simplifications (§4 Benchmarks, p. 420, not §3.5); the counterexample-generation description (mutation with KLEE is §2.3); the soundness definition, evaluation details and limits were added, and unsupported framing marked “Inference:”. Not checked: the references, the artifact, the PDF figures beyond the text layer, and the Verus and VL inferences, which are my own judgments and not claims of the paper.
Last edited: