From Fields to Invariants
SPAR’s central problem is not how to name the fields in a packet; it is how to represent the rules that make those fields meaningful together. This chapter focuses on that representation through Babel’s Update message. By the end, a reader should be able to look at a field range, a conditional layout, or a length calculation and ask the more important question: which other fields must agree with it for the packet to be valid?
A range is not a relationship
An allowed-value rule belongs to one field. If a protocol says that a type field must equal a particular value, or that a length must fit within a fixed width, a parser can check that field locally. Such rules are important, but they are not enough to describe a packet whose layout or meaning changes with its contents.
A semantic dependency connects two or more values. It can be written as a predicate: a condition that is true for acceptable combinations and false for combinations the protocol does not define as valid. The distinction is easiest to see with a simple contrast. “AE is between 0 and 3” is a range check. “If AE is 3, Omitted must be 0” is a relationship. The second rule cannot be evaluated correctly by inspecting either field in isolation.
This difference also changes how a test should be designed. A random value outside a field’s range tests whether the parser rejects an obviously malformed value. A relationship test keeps the surrounding packet plausible and changes one dependency. If a packet has a valid type, a permitted length, and a representable address-encoding value, but one field combination violates the protocol’s condition, the result tells us something much more specific about the implementation.
The paper behind SPAR describes formal format specifications in this way. A field has a type, a name, and a constraint. The constraint can be a predicate over one field or over several fields. A formal description therefore records more than the order of bytes: it makes dependencies explicit enough for a solver to reason about them and for a generator to construct packets that satisfy or violate them deliberately.
That formal step matters because RFCs are written for human readers. Their rules may be distributed across a packet diagram, a paragraph about one field, a definition in another section, and a cross-reference that supplies the missing context. A person familiar with the protocol can mentally combine those pieces. An automated method must either preserve the dependency or risk producing a polished but incomplete description.
Conditional layouts make fields depend on one another
Some dependencies concern validity directly. Others concern interpretation. A field may select which fields follow it, or determine how many bytes should be consumed. In those cases, the packet’s layout is conditional rather than fixed.
Consider a packet with a mode field followed by a value whose type depends on that mode. The mode does not merely carry information for the application; it controls the parser’s path. A format that lists every possible value type without recording the selector relationship may still look detailed, but it cannot say which layout is legal for a particular packet. The same problem appears when a count or prefix length determines the size of a later array.
Babel’s Update message contains both kinds of dependency. Its fields include the message type, body length, address encoding (AE), prefix length (Plen), omitted-byte count (Omitted), and the prefix data itself. AE determines how the address-related value is encoded. Plen describes the advertised prefix in bits. Omitted says how much prefix material is not carried at the beginning. The number of Prefix octets that remain is therefore not an arbitrary constant; it depends on the values already read.
In the formal example used by the paper, the Prefix length is represented as (Plen + 7) / 8 - Omitted. The exact expression is less important than the dependency it exposes. Before the parser can know how many Prefix bytes belong to this Update, it must interpret Plen and Omitted. A test generator that treats Prefix as an unrelated fixed-size blob can produce packets that are convenient to generate but do not exercise the real format.
This is why conditional layouts should be treated as semantic structure, not merely parser implementation detail. The condition determines both the shape of the packet and the meaning of the bytes occupying that shape. If a generator gets the condition wrong, it may test the wrong path. If a parser gets it wrong, it may consume bytes as one address representation when the protocol requires another.
The dependency has two directions. AE influences how the address-related data is interpreted, while Plen and Omitted influence how much data is present. In a real format, these relationships can form a small network of constraints rather than one simple parent-child link. A correct model must preserve the direction of influence without confusing it with the order in which fields happen to appear on the wire.
The diagram is intentionally small. It does not attempt to reproduce the whole Babel format. It shows the point that a field list hides: the Update is a structure, but it is also a set of constraints linking the structure’s parts. AE selects an interpretation; Plen and Omitted influence the amount of Prefix data; and the special rule for one encoding case constrains a second field.
The Babel Update rule is a contract over fields
RFC 8966 describes Babel’s packet encoding with a combination of local definitions and conditional statements. An Update TLV is identified by its type value. Its body has a length, and its address-related fields carry values that determine how a prefix is represented. A reader can understand each field’s ordinary purpose without yet seeing the complete validity condition.
The crucial condition is the special case for AE = 3: Omitted must be zero. For other address encodings, the omitted-byte count is bounded by the number of octets implied by Plen. In the formal representation shown in the paper, the rule appears as a predicate attached to the fields rather than as a note that can be separated from them: AE == 3 && Omitted == 0 for the special case, together with the corresponding bound for other cases.
Notice what this rule does not say. It does not say that AE is invalid, or that Omitted is always invalid when nonzero. The validity of Omitted depends on the value of AE. That conditional structure is exactly what field-by-field validation loses. A parser can check that the address encoding is in range and that the omitted count fits in its field width, yet still accept a combination the RFC forbids.
The rule also illustrates why field order and semantic dependency are not identical. AE appears before the address data, so it is natural for a parser to use it as a dispatch value. But the fact that AE is read first does not by itself express the obligation imposed on Omitted. The parser must carry the relationship forward into its validation logic. A format model must do the same.
There is a second source of difficulty: the full meaning of a field may be defined somewhere other than the paragraph that introduces a particular packet. The paper’s related Babel example concerns AddressEncoding, a parameterized case type used by an IHU structure. The IHU discussion describes only some address-encoding cases, while a separate address-encoding section supplies the broader mapping between AE, address family, compression, and length. Reading only the local structure can therefore produce a constraint that is correct for the examples mentioned there but incomplete for the type it invokes.
This is not an argument for giving an automated system every line of every RFC on every refinement step. Too much context can make it harder to focus on the mismatch being investigated. It is an argument for preserving dependencies when selecting context. If the validity of one field depends on a type, and that type is defined elsewhere, the related definition is part of the evidence needed to interpret the field.
The same principle applies beyond Babel. A flag may change the length of a following section. A count may be required to match the number of repeated elements. A checksum may cover a range whose boundary is determined by another field. A state value may permit one message type and forbid another. These examples share a structure: the parser must make a decision at one point, but the evidence for whether that decision is valid may be distributed across multiple fields and multiple parts of the specification.
From invariant to a meaningful test
Once the rule has been expressed, a semantics-aware test can be precise about what it is asking. A positive packet satisfies the Update structure and its relevant predicates. A negative packet can preserve the surrounding structure while negating one selected condition—for example, using the special AE value with a nonzero Omitted value. The test is not simply “send something unusual.” It is “send something that should be rejected because this one relationship is false.”
That distinction gives the result an interpretable boundary. If a reference parser rejects the negative packet, that is evidence that it enforces the selected rule. If it accepts it, the model and parser disagree. The disagreement does not automatically identify the guilty artifact; the formal rule may have been transcribed incorrectly, the parser may have omitted the check, or the RFC context may be insufficient. But the packet has done useful work: it has isolated a proposition that can be inspected.
The same contract can be used against an implementation. The paper describes an FRRouting Babel parser that lacked the AE/Omitted check. A negative packet that violated the relationship was accepted because the implementation did not enforce it. The paper connects the omission to incorrect address computation and routing consequences. The security significance comes from the semantic role of the fields, not from the packet’s ability to crash the process.
This is also why a formal constraint should retain its qualifiers. The rule about AE = 3 is one Babel invariant, not a complete account of Babel validity. It should not be merged with the separate rules governing reserved bits, Router-ID construction, sub-TLV handling, or other message types. Each relationship needs its own evidence and its own targeted test. Otherwise, a broad label such as “Babel parser correctness” hides which claim was actually checked.
The practical model is now clear. A field range describes what a value may be in isolation. A semantic invariant describes how values must agree. A conditional layout describes how one value changes the interpretation or size of another. A meaningful fuzz input is built from one of those claims, so that the parser’s decision can be compared with an explicit expectation.
SPAR’s next challenge is to make this model operational at scale. It must generate a formal format and a reference parser from natural-language RFCs, expose disagreements between them, and supply enough related context to repair a missing dependency without drowning the process in irrelevant text. The Babel Update rule is small enough to understand by hand; the method’s real test is whether the same discipline can be applied repeatedly across complex protocol formats.