Grammar-based fuzzers have shown immense promise in identifying bugs in software systems that have highly-structured and intricate input formats (\eg, XML). Many of the existing grammar-based fuzzers rely on context-free grammars (CFGs) to represent the target’s input structure. CFGs, however, are often insufficient to precisely capture many application input formats containing context-sensitive constraints. Application-specific fuzzers, albeit effective, lack generality to be adapted to new applications. In this paper, we present Goblin, a new input generation language and tool that helps bridge this gap. Given a context-free grammar annotated with semantic constraints, Goblin generates inputs that both conform to the grammar and satisfy the constraints. While a few prior techniques target this problem, our method is distinguished by: $(i)$ support for constraint solving over arbitrary SMT theories (e.g., bitvectors, integers, strings); $(ii)$ a minimal core input language with formal semantics that is smaller and less complex than prior work; and $(iii)$ a shift from global constraints to local, production rule constraints,
which enables easier integration with certain fuzzing workflows. Goblin’s input generation approach is inspired by DPLL-style SAT solvers and enjoys the following formal guarantees: \emph{solution soundness}, \emph{solution completeness}, and \emph{refutation soundness}. In addition to comparing Goblin with prior work, we demonstrate its effectiveness by incorporating it into a grammar-based network protocol fuzzer.