PaperlayerView exact revision on arXiv

Source-linked AI summary

Synthesizing Program Input Grammars

Osbert Bastani, Rahul Sharma, Alex Aiken, Percy Liang

arXiv:1608.01723v2cs.PL

TL;DR

Program-input grammar inference is difficult because existing algorithms rely on unavailable or incomplete examples and oracles, leading to poor or slow results. The paper introduces a blackbox synthesis algorithm implemented in GLADE, which learns regular and recursive structure from seeds and membership queries. GLADE outperforms established inference methods and improves valid-input fuzzing coverage by up to 6× against baseline fuzzers.

  • Problem

    Existing grammar inference algorithms can severely overgeneralize, be prohibitively slow, and depend on examples or oracles unavailable in blackbox program-input settings.

  • Method

    The paper synthesizes context-free program-input grammars from seed inputs and blackbox membership queries, learning regular properties before recursive productions.

  • Results

    GLADE substantially outperforms L-Star and RPNI and increases newly covered lines using valid inputs by up to 6× compared with two baseline fuzzers.

  • Takeaways & Limitations

    The synthesized grammars can drive grammar-based fuzzing and may also support input-format reverse engineering or input whitelisting.

  • Takeaways & Limitations

    Greedy search can synthesize suboptimal grammars that generate only a subset of the target language, even when selected candidates are precise.

Abstract

from arXiv · show

We present an algorithm for synthesizing a context-free grammar encoding the language of valid program inputs from a set of input examples and blackbox access to the program. Our algorithm addresses shortcomings of existing grammar inference algorithms, which both severely overgeneralize and are prohibitively slow. Our implementation, GLADE, leverages the grammar synthesized by our algorithm to fuzz test programs with structured inputs. We show that GLADE substantially increases the incremental coverage on valid inputs compared to two baseline fuzzers.

1. Introduction

The paper targets practical synthesis of program-input grammars from seed examples and blackbox membership queries, addressing limitations of existing inference algorithms. GLADE combines richer generalization with on-the-fly negative examples and improves grammar inference and valid-input fuzzing coverage.

  • Motivation: Poor or non-machine-readable input documentation motivates automatically synthesizing grammars for structured program inputs.Such grammars can support fuzzing, reverse engineering, input whitelisting, and other software-analysis applications.
  • Limitations of Existing Methods: Existing algorithms such as L-Star and RPNI can fail on simple input languages, overgeneralize or undergeneralize, and scale poorly in this setting.Their assumptions about complete positive examples and available negative or equivalence oracles do not hold for blackbox program-input learning.
  • Approach: The algorithm begins with the language of given positive examples and incrementally generalizes it while using membership queries to reject overgeneralizing candidates.Candidates add repetitions, alternations, recursive productions, or generalized constants.
  • Implementation: GLADE implements the approach and synthesizes grammars from seed inputs with blackbox program access.The implementation learns regular properties before recursive productions characteristic of matching-parentheses grammars.
  • Results: GLADE substantially outperforms L-Star and RPNI and increases newly covered lines using valid inputs by up to 6× compared with two baseline fuzzers.The valid-input fuzzing evaluation compares GLADE with a naïve fuzzer and afl-fuzz.

2. Problem Formulation

The problem is to approximate a structured target language of valid program inputs using seed inputs and blackbox membership queries. The synthesized context-free language is evaluated by precision and recall under distributions over valid and synthesized strings.

  • Target and Oracle: The target language L* is a structured subset of an input alphabet Σ*, and the goal is to synthesize an approximating language L̂.Blackbox access is represented by an oracle O that returns whether a queried input belongs to L*.
  • Target and Oracle: Seed inputs E_in ⊆ L* provide valid examples from which generalization begins.The paper notes that such seeds typically come from program test suites or documentation examples.
  • Running Example: In the XML-like running example, the target is the context-free language L(C_XML), with seed input α_XML and oracle O_XML.The grammar uses alternation and Kleene-star repetition to describe XML-like strings.
  • Evaluation Criteria: Exact learning cannot be guaranteed, so approximation quality is measured using probability distributions over the target and synthesized languages.The distributions are induced by sampling from probabilistic context-free grammars.
  • Evaluation Criteria: Precision is the probability that a synthesized string is valid, while recall is the probability that a valid target string is included in the synthesized language.The two measures capture different trade-offs between overly narrow and overly broad approximations.

3. Overview

The algorithm starts from a seed-only language and greedily applies ranked generalization steps whose candidates are tested with membership queries. It first learns regular structure, then translates to and further generalizes a context-free grammar with recursive productions.

  • Overview: The algorithm initializes the language as ˆL1 = {α_in} and constructs a sequence of increasingly general languages.If no candidate passes the checks, the current language is retained.
  • Overview: Steps R1-R9 generalize the seed language by adding repetitions and alternations, while steps C1-C2 add recursive productions.For the XML example, the regular-expression result is translated into a context-free grammar before recursive generalization.
  • Candidate Selection: Each generalization step constructs candidates ranked from most to least preferable and selects the first candidate that passes its checks.Candidates are monotone, so they contain the current language and can only increase recall.
  • Candidate Selection: Membership checks reject a candidate when any carefully chosen newly generated string is invalid under the blackbox oracle.Passing all finite checks makes a candidate potentially precision-preserving rather than proving it exactly.
  • Generalization Operators: The method considers repetition, alternation, recursive-grammar, and constant-generalization candidates to capture structured input languages.Figure 2 presents the candidate ordering, checks, and selected candidate throughout the example.

4. Phase One: Regular Expression Synthesis

Phase one greedily generalizes a seed input into a regular expression through repetition and alternation candidates, using oracle checks to avoid overgeneralization. Its candidate language covers essentially all regular languages, but efficiency comes at the cost of completeness.

  • Generalization steps: Phase one annotates the seed input with repetition or alternation opportunities and repeatedly generalizes one bracketed substring.The initial seed is annotated as [αin]rep; each step selects a bracketed substring and generates candidates from decompositions.
  • Candidate construction: Repetition candidates add starred subexpressions, while alternation candidates split a substring into two alternatives.The candidate rules require a nonempty repeated component or two nonempty alternating components; retaining the current expression is also a candidate.
  • Candidate construction: Candidates are monotone, so every proposed language contains the current language and can only increase recall.This property is stated as Proposition 4.1 for every phase-one candidate.
  • Candidate ordering: The algorithm ranks candidates heuristically, preferring decompositions expected to produce more general expressions, and greedily selects the first candidate whose checks pass.The ordering prioritizes shorter fixed prefixes and longer generalized components before ranking the unchanged candidate last.
  • Oracle checks: Finite residual-context checks test whether newly added strings are accepted by the membership oracle, rejecting a candidate when any check fails.Proposition 4.4 establishes that constructed contexts make these checks valid members of the candidate-minus-current language.
  • Complexity: O(n^3) is the phase-one complexity, with at most O(n^2) repetition candidates and O(n^3) alternation candidates for seed length n.The bound assumes each oracle query takes constant time.

5. Phase Two: Recursive Properties

Phase two translates the synthesized regular expression into a context-free grammar and merges repetition nonterminals to induce recursive structure. Membership checks constrain these merges, enabling generalized matching-parentheses grammars within O(n^4) overall complexity.

  • XML example: For the XML example, equating the tag and content repetition nonterminals yields matching tags without overgeneralizing the target language.The resulting language is non-regular because it contains matching-tag strings, while remaining contained in the XML language.
  • Translation: Phase two translates the regular expression into a context-free grammar whose nonterminals correspond to generalization steps and subexpressions.The translation preserves the regular-expression language while exposing repetition subexpressions as mergeable grammar components.
  • Merge candidates: The algorithm considers equating pairs of nonterminals corresponding to repetition subexpressions, an empirically motivated restriction that reduces imprecision.Recursive constructs are treated as typically repeatable, including matching-parentheses grammars.
  • Merge candidates: Each merge step compares an equated grammar with the unchanged grammar, selecting the preferred candidate only when heuristic membership checks pass.Equating nonterminals can only enlarge the generated language, so the candidates are monotone.
  • Expressiveness: Phase two can represent every generalized matching-parentheses grammar through a regular-expression translation followed by suitable merges.This is stated as Proposition 5.3 and its accompanying interpretation.
  • Complexity: O(n^4) is the overall complexity, because phase two examines pairs among at most O(n^2) repetition candidates.Here n is the length of the seed input.

6. Extensions

The extensions support multiple seed inputs and character generalization. Multiple inputs are combined before recursive merging, while terminal characters are generalized through oracle-tested alternatives.

  • Multiple seed inputs: With multiple seed inputs, phase one synthesizes one regular expression per input, combines them by alternation, and then applies phase two.Inputs already accepted by the accumulated expression can be skipped as an optimization.
  • Character generalization: Character generalization replaces a terminal with an alternation containing that terminal and another alphabet symbol, retaining the current language as an alternative.Each terminal-symbol pair is considered exactly once during this phase.
  • Character generalization: The character phase uses residuals and contexts to construct oracle checks for candidate substitutions.The checks combine a generalized residual with surrounding context from the current expression.
  • XML example: For XML, character generalization broadens content symbols from h and i toward a through z, while rejected checks prevent invalid substitutions such as replacing < with a.The resulting regular expression is later generalized by phase two into a grammar.

7. Discussion

GLADE’s evaluation shows near-perfect grammar recovery from 50 examples, with phase two providing an additional 5–10% improvement over phase one. Its greedy strategy is efficient but can produce suboptimal subsets of the target language.

  • Performance: Figure 4 compares F1 score and running time across L-Star, RPNI, GLADE without phase two, and full GLADE, plus XML sensitivity to seed count.The XML panel separates precision, recall, and running time using distinct line styles and y-axes.
  • Limitations: Greediness can synthesize a grammar that generates only a subset of the target language, even when every selected candidate is precise.The limitation arises because early choices can prevent later repetition nodes from being merged.
  • Greedy search: Greedy search is most suitable when target languages contain fewer nondeterministic constructs, because fewer incompatible candidates reduce suboptimal choices.The discussion relates this condition to many practical program input languages.

8. Evaluation

GLADE synthesizes context-free input grammars from blackbox access and seed inputs, then uses them for grammar-based fuzzing. Across language-inference and fuzzing experiments, it generally outperforms established baselines, while remaining subject to context-free and representation limitations.

  • Approach: GLADE synthesizes a context-free grammar from an oracle and seed inputs, then uses the grammar with a standard grammar-based fuzzer.The implementation supports both grammar synthesis and structured test-input generation.
  • Approach: The sampler recursively expands nonterminals and emits terminals, with production choices sampled uniformly.This sampling procedure defines the distribution used for evaluation and grammar-based fuzzing.
  • Language inference: With 50 training examples, GLADE learned each evaluated grammar with an F1-score near 1.0, indicating nearly 100% precision and recall.Its performance remained strong with few samples, and running time scaled well with the number of samples.
  • Language inference: GLADE performed 5-10% better than its phase-one variant, with most improvement attributed to active learning and the remainder to inducing context-free grammars.The full system was also faster than phase one in the multiple-input setting because it generalized better and used fewer samples.
  • Language inference: GLADE addresses incomplete examples and unavailable equivalence oracles more effectively than L-Star and RPNI, which can fail dramatically or require very long runtimes.RPNI can omit terminals absent from seed inputs, while L-Star may issue many membership queries and fail on small automata.
  • Limitations: GLADE’s synthesized grammar may differ structurally from the target grammar while generating the same language, and its XML grammar excludes repeated attributes.The repeated-attribute constraint is non-context-free, so GLADE learns a subset of the XML input language.
  • Fuzzing: For six of eight programs, GLADE generated valid inputs covering new code paths 1.3 to 7 times better than the naïve fuzzer, though it was weaker on Sed and only slightly better on Grep.The evaluation metric measures coverage from valid inputs while excluding lines already covered by the seed inputs.
  • Fuzzing: GLADE recovered more of the proxy coverage upper bound than the naïve fuzzer on several complex programs and quickly found high-coverage inputs as sample counts increased.A sizable gap remained against very large, purpose-built Python and Javascript test suites.

9. Related Work

The paper situates GLADE among grammar inference, input-format mining, and fuzzing research. Unlike prior approaches, it targets complex recursive program-input languages using blackbox access and membership queries.

  • Prior input-format mining often uses dynamic taint analysis or focuses on understanding given protocol inputs rather than learning grammars.
  • GLADE is fully blackbox, depends only on accepted inputs, and can learn formats for uninstrumentable or remote programs.
  • Existing learning algorithms such as L-Star and RPNI often require oracle-provided examples, whereas GLADE actively generates examples through a membership oracle.
  • Grammar-based fuzzing uses grammars to generate valid inputs, while whitebox fuzzing guides generation through program inspection or symbolic execution.
  • The paper claims to be the first work targeting complex recursive program-input languages such as XML, regular-expression formats, and programming-language syntax.

10. Conclusion

The conclusion presents GLADE as a practical algorithm for inferring program-input grammars and demonstrates its value for fuzz testing. The appendix proves properties of the algorithm’s generalization steps.

  • 10. Conclusion: GLADE is presented as the first practical algorithm for inferring program-input grammars.
  • A.2 Proof of Proposition 4.4: Phase-one candidates are monotone, and the contexts constructed by phase one satisfy the stated invariant.
  • A.2 Proof of Proposition 4.4: The proof analyzes repetition and alternation cases to show that newly constructed contexts preserve the invariant.

A.2 Proof of Proposition 4.4

The proof establishes that contexts constructed during phase two preserve the required invariant. It proceeds by separately analyzing repetition and alternation candidates.

  • The proof begins from the initial context and assumes the current context satisfies the required invariant.
  • Repetitions: For repetition candidates, the constructed contexts place surrounding fragments around the selected subexpression and preserve the invariant.
  • Alterations: For alternation candidates, the constructed contexts incorporate the alternative branch while preserving the invariant.
  • The section is a proof of the proposition governing the validity of these context constructions.

B.1 Correspondence to Derivations in Cregex

This appendix proves that the grammar class Cregex can represent regular expressions through the algorithm’s generalization steps. It handles concatenation, alternation, repetition, and empty-language cases by structural transformations.

  • Proposition 4.2 states that derivations in Cregex can be transformed into phase-one generalization steps.
  • The proof uses backward induction to reconstruct each preceding expression from a derivation step while preserving the required mapping.
  • Nonempty-factor assumptions ensure that reconstructed repetition and alternation expressions remain valid.
  • Proposition 4.3 shows that any regular language can be expressed as a finite union of regular expressions synthesizable by phase one.
  • The grammar is extended with a start symbol and productions so regular expressions can include top-level alternation and an explicit empty-language terminal.
  • An empty-string seed handles explicit empty-string alternatives, while multiple inputs handle top-level alternations.
  • Structural induction repeatedly transforms concatenation and alternation forms until components are terminals or repetitions, and termination follows from finite parse trees.
  • The transformation cases for concatenation, alternation, and repetition remain within the grammar class, establishing the claimed expressiveness.

C.1 Proof of Proposition 5.1

The proof shows that merging nonterminals preserves the relevant language inclusions and that the translation construction can match a generalized matching-parentheses grammar exactly.

  • Proposition 5.1: Merging nonterminals yields L(PR′Q) ⊆ L(˜C) and L(P′RQ′) ⊆ L(˜C).The result extends to any phase-two merge because later merges only enlarge the generated language and merge order does not affect the final grammar.
  • Proposition 5.1: A one-sided merge can add the productions for A′j while preserving L(PR′Q) ⊆ L(˜C).The added productions generate a language contained in the existing language for Ai, so they do not change the grammar's language.
  • Translation construction: The translation assigns nonterminals to derivation steps and adds productions according to the corresponding expansion, including auxiliary repetition nonterminals.Alternation steps add productions such as Ai → Aj | Ak, while repetition steps use auxiliary symbols.
  • Expressiveness construction: A directed graph over nonterminals identifies derivation contexts, with spanning-tree paths constructing the required derivations.An edge Si → Sj indicates that Sj occurs in a derivation of Si; absent paths identify nonterminals that cannot occur from S1.
  • Proposition 5.3: The expressiveness construction translates X and M into C′ with L(C) = L(C′).Each production of C appears in C′, and the invariant L(Xi) ⊆ L(C) survives every merge.
Loading 1608.01723v2…