Making Semantic Tests Scale

SPAR’s refinement loop is only useful if it can generate enough informative packets without turning every possible path into a new, expensive reasoning task. This chapter focuses on that engineering problem: how the method represents formats and parser control flow as graphs, uses accumulated constraints to generate positive and targeted negative packets, and selects RFC context without losing cross-field meaning. The result is a bounded test strategy, not an exhaustive enumeration of every malformed combination.

A graph turns a format into possible packets

A formal format is easier to test when its structure is explicit. SPAR represents a packet format as a packet format graph. Each vertex carries a field’s type, name, and constraint. An edge records the sequential relationship between fields. A path through the graph therefore represents one possible layout of a packet, together with the conditions that must hold along that path.

The same idea applies on the parser side, where the relevant graph is a control-flow graph. Its paths represent possible execution routes through the reference parser. The graphs are not interchangeable: a format graph describes a declarative layout, while a parser graph describes executable behavior. But both provide a way to select a bounded slice of the system and collect the constraints that govern it.

For a format path, SPAR gathers the constraints attached to its vertices and combines them. A path through a conditional field includes the condition that selects that case. A path through a structure includes the fields in their required order. The result is a single logical condition describing one possible packet layout. The graph is useful because it preserves both dimensions that a flat list loses: which fields occur together and which relationships must hold along that route.

Variable-length fields make this accumulation especially important. A later array may not have a constant size, but its size can be determined by values already encountered. Babel’s Prefix field is the paper’s example: the length depends on Plen and Omitted. When a path reaches that field, the solver can use the accumulated constraints to find values that make the resulting length concrete. The generator can then unfold the variable-length portion for that candidate instead of guessing a size unrelated to the preceding fields.

This is a boundary between packet structure and packet generation. The graph does not merely say that Prefix exists. It records the condition under which Prefix has a particular length. A generated packet that ignores that dependency may still be byte-shaped, but it would not test the Babel format that the RFC describes.

One constraint produces two kinds of packet

Once a path has a combined condition, a solver such as Z3 can search for values that satisfy it. The resulting positive packet is a concrete witness that the selected path and its constraints can coexist. It is useful for checking that a reference parser accepts a valid case and for exercising an implementation along a meaningful path.