From 0ffa2b4341297829f1ab24edf36a7c0d98ecd437 Mon Sep 17 00:00:00 2001 From: Daniel Noland Date: Tue, 11 Aug 2026 11:23:28 -0600 Subject: [PATCH 1/7] docs(testing): Record the config-algebra testing strategy A design note for testing the config-driven dataplane, plus links to it from the code guidelines and the property-testing guide. Nothing in it is implemented. Its value is mostly in the approaches it rejects, because each of those looked obviously right at the start of a conversation and turned out to be a dead end for a reason worth keeping: * Generating configuration values directly. A `TypeGenerator` over the config types yields syntactically valid, semantically impossible configurations -- colliding VNIs, peerings between VPCs that do not exist -- so the validator refuses nearly all of them and a coverage-guided fuzzer spends its budget exploring rejection paths. Filtering does not help, because the generator would then have to encode the validator's rules, leaving two copies to keep in agreement. Build configurations from an algebra of valid operations instead, and preconditions become unrepresentable rather than checked. * A shadow model as the oracle. It grows into a second dataplane, drifts from the first, and has to be rewritten whenever the real one is refactored. Operations emit claims about observable behaviour instead. * Reimplementing rule selection, or discovering precedence by ablation. Both are unnecessary: `acl/src/reference/` already answers "which rule should have won, and which did it shadow" in one pass, and the vocabulary in `match-action` is general enough to serve every function that consults a table. That reference scales with the match vocabulary rather than with the feature set, which is what keeps it from rotting. * Following the algebraic notation toward rigour. There is no inverse for "transmit a session", and the nearest thing to one advances the clock until transients decay. Chasing that ends in rebuilding a temporal logic. We want to find defects, not prove their absence, so the notation is a naming scheme for test shapes and nothing more. * Putting the oracles at the boundary of the whole pipeline. An ACL that drops traffic before the router sees it hides the router completely, and the expectation becomes a cross-product over domains. Contracts belong to individual network functions; pipeline behaviour is their composition. The recurring theme is that an oracle derived from the same source as the implementation cannot see that source being wrong, and that the way out is always to find something genuinely independent -- a parser, a transport protocol, a second walk over the same data. Two constraints are recorded as requirements on work that has not started yet, because both are cheap to honour in advance and expensive to retrofit: the generation-propagation logic of the planned network-function DAG has to be a pure state machine over a small hashable state, and a match-action rule has to name its action completely enough to serve as the specification for it. The note is a record under revision rather than settled doctrine; its open questions are live, and several of them are questions about this repository that nobody has answered yet. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: Daniel Noland (cherry picked from commit 74d430440c5b40bd309786b1a31baae693d4c679) --- development/code/README.md | 3 + development/code/config-algebra-testing.md | 982 +++++++++++++++++++++ development/code/property-testing.md | 8 + 3 files changed, 993 insertions(+) create mode 100644 development/code/config-algebra-testing.md diff --git a/development/code/README.md b/development/code/README.md index 7e512e6f92..8a87f3dff8 100644 --- a/development/code/README.md +++ b/development/code/README.md @@ -12,6 +12,8 @@ wrong thing. If you need to write a test, prefer [property-based tests] over simple unit tests. +For inputs too large to generate directly -- a whole configuration, say -- build them from an algebra of +valid operations and derive the oracles from that same algebra; see the [config algebra note][config-algebra]. If you need to handle errors, prefer `Result` types over panics in general, but see the [error handling guide][error] for details. @@ -21,6 +23,7 @@ If you need to [handle an error][error], follow the guidelines. [avoid-global-reasoning]: ./avoid-global-reasoning.md [property-based tests]: ./property-testing.md +[config-algebra]: ./config-algebra-testing.md [error]: ./error-handling.md ## Testing instructions diff --git a/development/code/config-algebra-testing.md b/development/code/config-algebra-testing.md new file mode 100644 index 0000000000..335dbc3bed --- /dev/null +++ b/development/code/config-algebra-testing.md @@ -0,0 +1,982 @@ +# Testing a config-driven dataplane with an operation algebra + +Status: **design note**. Nothing here is implemented yet. It records a strategy and, more importantly, +the reasoning that rejected the alternatives, so that the next attempt does not rediscover them. + +## The problem + +k8s and the config validator decide what configurations exist. The dataplane is bound by that +decision: it has no channel to tell an operator "I refused your config," so **everything which passes +the validator must in fact be enactable**. Testing that claim needs two things, and the second is the +hard one: + +1. a supply of valid configurations, and +2. a way to know whether the dataplane did the right thing with one. + +Neither is served by generating configuration values directly, and the reason generalises. + +## Why not generate configurations directly + +A [`TypeGenerator`] over the config types produces values that are *syntactically* valid and +*semantically* nonsense: colliding VNIs, peerings between VPCs that do not exist, features named +where they are not rendered. The validator rejects nearly all of them, so a coverage-guided fuzzer +spends its budget exploring the validator's rejection paths rather than the enactment path we care +about. + +Filtering does not rescue it. To generate configs that pass validation, the generator has to encode +the validator's rules -- and then there are two copies of those rules to keep in agreement, which is a +worse problem than the one being solved. + +Reaching for a narrower [`ValueGenerator`] each time the fuzzer cannot get somewhere does not scale +either, and there is local evidence. Covering `net::headers` needed four bespoke generators -- +`ShapedHeaders`, `ShapedQuote`, `ThinHeaders`, `SometimesHeadless` -- each written because the +previous one could not reach one more shape. They do not compose, and each encodes a little more +knowledge of the implementation. At the scale of a whole configuration that pattern does not +terminate. + +## The algebra + +Build configurations by construction instead. A configuration is a fold of operations over the blank +config: + +```text +X = E . D . C . B . A where A = blank, B = add a VPC, C = add another, D = peer those two, ... +``` + +The generator draws an **operation sequence**, not a configuration. Two consequences: + +- **Preconditions become unrepresentable rather than checked.** If `peer` takes handles to VPCs that + already exist, a peering between absent VPCs cannot be expressed. This is the same move as + enforcing an invariant in the type system rather than validating it at runtime, which the + [code guidelines](./README.md) already ask for. +- **Every generated configuration is valid by construction**, so the generator never needs to know + the validator's rules. + +A partially modelled algebra yields partial coverage of the configuration space. That is a feature: +model a manageable subset, fuzz it, fix what falls out, then extend the vocabulary. What grows is the +set of operations, not a collection of single-purpose generators. + +### Checking the algebra is not lying + +The algebra reaches exactly the configurations its operations compose to, which may be a strict subset +of what the validator accepts. Configurations outside its reach are invisible to the fuzzer, and +nothing about a green run says otherwise. + +So treat the algebra's completeness as its own property: take real configurations -- from CI, from the +field -- and assert each is expressible as an operation sequence. A configuration that is not points +at a missing operation. + +## Updates come along for free + +The property "the dataplane must be able to move from config `X` to config `Y`, for all legal `X` and +`Y`" is true and useless: the space of pairs is far too sparse to fuzz. + +Generating `X => A.X` instead -- one operation applied to an already-built configuration -- exercises a +single *species* of update at a time, which is both tractable and diagnosable. The general property is +recovered by composition: `A.X`, then `B.A.X`, then `C.B.A.X`. + +The dataplane does not have to observe the intermediate states. It may be handed several operations at +once, and should be, since batching is what production does. + +### Deletion is where the bugs live + +An algebra of only additive operations will look healthy and find little. The interesting failures are +in removal and modification, because a deletion's footprint is *everything that referred to the +deleted thing*. + +Both known scars are of this kind: rollback to a blank config leaves the previous config's ACL, NAT +and flow-filter tables live (the blank path returns early, before every table writer), and the +masquerade overlap defect was a config change underneath live NAT allocations. Model removal and +modification early. + +### Every operation needs an undo, and the undo is not a function of the operation alone + +For every `A` in the algebra there should be an `A^-1` that reverses it, which buys the whole +"configuration existed and was then removed" class -- as important as the add case and much less +travelled. + +It is not a group, though, and pretending otherwise will bite. The reverse of `set_flow_table_capacity(n)` +needs the *previous* capacity, so it is a function of the operation **and the state it was applied to**, +not of the operation alone. Model it as an undo log rather than an inverse element: + +```text +apply(A, X) -> (X', undo) where undo(X') == X +``` + +Two things fall out. + +**`undo . A` is the cleanest state-leak probe available.** The configuration afterwards is provably +identical to the configuration before, so *any* difference in observable behaviour is attributable to +runtime state and nothing else. No other experiment controls for configuration that exactly, which +makes this the sharpest available test of the "never resurrected" disposition below. + +**A missing undo is a product finding, not a test gap.** An operation whose reverse is not expressible +is a configuration change an operator cannot walk back. That is an operational hazard worth reporting +even though no test failed. + +### Algebraic laws are metamorphic relations + +Calling it an algebra earns something concrete: its laws are testable. If `A` and `B` commute then +`A . B . X` and `B . A . X` must agree, and that is checkable without knowing what either produces. + +Distinguish two strengths, because conflating them manufactures false positives: + +- **Configuration-level commutation** -- the resulting configurations are equal. Cheap, and a pure + property of the `config -> tables` half. +- **Behavioural commutation** -- the resulting dataplanes behave the same. Strictly stronger, and it can + fail while the configurations are equal, *legitimately*: the two orders allocate NAT ports in + different sequences, so live flows get different translations. State the property over the observable + projection -- verdicts and reachability -- never over raw state. + +### Derive commutation from read and write sets, do not declare it + +Commutation is *not* a property of a pair of operators. `peer(A, B)` and `add_vpc(C)` commute; `peer(A, B)` +and `add_vpc(A)` cannot be swapped at all, because `peer` needs A to exist. The difference is definedness +inherited from everything earlier in the sequence, so any table of commuting pairs is wrong as soon as it +leaves the position it was written for. + +Give each operation a **read set** and a **write set** instead, and derive commutation the way a database +scheduler does: + +| conflict | commutes | +| --- | --- | +| write-write | no | +| read-write | no | +| read-read | yes | + +`peer(A, B)` reads VPC A and VPC B and writes peering AB. `add_vpc(C)` writes VPC C -- no conflict, so they +commute. `add_vpc(A)` writes VPC A, which `peer(A, B)` reads -- a read-write conflict, so they do not. +**Preconditions stop being a special case**: a precondition is exactly a read of something an earlier +operation wrote. + +This costs `O(n)` footprints rather than `O(n^2)` declarations, is independent of position, and the write +set is the same metadata the frame condition already needs. Formally this makes the sequences a trace +monoid, but none of the theory is required -- only the conflict test. + +It also generates a test family for free: two sequences related by swaps of adjacent non-conflicting +operations must produce equivalent pipelines, so the whole equivalence class of a generated sequence is +checkable. + +## Oracles as contracts + +The tempting oracle is a shadow model: give each operation an `apply_to_model()` that maintains an +expected copy of the tables, then compare. Do not. The shadow model grows into a second dataplane, it +drifts from the first, and it has to be rewritten whenever the real one is refactored. It is the same +non-composing trap as the bespoke generators, one level up. + +Instead each operation emits **claims about observable behaviour**, stated in operator-facing terms. +`peer(A, B)` claims things like "traffic from A's subnet to B's subnet is not denied", "its +translation is reversible", "no verdict involving any other VPC changed". Claims conjoin, so oracles +compose; and because they describe behaviour rather than representation, they survive a rewrite of the +representation. + +Each operation then has four parts, which are the familiar contract pieces: + +| part | what it is | where it lives | +| --- | --- | --- | +| **precondition** | the state the operation needs | unrepresentable, by construction | +| **postcondition** | positive claims the operation adds | test-side, accumulated | +| **invariant** | local consistency of the structures it touched | `debug_assert!`, in place | +| **frame** | everything outside its footprint is unchanged | test-side, probe set | + +### The frame is the highest-value part + +Overlapping NAT and ACL rules are hard to oracle absolutely: predicting which of several matching +rules wins means reimplementing the matcher. But **overlap bugs are frame violations**, and the frame +is easy to state: + +> Adding a peering for VPC A changed nothing observable for VPC B. + +That is cheap, catches the entire cross-talk class, and is completely indifferent to how NAT is +implemented. + +Frames need a probe set re-run after each operation, so the cost is `operations x probes`. Keep it +affordable by deriving probes from the algebra too: each operation contributes a handful at its own +boundary -- inside the subnet, just outside it, the adjacent prefix -- which gives relevance without +enumerating address space. + +### The peering graph indexes the frame + +VPC peering is a graph relation, and it supplies the footprint the frame needs -- which is otherwise the +awkward part to pin down. + +Two graph notions are in play and they are **not** the same: + +- **Reachability is a direct edge.** `VpcPeering` is pairwise, narrowed further by what each side's + manifest exposes and by the peering-scoped ACL. It is not transitive: peerings `A-B` and `B-C` create + no path from `A` to `C`. +- **Non-interference is a disjoint component** of the transitive closure. If `A` and `B` fall in + different components, nothing done in one can be observed in the other. + +The second is tenant isolation, and it has two halves worth stating separately: + +1. **Spatially** -- no packet confined to one component is ever observed in another. +2. **Operationally** -- no configuration change or state mutation confined to one component changes any + verdict in another. + +The second half is exactly a frame condition, indexed by graph component instead of by operation +footprint. So for the whole family of VPC operations, the connected component *is* the footprint, and +the graph tells you which probes must come back unchanged. + +This is the highest-value property in the document. It is negative, so it is cheap to state and +indifferent to implementation; it is a *security* property, so its failures differ in kind from +functional bugs; and it is stated in domain terms, so it should outlive any rewrite underneath it. + +#### The generator has to be pushed into producing disjoint components + +Peering random pairs of VPCs produces a single giant component almost immediately -- the threshold is +around one edge per VPC -- and in a connected configuration the isolation property is vacuously true +and never tested. + +So the operation vocabulary needs to distinguish "peer two VPCs already in the same component" from +"peer across two components", and the generator has to be biased toward keeping several components +alive. Count configurations with two or more components and assert on it; this is precisely the kind of +reachability failure the [vacuity](#vacuity) guard exists to catch. + +### Making an oracle composable + +An oracle is a **projection plus a predicate**: a view of the world, and a claim about that view. It +names what it needs rather than where that lives, so a refactor re-points the projection and leaves +the predicate untouched. + +There is a working example in `net/src/headers/view.rs`: the `Addrs` trait projects a tuple of layer +references of any arity down to an array of addresses, and the predicate is plain equality. One check +covering eight arities, where previously the same check had to be hand-written per arity and so +existed at only two. + +## You never need an end-to-end oracle + +The reason a whole-dataplane oracle looks intractable is that it is framed as a function oracle: given +a config and a packet, what should happen? That requires a second dataplane. Decompose instead: + +```text +config --[A]--> tables --[B]--> verdict +``` + +- **A is a pure, total function.** A differential oracle is affordable here: write a slow, obviously + correct table builder and compare. No netlink, no FRR, no pipeline needed. +- **B is per-packet.** Use metamorphic relations and invariants. + +Oracles for `A` and `B` compose. `A . B` needs no oracle of its own, which is what makes the whole +thing tractable. + +This is one of *two* independent decompositions, and they cut along different axes. This one splits +configuration handling from packet handling. The other splits packet handling across the pipeline stages -- +see [contracts belong to network functions](#contracts-belong-to-network-functions-not-to-the-dag). Both are +needed and neither substitutes for the other. + +### Metamorphic relations for the per-packet half + +Do not say what the output is; say how outputs relate under transformations of the input. + +- **ACL** -- adding a deny never widens the accepted set; adding a permit never narrows it; reordering + rules with disjoint match sets changes no verdict. +- **NAT** -- translate then reverse is the identity on the 5-tuple; distinct live flows never collide + in translated space; translation preserves protocol and payload. +- **FIB** -- adding a less specific route changes no existing decision; adding a more specific one + changes decisions only for addresses inside it; deletion is the inverse. + +Rule *precedence* is deliberately absent from that list. It looks like it needs either a +reimplementation of the matcher or an ablation sweep -- removing rules one at a time to see when the +verdict changes, at `O(n)` executions per packet. Neither is necessary: see +[the selection oracle](#the-selection-oracle-is-already-built) below. + +## The part that is not free: state across transitions + +The dataplane is **not a pure function of its configuration.** Live flows, NAT port allocations, FIB +contents and neighbour state all survive a config change. + +So passing every oracle for every legal config `X`, with the dataplane born blank under `X`, is *not* +evidence of sensible behaviour having arrived at `X` from `W` carrying `W`'s state. The masquerade +overlap defect lived exactly in that gap. + +The fix is to extend the frame from config-derived tables to **runtime state**. Each operation +classifies every piece of live state it could touch into one of three dispositions, and each is a +claim: + +1. **Preserved** -- state still legal under the new config keeps behaving identically. Same verdict, + same translation. This is what "do not break established connections" means concretely. +2. **Invalidated attributably** -- state made illegal by the operation is torn down *and observably + so*: a counted drop with a reason, never a silent blackhole. +3. **Never resurrected** -- state from the old config must not leak into decisions under the new one. + A port allocation released by a removed VPC must not be handed out while anything still refers to + it. + +There is a cheap universal approximation of all three, worth having before any of them: + +> **No silent change.** After any config operation, every live flow either behaves exactly as it did +> before, or fails with an attributable reason. Never "works differently", and never "fails silently". + +## Run the related configurations side by side + +Production would never do this, but a test harness can hold several pipelines at once -- `X`, `A.X`, +`B.A.X` -- and feed all of them the *same* packets. That turns most of the relations above from +before-and-after bookkeeping into a live comparison, and it is the mechanism that makes them affordable: + +- **Frames become direct.** Pipelines `X` and `A.X` must agree on every packet outside `A`'s footprint. + No probe set to maintain, no replay, and the disagreement names the packet. +- **Isolation becomes direct.** A configuration change confined to one peering component must leave the + other pipeline's verdicts for that component's traffic untouched, packet for packet. +- **State leakage becomes measurable.** Run `P1` at configuration `X` fed stream `S`; run `P2` at `X`, + then `A`, then some stream `S'`, then `undo`, then the same `S`. The two configurations are now + identical by construction, so any divergence on `S` is state carried through the excursion -- and that + is the "never resurrected" claim made concrete. + +Three prerequisites, all of which have already bitten this codebase once: + +1. **Seed the non-determinism.** `apply_masquerade_config` sets `randomize(true)` unconditionally, so + two pipelines will allocate different ports for the same flow and a naive comparison fails + immediately. Either seed it identically per pipeline or keep it out of the compared projection. +2. **Advance timers in lockstep.** Flow timers are already known to leak between fuzz inputs; across + concurrent pipelines they must be driven explicitly rather than by wall clock. +3. **Compare projections, not state.** Counters and port allocations legitimately differ between two + pipelines that agree on every verdict. Compare what an operator can observe. + +## When the pipeline becomes a DAG + +The network function pipeline is currently a line graph. The plan is to give it a non-trivial topology, +and that changes what has to be tested. + +Do not confuse this graph with the peering graph above. They index frames in the same way but they are +different objects: the **peering graph** is dynamic and config-driven, describing which tenants may +reach each other; the **NF DAG** is static topology, fixed when the dataplane is built. That the NF +topology is static is precisely what makes the analysis below tractable -- the graph is not part of the +state space, so what remains is per-NF generation and packets in flight. + +The DAG also supplies a second footprint for free: two NFs on disjoint paths cannot interfere. So the +frame abstraction wants to be parameterised over *which graph defines the footprint* rather than +assuming peering. + +### The property that matters: no packet sees a torn config + +In a line graph a config generation can be swapped in between packets. In a DAG a packet is at several +NFs over its lifetime, so if `NF1` is on generation `N` while `NF2` has already adopted `N+1`, the packet +gets hybrid treatment. That is not hypothetical harm: an ACL can permit under `N` while NAT translates +under `N+1`, and the packet leaves carrying a translation the newer ACL would have denied. + +There are two defensible designs and they need different proofs: + +- **Barrier** -- packets drain before an NF adopts a new generation. Property: no packet spans a barrier. +- **Permitted hybrids** -- property: every hybrid traversal is equivalent to *some* single generation. + +Deciding which is affordable is a design question, best answered before the DAG is built. + +### The design constraint that decides everything else + +> The DAG's generation-propagation logic must be a **pure state machine over a small, `Hash`-able state**, +> separate from packet processing and free of I/O. + +Honour that and the coordination logic can be model-checked *directly* -- the checker exercises the code +production runs, so it is a genuine regression suite and belongs in CI. Miss it, and adoption logic ends +up scattered across NF implementations with kernel calls interleaved; the only way to check it is then to +write a shadow model, which is worth something once as design validation and nothing thereafter. + +The constraint is cheap to honour in advance and expensive to retrofit, which is why it is written down +here rather than left until the tests are wanted. + +### Notes on stateright, if it is used for this + +[`stateright`][stateright] is an explicit-state model checker (0.31.0, June 2026; small maintainer pool +but active). Its `Model` trait is a good fit: `next_state` returns `Option`, so inapplicable actions are +`None` and preconditions fall out the same way they do in the algebra. + +Three points worth knowing before starting: + +1. **Use `Model` directly, not `ActorModel`.** The actor layer models a *network* -- loss, duplication, + reordering -- which NFs inside one process do not suffer, so it manufactures counterexamples that + cannot occur. It is also where the state space explodes. From stateright's own documentation, the same + protocol with an unordered network: + + | configuration | unique states | + | --- | --- | + | 2 servers + 2 clients | 544 | + | 3 servers + 2 clients | 37,168,889 | + + The network state is the dominant term, not the component count. Explicit bounded ordered queues keep + a three-NF, two-generation, two-packet model in the hundreds of states -- which runs in milliseconds, + as an ordinary test. + +2. **`Sometimes` properties are the vacuity guard as a language feature.** Assert that two NFs are ever + observed on different generations; without it the model may never produce the interesting interleaving + and will pass for nothing. Two more habits worth copying: `unique_state_count()` is assertable, so a + model quietly changing shape fails a test, and `assert_discovery` pins a counterexample trace as a + permanent regression -- the analogue of a fuzzer's crash corpus. + +3. **`Hash` is required but `Eq` is not**, so the visited set is keyed on the hash alone. Two + consequences: collisions can silently prune states, so a state count is a lower bound on confidence; + and any state containing a `HashMap` is unusable, because its iteration order is not reproducible. + That is not a problem for generation counters and adoption flags. It *is* the reason real flow tables + and port allocators can never be the checked state. + +Whatever the checker validates must also be re-stated as a tier 0 or tier 1 check in the NFs themselves. +The checker sees the coordination core; nothing stops an NF from ignoring what the core tells it. Same +claims, two enforcement points. + +The house pattern to copy is the quartet in `concurrency/tests/` -- `quiescent_model.rs` (loom/shuttle +interleavings), `quiescent_protocol.rs` (real threads), `quiescent_properties.rs` (bolero), and +`quiescent_shuttle.rs` (bolero x shuttle) -- and `#[concurrency::test]`, which routes one body to +whichever backend is active. Model checking already runs in CI here; this would not be a new practice. + +## Session-level oracles: let a real protocol be the oracle + +Every oracle above computes an expectation and compares. A transport protocol does not need one: run a +TCP session across the dataplane and the protocol itself decides whether the path worked. Sequence +numbers, checksums, retransmission and final byte-stream equality give a verdict with **no model of what +the dataplane should have done**. + +That is a different kind of oracle from the rest of this document, and it is strong enough that it may +retire the differential tier below -- which is the only place a reference implementation survives, and +the piece most exposed to a pipeline rewrite. + +Use [`smoltcp`][smoltcp] rather than writing a stack. It is `0BSD`, so it raises none of the licensing +problems that put FRR out of reach, and it takes its clock from the caller -- `poll(timestamp, ...)` -- +which is what makes runs deterministic, replayable, and advanceable in lockstep across the parallel +pipelines above. A home-grown stack would lose the property that matters most: the oracle has to be +*independent*, and protocol code written by the same team under the same assumptions is not. + +### What a session catches that a packet cannot + +- **The TCP checksum after a NAT rewrite.** It covers a pseudo-header containing the IP addresses, so + NAT must recompute it. A single-packet test never looks; a session stalls. +- **MSS clamping and MTU handling.** Invisible to one packet, fatal to a transfer. +- **Bidirectional translation consistency over a real flow**, including retransmissions and reordering. +- **"Established connections keep working."** Establish a session, apply a config operation, watch + whether bytes keep moving. That is the *preserved* disposition above, answered for free. +- Flow table eviction under sustained load. + +### A stall is not a refusal + +"Eventually completes" has to be bounded -- some number of polls of virtual time -- and the expectation +has to come from the algebra: this session *should* complete, or it *should* be refused. A refusal has +to be **attributable**: a RST, an ICMP unreachable, or a counted drop carrying a reason. + +Never a stall. Hunting stalls is most of the value, because a silent stall is exactly the failure an +operator cannot diagnose. This is [no silent change](#the-part-that-is-not-free-state-across-transitions) +restated at session granularity. + +### Two guards, and one staging decision + +- **Run a null path first.** Every session oracle should also run client-to-server directly, with no + dataplane in between. A failure there is the harness or the stack, not us. That converts "what if + `smoltcp` has a bug" from a source of false positives into a detected condition. +- **Bound the transfer.** A bulk transfer is thousands of packets. Fuzz cases want the minimum that + exercises handshake, a few segments and teardown; save large transfers for the window and MTU + properties specifically. Throughput is coverage. +- **Start in `Medium::Ip`, not Ethernet.** IP mode skips ARP and neighbour discovery, so those do not + have to work before any session test can pass. Add Ethernet mode later, at which point ARP/ND becomes + its own testable surface rather than a prerequisite. + +### How it composes with the algebra + +Each operation's postcondition becomes a claim about sessions rather than packets: + +- `peer(A, B)` -- a session from A's exposed prefixes to B's completes; one to a prefix the manifest does + not expose is refused, attributably. +- `undo(peer(A, B))` -- new sessions are refused, and *established* ones either drain or die. Which of + those is correct is a product decision; the point is that a session oracle makes the answer + observable rather than theoretical. +- **Disjoint peering components** -- no session across them ever completes. +- **Frame condition** -- establish sessions inside one component, operate inside another, and assert the + first component's sessions keep moving bytes. Tenant isolation, probed as hard as it can be probed. + +## The selection oracle is already built + +Every network function that consults a table has two separable halves, and only one of them is hard to +oracle: + +| half | question | oracle | +| --- | --- | --- | +| **selection** | which rule matched? | differential, against a trivial reference matcher | +| **action** | was the right thing then done? | invariants and metamorphic relations | + +Selection is where the frightening bugs live -- overlapping NAT rules, ACL precedence, LPM +disambiguation -- and it is also the half that already has a reference implementation in this tree. +`acl/src/reference/` provides: + +```rust +pub fn lookup(&self, key: &K) -> Option<&A> // the winner +pub fn matches(&self, key: &K) -> Vec<&RefRule> // every matching rule, in order +``` + +with a test named `matches_is_nonlossy_and_retains_shadowed_losers`. So "which rule should have won, and +which ones it shadowed" is answerable in a single pass, for any key. + +### Why this generalises past ACL + +`match_action::FieldKind` is `{Prefix, Mask, Range, Exact}` -- the P4 and DPDK classifier vocabulary -- +and rule selection in every function discussed here fits inside it: + +| function | selection expressed as | +| --- | --- | +| ACL | prefix + range + exact over the 5-tuple | +| FIB / LPM | prefix on destination | +| static NAT | exact or prefix on source and destination | +| masquerade | prefix, to choose the pool | +| port forwarding | range over ports | + +One trivial reference mechanic therefore serves as the selection oracle for all of them. It is also the +piece *least* exposed to the pipeline rework, because the vocabulary says nothing about topology -- it +does not care whether the functions form a line or a DAG. + +### Per-rule counters are the aggregate form + +Comparing per-rule hit counts across a whole traffic stream is cheaper than a per-packet comparison -- +nothing lands in the hot path -- and strictly stronger, because it catches *distribution* differences. A +rule winning three percent too often is invisible packet by packet and obvious in aggregate. + +Counters are wanted for operational reasons regardless, which makes this the best kind of test +dependency: one that pays for itself elsewhere. + +### Three boundaries to respect + +**Selection is not action.** The oracle says which rule should have matched. It says nothing about +whether NAT then allocated the right port, built consistent bidirectional state, or handled the reverse +direction. That half is stateful and already has its own properties -- the exclusivity and injectivity +claims in `nat/src/masquerade/apalloc/`. Two oracles for two halves, which is a decomposition rather +than a shortfall. + +**It speaks only to flow-establishing packets.** A flow table hit bypasses rule lookup entirely, so the +reference has nothing to say about subsequent packets of an established flow. Those get a different and +easier claim: treatment consistent with what the first packet established. + +**Build the reference from the configuration, not from the production table.** This one matters. If both +sides consume the same built table then a bug in `config -> table` is invisible, because both agree on +it -- the same-source problem that makes shadow models worthless. The reference must go from +configuration to its own naive rule list. Check which way `acl/tests/eal_classify_via_projection.rs` +does it; the name suggests a projection of the real table, which is the weaker arrangement. + +### Footprints come from predicates, not from document structure + +A rule mutation's footprint is **the rule's own match predicate**: the set of keys it matches. That is +exact, computed rather than declared, and it needs no analysis of the configuration document's shape. + +`matches()` supplies the rest. Adding a rule changes verdicts for the keys it matches *minus* those where +something else still wins, and the shadow set is precisely what `matches()` returns. So the reference +matcher is not only the selection oracle -- **it is also the footprint calculator.** + +This supersedes an earlier line of thinking worth recording so it is not re-derived. The configuration +document is a tree, so it is tempting to take an entity's subtree as its footprint and recurse: a VPC's +subtree, an ACL's rule array, an LPM's prefix subtree. Two things go wrong. + +**"Technically a tree" is not the property that matters; locality is.** An LPM trie gives a genuinely local +footprint -- the subtree under a prefix is exactly the more-specific routes. An ACL rule array is a `Vec`, +and modelling it as a linked list is true but useless: the "subtree" of rule *i* is every rule after it, so +the footprint is `O(n)` and the frame is a predicate over packets rather than a region of the document. The +recursion recovers the *shape* and loses the only property the shape was wanted for. + +**Cross-references break subtree containment, and delegating them to the validator does not help.** The +validator's concern is whether a reference resolves. The frame's concern is that a mutation inside VPC A's +subtree can change behaviour governed by the peering that references A -- so the footprint is the subtree +*plus everything referencing into it*. That is the **inbound** closure, which is the one direction a +document structure does not give you. It is also the same fact as "a deletion's footprint is everything +that referred to the deleted thing": cross-references are the deletion problem seen from the configuration +side. + +What survives, then: + +- **At the table level**, footprints come from predicates. No tree, no index. +- **At the configuration level**, a reverse-reference index is still required, for exactly the deletion and + modification cases. The validator needs the same index, so it is shared machinery rather than a second + mechanism. +- **Set versus sequence semantics still predicts cost**, and is now a property of a table's disambiguation + rather than of the document: + + | disambiguation | insertion order | footprint | mutations commute | + | --- | --- | --- | --- | + | most specific wins (LPM) | irrelevant | the predicate | freely | + | first match wins (`Vec`) | *is* the meaning | predicate minus shadowing, positional | rarely | + + Both are computable from `matches()`. The second is simply more expensive to reason about, which is worth + knowing when choosing a representation: priority-tagged rules with validator-enforced disjointness would + move a table into the cheap column. Whether that is worth the change to operator-visible semantics is a + product question, not a testing one. + +### Actions need no reference implementation + +Stopping the reference at selection sounds like it leaves the action half unchecked. It does not, and the +reason is structural rather than a rule of thumb: + +- **Selection has no local invariant.** "Which of these overlapping rules should have won" can only be + answered by comparing against something, so it needs a differential. +- **Actions do have local invariants.** "What did you do to this packet" is a relation between before and + after, checkable in place. + +Sorted by what they require, and note that nothing here needs a second implementation: + +| requires | examples | +| --- | --- | +| the output alone | the packet still parses; source is not a multicast address; the checksum is self-consistent | +| input and output | TTL exactly one less, or dropped; payload unchanged; only fields NAT may rewrite differ | +| output + matched rule | dest MAC is the nexthop's resolved MAC per that rule; translated addr in that rule's pool | +| two executions | forward then reverse is the identity on the 5-tuple | +| enumerable state | distinct live flows never collide; the mapping just created is in the overlay | + +#### The selected rule is the specification for the action + +The third row is what makes a whole-pipeline fuzz possible. Never compute what the output should be. +Verify two things and chain them: + +1. the right rule was selected -- differential, against the reference matcher; +2. the output is consistent with the rule that was selected -- invariant, no reference. + +Composed, those give end-to-end correctness with no parallel dataplane anywhere. This is why stopping the +reference at selection costs nothing. + +It does impose a design requirement, and a cheap-now-expensive-later one: **a rule must name its action +completely enough to serve as a specification.** If a rule says "masquerade" while the pool it draws from +lives somewhere else, the rule is not a spec and the action cannot be checked against it. + +#### Duplicate no semantics; expose whatever state you need + +"Non-intrusive" was the wrong way to state the constraint. The distinction that matters is: + +- An **observability seam** -- counters, an overlay, an event log -- exposes state. It encodes no semantics, + so it cannot drift. The worst it can become is stale API. +- A **reference implementation** duplicates semantics. It drifts by construction, because two encodings of + one rule diverge under maintenance. + +Rot comes from duplicated semantics, not from exposed state. Per-rule counters are already an intrusion of +the first kind and are entirely fine. + +An overlay over NAT's mappings is the same class of intrusion, and it buys **enumerability**: without one +you can see that a packet was translated but cannot enumerate every mapping a batch created. That is what +turns per-packet checks into set-level ones, and set level is where injectivity, exact accounting and leak +detection live. A batch of zero packets is a useful degenerate case -- it asserts that nothing is allocated +when nothing flows. + +Two requirements fall out of it: + +- **Record events, not a final set.** A create/destroy/create sequence within one batch collapses to a + single create if only the endpoints are diffed, and that is exactly where the interesting bug hides. +- **Timers need the caller-supplied clock**, the same one the session oracles need. Build the virtual clock + once and properly rather than twice badly; flow timers leaking between fuzz inputs has already been a + real defect here. + +#### Re-point the existing property tests rather than writing new ones + +`net/` already contains a large body of property tests asserting that the header machinery is +self-consistent. The **same predicates**, applied to `(packet_in, packet_out)` pairs, assert that an action +used that machinery correctly. Same predicates, different subject -- re-pointing rather than copying, so it +adds no maintenance surface. + +`Checksum::validate_checksum` is public and usable as an action invariant today. `parse_back_test` in +`net/src/headers/mod.rs` is the round-trip oracle and needs only to be `pub(crate)` to be reused. + +### Why this is not "a parallel dataplane" + +Casting selection as a reference implementation invites the objection that we are building a second +dataplane to check the first. The objection is worth answering precisely, because the answer is also the +maintenance argument. + +What differs between the two paths is the **table build** and the **lookup algorithm** -- optimised trie or +hash against a naive linear scan. What is *held fixed* is the meaning of a rule and the meaning of an +action. So this is a differential test of construction and lookup, not a reimplementation of semantics. + +The consequence that matters: **the reference scales with the match vocabulary, not with the feature set.** +There are four `FieldKind`s. Add ten network functions and the reference does not change; it changes only +if a genuinely new kind of match is introduced. A parallel dataplane would scale with features and would +therefore rot. + +Three things to hold onto: + +- **The reference must consume configuration and emit verdicts, and touch nothing internal.** Its + independence from internal structures is what stops it breaking when they change. Refusing intrusive + dependency is not a nicety here; it is the whole reason the thing stays maintainable. +- **Stop at selection.** It will be tempting to have the reference also compute the translated packet, the + checksum fixup, the encapsulation. That is the line where it *does* become a parallel dataplane and does + start to drift. The action half is oracled by invariants, metamorphic relations and session-level checks + -- never by a reference. +- **`FieldPredicate` is genuinely shared**, so a bug in what "prefix /24 matches" means is invisible to the + differential. It is small enough to property-test directly against a naive bit-by-bit implementation, and + that is worth doing precisely because it is the one place the same-source objection lands. + +One qualifier on the longer-term ambition of casting the whole dataplane in match-action terms: match-action +describes the *stateless classification* in each function. The stateful part -- flow tables, NAT sessions, +connection tracking -- is match-action *plus* mutable state, which is why a concurrent bimap is needed for +NAT rather than a table alone. + +That is the same boundary as the selection/action split, restated one level up. When the test structure and +the architecture divide along the same line, the tests survive changes to either side; when they do not, +every refactor invalidates a test suite. This one divides along the same line, which is the strongest reason +to think the approach will hold. + +A note on the interim NAT representation: an `Arc>` forward/reverse pair is fine for an oracle, +but it means the oracle cannot live in a per-packet path even in debug builds. So selection oracles run +test-side, and the in-place tier 0 assertions stay confined to structural invariants that need no lock. + +## Contracts belong to network functions, not to the DAG + +The natural first instinct is to put the oracles at the boundary of the whole pipeline: feed traffic in one +end, judge what comes out the other, and let one set of mutations cover ACL, router, NAT and everything +else together. **That does not work, and the reason is masking.** + +An ACL rule that drops traffic before the router ever sees it hides the router entirely. At the pipeline +boundary there is no way to distinguish "the ACL correctly dropped this" from "the router would have +misrouted it and we never found out". Worse, the oracle has to predict the *composition* -- what the ACL +did, and then what the router would have done to whatever survived -- so the expectation becomes a +cross-product over domains and grows unmanageable exactly as the vocabulary grows. + +### Masking is a vacuity problem wearing a disguise + +Notice what masking actually costs: coverage of the router's logic silently falls to zero for that class of +traffic, and a green run says nothing about it. Tighten an upstream ACL and downstream oracles quietly stop +being exercised. + +Per-function contracts make that measurable rather than invisible. Count arrivals at each function's input. +If a mutation upstream causes that count to collapse, the [vacuity](#vacuity) guard fires and names the +function that stopped being tested. At the pipeline boundary the same change looks like a pass. + +### The decomposition + +Each network function gets its own contract: + +- a **precondition** -- what it may assume about a packet arriving, and +- a **postcondition** -- what it guarantees about a packet departing. + +Pipeline behaviour is then the *composition* of those contracts, and no pipeline-level oracle is needed. +When a function drops a packet, the next function's contract is vacuously satisfied for it -- no input, no +obligation -- which is both the correct semantics and free. + +ACL, router, NAT and the rest are **distinct domains**. This is consistent with deriving commutation from +read and write sets: mutations in different domains usually touch disjoint state and therefore commute by +that test, without needing to be told they are unrelated. Where they genuinely conflict is where their +domains share a referenced entity -- an ACL rule reading a VPC that another mutation removes -- and that is +exactly the deletion footprint that makes removal the interesting case. + +### Two levels of contract, kept apart + +The word "precondition" is now doing two jobs, and confusing them will cause trouble: + +| | subject | precondition | postcondition | frame | +| --- | --- | --- | --- | --- | +| **mutation** | configuration state | definedness (its read set) | the claims it adds | its write set | +| **network function** | packet and flow state | what may arrive | what departs | untouched fields | + +The link between them: a mutation's claims are ultimately claims *about network function contracts*. +`peer(A, B)` does not directly assert anything about a packet -- it changes what the ACL function's +postcondition is for traffic between A and B. + +### Why this is where `debug_assert!` belongs + +A function's pre- and postconditions live at its entry and exit, which is literally where an assertion goes. +So tier 0 and this decomposition are the same idea, and that has two consequences worth having: + +- **The oracle moves with the code.** Rework the DAG and a function's contract travels with the function, + because it is written at its boundary rather than in a test that knows the old topology. +- **Failures localise.** A stalled session says only "something in the pipeline is wrong". The first + violated postcondition names the function. That repairs the one real weakness of in-place assertions -- + that they fire where a problem is observed rather than where it was caused. + +### What it costs + +Writing these contracts down forces every implicit assumption a function makes about its predecessors to +become explicit, and some of those assumptions will turn out to be disputed. That is the point rather than a +side effect -- undocumented coupling between stages is the defect, not the documentation of it -- but it is +real work and it will surface disagreements. + +One consequence specific to the DAG: a function may have several predecessors, so its precondition has to +hold for packets arriving from *any* of them. That is strictly stronger than the line-graph case, and it is +a question the DAG design has to answer rather than one the tests can. + +## Deriving the oracles from the algebra + +Everything above describes oracles that *could* be written. This section is about not writing them by +hand. + +Treat configuration operations and traffic as members of one monoid acting on pipeline state. Write +`Tcp(p)` for pushing a session `p` through the pipeline and `A` for a configuration mutation, composed +right to left, so `Tcp(p) . B . A . P` means "apply `A`, then `B`, then run session `p`". This matters +because **traffic mutates state too** -- flow tables, NAT allocations -- so treating it as a read-only +probe misses a class of failure. + +### This is a naming scheme, not a logic + +The algebraic notation is suggestive and it leaks. Do not try to reason in it: + +- **There is no `Tcp(p)^-1`.** Not merely unimplemented -- semantically meaningless, and it fails + uniqueness of inverses. The nearest thing to `Tcp(p)^-1 . Tcp(p) . P` is `time(+t) . Tcp(p) . P` for a + `t` long enough to decay whatever transient `Tcp(p)` left behind. +- **It is a groupoid, not a group.** The undo of an operation depends on the state it was applied to, so + `[B, A] = B A B^-1 A^-1` is not literally formable. +- **The operators are relations, not functions.** `apply_masquerade_config` sets `randomize(true)` + unconditionally, so a session's port allocation is not determined by the input. Either seed it or keep + it out of the compared projection. +- **`~=` is transitive only with a growing bound.** If `P ~= Q` within `K` steps and `Q ~= R` within `K`, + then `P ~= R` within `2K`. Short expressions only. + +Following those leaks toward rigour ends in rebuilding a temporal logic, which is not a project this team +can afford and not one it needs: **we want to find defects, not prove their absence.** Testing needs none +of the properties the notation appears to promise. It needs a way to enumerate expressions, a way to run +two of them, and a projection to compare. + +Where genuine temporal reasoning *is* wanted -- liveness over unbounded interleavings -- that is what the +model checker is for, over the small coordination state space described above. The division of labour: + +| | state space | how "eventually" is discharged | +| --- | --- | --- | +| model checker | small, exhaustive | a liveness property over all interleavings | +| algebra-derived oracles | large, sampled | advance virtual time to quiescence, then compare | + +### The mechanism + +Each operation in the vocabulary carries three pieces of metadata, all cheap and all derivable from its +arguments: + +- **`footprint(A)`** -- which peering components, VPCs or NFs it can affect. +- **`undo(A, X)`** -- its state-dependent reverse. +- **`commutes_with(A)`** -- a declaration, which the tests then check. + +From those alone, five families of test are generated. No test in any family is hand-written, so adding +an operation to the vocabulary adds tests to all five: + +| family | shape | catches | +| --- | --- | --- | +| postcondition | `Tcp(p) . A . P` for `p` inside `footprint(A)` | the operation did what it claims | +| frame | `[Tcp(p), A] = 0` for `p` outside `footprint(A)` | config disturbing unrelated traffic | +| traffic isolation | `[Tcp(p), Tcp(q)] = 0` for `p`, `q` in disjoint components | interference via shared resources | +| transience | `O(undo(A) . Tcp(p) . A . P) ~= O(P)` | state orphaned when config is removed | +| commutation | declared `[B, A] = 0` implies observable equivalence | order dependence the config data hides | + +Two notes on reading that table. + +**The frame condition is a vanishing commutator.** That is the general form; the probe-set formulation +earlier in this document is the special case where the two orders are run as a before-and-after rather +than side by side. A *non*-vanishing commutator is more than a failure signal -- its magnitude is how much +the configuration change disturbed the traffic, which is "established connections keep working" with a +number attached. + +**Transience is stated over the behaviour function, not the state.** `O(P)` maps a session to a verdict. +The claim is that no effect of traffic is observable in the verdict of a later independent session -- *not* +that traffic leaves no trace. Some traces are legitimate and must survive: a neighbour cache entry created +by traffic should persist. Stating it over verdicts permits that and still catches the case that matters, +which is an allocation orphaned by a peering that no longer exists. + +### Implementation shape + +Enough of the structure is settled to sketch it. Start from the blank configuration -- which already exists +as `ExternalConfig::BLANK_GENID` -- as the identity the sequences fold over. Worth noting that the blank +config is also where the rollback defect lives, so the identity element of the algebra is a known-bad state +and the first test written lands on the worst path. + +```rust +trait Mutation { + /// Apply, returning the state-dependent reverse. + fn apply(&self, p: &mut Pipeline) -> Undo; + + /// Ordering and definedness: a precondition is a read of what someone else wrote. + fn reads(&self) -> Footprint; + + /// The frame: everything outside this is unchanged. + fn writes(&self) -> Footprint; + + /// Which probes this mutation must make a difference to. Derived, not written, in the common case. + fn interested_in(&self, probe: &Probe) -> bool { + self.writes().intersects(probe.touches()) + } +} +``` + +Three things this sketch deliberately does *not* have. + +**No per-mutation expectation object.** An expectation that closes over the two states it was born between +goes stale as soon as the sequence continues past it. Make it a pure function of `(probe, &Pipeline)` and it +stays valid everywhere -- but then it is not per-mutation at all, it is a claim about correct behaviour given +a configuration. So there is a *small* reusable set of expectation predicates, one per kind of observable, +and one `interested_in` per mutation. That is far cheaper than one oracle per mutation and it puts all the +domain knowledge in a handful of named predicates. + +**No inverse oracle.** A differential oracle between `P` and `P'` is direction-agnostic: same interest set, +same expectation. The reverse mutation reuses it. + +**No global oracle array.** Configurations snapshot cheaply because they are data; live pipelines with their +flow tables and port allocations do not. So the oracles are a *stream checked with a window of two* -- three +for transience: before, after the mutation plus traffic, after the undo. Each mutation is checked against its +immediate neighbours rather than against the final state. The abstraction reads as though it is global; the +implementation cannot be, and pretending otherwise will run the harness out of memory. + +**The interest partition is what does the work.** For a given probe, split the mutations into those that +claim interest and those that do not. The uninterested ones must leave the probe's verdict unchanged -- that +is the frame. The interested ones must change it -- and a mutation that claims interest but changes nothing +is a mutation that was accepted and silently not enacted, which is the defect class the IPv6 peering +reproducer belongs to. + +## Where the checks live + +Four tiers, cheapest and most local first: + +| tier | kind | survives refactoring | +| --- | --- | --- | +| 0 | local invariants, `debug_assert!` in place | while the structures do | +| 1 | metamorphic relations, test-side | best -- stated in domain terms | +| 2 | differential against a reference matcher, for *rule selection* | well -- the vocabulary is topology-independent | +| 3 | end to end: session oracles plus conservation laws (in = out + drops, attributable) | best; cheapest | + +Factor each check as a **named function** callable from both tests and `debug_assert!`. That, rather +than the assertion itself, is what survives a rewrite. + +### Rules for the in-place checks + +- **Only the assertion bodies may compile out.** If a `#[cfg]` reaches the code under test, the fuzzed + binary is not the shipped binary and the results do not transfer. +- **Tier the cost.** For a coverage-guided fuzzer, throughput *is* coverage: a debug build ten times + slower explores a tenth as much. Cheap invariants can be always-on in debug; anything `O(n)` in a + per-packet path belongs behind its own feature. +- **`debug_assert!` is a net, not a specification.** It catches falls; it does not state what correct + means. Five hundred of them still do not answer "does this ACL do what the config asked". That + question needs tier 2. + +## Vacuity + +An algebra can quietly stop producing interesting sequences -- every operation refused by its +preconditions, say -- and a suite of claims that are never exercised passes beautifully. + +Count what was actually reached and assert on it, as `agreement_is_not_vacuous` in +`net/src/headers/view.rs` does. In this campaign that guard has repeatedly been the only thing +standing between a green run and a meaningless one. + +## Shrinking + +When an operation sequence fails, the useful artefact is the minimal failing subsequence, and a +state-dependent generator makes that harder than usual. + +Because the drawable operations at each step are a function of the configuration built so far, removing an +earlier operation changes what every later draw *means*. Byte-level shrinking therefore yields a +*different* sequence rather than a smaller one, and the failure usually evaporates for reasons unrelated to +the bug. + +Two things help: + +- **Shrink at the sequence level.** Try removing each operation, re-run, and keep the removal if the failure + survives. This is a handful of lines and it is the only shrinker that respects the dependency structure. +- **Select arguments by index modulo what exists** -- "the third VPC present" rather than "VPC with id 7" -- + so that deleting an earlier operation degrades the rest of the sequence instead of scrambling it. + +## What this does not give you + +- It does not prove the validator is right, only that the dataplane agrees with it. +- It reaches only the configurations the modelled operations compose to. +- Environmental failures -- netlink refusing an operation, FRR being down -- are not config-derived and + cannot be tested this way. They need retry-to-convergence and reporting, not a config oracle. +- It says nothing about whether the dataplane is *fast*, and several of the checks here are affordable + only because they are compiled out of release builds. + +## Open questions + +- The peering graph supplies the frame's footprint for VPC operations. What supplies it for the + operations that are not VPC-scoped -- device and tracing configuration, flow table capacity? +- Whether a per-packet assertion of any kind is affordable in a debug datapath is unmeasured. If it is + not, tier 0 has to move out of the packet path and into the structures it mutates. +- Does `acl/tests/eal_classify_via_projection.rs` build its reference from the configuration or by + projecting the production table? If the latter, the `config -> table` build is untested by it, and that + is the arrangement to fix before leaning on the selection oracle anywhere else. +- `acl/src/dpdk/dyn_table.rs` is the largest in-scope gap in `acl` at 82.4%, 104 uncovered lines. The + production side of the selection machinery is well tested but not fully. +- Where the session endpoints attach relative to VXLAN encapsulation. This has to be settled before the + harness is written, and it is not obvious. +- Barrier versus permitted hybrids for config adoption across the DAG. This is the question the model + checker exists to answer. + +[smoltcp]: https://docs.rs/smoltcp +[stateright]: https://www.stateright.rs/title-page.html +[`TypeGenerator`]: https://docs.rs/bolero/latest/bolero/generator/trait.TypeGenerator.html +[`ValueGenerator`]: https://docs.rs/bolero/latest/bolero/generator/trait.ValueGenerator.html diff --git a/development/code/property-testing.md b/development/code/property-testing.md index a9ab2b32ec..4e06999a7b 100644 --- a/development/code/property-testing.md +++ b/development/code/property-testing.md @@ -20,5 +20,13 @@ A type may implement [`ValueGenerator`] to provide a more restricted set of valu This is useful if you wish to focus fuzzing efforts more narrowly than a correct implementation of [`TypeGenerator`] allows. +## Generating large structured inputs + +Reaching for a narrower [`ValueGenerator`] each time the fuzzer cannot get somewhere stops scaling once +the input is as large as a whole configuration: the generators do not compose, and each one encodes a +little more knowledge of the implementation. For those cases, build the input from an algebra of valid +operations instead, and derive the oracles from the same algebra -- see +[testing a config-driven dataplane with an operation algebra](./config-algebra-testing.md). + [`TypeGenerator`]: https://docs.rs/bolero/latest/bolero/generator/trait.TypeGenerator.html [`ValueGenerator`]: https://docs.rs/bolero/latest/bolero/generator/trait.ValueGenerator.html From 63a873b0cd40d98c449cbb81796e995008c68e7b Mon Sep 17 00:00:00 2001 From: Daniel Noland Date: Mon, 17 Aug 2026 16:42:23 -0600 Subject: [PATCH 2/7] feat(config): Generate a set of static NAT exposes for one manifest `StaticNatExpose` draws one expose, and one expose builds a table with one rule in it. A property about a *lookup* wants several, because one rule gives a longest-prefix match nothing to choose between. Repeating the single-expose generator does not work. Two independent draws are refused by a manifest almost every time, for two separate reasons: * **Overlap.** Every expose is laid out from the same two bases -- 10.0.0.0 for the private side and 172.16.0.0 for the public one -- so two of them cover the same addresses and validation refuses the pair. * **Address family.** A peering's manifests must agree on one family, so a v4 expose beside a v6 one is refused as well. Both belong in the generator rather than in each caller, since both are facts about what a manifest accepts. `StaticNatExposes` draws the family once and places each expose in a block of its own, `BLOCK_STRIDE` apart -- wider than the widest span one expose can occupy, so distinct blocks cannot collide whatever the draw. ## It was two thirds of the budget Measured on the static NAT network function properties that motivated this, which draw between one and three exposes: * repeating `StaticNatExpose`: 33% of configurations validated, * one block per expose: 59%, * one block and one family: 100%. So two thirds of the fuzzing budget was being spent building configurations that were thrown away, and -- worse than the waste -- multi-expose configurations were nearly unreachable. The interesting case was the one being skipped, which is the same generator gap this campaign has now found several times: code that is unreachable rather than wrong. `StaticNatExpose` is unchanged and still draws a single expose, so the existing callers in `nat` and `mgmt` are untouched. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: Daniel Noland (cherry picked from commit 7f98556dfbb22d811d822f615a3e1d4f4b64ccc7) --- config/src/external/overlay/vpcpeering.rs | 100 ++++++++++++++++------ 1 file changed, 75 insertions(+), 25 deletions(-) diff --git a/config/src/external/overlay/vpcpeering.rs b/config/src/external/overlay/vpcpeering.rs index 09336ae3a6..5c12ba76e9 100644 --- a/config/src/external/overlay/vpcpeering.rs +++ b/config/src/external/overlay/vpcpeering.rs @@ -1213,30 +1213,78 @@ pub mod contract { #[derive(Debug, Clone, Copy, Default)] pub struct StaticNatExpose; + /// Several static NAT exposes for one manifest, which a manifest will accept together. + /// + /// [`StaticNatExpose`] draws one expose, and one expose builds a table with one rule in it. + /// Several are what give a longest-prefix match anything to choose between, so anything testing + /// a lookup wants this rather than a repeated draw of the single-expose generator. + /// + /// Two independent draws are refused by a manifest almost every time, for two reasons that both + /// have to be handled here rather than by the caller: + /// + /// * **Overlap.** Every expose is laid out from the same two bases, so two of them cover the + /// same addresses. Each is placed in a block of its own instead, [`BLOCK_STRIDE`] apart, which + /// is wider than the widest span one expose can occupy. + /// * **Address family.** A peering's manifests must agree on one family, so a v4 expose beside a + /// v6 one is refused. The family is drawn once here and shared. + /// + /// The field is the largest number of exposes to draw; the generator draws between one and that. + #[derive(Debug, Clone, Copy)] + pub struct StaticNatExposes(pub u8); + + impl Default for StaticNatExposes { + fn default() -> Self { + Self(3) + } + } + /// The largest total either side covers, as a power of two. Small enough to enumerate. const MAX_TOTAL_LOG: u8 = 6; + /// The distance between two blocks. + /// + /// A side lays out at most `2^MAX_TOTAL_LOG` addresses, each part followed by a gap of its own + /// size, so it spans at most twice that. Double it again for room to grow. + const BLOCK_STRIDE: u128 = 4 << MAX_TOTAL_LOG; + impl ValueGenerator for StaticNatExpose { type Output = VpcExpose; fn generate(&self, driver: &mut D) -> Option { let v4 = driver.produce::()?; - let total_log = driver.gen_u8(Included(&0), Included(&MAX_TOTAL_LOG))?; + static_nat_expose(driver, v4, 0) + } + } - let privates = place(v4, Side::Private, &split(driver, total_log)?)?; - let publics = place(v4, Side::Public, &split(driver, total_log)?)?; + impl ValueGenerator for StaticNatExposes { + type Output = Vec; - let mut expose = VpcExpose::empty().make_static_nat().ok()?; - for prefix in privates { - expose = expose.ip(PrefixWithOptionalPorts::new(prefix, None)); - } - for prefix in publics { - expose = expose - .as_range(PrefixWithOptionalPorts::new(prefix, None)) - .ok()?; - } - Some(expose) + fn generate(&self, driver: &mut D) -> Option> { + let v4 = driver.produce::()?; + let count = driver.gen_u8(Included(&1), Included(&self.0.max(1)))?; + (0..count) + .map(|block| static_nat_expose(driver, v4, block)) + .collect() + } + } + + /// One static NAT expose of the given family, laid out in the given block. + fn static_nat_expose(driver: &mut D, v4: bool, block: u8) -> Option { + let total_log = driver.gen_u8(Included(&0), Included(&MAX_TOTAL_LOG))?; + + let privates = place(v4, Side::Private, block, &split(driver, total_log)?)?; + let publics = place(v4, Side::Public, block, &split(driver, total_log)?)?; + + let mut expose = VpcExpose::empty().make_static_nat().ok()?; + for prefix in privates { + expose = expose.ip(PrefixWithOptionalPorts::new(prefix, None)); + } + for prefix in publics { + expose = expose + .as_range(PrefixWithOptionalPorts::new(prefix, None)) + .ok()?; } + Some(expose) } // Split 2^total_log into powers of two, largest first. Halving a part keeps the total the @@ -1271,19 +1319,21 @@ pub mod contract { // Each part is followed by a gap of its own size. Placed end to end they would be aligned // siblings, and validation normalizes those back into one prefix -- so the shape the generator // worked out to differ between the sides would be collapsed away before anything saw it. - fn place(v4: bool, side: Side, parts: &[u8]) -> Option> { - let mut cursor = if v4 { - u128::from(match side { - Side::Private => 0x0A00_0000u32, - Side::Public => 0xAC10_0000, - }) - } else { - let selector = match side { - Side::Private => 0u128, - Side::Public => 1, + fn place(v4: bool, side: Side, block: u8, parts: &[u8]) -> Option> { + let offset = u128::from(block) * BLOCK_STRIDE; + let mut cursor = offset + + if v4 { + u128::from(match side { + Side::Private => 0x0A00_0000u32, + Side::Public => 0xAC10_0000, + }) + } else { + let selector = match side { + Side::Private => 0u128, + Side::Public => 1, + }; + (0x2001_0db8u128 << 96) | (selector << 80) }; - (0x2001_0db8u128 << 96) | (selector << 80) - }; let mut out = Vec::with_capacity(parts.len()); for &log in parts { From 38e57e76a41c9d1ac72ae34244aca3105e27a4ff Mon Sep 17 00:00:00 2001 From: Daniel Noland Date: Mon, 17 Aug 2026 16:42:47 -0600 Subject: [PATCH 3/7] test(nat): Drive static NAT with configuration-relative packets The fuzzing so far has been small, focused and intrusive: it reaches into a structure, exercises it directly, and asserts something about that structure. This is the first of the other kind -- configure a network function, put generated packets through it, and assert properties that would hold of any static NAT rather than of this one. ## Packets have to be drawn relative to the configuration `Packet` has a `TypeGenerator`, and pointing it at a generated NAT configuration is useless: every packet misses every table, the fuzzer explores the miss path, and the run is vacuous while looking enormous. This is the same failure the design note rejects for configuration values, one level down, so it takes the same answer. The configuration is a **parameter to resolution**, not a predicate to filter against. A `ProbeSpec` is drawn with no reference to any configuration -- it is a handful of indices -- and `resolve` interprets it against the built `Fabric`. Resolution is total, so no draw is discarded and no rejection loop skews the distribution. `acl-filter`'s `ProbeSpec` resolves against a built overlay the same way; this generalises the shape to a stage that takes real packets. ## The arrival state is the stage's precondition `StaticNat` sits mid-pipeline and assumes its predecessors annotated the packet: two vpc discriminants, the overlay flag, and the flags saying which directions of translation are wanted. Nothing says so in the type system -- `process` passes silently over a packet that lacks them. `Arrival` writes that down once, which is what the design note asks for when it puts contracts on network functions rather than on the pipeline: the assumption travels with the stage. `masquerade`'s tests hand-roll the same thing as a mock stage, and that is the drift this avoids. ## What is actually new `setup::config_driven` already proves the *mapping* right by enumeration. Nothing there touches a packet, its metadata, or `StaticNat`. These cover the half where the decisions live, and none of them needs an oracle -- each is a metamorphic relation or an invariant, so nothing here is a second copy of `RangeBuilder`: * **round trip** -- a translated source comes back. The outbound packet is rewritten by the local vpc's table, built from the local side of the peering; the reply is rewritten by the peer's table, built from the remote side, by a different code path. Whatever the first did, the second must undo. This is the one property that ties the two halves together. * **injectivity** -- distinct sources stay distinct, through the stage rather than through the table. A collision is a tenant isolation defect. * **frame** -- translating the source touches nothing else. The generated exposes carry no port ranges, so a rewritten port would be a mapping reaching further than it was configured to. * **permission** -- nothing is translated that did not ask. Covers every reason: not requested, already done, annotations missing or naming something absent, source not exposed. * **attribution** -- a packet that cannot be looked up is dropped with a `DoneReason`, not passed silently. A silent pass forwards untranslated traffic under a configuration that never mentioned it. * **marking** -- a packet whose address changed carries `src_natted` and `checksum_refresh`. Without the second it goes out with a checksum for an address it no longer has, and is discarded by the receiver rather than by anything that could report it. ## Every one of them was verified by breaking the code A property that cannot fail is not evidence. Each break fired exactly the property it should and left the others green: | break | fires | | --- | --- | | mapping shifted by one | round trip | | every address mapped to its range start | round trip, injectivity | | `set_checksum_refresh` dropped | marking | | `src_natted` mark dropped | marking | | silent pass on a missing source vni | attribution | | both permission gates ignored | permission | | a port rewritten the mapping never named | frame | ## Vacuity Every property counts what it reached and asserts a floor, because the failure that matters is an assertion that stops running rather than one that is wrong. All six now build 100% of the configurations they draw, and reach between 2,100 and 21,700 probes per second-long run. `Packet::enforce` removes a dropped packet from the output, so probes carry `keep`: without it a drop and a pass-through are the same event from outside, and attribution could not be stated at all. ## Why the vacuity floor is a ratio Each property counts the draws that reached its assertion and fails the run if too few did. That floor is relative -- at least one reaching draw per two configurations built, plus a small absolute minimum -- rather than an absolute count, because an absolute count measures how fast the machine was rather than whether the property ran. A property that reaches a couple of thousand draws on its own reaches a few dozen under coverage instrumentation beside nine hundred other tests, and a floor tuned to the fast case then fails for a reason that has nothing to do with the code under test. Both counts scale with the iteration budget, so their ratio does not, and a property that has genuinely stopped reaching its assertion still collapses the ratio to zero -- which is the only thing the guard was ever for. This shape was arrived at the hard way: the first `just coverage` run over `nat`, `net`, `flow-entry`, `acl-filter`, `config` and `mgmt` failed on a count-based floor rather than on a defect. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: Daniel Noland (cherry picked from commit 7d670e3e2a0a8eeffcd207384e9659443c711a37) --- nat/src/static_nat/fuzz.rs | 498 ++++++++++++++++++++++++++++++++++++ nat/src/static_nat/mod.rs | 2 + nat/src/static_nat/probe.rs | 467 +++++++++++++++++++++++++++++++++ 3 files changed, 967 insertions(+) create mode 100644 nat/src/static_nat/fuzz.rs create mode 100644 nat/src/static_nat/probe.rs diff --git a/nat/src/static_nat/fuzz.rs b/nat/src/static_nat/fuzz.rs new file mode 100644 index 0000000000..dcd0972c9c --- /dev/null +++ b/nat/src/static_nat/fuzz.rs @@ -0,0 +1,498 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! Properties of the static NAT network function, driven by generated configurations and packets. +//! +//! `setup::config_driven` already proves the *mapping* correct by enumeration: it builds the tables +//! a generated expose implies and checks that the two sides pair up one to one. Nothing there +//! touches a packet, a `Packet`'s metadata, or [`StaticNat`] itself. +//! +//! This module covers the rest of the stage, which is the half where the decisions live: +//! +//! * whether the mapping is applied to the packet's headers at all, and to which ones; +//! * whether it is applied when the arrival state does not ask for it, or forbids it; +//! * whether a packet it cannot look up is dropped with a reason or silently; and +//! * whether the two independently built halves of one expose still agree once each has been +//! applied to a real packet by real code. +//! +//! # No oracle +//! +//! None of these predicts what a source address should translate to. Each is either a metamorphic +//! relation -- a statement about how two runs relate -- or an invariant over one run's output. +//! Following the development guide's decomposition, the `config -> tables` half gets a differential +//! oracle by enumeration and the per-packet half gets relations, and the two compose without +//! anything needing to know the answer in advance. A property here that had to predict an address +//! would be a second copy of `RangeBuilder`, and two copies disagree. +//! +//! # Vacuity +//! +//! The failure mode that matters is not a wrong assertion but an assertion that never runs. A probe +//! that misses every table satisfies most of what follows trivially, and a generated overlay that +//! fails to validate satisfies all of it. Each property counts what it actually exercised and +//! asserts a floor on that count, so a change that quietly stops reaching the code leaves a failing +//! test rather than a green one. + +#![cfg(test)] + +use crate::static_nat::nf::StaticNat; +use crate::static_nat::probe::{Fabric, ProbeSpec, Stray}; +use bolero::{Driver, TypeGenerator, ValueGenerator}; +use concurrency::sync::atomic::{AtomicUsize, Ordering}; +use config::external::overlay::vpcpeering::VpcExpose; +use config::external::overlay::vpcpeering::contract::StaticNatExposes; +use net::buffer::TestBuffer; +use net::ip::NextHeader; +use net::packet::{DoneReason, Packet}; +use pipeline::NetworkFunction; +use std::collections::BTreeMap; +use std::net::IpAddr; + +/// Exposes per configuration. More than one is what makes the tables hold several rules, which is +/// where a longest-prefix match has a choice to get wrong. +const MAX_EXPOSES: u8 = 3; + +/// The fewest reaching draws any property may see before it is considered vacuous. +const MIN_REACHED: usize = 8; + +/// Probes per configuration. Building the configuration costs far more than resolving a probe +/// against it, so a batch amortizes the expensive half over the interesting one. +const PROBES: usize = 8; + +/// A configuration and a batch of packets to put through it. +/// +/// The two halves are drawn from the same driver but independently of each other: a [`ProbeSpec`] +/// is indices and raw values, and means something only once [`ProbeSpec::resolve`] interprets it +/// against the fabric the exposes built. +#[derive(Debug, Clone, Copy)] +struct Scenario { + /// Whether probes may deviate from a packet the configuration translates. + /// + /// Off for the properties that are about the mapping surviving the round trip, since a probe + /// that is meant to miss has nothing to round trip; on for the ones about the stage's own + /// decisions, which is all a stray exercises. + strays: bool, +} + +impl ValueGenerator for Scenario { + type Output = (Vec, Vec); + + fn generate(&self, driver: &mut D) -> Option { + let exposes = StaticNatExposes(MAX_EXPOSES).generate(driver)?; + + let mut probes = Vec::with_capacity(PROBES); + for _ in 0..PROBES { + let mut probe = ProbeSpec::generate(driver)?; + if !self.strays { + probe.clear_stray(); + } + probes.push(probe); + } + Some((exposes, probes)) + } +} + +/// Put a batch through the stage and collect what comes out. +/// +/// Nothing is filtered: every probe carries `keep`, so a packet the stage drops still appears in +/// the output with its reason attached. Without that a drop is indistinguishable from a +/// pass-through, and half of what follows could not be stated. +fn run(nf: &mut StaticNat, packets: Vec>) -> Vec> { + nf.process(packets.into_iter()).collect() +} + +/// Build the fabric a scenario describes, or report that the overlay was refused. +/// +/// A refusal is legitimate: each expose is valid on its own by construction, but two of them may +/// overlap, and a manifest rejects that. Callers count refusals rather than ignoring them. +fn fabric(exposes: &[VpcExpose]) -> Option { + let fabric = Fabric::build(exposes)?; + fabric.is_probeable().then_some(fabric) +} + +/// How much of a run actually reached the code under test. +#[derive(Default)] +struct Tally { + /// Scenarios drawn. + seen: AtomicUsize, + /// Scenarios whose overlay validated and built a non-empty table. + built: AtomicUsize, + /// Probes that reached the assertion the property is about. + reached: AtomicUsize, +} + +impl Tally { + /// Assert the run was not vacuous. + /// + /// The floor is **relative to the configurations actually built**, not an absolute count, because + /// an absolute one is really a measure of how fast the machine was. A property that reached + /// thousands of probes alone can reach a few dozen when it runs beside nine hundred other + /// tests on a loaded machine or under coverage instrumentation, and a floor tuned to the fast + /// case then fails for a reason that has nothing to do with the code under test. + /// + /// Both counts scale with the iteration budget, so their ratio does not. What the guard is for is + /// a property that has stopped reaching its assertion at all -- and a collapse to zero is just as + /// visible in the ratio. + fn report(&self, what: &str) { + let (seen, built, reached) = ( + self.seen.load(Ordering::Relaxed), + self.built.load(Ordering::Relaxed), + self.reached.load(Ordering::Relaxed), + ); + println!("{what}: {built}/{seen} configurations built, {reached} probes reached it"); + assert!( + built * 2 >= seen, + "only {built} of {seen} configurations built, so this checked much less than it looks \ + like it did" + ); + // At least one reaching probes for every two configurations built, and never zero. + assert!( + reached >= MIN_REACHED && reached * 2 >= built, + "{reached} probes reached the {what} assertion across {built} configurations; \ + this property has gone vacuous" + ); + } +} + +/// A translated source address comes back to where it started. +/// +/// The headline property, and the one that needs two tables. A packet leaving the local vpc has its +/// source rewritten by that vpc's table, which was built from the *local* side of the peering. The +/// reply arrives at the peer, whose table rewrites destinations and was built from the *remote* +/// side of the same peering -- a separate pass over separate data, by a separate code path +/// (`find_dst_mapping` against `dst_nat` rather than `find_src_mapping` against `src_nat`). +/// +/// So this is the one statement that ties the two halves together, and it is stated without knowing +/// what either produces: whatever the first one did, the second must undo. +/// +/// The development guide names this relation directly -- *translate then reverse is the identity on +/// the five-tuple* -- as the per-packet half of the decomposition. +#[test] +fn a_translated_source_comes_back() { + let tally = Tally::default(); + + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + let source = probe.source; + let out = run(&mut nf, vec![probe.take()]); + let translated = out[0] + .ip_source() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")); + + // An exposed source the tables do not cover is not a finding here: the mapping's + // completeness is proved by enumeration in `setup::config_driven`. This property is + // about what happens once a translation has occurred. + if translated == source { + continue; + } + + let back = run(&mut nf, vec![probe.reply(translated)]); + let returned = back[0] + .ip_destination() + .unwrap_or_else(|| unreachable!("a reply is always an ip packet")); + + assert_eq!( + returned, source, + "{source} translated to {translated} on the way out, and the reply to \ + {translated} came back to {returned} instead of {source}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("round trip"); +} + +/// Two sources that differ stay different after translation. +/// +/// Static NAT is one-to-one by definition, so a collision is a security defect rather than a +/// performance one: two tenants' flows arriving at the peer as the same address are +/// indistinguishable to everything downstream, including the reverse mapping. +/// +/// `setup::config_driven` proves the *table* injective. This proves the stage is, which is a +/// different claim: the table could be right and the write to the packet's header wrong, and no +/// table-level property would see it. +#[test] +fn distinct_sources_stay_distinct() { + let tally = Tally::default(); + + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + // Every private address the configuration offers, not just the drawn ones: the drawn + // ones may repeat, and a collision is only visible across distinct inputs. + let sources = fabric.private.clone(); + let _ = probes; + + let batch: Vec> = sources + .iter() + .map(|source| fabric.outbound_to_peer(*source)) + .collect(); + let out = run(&mut nf, batch); + + let mut taken: BTreeMap = BTreeMap::new(); + for (source, packet) in sources.iter().zip(out.iter()) { + let translated = packet + .ip_source() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")); + if translated == *source { + continue; + } + if let Some(previous) = taken.insert(translated, *source) { + panic!( + "{source} and {previous} both translated to {translated}, so static NAT is \ + not one to one for {exposes:#?}" + ); + } + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("injectivity"); +} + +/// Translating the source leaves everything else alone. +/// +/// The frame condition for this stage. The generated exposes carry no port ranges, so the address +/// translation path is the one taken and ports are not part of it -- a rewritten port here would be +/// a mapping reaching further than it was configured to. +/// +/// The destination matters most: the local vpc's table also holds a destination half, built from +/// its peer's manifest. The peer offers no translation, so an outbound packet's destination must +/// come through untouched, and a rewrite would mean the two halves of the table are bleeding into +/// each other. +#[test] +fn translation_touches_only_the_source() { + let tally = Tally::default(); + + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + let (destination, sport, dport) = (probe.destination, probe.sport, probe.dport); + let proto = if probe.tcp { + NextHeader::TCP + } else { + NextHeader::UDP + }; + let out = run(&mut nf, vec![probe.take()]); + let packet = &out[0]; + + assert_eq!( + packet.ip_destination(), + Some(destination), + "source translation rewrote the destination" + ); + assert_eq!( + packet.transport_src_port().map(std::num::NonZero::get), + Some(sport), + "source translation rewrote the source port, which no expose asked for" + ); + assert_eq!( + packet.transport_dst_port().map(std::num::NonZero::get), + Some(dport), + "source translation rewrote the destination port" + ); + assert_eq!( + packet.ip_proto(), + Some(proto), + "source translation changed the transport protocol" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("frame"); +} + +/// Nothing is translated that did not ask to be. +/// +/// The arrival state is the stage's precondition, and every flag in it is a decision an upstream +/// stage made. `requires_static_nat_src` says this packet is to be translated; `is_src_natted` says +/// something already has. Ignoring either means translating a packet twice, or translating one the +/// pipeline had decided to leave alone -- both of which produce an address the reverse mapping +/// cannot undo. +/// +/// A source the exposes do not offer is the same claim from the other side: the stage may only act +/// on what the configuration named. +#[test] +fn nothing_is_translated_without_permission() { + let tally = Tally::default(); + + bolero::check!() + .with_generator(Scenario { strays: true }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + // Every reason a probe may not be translated, taken together: the request was not + // made, an earlier stage already made it, the annotations needed to answer it are + // missing or name something the configuration does not have, or the source is an + // address no expose offers. Whichever it is, the source must come out as it went in. + if probe.asks_for_translation() && probe.exposed { + continue; + } + + let (source, stray, arrival) = (probe.source, probe.stray, probe.arrival); + let out = run(&mut nf, vec![probe.take()]); + let packet = &out[0]; + + assert_eq!( + packet.ip_source(), + Some(source), + "static NAT translated {source} although {stray:?} forbade it; the packet \ + arrived as {arrival:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("permission"); +} + +/// A packet the stage cannot look up is dropped, and says why. +/// +/// The dataplane's universal obligation, and the cheapest one to state: an outcome the operator can +/// see beats a correct outcome nobody can explain. `DoneReason` is the vocabulary, so the assertion +/// is only that the packet carries one -- not which -- with the reasons that would mean something +/// else entirely ruled out. +/// +/// A silent pass here is the real failure: a packet whose source vpc is unknown has no table, so +/// letting it through means forwarding untranslated traffic under a configuration that never +/// mentioned it. +#[test] +fn a_packet_that_cannot_be_looked_up_says_so() { + let tally = Tally::default(); + + bolero::check!() + .with_generator(Scenario { strays: true }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + let unroutable = matches!( + probe.stray, + Some(Stray::NoSourceVni | Stray::UnknownSourceVni) + ); + if !unroutable { + continue; + } + + let (source, stray) = (probe.source, probe.stray); + let out = run(&mut nf, vec![probe.take()]); + let packet = &out[0]; + + let reason = packet.get_done().unwrap_or_else(|| { + panic!( + "a packet with {stray:?} passed static NAT with no verdict at all, so \ + {source} would be forwarded untranslated" + ) + }); + assert_eq!( + reason, + DoneReason::Unroutable, + "a packet with {stray:?} was dropped for {reason:?}, which does not describe \ + what happened to it" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("attribution"); +} + +/// A packet whose addresses changed is marked as having changed. +/// +/// Static NAT rewrites addresses in place and leaves the transport checksum stale, relying on +/// `checksum_refresh` to have a later stage fix it. So the mark is not bookkeeping: a translated +/// packet that is not marked goes out with a checksum for the address it no longer carries, and is +/// discarded by the receiver rather than by anything that could report it. +/// +/// `is_src_natted` carries the same weight in the other direction -- it is what stops a second NAT +/// stage translating the packet again. +#[test] +fn a_modified_packet_is_always_marked() { + let tally = Tally::default(); + + bolero::check!() + .with_generator(Scenario { strays: true }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + let source = probe.source; + let out = run(&mut nf, vec![probe.take()]); + let packet = &out[0]; + + let translated = packet + .ip_source() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")) + != source; + if !translated { + continue; + } + + assert!( + packet.meta().is_src_natted(), + "{source} was translated without the source-natted mark, so a later stage \ + would translate it again" + ); + assert!( + packet.meta().checksum_refresh(), + "{source} was translated without asking for a checksum refresh, so the packet \ + goes out with a checksum for an address it no longer carries" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("marking"); +} diff --git a/nat/src/static_nat/mod.rs b/nat/src/static_nat/mod.rs index 844cefa19a..a2bf321741 100644 --- a/nat/src/static_nat/mod.rs +++ b/nat/src/static_nat/mod.rs @@ -3,8 +3,10 @@ //! Static NAT implementation +pub(crate) mod fuzz; pub mod natrw; pub mod nf; +pub(crate) mod probe; pub mod setup; pub(crate) mod test; diff --git a/nat/src/static_nat/probe.rs b/nat/src/static_nat/probe.rs new file mode 100644 index 0000000000..ff6876eadf --- /dev/null +++ b/nat/src/static_nat/probe.rs @@ -0,0 +1,467 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! Packets drawn relative to a static NAT configuration. +//! +//! A [`bolero::TypeGenerator`] over `Packet` produces packets that miss every table a generated +//! configuration builds, so a property driven by one explores the miss path and nothing else. The +//! [development guide][crate] makes the same argument one level up, about generating configuration +//! values rather than building configurations from operations: a generator that does not know what +//! the thing under test is configured for reaches only its rejection paths. +//! +//! So the configuration is a **parameter to resolution**, not a predicate to filter against. A +//! [`ProbeSpec`] is drawn without reference to any configuration -- it is a handful of indices -- +//! and [`ProbeSpec::resolve`] interprets it against a [`Fabric`]. Resolution is total: every draw +//! becomes a packet, and the ones that are *meant* to miss miss deliberately, named by [`Stray`], +//! rather than by accident. +//! +//! This mirrors `acl-filter`'s `ProbeSpec`, which resolves against a built overlay the same way. +//! +//! # The arrival state is the network function's precondition +//! +//! [`StaticNat`] sits in the middle of the pipeline and assumes its predecessors have annotated the +//! packet: a source and destination VPC discriminant, the overlay flag, and the two flags saying +//! which directions of translation are wanted. Nothing in the type system says so -- `process` +//! silently passes over a packet that lacks them, and `process_packet` drops one whose +//! discriminants are missing. +//! +//! [`Arrival`] writes that state down in one place. It is the network function's precondition made +//! explicit, which is what the development guide asks for when it puts contracts on functions +//! rather than on the pipeline: the assumption travels with the stage instead of being re-derived +//! by every test that drives it. `masquerade`'s tests hand-roll the same thing as a mock stage. + +#![cfg(test)] + +use crate::static_nat::nf::StaticNat; +use crate::static_nat::setup::build_nat_configuration; +use bolero::TypeGenerator; +use config::external::overlay::vpcpeering::VpcExpose; +use config::external::overlay::vpcpeering::contract::{ + LOCAL_VNI, REMOTE_VNI, overlay_with_exposes, +}; +use lpm::prefix::PrefixWithOptionalPorts; +use net::buffer::TestBuffer; +use net::ip::{NextHeader, UnicastIpAddr}; +use net::packet::test_utils::{ + build_test_ipv4_packet_with_transport, build_test_ipv6_packet_with_transport, +}; +use net::packet::{Packet, VpcDiscriminant}; +use net::tcp::port::TcpPort; +use net::udp::UdpPort; +use net::vxlan::Vni; +use std::collections::BTreeSet; +use std::net::IpAddr; + +/// The TTL every probe is built with, so that a property can tell a translation from a rewrite of +/// anything else. +pub(crate) const PROBE_TTL: u8 = 64; + +/// A VNI no generated configuration uses, for the probe that asks to be looked up in a table that +/// does not exist. +const ABSENT_VNI: u32 = 4_000; + +pub(crate) fn vni(raw: u32) -> Vni { + Vni::new_checked(raw).unwrap_or_else(|_| unreachable!("{raw} is a legal vni")) +} + +/// Every address a set of prefixes covers. +/// +/// The static NAT generator keeps both sides of an expose small enough that this is a handful of +/// addresses, which is what lets a property enumerate rather than sample. +pub(crate) fn addresses(prefixes: &BTreeSet) -> Vec { + let mut out = Vec::new(); + for prefix in prefixes { + let prefix = prefix.prefix(); + let (start, end) = (prefix.as_address(), prefix.last_address()); + let (mut bits, last) = match (start, end) { + (IpAddr::V4(a), IpAddr::V4(b)) => (u128::from(a.to_bits()), u128::from(b.to_bits())), + (IpAddr::V6(a), IpAddr::V6(b)) => (a.to_bits(), b.to_bits()), + _ => unreachable!("a prefix does not change address family"), + }; + while bits <= last { + out.push(match start { + IpAddr::V4(_) => IpAddr::V4( + u32::try_from(bits) + .unwrap_or_else(|_| unreachable!()) + .into(), + ), + IpAddr::V6(_) => IpAddr::V6(bits.into()), + }); + bits += 1; + } + } + out +} + +/// A built static NAT configuration, and the address sets it declares. +/// +/// The two vpcs are the ones [`overlay_with_exposes`] builds: `VPC-1` at [`LOCAL_VNI`] offers the +/// generated exposes, and `VPC-2` at [`REMOTE_VNI`] offers one unrelated prefix with no translation +/// on it. That asymmetry is what makes the round trip a property over two independently built +/// tables rather than over one: +/// +/// * `VPC-1`'s table translates **sources**, private to public, since the exposes are its own; and +/// * `VPC-2`'s table translates **destinations**, public back to private, since it builds that half +/// from its peer's manifest. +/// +/// So a packet leaving `VPC-1` and the reply coming back to it are handled by different tables built +/// from opposite ends of the same expose, and the two must agree. +pub(crate) struct Fabric { + writer: crate::static_nat::natrw::NatTablesWriter, + /// Every address the local exposes offer, before translation. + pub(crate) private: Vec, + /// Every address the local exposes translate to. + pub(crate) public: Vec, + /// Addresses in the peer vpc, which no expose translates. + pub(crate) peer: Vec, +} + +impl Fabric { + /// Build the tables a set of exposes implies, or `None` if the overlay they form is not valid. + /// + /// A rejection here is a legitimate outcome rather than a failure: exposes are generated one at + /// a time and two of them may overlap, which a manifest refuses. The properties count how often + /// it happens so that a generator change that starts rejecting everything cannot pass quietly. + pub(crate) fn build(exposes: &[VpcExpose]) -> Option { + let private: Vec = exposes.iter().flat_map(|e| addresses(&e.ips)).collect(); + let public: Vec = exposes + .iter() + .filter_map(|e| e.nat.as_ref()) + .flat_map(|nat| addresses(&nat.as_range)) + .collect(); + + let overlay = overlay_with_exposes(exposes.to_vec()).ok()?; + let validated = overlay.validate().ok()?; + let tables = build_nat_configuration(validated.vpc_table()).ok()?; + + // The peer prefix `overlay_with_exposes` fixes, in whichever family the exposes chose. + let peer = match private.first() { + Some(IpAddr::V6(_)) => vec![ + "2001:db8:ffff::1" + .parse() + .unwrap_or_else(|_| unreachable!()), + "2001:db8:ffff::2" + .parse() + .unwrap_or_else(|_| unreachable!()), + ], + _ => vec![ + "3.3.3.1".parse().unwrap_or_else(|_| unreachable!()), + "3.3.3.2".parse().unwrap_or_else(|_| unreachable!()), + ], + }; + + let mut writer = crate::static_nat::natrw::NatTablesWriter::new(); + writer.update_nat_tables(tables); + Some(Self { + writer, + private, + public, + peer, + }) + } + + /// A network function reading these tables. + /// + /// Fresh per call: `StaticNat` holds no state of its own, so a property that wants to know a + /// batch was not influenced by an earlier one can simply take another. + pub(crate) fn nf(&self) -> StaticNat { + StaticNat::with_reader("probe", self.writer.get_reader()) + } + + /// An outbound packet from `source` to the peer, with fixed ports. + /// + /// For a property that wants to sweep every address the configuration offers rather than the + /// drawn ones -- injectivity, which is only visible across distinct inputs and so cannot be + /// left to a draw that may repeat. + pub(crate) fn outbound_to_peer(&self, source: IpAddr) -> Packet { + let mut packet = build(source, self.peer[0], false, 1024, 80); + Arrival::outbound().stamp(&mut packet); + packet + } + + /// Whether this fabric can be probed at all. + /// + /// An expose whose two sides are empty builds a table with nothing in it, and every probe + /// against it misses. Properties skip those rather than count them as passes. + pub(crate) fn is_probeable(&self) -> bool { + !self.private.is_empty() && !self.public.is_empty() + } +} + +/// The metadata a packet must carry for [`StaticNat`] to look at it. +/// +/// Every field here is something an upstream stage sets in production. Writing them out is what +/// makes this a test of static NAT rather than a test of whatever mock supplies them. +#[derive(Debug, Clone, Copy)] +pub(crate) struct Arrival { + /// The vpc the packet came from, which selects the table. + pub(crate) src_vpcd: Option, + /// The vpc the packet is going to, which selects the source-translation half of it. + pub(crate) dst_vpcd: Option, + pub(crate) wants_src_nat: bool, + pub(crate) wants_dst_nat: bool, + /// Set when an earlier stage has already translated the source, which static NAT must respect. + pub(crate) already_src_natted: bool, +} + +impl Arrival { + /// Leaving the local vpc for its peer: source translation, private to public. + pub(crate) fn outbound() -> Self { + Self { + src_vpcd: Some(vni(LOCAL_VNI)), + dst_vpcd: Some(vni(REMOTE_VNI)), + wants_src_nat: true, + wants_dst_nat: false, + already_src_natted: false, + } + } + + /// The reply, arriving at the peer for the local vpc: destination translation, public back to + /// private. + pub(crate) fn inbound() -> Self { + Self { + src_vpcd: Some(vni(REMOTE_VNI)), + dst_vpcd: Some(vni(LOCAL_VNI)), + wants_src_nat: false, + wants_dst_nat: true, + already_src_natted: false, + } + } + + /// Stamp the state onto a packet. + /// + /// `set_keep` is what makes a dropped packet observable: `Packet::enforce` removes a dropped + /// packet from the output iterator, so without it a drop and a translation-that-did-nothing are + /// the same event seen from outside, and no property could tell them apart. + pub(crate) fn stamp(self, packet: &mut Packet) { + let meta = packet.meta_mut(); + meta.src_vpcd = self.src_vpcd.map(VpcDiscriminant::from_vni); + meta.dst_vpcd = self.dst_vpcd.map(VpcDiscriminant::from_vni); + meta.set_overlay(true); + meta.set_keep(true); + meta.set_static_nat_src(self.wants_src_nat); + meta.set_static_nat_dst(self.wants_dst_nat); + meta.src_natted(self.already_src_natted); + } +} + +/// A deliberate deviation from a packet the configuration translates. +/// +/// Each one is a question about the network function's own decisions rather than about the mapping: +/// the mapping is covered by enumeration at the table level, and none of these reach it. +#[derive(Debug, Clone, Copy, TypeGenerator)] +pub(crate) enum Stray { + /// A source address no expose offers. Nothing should translate it. + SourceNotExposed, + /// No source vpc annotation, which the stage cannot proceed without. + NoSourceVni, + /// A source vpc with no table of its own. + UnknownSourceVni, + /// A destination vpc the local vpc does not peer with, so the source half finds no table. + UnknownDestVni, + /// An earlier stage has already translated the source. + AlreadySourceNatted, + /// Nothing asked for translation, so the stage should pass the packet through untouched. + NotAskedFor, +} + +/// A drawn probe, before it knows anything about a configuration. +/// +/// Deliberately all indices and raw values: nothing here refers to a prefix, an address or a vni, so +/// the same draw is meaningful against any fabric and shrinking stays interpretable. +#[derive(Debug, Clone, Copy, TypeGenerator)] +pub(crate) struct ProbeSpec { + source: u8, + peer: u8, + tcp: bool, + sport: u16, + dport: u16, + stray: Option, +} + +/// A probe resolved against a fabric: the packet, and the facts a property may reason from. +/// +/// The facts are all *inputs* -- what was built and what was asked for. None of them is a +/// prediction of what static NAT should produce, because a prediction is a second implementation of +/// the mapping and the point of resolving against the configuration is not to need one. +pub(crate) struct Probe { + /// The packet itself, taken out by [`Probe::take`] when it is handed to the stage. + /// + /// Held in an `Option` so that taking it does not move out of the probe: the remaining fields + /// are what a property asserts against afterwards, and [`Probe::reply`] needs them once the + /// outbound packet is gone. + packet: Option>, + /// The source address as built. + pub(crate) source: IpAddr, + /// The destination address as built. + pub(crate) destination: IpAddr, + pub(crate) sport: u16, + pub(crate) dport: u16, + pub(crate) tcp: bool, + /// Whether the local exposes offer `source`. + pub(crate) exposed: bool, + /// The arrival state the packet carries. + pub(crate) arrival: Arrival, + pub(crate) stray: Option, +} + +impl Probe { + /// The packet, to hand to the stage. + /// + /// # Panics + /// + /// Panics if called twice. A probe is one packet; a property that wants the same five-tuple + /// again should resolve the spec again, which is cheap and says so plainly. + pub(crate) fn take(&mut self) -> Packet { + self.packet + .take() + .unwrap_or_else(|| unreachable!("a probe's packet is taken once")) + } + + /// Whether static NAT was both asked to translate the source and given everything it needs to. + /// + /// This is a statement about the *request*, not about the mapping: a probe that is `expected` may + /// still legitimately go untranslated if no rule covers its source. What it may not do is come + /// out translated when this is false. + pub(crate) fn asks_for_translation(&self) -> bool { + self.arrival.wants_src_nat + && !self.arrival.already_src_natted + && self.arrival.src_vpcd == Some(vni(LOCAL_VNI)) + && self.arrival.dst_vpcd == Some(vni(REMOTE_VNI)) + } + + /// The packet that answers this one, addressed to `translated`. + /// + /// The reply is what the peer would send back: the two ends swapped, and the local end named by + /// whatever the outbound translation produced rather than by the address the sender used. It + /// arrives at the peer's vpc, so it is looked up in the peer's table -- the other half of the + /// same expose, built independently. + pub(crate) fn reply(&self, translated: IpAddr) -> Packet { + let mut packet = build( + self.destination, + translated, + self.tcp, + self.dport, + self.sport, + ); + Arrival::inbound().stamp(&mut packet); + packet + } +} + +impl ProbeSpec { + /// Drop the deviation, leaving a probe the configuration is meant to translate. + /// + /// For the properties about what happens *after* a translation: a probe that misses on purpose + /// has no translation to say anything about, and would only dilute the batch. + pub(crate) fn clear_stray(&mut self) { + self.stray = None; + } + + /// Interpret this draw against a fabric. + /// + /// Total by construction: an index is taken modulo the set it selects from, so there is no draw + /// that fails to become a packet and no rejection loop to bias the distribution. + pub(crate) fn resolve(self, fabric: &Fabric) -> Probe { + let mut arrival = Arrival::outbound(); + let mut source = fabric.private[self.source as usize % fabric.private.len()]; + let destination = fabric.peer[self.peer as usize % fabric.peer.len()]; + let mut exposed = true; + + match self.stray { + None => {} + Some(Stray::SourceNotExposed) => { + source = destination; + exposed = false; + } + Some(Stray::NoSourceVni) => arrival.src_vpcd = None, + Some(Stray::UnknownSourceVni) => arrival.src_vpcd = Some(vni(ABSENT_VNI)), + Some(Stray::UnknownDestVni) => arrival.dst_vpcd = Some(vni(ABSENT_VNI)), + Some(Stray::AlreadySourceNatted) => arrival.already_src_natted = true, + Some(Stray::NotAskedFor) => { + arrival.wants_src_nat = false; + arrival.wants_dst_nat = false; + } + } + + // Port 0 is not a legal port on either transport, and the mapping is not about ports here. + let sport = self.sport.max(1); + let dport = self.dport.max(1); + let mut packet = build(source, destination, self.tcp, sport, dport); + arrival.stamp(&mut packet); + + Probe { + packet: Some(packet), + source, + destination, + sport, + dport, + tcp: self.tcp, + exposed, + arrival, + stray: self.stray, + } + } +} + +/// Build a packet with the given five-tuple. +/// +/// # Panics +/// +/// Panics if the two addresses are of different families. Resolution never mixes them, since an +/// expose is of one family throughout and the peer prefix is chosen to match. +pub(crate) fn build( + source: IpAddr, + destination: IpAddr, + tcp: bool, + sport: u16, + dport: u16, +) -> Packet { + let next_header = if tcp { + NextHeader::TCP + } else { + NextHeader::UDP + }; + let mut packet = match (source, destination) { + (IpAddr::V4(_), IpAddr::V4(_)) => { + build_test_ipv4_packet_with_transport(PROBE_TTL, Some(next_header)) + .unwrap_or_else(|e| unreachable!("{e:?}")) + } + (IpAddr::V6(_), IpAddr::V6(_)) => { + build_test_ipv6_packet_with_transport(PROBE_TTL, Some(next_header)) + .unwrap_or_else(|e| unreachable!("{e:?}")) + } + _ => unreachable!("a probe never mixes address families"), + }; + + packet + .set_ip_source(UnicastIpAddr::try_from(source).unwrap_or_else(|_| { + unreachable!("{source} is drawn from a prefix an expose offers, so it is unicast") + })) + .unwrap_or_else(|e| unreachable!("{e:?}")); + packet + .set_ip_destination(destination) + .unwrap_or_else(|e| unreachable!("{e:?}")); + + if tcp { + packet + .set_tcp_source_port(TcpPort::new_checked(sport).unwrap_or_else(|_| unreachable!())) + .unwrap_or_else(|e| unreachable!("{e:?}")); + packet + .set_tcp_destination_port( + TcpPort::new_checked(dport).unwrap_or_else(|_| unreachable!()), + ) + .unwrap_or_else(|e| unreachable!("{e:?}")); + } else { + packet + .set_udp_source_port(UdpPort::new_checked(sport).unwrap_or_else(|_| unreachable!())) + .unwrap_or_else(|e| unreachable!("{e:?}")); + packet + .set_udp_destination_port( + UdpPort::new_checked(dport).unwrap_or_else(|_| unreachable!()), + ) + .unwrap_or_else(|e| unreachable!("{e:?}")); + } + + packet +} From 37b299ce61a9a41f57315e7427105c40e9d6f6db Mon Sep 17 00:00:00 2001 From: Daniel Noland Date: Mon, 17 Aug 2026 16:48:59 -0600 Subject: [PATCH 4/7] docs(testing): Mark the config-algebra note as partly implemented The note was written before any of it existed and said so. The per-packet half of its decomposition now has a worked example -- packets drawn relative to a generated configuration, put through a real network function, judged by metamorphic relations -- so the blanket claim is no longer true and would mislead the next reader into rebuilding it. The operation algebra itself is still unbuilt, and the enactment path refactor it implies is still deferred, so the status line says which half is which rather than simply flipping. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: Daniel Noland (cherry picked from commit aecbf11be5afcb2ebed3b43e0dece9c9210a00e6) --- development/code/config-algebra-testing.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/development/code/config-algebra-testing.md b/development/code/config-algebra-testing.md index 335dbc3bed..c2059322aa 100644 --- a/development/code/config-algebra-testing.md +++ b/development/code/config-algebra-testing.md @@ -1,7 +1,13 @@ # Testing a config-driven dataplane with an operation algebra -Status: **design note**. Nothing here is implemented yet. It records a strategy and, more importantly, -the reasoning that rejected the alternatives, so that the next attempt does not rediscover them. +Status: **design note, partly implemented**. It records a strategy and, more importantly, the +reasoning that rejected the alternatives, so that the next attempt does not rediscover them. + +The per-packet half of the decomposition has a first worked example in `nat/src/static_nat/probe.rs` +and `nat/src/static_nat/fuzz.rs`: packets drawn relative to a generated configuration, put through a +real network function, and judged by metamorphic relations rather than by an oracle. The operation +algebra itself -- sequences, undo, commutation from read and write sets -- is still unbuilt, and the +enactment path refactor it implies is still deferred. ## The problem From f73d124489bba29abeb5c3c336cd5d7a576b53cf Mon Sep 17 00:00:00 2001 From: Daniel Noland Date: Mon, 17 Aug 2026 17:36:54 -0600 Subject: [PATCH 5/7] test(nat): Cover the static NAT path that maps ports as well as addresses Static NAT permits a port range on a prefix, and a prefix that carries one takes the mapping down a second path entirely: `NatTableValue::Pat` and `PortAddrTranslationValue` rather than `NatTableValue::Nat` and `AddrTranslationValue`. The expose generator produced no port ranges, so that path had no configuration-driven coverage at all. ## The rule makes it the harder path Validation asks that the two sides cover the same **total**, counting addresses times ports. So a `/32` carrying 64 ports is a legal answer to a `/30` carrying 16, and the mapping has to run across both dimensions at once. That asymmetry is the reason the path exists, so `StaticNatExposes::with_ports` draws it on purpose: one total per expose, divided into addresses and ports independently per side, with both port ranges starting at a drawn offset so a mapping that quietly assumes they begin at the same port fails here. Worth noting what is legal for static NAT and not for port forwarding, which requires the two prefix lengths and the two port counts to match individually. The two flavours do not share this rule and must not share a generator. ## What changed in the harness An address on its own is no longer a thing the configuration maps -- the address-and-port pair is. So `Endpoint` replaces the bare address, carrying the range its prefix declares, and a probe draws its port from that range rather than freely, or it would miss. Three consequences: * the reply in the round trip must be addressed to the **translated** port, since that is the port the peer was contacted from; * injectivity sweeps every pair rather than every address -- an address-only sweep checks a diagonal of the space and calls it injective; and * the frame differs between the paths. With no port range the transport ports are part of the frame and must survive untouched; with one they are part of what is being translated, and only the destination and protocol remain. One property per flavour rather than one over a mix, following the same reasoning as the NAT flavour properties in `mgmt`: a mixed property reaches each path eventually, one that asks for a path reaches it every time and says in its name which one failed. ## The two suites provably exercise different code Break `PortAddrTranslationValue::get_entry` and the two port properties fail while all four address properties pass. Break `AddrTranslationValue::get_entry` and exactly the reverse happens. That mutual isolation is the evidence that the extra properties are earning their place rather than re-running the same paths under new names. All eleven properties build 100% of the configurations they draw. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: Daniel Noland (cherry picked from commit d3ac66814c92ad289717249b753d7e99fc7dc9ba) --- config/src/external/overlay/vpcpeering.rs | 84 +++++- nat/src/static_nat/fuzz.rs | 319 ++++++++++++++-------- nat/src/static_nat/probe.rs | 141 +++++++--- 3 files changed, 391 insertions(+), 153 deletions(-) diff --git a/config/src/external/overlay/vpcpeering.rs b/config/src/external/overlay/vpcpeering.rs index 5c12ba76e9..e65cb1d8b2 100644 --- a/config/src/external/overlay/vpcpeering.rs +++ b/config/src/external/overlay/vpcpeering.rs @@ -1207,9 +1207,8 @@ pub mod contract { /// sampling. Parts are placed largest first from an aligned base, which keeps every prefix /// aligned to its own size and keeps them from overlapping. /// - /// No port ranges yet: static NAT permits them, and they take the mapping down a second path - /// (`PortAddrTranslationValue` rather than `AddrTranslationValue`) that carries its own - /// unfinished work. That path wants a generator of its own. + /// Addresses only. For the port-range form, which takes the mapping down a different path, see + /// [`StaticNatExposes::with_ports`]. #[derive(Debug, Clone, Copy, Default)] pub struct StaticNatExpose; @@ -1228,13 +1227,44 @@ pub mod contract { /// * **Address family.** A peering's manifests must agree on one family, so a v4 expose beside a /// v6 one is refused. The family is drawn once here and shared. /// - /// The field is the largest number of exposes to draw; the generator draws between one and that. + /// # Ports + /// + /// Static NAT permits a port range on each prefix, and that takes the mapping down a second + /// path: `NatTableValue::Pat` and `PortAddrTranslationValue` rather than + /// `NatTableValue::Nat` and `AddrTranslationValue`. The rule validation applies is that the two + /// sides cover the same **total**, counting addresses times ports -- so a `/32` carrying 64 + /// ports is a legal answer to a `/30` carrying 16, and the mapping has to run across both + /// dimensions at once. + /// + /// That asymmetry is the whole reason the path exists, so [`StaticNatExposes::with_ports`] + /// draws it deliberately: one total per expose, split into addresses and ports **independently + /// per side**. Note that this is legal for static NAT and *illegal* for port forwarding, which + /// requires the two lengths and the two port counts to match individually. #[derive(Debug, Clone, Copy)] - pub struct StaticNatExposes(pub u8); + pub struct StaticNatExposes { + /// The most exposes to draw. The generator draws between one and this. + pub max: u8, + /// Whether each prefix carries a port range. + pub ports: bool, + } impl Default for StaticNatExposes { fn default() -> Self { - Self(3) + Self::addresses_only(3) + } + } + + impl StaticNatExposes { + /// Exposes whose prefixes carry no port range, mapping address to address. + #[must_use] + pub fn addresses_only(max: u8) -> Self { + Self { max, ports: false } + } + + /// Exposes whose prefixes carry port ranges, mapping address and port together. + #[must_use] + pub fn with_ports(max: u8) -> Self { + Self { max, ports: true } } } @@ -1261,9 +1291,15 @@ pub mod contract { fn generate(&self, driver: &mut D) -> Option> { let v4 = driver.produce::()?; - let count = driver.gen_u8(Included(&1), Included(&self.0.max(1)))?; + let count = driver.gen_u8(Included(&1), Included(&self.max.max(1)))?; (0..count) - .map(|block| static_nat_expose(driver, v4, block)) + .map(|block| { + if self.ports { + static_nat_pat_expose(driver, v4, block) + } else { + static_nat_expose(driver, v4, block) + } + }) .collect() } } @@ -1287,6 +1323,38 @@ pub mod contract { Some(expose) } + /// One static NAT expose whose two sides carry port ranges. + /// + /// One prefix per side rather than a split, because the interesting asymmetry here is between + /// the two *dimensions* -- how a total is divided between addresses and ports -- and adding a + /// prefix split on top only makes the case harder to read for no new coverage. + /// + /// Each side draws its own division of the same total, so a `/32` carrying 64 ports opposite a + /// `/30` carrying 16 is a shape this produces on purpose. Both sides' port ranges start at a + /// drawn offset, so a mapping that quietly assumes the two ranges begin at the same port fails + /// here rather than in the field. + fn static_nat_pat_expose(driver: &mut D, v4: bool, block: u8) -> Option { + let total_log = driver.gen_u8(Included(&0), Included(&MAX_TOTAL_LOG))?; + + let mut side = |which| -> Option { + let port_log = driver.gen_u8(Included(&0), Included(&total_log))?; + let addr_log = total_log - port_log; + let prefix = *place(v4, which, block, &[addr_log])?.first()?; + let ports = port_range(driver, 1u16 << port_log)?; + Some(PrefixWithOptionalPorts::new(prefix, Some(ports))) + }; + + let private = side(Side::Private)?; + let public = side(Side::Public)?; + + VpcExpose::empty() + .make_static_nat() + .ok()? + .ip(private) + .as_range(public) + .ok() + } + // Split 2^total_log into powers of two, largest first. Halving a part keeps the total the // same, which is what lets the two sides be split independently and still agree. fn split(driver: &mut D, total_log: u8) -> Option> { diff --git a/nat/src/static_nat/fuzz.rs b/nat/src/static_nat/fuzz.rs index dcd0972c9c..a1209ef8cf 100644 --- a/nat/src/static_nat/fuzz.rs +++ b/nat/src/static_nat/fuzz.rs @@ -46,6 +46,7 @@ use net::packet::{DoneReason, Packet}; use pipeline::NetworkFunction; use std::collections::BTreeMap; use std::net::IpAddr; +use std::num::NonZero; /// Exposes per configuration. More than one is what makes the tables hold several rules, which is /// where a longest-prefix match has a choice to get wrong. @@ -71,13 +72,37 @@ struct Scenario { /// that is meant to miss has nothing to round trip; on for the ones about the stage's own /// decisions, which is all a stray exercises. strays: bool, + /// Which flavour of expose to draw. + exposes: StaticNatExposes, +} + +impl Scenario { + /// Address-to-address exposes, taking the mapping down `AddrTranslationValue`. + fn addresses(strays: bool) -> Self { + Self { + strays, + exposes: StaticNatExposes::addresses_only(MAX_EXPOSES), + } + } + + /// Exposes carrying port ranges, taking the mapping down `PortAddrTranslationValue` instead. + /// + /// A separate property per flavour rather than one over a mix. A mixed property reaches each + /// path eventually; one that asks for a path reaches it every time and says in its name which + /// one failed. + fn ports(strays: bool) -> Self { + Self { + strays, + exposes: StaticNatExposes::with_ports(MAX_EXPOSES), + } + } } impl ValueGenerator for Scenario { type Output = (Vec, Vec); fn generate(&self, driver: &mut D) -> Option { - let exposes = StaticNatExposes(MAX_EXPOSES).generate(driver)?; + let exposes = self.exposes.generate(driver)?; let mut probes = Vec::with_capacity(PROBES); for _ in 0..PROBES { @@ -109,6 +134,30 @@ fn fabric(exposes: &[VpcExpose]) -> Option { fabric.is_probeable().then_some(fabric) } +/// The source half of a packet's five-tuple. +/// +/// Address and port together, because that is the granularity static NAT maps at once an expose +/// carries port ranges: comparing addresses alone would call a translation that moved only the port +/// "unchanged", and every property below would then skip it. +fn five_tuple_source(packet: &Packet) -> (IpAddr, u16) { + ( + packet + .ip_source() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")), + packet.transport_src_port().map_or(0, NonZero::get), + ) +} + +/// The destination half, for judging a reply. +fn five_tuple_destination(packet: &Packet) -> (IpAddr, u16) { + ( + packet + .ip_destination() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")), + packet.transport_dst_port().map_or(0, NonZero::get), + ) +} + /// How much of a run actually reached the code under test. #[derive(Default)] struct Tally { @@ -153,7 +202,7 @@ impl Tally { } } -/// A translated source address comes back to where it started. +/// A translated source comes back to where it started. /// /// The headline property, and the one that needs two tables. A packet leaving the local vpc has its /// source rewritten by that vpc's table, which was built from the *local* side of the peering. The @@ -166,14 +215,11 @@ impl Tally { /// /// The development guide names this relation directly -- *translate then reverse is the identity on /// the five-tuple* -- as the per-packet half of the decomposition. -#[test] -fn a_translated_source_comes_back() { +fn drive_round_trip(scenario: Scenario) { let tally = Tally::default(); - bolero::check!() - .with_generator(Scenario { strays: false }) - .cloned() - .for_each(|(exposes, probes): (Vec, Vec)| { + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { tally.seen.fetch_add(1, Ordering::Relaxed); let Some(fabric) = fabric(&exposes) else { return; @@ -183,53 +229,64 @@ fn a_translated_source_comes_back() { for spec in &probes { let mut probe = (*spec).resolve(&fabric); - let source = probe.source; + let (source, sport) = (probe.source, probe.sport); let out = run(&mut nf, vec![probe.take()]); - let translated = out[0] - .ip_source() - .unwrap_or_else(|| unreachable!("a probe is always an ip packet")); + let (translated, translated_port) = five_tuple_source(&out[0]); // An exposed source the tables do not cover is not a finding here: the mapping's // completeness is proved by enumeration in `setup::config_driven`. This property is // about what happens once a translation has occurred. - if translated == source { + if (translated, translated_port) == (source, sport) { continue; } - let back = run(&mut nf, vec![probe.reply(translated)]); - let returned = back[0] - .ip_destination() - .unwrap_or_else(|| unreachable!("a reply is always an ip packet")); + let back = run(&mut nf, vec![probe.reply(translated, translated_port)]); + let (returned, returned_port) = five_tuple_destination(&back[0]); assert_eq!( - returned, source, - "{source} translated to {translated} on the way out, and the reply to \ - {translated} came back to {returned} instead of {source}" + (returned, returned_port), + (source, sport), + "{source}:{sport} translated to {translated}:{translated_port} on the way out, \ + and the reply came back to {returned}:{returned_port}" ); tally.reached.fetch_add(1, Ordering::Relaxed); } - }); + }, + ); tally.report("round trip"); } +#[test] +fn a_translated_source_comes_back() { + drive_round_trip(Scenario::addresses(false)); +} + +/// The same, where the mapping moves the port as well as the address. +/// +/// A second code path entirely -- `PortAddrTranslationValue` rather than `AddrTranslationValue` -- +/// and the harder one, since the two sides may divide their common total between addresses and +/// ports differently. A `/32` carrying 64 ports is a legal answer to a `/30` carrying 16, so the +/// reverse mapping cannot recover the address without also accounting for the port. +#[test] +fn a_translated_source_and_port_come_back() { + drive_round_trip(Scenario::ports(false)); +} + /// Two sources that differ stay different after translation. /// -/// Static NAT is one-to-one by definition, so a collision is a security defect rather than a -/// performance one: two tenants' flows arriving at the peer as the same address are +/// Static NAT is one-to-one by definition, so a collision is a tenant isolation defect rather than a +/// performance one: two flows arriving at the peer as the same address and port are /// indistinguishable to everything downstream, including the reverse mapping. /// /// `setup::config_driven` proves the *table* injective. This proves the stage is, which is a -/// different claim: the table could be right and the write to the packet's header wrong, and no +/// different claim: the table could be right and the write to the packet's headers wrong, and no /// table-level property would see it. -#[test] -fn distinct_sources_stay_distinct() { +fn drive_injectivity(scenario: Scenario) { let tally = Tally::default(); - bolero::check!() - .with_generator(Scenario { strays: false }) - .cloned() - .for_each(|(exposes, probes): (Vec, Vec)| { + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, _probes): (Vec, Vec)| { tally.seen.fetch_add(1, Ordering::Relaxed); let Some(fabric) = fabric(&exposes) else { return; @@ -237,56 +294,71 @@ fn distinct_sources_stay_distinct() { tally.built.fetch_add(1, Ordering::Relaxed); let mut nf = fabric.nf(); - // Every private address the configuration offers, not just the drawn ones: the drawn - // ones may repeat, and a collision is only visible across distinct inputs. - let sources = fabric.private.clone(); - let _ = probes; - + // Everything the configuration maps, not the drawn probes: the draws may repeat, and a + // collision is only visible across distinct inputs. + let sources = fabric.every_source(); let batch: Vec> = sources .iter() - .map(|source| fabric.outbound_to_peer(*source)) + .map(|(endpoint, port)| fabric.outbound_to_peer(*endpoint, *port)) .collect(); let out = run(&mut nf, batch); - let mut taken: BTreeMap = BTreeMap::new(); - for (source, packet) in sources.iter().zip(out.iter()) { - let translated = packet - .ip_source() - .unwrap_or_else(|| unreachable!("a probe is always an ip packet")); - if translated == *source { + let mut taken: BTreeMap<(IpAddr, u16), (IpAddr, u16)> = BTreeMap::new(); + for ((endpoint, port), packet) in sources.iter().zip(out.iter()) { + let before = (endpoint.addr, *port); + let after = five_tuple_source(packet); + if after == before { continue; } - if let Some(previous) = taken.insert(translated, *source) { + if let Some(previous) = taken.insert(after, before) { + let (addr, port) = after; + let (pa, pp) = previous; + let (ba, bp) = before; panic!( - "{source} and {previous} both translated to {translated}, so static NAT is \ - not one to one for {exposes:#?}" + "{ba}:{bp} and {pa}:{pp} both translated to {addr}:{port}, so static NAT \ + is not one to one for {exposes:#?}" ); } tally.reached.fetch_add(1, Ordering::Relaxed); } - }); + }, + ); tally.report("injectivity"); } +#[test] +fn distinct_sources_stay_distinct() { + drive_injectivity(Scenario::addresses(false)); +} + +/// The same over address-and-port pairs. +/// +/// Sweeping addresses alone here would check a diagonal of the space and call it injective: with +/// port ranges the thing the mapping is one to one over is the pair, so two ports on one address +/// colliding is a defect an address-only sweep cannot see. +#[test] +fn distinct_sources_and_ports_stay_distinct() { + drive_injectivity(Scenario::ports(false)); +} + /// Translating the source leaves everything else alone. /// -/// The frame condition for this stage. The generated exposes carry no port ranges, so the address -/// translation path is the one taken and ports are not part of it -- a rewritten port here would be -/// a mapping reaching further than it was configured to. +/// The frame condition for this stage, and it differs between the two paths -- which is the point of +/// stating it per flavour rather than once. With no port range on the expose the transport ports are +/// part of the frame and a rewrite would be a mapping reaching further than it was configured to; +/// with one they are part of what is being translated, and only the destination and the protocol +/// remain. /// -/// The destination matters most: the local vpc's table also holds a destination half, built from -/// its peer's manifest. The peer offers no translation, so an outbound packet's destination must -/// come through untouched, and a rewrite would mean the two halves of the table are bleeding into -/// each other. -#[test] -fn translation_touches_only_the_source() { +/// The destination matters in both. The local vpc's table also holds a destination half, built from +/// its peer's manifest; the peer offers no translation, so an outbound packet's destination must come +/// through untouched, and a rewrite would mean the two halves of the table are bleeding into each +/// other. +fn drive_frame(scenario: Scenario) { let tally = Tally::default(); - bolero::check!() - .with_generator(Scenario { strays: false }) - .cloned() - .for_each(|(exposes, probes): (Vec, Vec)| { + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { tally.seen.fetch_add(1, Ordering::Relaxed); let Some(fabric) = fabric(&exposes) else { return; @@ -311,12 +383,7 @@ fn translation_touches_only_the_source() { "source translation rewrote the destination" ); assert_eq!( - packet.transport_src_port().map(std::num::NonZero::get), - Some(sport), - "source translation rewrote the source port, which no expose asked for" - ); - assert_eq!( - packet.transport_dst_port().map(std::num::NonZero::get), + packet.transport_dst_port().map(NonZero::get), Some(dport), "source translation rewrote the destination port" ); @@ -325,13 +392,31 @@ fn translation_touches_only_the_source() { Some(proto), "source translation changed the transport protocol" ); + if !fabric.uses_ports { + assert_eq!( + packet.transport_src_port().map(NonZero::get), + Some(sport), + "source translation rewrote the source port, which no expose asked for" + ); + } tally.reached.fetch_add(1, Ordering::Relaxed); } - }); + }, + ); tally.report("frame"); } +#[test] +fn translation_touches_only_the_source() { + drive_frame(Scenario::addresses(false)); +} + +#[test] +fn port_translation_touches_only_the_source() { + drive_frame(Scenario::ports(false)); +} + /// Nothing is translated that did not ask to be. /// /// The arrival state is the stage's precondition, and every flag in it is a decision an upstream @@ -342,14 +427,11 @@ fn translation_touches_only_the_source() { /// /// A source the exposes do not offer is the same claim from the other side: the stage may only act /// on what the configuration named. -#[test] -fn nothing_is_translated_without_permission() { +fn drive_permission(scenario: Scenario) { let tally = Tally::default(); - bolero::check!() - .with_generator(Scenario { strays: true }) - .cloned() - .for_each(|(exposes, probes): (Vec, Vec)| { + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { tally.seen.fetch_add(1, Ordering::Relaxed); let Some(fabric) = fabric(&exposes) else { return; @@ -367,41 +449,48 @@ fn nothing_is_translated_without_permission() { continue; } - let (source, stray, arrival) = (probe.source, probe.stray, probe.arrival); + let (source, sport) = (probe.source, probe.sport); + let (stray, arrival) = (probe.stray, probe.arrival); let out = run(&mut nf, vec![probe.take()]); - let packet = &out[0]; assert_eq!( - packet.ip_source(), - Some(source), - "static NAT translated {source} although {stray:?} forbade it; the packet \ - arrived as {arrival:?}" + five_tuple_source(&out[0]), + (source, sport), + "static NAT translated {source}:{sport} although {stray:?} forbade it; the \ + packet arrived as {arrival:?}" ); tally.reached.fetch_add(1, Ordering::Relaxed); } - }); + }, + ); tally.report("permission"); } +#[test] +fn nothing_is_translated_without_permission() { + drive_permission(Scenario::addresses(true)); +} + +#[test] +fn no_port_is_translated_without_permission() { + drive_permission(Scenario::ports(true)); +} + /// A packet the stage cannot look up is dropped, and says why. /// /// The dataplane's universal obligation, and the cheapest one to state: an outcome the operator can /// see beats a correct outcome nobody can explain. `DoneReason` is the vocabulary, so the assertion -/// is only that the packet carries one -- not which -- with the reasons that would mean something -/// else entirely ruled out. +/// is that the packet carries one and that it is the one that describes what happened. /// /// A silent pass here is the real failure: a packet whose source vpc is unknown has no table, so /// letting it through means forwarding untranslated traffic under a configuration that never /// mentioned it. -#[test] -fn a_packet_that_cannot_be_looked_up_says_so() { +fn drive_attribution(scenario: Scenario) { let tally = Tally::default(); - bolero::check!() - .with_generator(Scenario { strays: true }) - .cloned() - .for_each(|(exposes, probes): (Vec, Vec)| { + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { tally.seen.fetch_add(1, Ordering::Relaxed); let Some(fabric) = fabric(&exposes) else { return; @@ -421,9 +510,8 @@ fn a_packet_that_cannot_be_looked_up_says_so() { let (source, stray) = (probe.source, probe.stray); let out = run(&mut nf, vec![probe.take()]); - let packet = &out[0]; - let reason = packet.get_done().unwrap_or_else(|| { + let reason = out[0].get_done().unwrap_or_else(|| { panic!( "a packet with {stray:?} passed static NAT with no verdict at all, so \ {source} would be forwarded untranslated" @@ -437,28 +525,31 @@ fn a_packet_that_cannot_be_looked_up_says_so() { ); tally.reached.fetch_add(1, Ordering::Relaxed); } - }); + }, + ); tally.report("attribution"); } -/// A packet whose addresses changed is marked as having changed. +#[test] +fn a_packet_that_cannot_be_looked_up_says_so() { + drive_attribution(Scenario::addresses(true)); +} + +/// A packet whose five-tuple changed is marked as having changed. /// -/// Static NAT rewrites addresses in place and leaves the transport checksum stale, relying on +/// Static NAT rewrites headers in place and leaves the transport checksum stale, relying on /// `checksum_refresh` to have a later stage fix it. So the mark is not bookkeeping: a translated -/// packet that is not marked goes out with a checksum for the address it no longer carries, and is +/// packet that is not marked goes out with a checksum for the addresses it no longer carries, and is /// discarded by the receiver rather than by anything that could report it. /// /// `is_src_natted` carries the same weight in the other direction -- it is what stops a second NAT /// stage translating the packet again. -#[test] -fn a_modified_packet_is_always_marked() { +fn drive_marking(scenario: Scenario) { let tally = Tally::default(); - bolero::check!() - .with_generator(Scenario { strays: true }) - .cloned() - .for_each(|(exposes, probes): (Vec, Vec)| { + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { tally.seen.fetch_add(1, Ordering::Relaxed); let Some(fabric) = fabric(&exposes) else { return; @@ -468,31 +559,39 @@ fn a_modified_packet_is_always_marked() { for spec in &probes { let mut probe = (*spec).resolve(&fabric); - let source = probe.source; + let before = (probe.source, probe.sport); let out = run(&mut nf, vec![probe.take()]); let packet = &out[0]; - let translated = packet - .ip_source() - .unwrap_or_else(|| unreachable!("a probe is always an ip packet")) - != source; - if !translated { + if five_tuple_source(packet) == before { continue; } + let (source, sport) = before; assert!( packet.meta().is_src_natted(), - "{source} was translated without the source-natted mark, so a later stage \ - would translate it again" + "{source}:{sport} was translated without the source-natted mark, so a later \ + stage would translate it again" ); assert!( packet.meta().checksum_refresh(), - "{source} was translated without asking for a checksum refresh, so the packet \ - goes out with a checksum for an address it no longer carries" + "{source}:{sport} was translated without asking for a checksum refresh, so the \ + packet goes out with a checksum for headers it no longer carries" ); tally.reached.fetch_add(1, Ordering::Relaxed); } - }); + }, + ); tally.report("marking"); } + +#[test] +fn a_modified_packet_is_always_marked() { + drive_marking(Scenario::addresses(true)); +} + +#[test] +fn a_port_modified_packet_is_always_marked() { + drive_marking(Scenario::ports(true)); +} diff --git a/nat/src/static_nat/probe.rs b/nat/src/static_nat/probe.rs index ff6876eadf..ee6efeea70 100644 --- a/nat/src/static_nat/probe.rs +++ b/nat/src/static_nat/probe.rs @@ -39,7 +39,7 @@ use config::external::overlay::vpcpeering::VpcExpose; use config::external::overlay::vpcpeering::contract::{ LOCAL_VNI, REMOTE_VNI, overlay_with_exposes, }; -use lpm::prefix::PrefixWithOptionalPorts; +use lpm::prefix::{PortRange, PrefixWithOptionalPorts}; use net::buffer::TestBuffer; use net::ip::{NextHeader, UnicastIpAddr}; use net::packet::test_utils::{ @@ -64,14 +64,46 @@ pub(crate) fn vni(raw: u32) -> Vni { Vni::new_checked(raw).unwrap_or_else(|_| unreachable!("{raw} is a legal vni")) } -/// Every address a set of prefixes covers. +/// One address the configuration names, and the ports it names alongside it. +/// +/// Static NAT permits a port range on a prefix, and a prefix that carries one is mapped address and +/// port *together*: the private side's total, counted as addresses times ports, has to equal the +/// public side's, but the two may divide that total differently. So an address on its own is not a +/// thing the configuration maps -- the pair is -- and a probe has to carry the range it may draw a +/// port from or it will miss. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] +pub(crate) struct Endpoint { + pub(crate) addr: IpAddr, + /// The ports the prefix this address came from carries, if any. + pub(crate) ports: Option, +} + +impl Endpoint { + /// A port this endpoint is mapped on, chosen by an arbitrary index. + /// + /// Total, so a draw always lands on a port the configuration covers rather than near one. Port + /// 0 is not a legal port on either transport and no expose may name it. + pub(crate) fn port(&self, index: u16) -> u16 { + match self.ports { + None => index.max(1), + Some(range) => { + let len = u32::try_from(range.len()).unwrap_or(u32::from(u16::MAX)); + let offset = u32::from(index) % len.max(1); + u16::try_from(u32::from(range.start()) + offset).unwrap_or(range.end()) + } + } + } +} + +/// Every address-and-ports pair a set of prefixes covers. /// /// The static NAT generator keeps both sides of an expose small enough that this is a handful of -/// addresses, which is what lets a property enumerate rather than sample. -pub(crate) fn addresses(prefixes: &BTreeSet) -> Vec { +/// endpoints, which is what lets a property enumerate rather than sample. +pub(crate) fn endpoints(prefixes: &BTreeSet) -> Vec { let mut out = Vec::new(); - for prefix in prefixes { - let prefix = prefix.prefix(); + for prefix_with_ports in prefixes { + let ports = prefix_with_ports.ports(); + let prefix = prefix_with_ports.prefix(); let (start, end) = (prefix.as_address(), prefix.last_address()); let (mut bits, last) = match (start, end) { (IpAddr::V4(a), IpAddr::V4(b)) => (u128::from(a.to_bits()), u128::from(b.to_bits())), @@ -79,13 +111,16 @@ pub(crate) fn addresses(prefixes: &BTreeSet) -> Vec unreachable!("a prefix does not change address family"), }; while bits <= last { - out.push(match start { - IpAddr::V4(_) => IpAddr::V4( - u32::try_from(bits) - .unwrap_or_else(|_| unreachable!()) - .into(), - ), - IpAddr::V6(_) => IpAddr::V6(bits.into()), + out.push(Endpoint { + addr: match start { + IpAddr::V4(_) => IpAddr::V4( + u32::try_from(bits) + .unwrap_or_else(|_| unreachable!()) + .into(), + ), + IpAddr::V6(_) => IpAddr::V6(bits.into()), + }, + ports, }); bits += 1; } @@ -108,12 +143,18 @@ pub(crate) fn addresses(prefixes: &BTreeSet) -> Vec, - /// Every address the local exposes translate to. - pub(crate) public: Vec, + /// Every endpoint the local exposes offer, before translation. + pub(crate) private: Vec, + /// Every endpoint the local exposes translate to. + pub(crate) public: Vec, /// Addresses in the peer vpc, which no expose translates. pub(crate) peer: Vec, + /// Whether the exposes carry port ranges, so the mapping moves ports as well as addresses. + /// + /// The two paths differ in what a property may assert: with no port range the transport ports + /// are part of the frame and must survive untouched, and with one they are part of what is + /// being translated. + pub(crate) uses_ports: bool, } impl Fabric { @@ -123,19 +164,20 @@ impl Fabric { /// a time and two of them may overlap, which a manifest refuses. The properties count how often /// it happens so that a generator change that starts rejecting everything cannot pass quietly. pub(crate) fn build(exposes: &[VpcExpose]) -> Option { - let private: Vec = exposes.iter().flat_map(|e| addresses(&e.ips)).collect(); - let public: Vec = exposes + let private: Vec = exposes.iter().flat_map(|e| endpoints(&e.ips)).collect(); + let public: Vec = exposes .iter() .filter_map(|e| e.nat.as_ref()) - .flat_map(|nat| addresses(&nat.as_range)) + .flat_map(|nat| endpoints(&nat.as_range)) .collect(); + let uses_ports = private.iter().chain(&public).any(|e| e.ports.is_some()); let overlay = overlay_with_exposes(exposes.to_vec()).ok()?; let validated = overlay.validate().ok()?; let tables = build_nat_configuration(validated.vpc_table()).ok()?; // The peer prefix `overlay_with_exposes` fixes, in whichever family the exposes chose. - let peer = match private.first() { + let peer = match private.first().map(|e| e.addr) { Some(IpAddr::V6(_)) => vec![ "2001:db8:ffff::1" .parse() @@ -157,6 +199,7 @@ impl Fabric { private, public, peer, + uses_ports, }) } @@ -168,17 +211,34 @@ impl Fabric { StaticNat::with_reader("probe", self.writer.get_reader()) } - /// An outbound packet from `source` to the peer, with fixed ports. + /// An outbound packet from `source` on `port` to the peer. /// - /// For a property that wants to sweep every address the configuration offers rather than the - /// drawn ones -- injectivity, which is only visible across distinct inputs and so cannot be - /// left to a draw that may repeat. - pub(crate) fn outbound_to_peer(&self, source: IpAddr) -> Packet { - let mut packet = build(source, self.peer[0], false, 1024, 80); + /// For a property that wants to sweep everything the configuration offers rather than the drawn + /// ones -- injectivity, which is only visible across distinct inputs and so cannot be left to a + /// draw that may repeat. + pub(crate) fn outbound_to_peer(&self, source: Endpoint, port: u16) -> Packet { + let mut packet = build(source.addr, self.peer[0], false, port, 80); Arrival::outbound().stamp(&mut packet); packet } + /// Every distinct thing the configuration maps, as a source and a port to send it from. + /// + /// With no port range that is one entry per address. With one it is every address-and-port pair, + /// since the pair is what the mapping is one to one over -- sweeping addresses alone would check + /// a diagonal of the space and call it injective. + pub(crate) fn every_source(&self) -> Vec<(Endpoint, u16)> { + self.private + .iter() + .flat_map(|endpoint| match endpoint.ports { + None => vec![(*endpoint, 1024)], + Some(range) => (range.start()..=range.end()) + .map(|port| (*endpoint, port)) + .collect(), + }) + .collect() + } + /// Whether this fabric can be probed at all. /// /// An expose whose two sides are empty builds a table with nothing in it, and every probe @@ -333,16 +393,20 @@ impl Probe { /// The packet that answers this one, addressed to `translated`. /// /// The reply is what the peer would send back: the two ends swapped, and the local end named by - /// whatever the outbound translation produced rather than by the address the sender used. It - /// arrives at the peer's vpc, so it is looked up in the peer's table -- the other half of the - /// same expose, built independently. - pub(crate) fn reply(&self, translated: IpAddr) -> Packet { + /// whatever the outbound translation produced rather than by what the sender used. It arrives at + /// the peer's vpc, so it is looked up in the peer's table -- the other half of the same expose, + /// built independently. + /// + /// The port matters as much as the address once the expose carries port ranges: the peer + /// answers the port it was contacted *from*, which is the translated one, and a reply sent to + /// the original port would miss the mapping and prove nothing. + pub(crate) fn reply(&self, translated: IpAddr, translated_port: u16) -> Packet { let mut packet = build( self.destination, translated, self.tcp, self.dport, - self.sport, + translated_port, ); Arrival::inbound().stamp(&mut packet); packet @@ -364,14 +428,21 @@ impl ProbeSpec { /// that fails to become a packet and no rejection loop to bias the distribution. pub(crate) fn resolve(self, fabric: &Fabric) -> Probe { let mut arrival = Arrival::outbound(); - let mut source = fabric.private[self.source as usize % fabric.private.len()]; + let endpoint = fabric.private[self.source as usize % fabric.private.len()]; + let destination = fabric.peer[self.peer as usize % fabric.peer.len()]; + let mut source = endpoint.addr; + // Drawn from the range the endpoint's prefix carries, so a probe against a configuration + // that maps ports lands on one it maps rather than beside it. + let mut sport = endpoint.port(self.sport); let mut exposed = true; match self.stray { None => {} Some(Stray::SourceNotExposed) => { source = destination; + // The peer's prefix carries no port range, so no port is the right one either. + sport = self.sport.max(1); exposed = false; } Some(Stray::NoSourceVni) => arrival.src_vpcd = None, @@ -384,8 +455,8 @@ impl ProbeSpec { } } - // Port 0 is not a legal port on either transport, and the mapping is not about ports here. - let sport = self.sport.max(1); + // Port 0 is not a legal port on either transport. The destination is in the peer vpc, which + // no expose translates, so its port is free. let dport = self.dport.max(1); let mut packet = build(source, destination, self.tcp, sport, dport); arrival.stamp(&mut packet); From 1a749b416729d0c417e012af6134e2c47fbac2c0 Mon Sep 17 00:00:00 2001 From: Daniel Noland Date: Mon, 17 Aug 2026 17:46:28 -0600 Subject: [PATCH 6/7] test(nat): Drive masquerade with configuration-relative flows The second network function, and the first stateful one. Static NAT's answer for a packet is fixed by its tables; masquerade's is whatever the allocator handed out the first time it saw the flow, kept in the flow table and reused after. Every property here is really about that state being kept consistently, which is a different subject from anything the allocator's own tests can reach. ## A probe is a flow, not a packet The first packet of a flow allocates and writes a flow entry; the second finds that entry and reuses it. Different code, and the interesting properties relate the two. So `Probe::packet` hands back a fresh packet on every call rather than being consumed once, because sending the same flow twice is how the hot path is reached at all. ## The stage order is load-bearing, and getting it wrong made the harness lie `FlowLookup` attaches a flow entry only to a packet whose `dst_vpcd` is **absent**, and the flow filter that sets `dst_vpcd` runs *after* it. `Masquerade` then requires `dst_vpcd` to be present. So the annotation has to arrive between the two stages -- not before both, not after. The first version of this harness stamped both annotations up front, the way the static NAT one does. Nothing crashed. What happened instead is that no packet was ever given flow state, every packet took the allocation path, and a flow appeared to be re-allocated on each packet. Two properties failed and were right to: the harness was describing a pipeline that does not exist. That is the sharper form of the arrival-state point from the static NAT work. A network function's precondition is not always a stamp a test can apply in one go -- here part of it is supplied by a stage that must run *after* another stage that requires its absence, and no test that ignores the ordering describes the real thing. ## The three prerequisites, handled rather than assumed The design note lists what has to be true before a stateful stage can be compared at all: * **Seeded non-determinism** -- `set_randomize(false)`, or two fabrics built from one configuration disagree on every flow. * **Timers** -- rather than fake a clock, every property completes inside one flow lifetime, so none depends on expiry either happening or not. Expiry is a separate subject and wants the explicitly driven clock the note asks for, not a wall clock a property happens to outrun. * **Projections, not state** -- nothing here inspects the allocator or the flow table. Every assertion is over what came out of the pipeline. The properties also need a tokio runtime, since `FlowTable::insert` spawns a per-flow expiry timer. The existing tests get one from `#[tokio::test]`; a bolero body is synchronous, so it enters a runtime instead. ## The properties None predicts which address and port a flow will be given -- that is the allocator's business and predicting it would be a second copy of it. * **reversibility** -- the reply comes back to where the flow started. Unlike static NAT there is no second table built from the other side of the peering: the reverse translation exists only because the forward packet recorded it. A forward translation not faithfully recorded is a connection that never gets an answer. * **stability** -- a flow keeps the translation it was first given. A stage that re-allocated would produce a legal-looking packet every time, and the connection would break in a way no allocator-level test could see, because the two allocations are individually correct. * **exclusivity** -- two live flows never share a translation. Distinct source ports as well as addresses, since masquerade collapses many private addresses onto few public ones and the port is what keeps them apart after. * **containment** -- every translation lands inside a range the configuration named. The one property that consults the configuration, and legitimately: a membership test, not a prediction of which member. An address from outside the declared set is unroutable, so the flow is a blackhole that looks like success from inside the box. * **permission** and **attribution** -- as for static NAT. Permission matters more here, because a translation is not merely applied but *recorded*: a packet masqueraded without permission leaves an entry behind that keeps translating its successors. ## Break tested | break | fires | | --- | --- | | flow hot path disabled | stability, reversibility | | `requires_masquerade` ignored | permission | | allocation reported outside the declared range | containment, exclusivity | | allocation failure passed silently | attribution | Reversibility surviving the third of those is the correct answer rather than a gap: it asserts the reverse undoes the forward, which stays true when both use the same wrong address. ## Generator `MasqueradeExposes` gets the same treatment `StaticNatExposes` did, for the same two reasons -- `MasqueradeExpose` draws its base index freely, so two exposes collide whenever their index ranges intersect, and independent draws mix address families. One slot of four indices per expose, family drawn once. All six properties build 100% of the configurations they draw. The vacuity guard is a ratio rather than an absolute count, for the reason recorded with the static NAT properties: a count measures how fast the machine was, and fails under coverage instrumentation for reasons that have nothing to do with the code under test. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: Daniel Noland (cherry picked from commit 2491063c88c6c4ed0b1286a749a33b5e69295ae9) --- config/src/external/overlay/vpcpeering.rs | 80 +++- nat/src/masquerade/fuzz.rs | 480 ++++++++++++++++++++++ nat/src/masquerade/mod.rs | 2 + nat/src/masquerade/probe.rs | 332 +++++++++++++++ 4 files changed, 872 insertions(+), 22 deletions(-) create mode 100644 nat/src/masquerade/fuzz.rs create mode 100644 nat/src/masquerade/probe.rs diff --git a/config/src/external/overlay/vpcpeering.rs b/config/src/external/overlay/vpcpeering.rs index e65cb1d8b2..d8aae9f377 100644 --- a/config/src/external/overlay/vpcpeering.rs +++ b/config/src/external/overlay/vpcpeering.rs @@ -1136,37 +1136,73 @@ pub mod contract { #[derive(Debug, Clone, Copy, Default)] pub struct MasqueradeExpose; + /// Several masquerade exposes for one manifest, which a manifest will accept together. + /// + /// The same two problems [`StaticNatExposes`] solves, for the same reasons. [`MasqueradeExpose`] + /// draws its base index freely, so two of them collide whenever their index ranges intersect -- + /// which is often, since each covers up to three consecutive indices. Here each expose gets a + /// slot of [`MASQUERADE_SLOT`] indices, wider than the widest one can occupy, and the address + /// family is drawn once and shared. + #[derive(Debug, Clone, Copy)] + pub struct MasqueradeExposes(pub u8); + + impl Default for MasqueradeExposes { + fn default() -> Self { + Self(3) + } + } + + /// Indices reserved per expose. [`MasqueradeExpose`] uses at most three consecutive ones. + const MASQUERADE_SLOT: u8 = 4; + + impl ValueGenerator for MasqueradeExposes { + type Output = Vec; + + fn generate(&self, driver: &mut D) -> Option> { + let v4 = driver.produce::()?; + let count = driver.gen_u8(Included(&1), Included(&self.0.max(1)))?; + (0..count) + .map(|slot| masquerade_expose(driver, v4, slot.wrapping_mul(MASQUERADE_SLOT))) + .collect() + } + } + impl ValueGenerator for MasqueradeExpose { type Output = VpcExpose; fn generate(&self, driver: &mut D) -> Option { let v4 = driver.produce::()?; - let privates = driver.gen_u8(Included(&1), Included(&3))?; - let publics = driver.gen_u8(Included(&1), Included(&2))?; let base = driver.produce::()?; - let idle_timeout = match driver.gen_u8(Included(&0), Included(&2))? { - 0 => None, - 1 => Some(Duration::from_secs(30)), - _ => Some(Duration::from_mins(2)), - }; + masquerade_expose(driver, v4, base) + } + } + + /// One masquerade expose of the given family, from the given base index. + fn masquerade_expose(driver: &mut D, v4: bool, base: u8) -> Option { + let privates = driver.gen_u8(Included(&1), Included(&3))?; + let publics = driver.gen_u8(Included(&1), Included(&2))?; + let idle_timeout = match driver.gen_u8(Included(&0), Included(&2))? { + 0 => None, + 1 => Some(Duration::from_secs(30)), + _ => Some(Duration::from_mins(2)), + }; - let mut expose = VpcExpose::empty().make_masquerade(idle_timeout).ok()?; - for index in 0..privates { - expose = expose.ip(PrefixWithOptionalPorts::new( - block(v4, Side::Private, base.wrapping_add(index))?, + let mut expose = VpcExpose::empty().make_masquerade(idle_timeout).ok()?; + for index in 0..privates { + expose = expose.ip(PrefixWithOptionalPorts::new( + block(v4, Side::Private, base.wrapping_add(index))?, + None, + )); + } + for index in 0..publics { + expose = expose + .as_range(PrefixWithOptionalPorts::new( + block(v4, Side::Public, base.wrapping_add(index))?, None, - )); - } - for index in 0..publics { - expose = expose - .as_range(PrefixWithOptionalPorts::new( - block(v4, Side::Public, base.wrapping_add(index))?, - None, - )) - .ok()?; - } - Some(expose) + )) + .ok()?; } + Some(expose) } #[derive(Clone, Copy)] diff --git a/nat/src/masquerade/fuzz.rs b/nat/src/masquerade/fuzz.rs new file mode 100644 index 0000000000..d35e7c447c --- /dev/null +++ b/nat/src/masquerade/fuzz.rs @@ -0,0 +1,480 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! Properties of the masquerade network function, driven by generated configurations and packets. +//! +//! `static_nat::fuzz` covers a stage that is a pure function of its configuration. This one is not: +//! masquerade's answer for a flow is whatever the allocator handed out the first time it saw it, +//! and every property here is really about that state being kept consistently. +//! +//! # What can be asserted without an oracle +//! +//! Nothing here predicts which address and port a flow will be given -- that is the allocator's +//! business and predicting it would be a second copy of it. What can be said is how the answers +//! relate to each other and to the configuration: +//! +//! * the reply to a translated flow comes back to where the flow started (**reversibility**); +//! * the same flow gets the same answer every time (**stability**); +//! * two flows never get the same answer at once (**exclusivity**); +//! * every answer is inside a range the configuration named (**containment**). +//! +//! Containment is the one that consults the configuration, and legitimately: it is a statement that +//! the output is a member of a declared set, not a prediction of which member. An allocator handing +//! out an address nobody gave it is the failure that check exists for. +//! +//! # No timers +//! +//! Every property completes within one flow lifetime, so none depends on expiry either happening or +//! not. Expiry is a separate subject and needs the explicitly driven clock the development guide +//! asks for, rather than a wall clock a property happens to outrun. + +#![cfg(test)] + +use crate::masquerade::probe::{Arrival, Fabric, ProbeSpec, Stray, run}; +use bolero::{Driver, TypeGenerator, ValueGenerator}; +use concurrency::sync::atomic::{AtomicUsize, Ordering}; +use config::external::overlay::vpcpeering::VpcExpose; +use config::external::overlay::vpcpeering::contract::MasqueradeExposes; +use net::buffer::TestBuffer; +use net::packet::Packet; +use std::collections::BTreeMap; +use std::net::IpAddr; +use std::num::NonZero; + +/// Exposes per configuration. +const MAX_EXPOSES: u8 = 3; + +/// The fewest reaching draws any property may see before it is considered vacuous. +const MIN_REACHED: usize = 8; + +/// Flows per configuration. +const PROBES: usize = 8; + +/// A configuration and a batch of flows to put through it. +#[derive(Debug, Clone, Copy)] +struct Scenario { + strays: bool, +} + +impl ValueGenerator for Scenario { + type Output = (Vec, Vec); + + fn generate(&self, driver: &mut D) -> Option { + let exposes = MasqueradeExposes(MAX_EXPOSES).generate(driver)?; + + let mut probes = Vec::with_capacity(PROBES); + for _ in 0..PROBES { + let mut probe = ProbeSpec::generate(driver)?; + if !self.strays { + probe.clear_stray(); + } + probes.push(probe); + } + Some((exposes, probes)) + } +} + +/// Run a property inside a tokio runtime. +/// +/// `FlowTable::insert` spawns a per-flow expiry timer, so an insert outside a runtime context +/// panics. The existing masquerade tests get one from `#[tokio::test]`; a bolero property's body is +/// synchronous, so it enters a runtime rather than becoming async. +/// +/// A current-thread runtime with time enabled, and nothing ever awaits it: the timers exist so that +/// spawning them succeeds, and every property here finishes well inside the shortest flow timeout. +fn with_runtime(body: impl FnOnce()) { + let runtime = tokio::runtime::Builder::new_current_thread() + .enable_time() + .build() + .unwrap_or_else(|e| unreachable!("{e}")); + let _guard = runtime.enter(); + body(); +} + +fn fabric(exposes: &[VpcExpose]) -> Option { + let fabric = Fabric::build(exposes)?; + fabric.is_probeable().then_some(fabric) +} + +/// The source half of a packet's five-tuple. +fn source_of(packet: &Packet) -> (IpAddr, u16) { + ( + packet + .ip_source() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")), + packet.transport_src_port().map_or(0, NonZero::get), + ) +} + +/// The destination half. +fn destination_of(packet: &Packet) -> (IpAddr, u16) { + ( + packet + .ip_destination() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")), + packet.transport_dst_port().map_or(0, NonZero::get), + ) +} + +/// How much of a run actually reached the code under test. +#[derive(Default)] +struct Tally { + seen: AtomicUsize, + built: AtomicUsize, + reached: AtomicUsize, +} + +impl Tally { + /// Assert the run was not vacuous. + /// + /// The floor is **relative to the configurations actually built**, not an absolute count, because + /// an absolute one is really a measure of how fast the machine was. A property that reached + /// thousands of flows alone can reach a few dozen when it runs beside nine hundred other + /// tests on a loaded machine or under coverage instrumentation, and a floor tuned to the fast + /// case then fails for a reason that has nothing to do with the code under test. + /// + /// Both counts scale with the iteration budget, so their ratio does not. What the guard is for is + /// a property that has stopped reaching its assertion at all -- and a collapse to zero is just as + /// visible in the ratio. + fn report(&self, what: &str) { + let (seen, built, reached) = ( + self.seen.load(Ordering::Relaxed), + self.built.load(Ordering::Relaxed), + self.reached.load(Ordering::Relaxed), + ); + println!("{what}: {built}/{seen} configurations built, {reached} flows reached it"); + assert!( + built * 2 >= seen, + "only {built} of {seen} configurations built, so this checked much less than it looks \ + like it did" + ); + // At least one reaching flows for every two configurations built, and never zero. + assert!( + reached >= MIN_REACHED && reached * 2 >= built, + "{reached} flows reached the {what} assertion across {built} configurations; \ + this property has gone vacuous" + ); + } +} + +/// The reply to a masqueraded flow comes back to where the flow started. +/// +/// The stateful analogue of static NAT's round trip, and it works quite differently. There is no +/// second table built from the other side of the peering: the reverse translation exists only +/// because the forward packet created a flow entry holding it, `FlowLookup` finds that entry, and +/// `Masquerade` applies it. +/// +/// So this is a statement about state rather than about configuration -- whatever the allocator +/// chose, the entry it wrote down has to describe the inverse of what was done to the packet. A +/// forward translation that is not faithfully recorded is a connection that never gets an answer, +/// which is the characteristic masquerade failure and is invisible to any test of the allocator on +/// its own. +#[test] +fn a_masqueraded_flow_comes_back() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + let before = (probe.source, probe.sport); + let out = run( + &mut lookup, + &mut masq, + vec![probe.packet()], + probe.arrival.dst_vpcd, + ); + let after = source_of(&out[0]); + if after == before || out[0].is_done() { + continue; + } + + let back = run( + &mut lookup, + &mut masq, + vec![probe.reply(after.0, after.1)], + Arrival::inbound().dst_vpcd, + ); + assert_eq!( + destination_of(&back[0]), + before, + "{:?} was masqueraded to {after:?}, and the reply came back to {:?}", + before, + destination_of(&back[0]) + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("reversibility"); +} + +/// A flow keeps the translation it was first given. +/// +/// The second packet of a flow takes a different path from the first: the first allocates and +/// writes a flow entry, the second finds that entry and reuses it. A stage that allocated again +/// would still produce a legal-looking packet, and the connection would break in a way nothing at +/// the allocator level could see -- the two allocations are individually correct. +#[test] +fn a_flow_keeps_its_translation() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + let before = (probe.source, probe.sport); + let first = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + if out_unchanged(&first, before) { + continue; + } + let second = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + + assert_eq!( + source_of(&second[0]), + source_of(&first[0]), + "the same flow from {before:?} was given {:?} and then {:?}, so its reply can \ + only reach one of them", + source_of(&first[0]), + source_of(&second[0]) + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("stability"); +} + +/// Whether a batch's first packet came out as it went in. +fn out_unchanged(out: &[Packet], before: (IpAddr, u16)) -> bool { + out[0].is_done() || source_of(&out[0]) == before +} + +/// Two live flows never share a translation. +/// +/// The exclusivity claim the allocator exists to keep, stated where it matters: at the stage, over +/// packets, with the flow table in the loop. Two flows sharing an address and port are +/// indistinguishable on the way back, so one of them receives the other's traffic -- a tenant +/// isolation failure rather than a routing one. +/// +/// Distinct source *ports* as well as addresses, since masquerade puts many private addresses behind +/// few public ones and the port is what keeps them apart once the addresses have collapsed. +#[test] +fn distinct_flows_do_not_share_a_translation() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + let mut taken: BTreeMap<(IpAddr, u16), (IpAddr, u16)> = BTreeMap::new(); + for (index, spec) in probes.iter().enumerate() { + let mut probe = (*spec).resolve(&fabric); + // A distinct port per probe, so that repeated draws are still distinct flows and + // the property is about contention rather than about the draw. + probe.sport = u16::try_from(1024 + index).unwrap_or(1024); + let before = (probe.source, probe.sport); + let out = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + if out_unchanged(&out, before) { + continue; + } + let after = source_of(&out[0]); + + if let Some(previous) = taken.insert(after, before) { + assert_eq!( + previous, before, + "flows from {previous:?} and {before:?} were both masqueraded to {after:?}, \ + so a reply can only reach one of them" + ); + } + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("exclusivity"); +} + +/// Every translation lands inside a range the configuration named. +/// +/// The containment claim, and the one place a property here looks at the configuration. It is a +/// membership test rather than a prediction: which public address a flow gets is the allocator's +/// business, but *some* public address the operator declared is not negotiable. +/// +/// An address from outside the declared set is not merely wrong, it is unroutable -- the fabric has +/// no path back to it, so the flow is a blackhole that looks like a successful translation from +/// inside the box. +#[test] +fn a_translation_stays_inside_the_public_range() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + let before = (probe.source, probe.sport); + let out = run( + &mut lookup, + &mut masq, + vec![probe.packet()], + probe.arrival.dst_vpcd, + ); + if out_unchanged(&out, before) { + continue; + } + let (addr, port) = source_of(&out[0]); + + assert!( + fabric.is_public(addr), + "{before:?} was masqueraded to {addr}:{port}, which no expose offers; the \ + fabric has no route back to it" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("containment"); +} + +/// Nothing is masqueraded that did not ask to be. +/// +/// The same precondition claim as static NAT's, over masquerade's own flags. Getting this wrong is +/// worse here than there, because a translation is not just applied but *recorded*: a packet +/// masqueraded without permission leaves a flow entry behind that will keep translating its +/// successors long after the mistaken packet is gone. +#[test] +fn nothing_is_masqueraded_without_permission() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: true }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + if probe.asks_for_translation() && probe.exposed { + continue; + } + let before = (probe.source, probe.sport); + let (stray, arrival) = (probe.stray, probe.arrival); + let out = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + + // A dropped packet is a legitimate answer for a flow the configuration cannot + // place; what is not legitimate is translating it. + if out[0].is_done() { + tally.reached.fetch_add(1, Ordering::Relaxed); + continue; + } + assert_eq!( + source_of(&out[0]), + before, + "masquerade translated {before:?} although {stray:?} forbade it; the packet \ + arrived as {arrival:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("permission"); +} + +/// A flow that cannot be masqueraded is dropped, and says why. +/// +/// Same obligation as everywhere else, and masquerade has an unusually rich failure vocabulary -- +/// no allocator, allocation refused, capacity exceeded, unsupported protocol -- so the assertion is +/// that *some* reason is attached rather than which. What it rules out is the silent pass, which +/// here means letting a private address out onto the fabric untranslated. +#[test] +fn a_flow_that_cannot_be_masqueraded_says_so() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: true }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + // The flows the configuration genuinely cannot place: a source it never named, or a + // vpc pair it has no allocator for. Masquerade must not simply forward these. + let unplaceable = matches!( + probe.stray, + Some(Stray::SourceNotExposed | Stray::UnknownSourceVni | Stray::UnknownDestVni) + ); + if !unplaceable { + continue; + } + let before = (probe.source, probe.sport); + let stray = probe.stray; + let out = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + let packet = &out[0]; + + assert!( + packet.is_done(), + "a flow from {before:?} with {stray:?} passed masquerade with no verdict, so \ + a private address reaches the fabric untranslated" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("attribution"); +} diff --git a/nat/src/masquerade/mod.rs b/nat/src/masquerade/mod.rs index d7b2861dba..5e149bb06f 100644 --- a/nat/src/masquerade/mod.rs +++ b/nat/src/masquerade/mod.rs @@ -5,10 +5,12 @@ pub(crate) mod allocation; mod allocator_writer; pub mod apalloc; pub(crate) mod flows; +mod fuzz; pub(crate) mod icmp_handling; mod natip; mod nf; mod packet; +mod probe; mod protocol; mod state; mod test; diff --git a/nat/src/masquerade/probe.rs b/nat/src/masquerade/probe.rs new file mode 100644 index 0000000000..4d05b328ac --- /dev/null +++ b/nat/src/masquerade/probe.rs @@ -0,0 +1,332 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! Packets drawn relative to a masquerade configuration. +//! +//! The same shape as `static_nat::probe` -- a [`ProbeSpec`] of bare indices, resolved against a +//! built [`Fabric`] -- and the same reason for it. What differs is everything that follows from +//! masquerade being **stateful**, and that difference is the whole point of doing it second. +//! +//! # Static NAT is a function of its configuration; masquerade is not +//! +//! Static NAT's answer for a packet is fixed by the tables. Masquerade's is whatever the allocator +//! handed out the first time it saw the flow, kept in the flow table and reused thereafter. So: +//! +//! * **A probe is a flow, not a packet.** The first packet of a flow takes the allocation path; the +//! second takes the hot path through `flow_info`. They are different code and the interesting +//! properties relate them. +//! * **The reply needs a stage in front.** `Masquerade` recovers the reverse translation from +//! `flow_info`, which `FlowLookup` attaches, and only when `dst_vpcd` is absent. So the harness +//! runs two stages, and the reply arrives with the annotation deliberately left off. +//! * **Order matters.** Two runs of the same batch against the same fabric are not required to +//! agree, because the first left allocations behind. Every property here either states something +//! about one run or builds a fresh fabric. +//! +//! # The three prerequisites +//! +//! The development guide lists what has to be true before a stateful stage can be compared at all, +//! and all three are handled here rather than assumed: +//! +//! 1. **Seeded non-determinism.** `apply_masquerade_config` randomizes port selection, so two +//! fabrics allocate differently for the same flow. [`Fabric::build`] sets `set_randomize(false)`. +//! 2. **Timers.** Flow entries expire on a wall clock the harness does not drive. Rather than fake +//! it, every property here is written to complete within one flow lifetime -- the shortest +//! masquerade timeout is five seconds and a probe is a handful of packets -- so no property +//! depends on expiry either happening or not. Expiry is a separate subject and wants the +//! explicit clock the guide asks for. +//! 3. **Projections, not state.** Nothing here inspects the allocator or the flow table. Every +//! assertion is over what came out of the pipeline. + +#![cfg(test)] + +use crate::masquerade::{MasqueradeConfig, NatAllocatorWriter}; +use bolero::TypeGenerator; +use concurrency::sync::Arc; +use config::external::overlay::vpcpeering::VpcExpose; +use config::external::overlay::vpcpeering::contract::{ + LOCAL_VNI, REMOTE_VNI, overlay_with_exposes, +}; +use flow_entry::flow_table::{FlowLookup, FlowTable}; +use lpm::prefix::Prefix; +use net::buffer::TestBuffer; +use net::packet::{Packet, VpcDiscriminant}; +use net::vxlan::Vni; +use pipeline::NetworkFunction; +use std::net::IpAddr; + +use crate::Masquerade; +use crate::static_nat::probe::{build, vni}; + +/// Flow table capacity. Large enough that no property here can exhaust it, so a translation failure +/// is never the table being full. +const FLOW_CAPACITY: usize = 4096; + +/// A VNI no generated configuration uses. +const ABSENT_VNI: u32 = 4_000; + +/// A built masquerade configuration, and the addresses it declares. +pub(crate) struct Fabric { + flow_table: Arc, + allocator: NatAllocatorWriter, + /// Every address the local exposes offer. + pub(crate) private: Vec, + /// The prefixes translations must land inside. + pub(crate) public: Vec, + /// Addresses in the peer vpc. + pub(crate) peer: Vec, +} + +impl Fabric { + /// Build the allocator a set of exposes implies, or `None` if the overlay is not valid. + pub(crate) fn build(exposes: &[VpcExpose]) -> Option { + let overlay = overlay_with_exposes(exposes.to_vec()).ok()?; + let validated = overlay.validate().ok()?; + + // Only the first address of each private prefix: masquerade puts many private addresses + // behind few public ones, so the prefixes are /24s and enumerating them would be tens of + // thousands of probes for no new behaviour. What matters is that distinct sources contend + // for the same public range, and a handful of them does that. + let private: Vec = exposes + .iter() + .flat_map(|e| e.ips.iter().map(|p| p.prefix().as_address())) + .collect(); + let public: Vec = exposes + .iter() + .filter_map(|e| e.nat.as_ref()) + .flat_map(|nat| { + nat.as_range + .iter() + .map(lpm::prefix::PrefixWithOptionalPorts::prefix) + }) + .collect(); + + let peer = match private.first() { + Some(IpAddr::V6(_)) => vec![ + "2001:db8:ffff::1" + .parse() + .unwrap_or_else(|_| unreachable!()), + "2001:db8:ffff::2" + .parse() + .unwrap_or_else(|_| unreachable!()), + ], + _ => vec![ + "3.3.3.1".parse().unwrap_or_else(|_| unreachable!()), + "3.3.3.2".parse().unwrap_or_else(|_| unreachable!()), + ], + }; + + let flow_table = Arc::new(FlowTable::new(FLOW_CAPACITY)); + let mut allocator = NatAllocatorWriter::new(); + // Randomized port selection would make two fabrics built from one configuration disagree on + // every flow, which is legitimate behaviour and useless to compare. + let config = MasqueradeConfig::new(validated.vpc_table()).set_randomize(false); + allocator.update_nat_allocator(config, 1, &flow_table); + + Some(Self { + flow_table, + allocator, + private, + public, + peer, + }) + } + + /// The two stages a masqueraded packet passes through. + /// + /// `FlowLookup` first, because it is what turns a reply into something `Masquerade` can + /// recognise: the reverse translation lives in the flow entry the forward packet created, and + /// nothing else puts it on the packet. + pub(crate) fn stages(&self) -> (FlowLookup, Masquerade) { + ( + FlowLookup::new("flow-lookup", self.flow_table.clone()), + Masquerade::new( + "masquerade", + self.flow_table.clone(), + self.allocator.get_reader(), + ), + ) + } + + /// Whether this fabric can be probed at all. + pub(crate) fn is_probeable(&self) -> bool { + !self.private.is_empty() && !self.public.is_empty() + } + + /// Whether `addr` is inside one of the public prefixes the configuration named. + pub(crate) fn is_public(&self, addr: IpAddr) -> bool { + self.public.iter().any(|p| p.covers_addr(&addr)) + } +} + +/// Put a batch through the stages, in the order the real pipeline uses. +/// +/// **The order is the whole point, and getting it wrong makes the harness lie.** `FlowLookup` +/// attaches a flow entry only to a packet whose `dst_vpcd` is *absent*, and the flow filter that +/// sets `dst_vpcd` runs after it. So a harness that stamps both annotations up front never attaches +/// any flow state, every packet takes the allocation path, and a flow appears to be re-allocated on +/// every packet -- which is what this harness did until it was corrected. +/// +/// `Masquerade` then requires `dst_vpcd` to be present, so the annotation genuinely has to arrive +/// between the two stages rather than before or after both. That is the flow filter's job in +/// production and `TestFlowFilter`'s in the existing tests; here it is one assignment, which is all +/// of it that matters to masquerade. +pub(crate) fn run( + lookup: &mut FlowLookup, + masq: &mut Masquerade, + packets: Vec>, + dst_vpcd: Option, +) -> Vec> { + let mut looked: Vec<_> = lookup.process(packets.into_iter()).collect(); + for packet in &mut looked { + packet.meta_mut().dst_vpcd = dst_vpcd.map(VpcDiscriminant::from_vni); + } + masq.process(looked.into_iter()).collect() +} + +/// The metadata a packet must carry for [`Masquerade`] to look at it. +/// +/// Split in two on purpose. Everything here except `dst_vpcd` is set before the flow lookup; +/// `dst_vpcd` is set between the lookup and masquerade, because the lookup refuses to attach flow +/// state to a packet that already carries it. See [`run`]. +#[derive(Debug, Clone, Copy)] +pub(crate) struct Arrival { + pub(crate) src_vpcd: Option, + /// Supplied *after* the flow lookup, by [`run`], standing in for the flow filter. + pub(crate) dst_vpcd: Option, + pub(crate) wants_masquerade: bool, +} + +impl Arrival { + /// The first packet of a flow leaving the local vpc. + pub(crate) fn outbound() -> Self { + Self { + src_vpcd: Some(vni(LOCAL_VNI)), + dst_vpcd: Some(vni(REMOTE_VNI)), + wants_masquerade: true, + } + } + + /// The reply, arriving from the peer. The flow filter resolves its destination back to the + /// local vpc from the flow entry, which is what [`run`] stands in for. + pub(crate) fn inbound() -> Self { + Self { + src_vpcd: Some(vni(REMOTE_VNI)), + dst_vpcd: Some(vni(LOCAL_VNI)), + wants_masquerade: true, + } + } + + /// Everything an upstream stage sets *before* the flow lookup. + pub(crate) fn stamp(self, packet: &mut Packet) { + let meta = packet.meta_mut(); + meta.src_vpcd = self.src_vpcd.map(VpcDiscriminant::from_vni); + meta.set_overlay(true); + meta.set_keep(true); + meta.set_masquerade(self.wants_masquerade); + } +} + +/// A deliberate deviation from a flow the configuration masquerades. +#[derive(Debug, Clone, Copy, TypeGenerator)] +pub(crate) enum Stray { + /// A source address no expose offers, which the allocator has no range for. + SourceNotExposed, + /// A source vpc with no allocator entry of its own. + UnknownSourceVni, + /// A destination vpc the local vpc does not peer with. + UnknownDestVni, + /// Nothing asked for masquerade, so the stage should pass the packet through untouched. + NotAskedFor, +} + +/// A drawn probe, before it knows anything about a configuration. +#[derive(Debug, Clone, Copy, TypeGenerator)] +pub(crate) struct ProbeSpec { + source: u8, + peer: u8, + /// UDP throughout. TCP is refused unless the packet is a first segment, which is a separate + /// question from the mapping and would only add a rejection path to every property here. + sport: u16, + dport: u16, + stray: Option, +} + +/// A probe resolved against a fabric. +pub(crate) struct Probe { + pub(crate) source: IpAddr, + pub(crate) destination: IpAddr, + pub(crate) sport: u16, + pub(crate) dport: u16, + pub(crate) exposed: bool, + pub(crate) arrival: Arrival, + pub(crate) stray: Option, +} + +impl Probe { + /// Whether masquerade was asked to translate this flow and given what it needs to. + pub(crate) fn asks_for_translation(&self) -> bool { + self.arrival.wants_masquerade + && self.arrival.src_vpcd == Some(vni(LOCAL_VNI)) + && self.arrival.dst_vpcd == Some(vni(REMOTE_VNI)) + } + + /// The outbound packet, which may be built more than once. + /// + /// Unlike the static NAT probe this hands back a fresh packet each time on purpose: sending the + /// same flow twice is how the hot path is reached, and a property that wants to compare the two + /// needs both. + pub(crate) fn packet(&self) -> Packet { + let mut packet = build(self.source, self.destination, false, self.sport, self.dport); + self.arrival.stamp(&mut packet); + packet + } + + /// The reply to a flow that was translated to `translated`. + pub(crate) fn reply(&self, translated: IpAddr, translated_port: u16) -> Packet { + let mut packet = build( + self.destination, + translated, + false, + self.dport, + translated_port, + ); + Arrival::inbound().stamp(&mut packet); + packet + } +} + +impl ProbeSpec { + /// Drop the deviation, leaving a flow the configuration is meant to masquerade. + pub(crate) fn clear_stray(&mut self) { + self.stray = None; + } + + /// Interpret this draw against a fabric. + pub(crate) fn resolve(self, fabric: &Fabric) -> Probe { + let mut arrival = Arrival::outbound(); + let mut source = fabric.private[self.source as usize % fabric.private.len()]; + let destination = fabric.peer[self.peer as usize % fabric.peer.len()]; + let mut exposed = true; + + match self.stray { + None => {} + Some(Stray::SourceNotExposed) => { + source = destination; + exposed = false; + } + Some(Stray::UnknownSourceVni) => arrival.src_vpcd = Some(vni(ABSENT_VNI)), + Some(Stray::UnknownDestVni) => arrival.dst_vpcd = Some(vni(ABSENT_VNI)), + Some(Stray::NotAskedFor) => arrival.wants_masquerade = false, + } + + Probe { + source, + destination, + sport: self.sport.max(1), + dport: self.dport.max(1), + exposed, + arrival, + stray: self.stray, + } + } +} From 101795990a7ee713693fb973fd984c3980e3f28d Mon Sep 17 00:00:00 2001 From: Daniel Noland Date: Mon, 17 Aug 2026 17:50:45 -0600 Subject: [PATCH 7/7] test(acl): Carry the acl properties from the lookup to the network function `acl-filter/src/fuzz.rs` has the strongest oracle in this codebase: it evaluates the validated configuration directly and compares that against the lowered tables, so a lowering mistake cannot hide behind the thing it produced. What it never touches is a packet. Every probe there is a `PacketSummary` handed straight to `lookup`. Two pieces of production code sit between a packet and that summary, and neither had any coverage from a generated configuration: * **`PacketSummary::try_from`**, which reads the five-tuple and both discriminants out of the headers; and * **`AclFilter::process_packet`**, which turns a verdict into a fate -- `DoneReason::AclDropped`, `invalidate_flows`, and the `is_overlay` gate deciding whether any of it happens. This re-points the existing generators rather than writing new ones. The `OverlaySpec` and `ProbeSpec` are unchanged; a probe now becomes a packet and the answer is read off the packet's fate. The oracle is the same `oracle_resolved_action`, asked the same question, so this is a differential test over the packet path rather than a second ACL. ## The gap was real, and the break test shows exactly how big Misread one field -- take the source address from where the destination lives: ```rust let src_ip = net.dst_addr(); let dst_ip = net.dst_addr(); ``` **All five pre-existing `fuzz::` properties pass.** They never build the packet that is misread, so there is nothing for them to see. Both new properties fail. That is the whole argument for this change, demonstrated rather than asserted. ## The properties * **stage verdict** -- a packet the configuration denies is dropped with `AclDropped`; one it allows survives untouched. This tests the extraction implicitly: a field read from the wrong place makes the stage judge a different tuple from the one the oracle judged, and they disagree wherever that field decides the answer. * **summary round trip** -- the five-tuple read back is the one the packet was built with. Direct rather than implicit, so it also catches the misread that happens to be harmless for the ruleset drawn. * **missing discriminant** -- a packet naming no destination vpc is refused as `Unroutable`. An ACL is indexed by the vpc pair, so such a packet cannot be judged at all, and letting it through applies no policy whatsoever. * **underlay gate** -- traffic that is not overlay traffic is left alone. No ACL in the configuration describes it. Break tested: dropping the `done(AclDropped)` fires the stage verdict; the misread above fires both it and the round trip; removing the `is_overlay` gate fires the underlay property. Each leaves the others green. ## Scope Only TCP and UDP become packets. A probe drawing ICMP or an arbitrary next header is counted and skipped rather than approximated, because a packet whose headers did not match the summary it came from would make every disagreement meaningless. The same goes for the generator's `CrossVersion` stray, which asks for a v4 source with a v6 destination -- there is no such packet, and that case stays with the summary-level properties where it belongs. The vacuity guard here counts denials as well as arrivals: a run that only ever saw permits would pass while the drop path -- the only path where the stage does anything -- went entirely unexercised. Around a quarter of probes are denied in practice. The vacuity guard is a ratio rather than an absolute count, for the reason recorded with the static NAT properties: a count measures how fast the machine was, and fails under coverage instrumentation for reasons that have nothing to do with the code under test. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: Daniel Noland (cherry picked from commit e73a570ad2dae8fa54818879657b1dd5de3dc3d1) --- acl-filter/src/fuzz.rs | 16 ++ acl-filter/src/lib.rs | 2 + acl-filter/src/nf_fuzz.rs | 342 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 360 insertions(+) create mode 100644 acl-filter/src/nf_fuzz.rs diff --git a/acl-filter/src/fuzz.rs b/acl-filter/src/fuzz.rs index 156fbe82c9..04fc51239a 100644 --- a/acl-filter/src/fuzz.rs +++ b/acl-filter/src/fuzz.rs @@ -127,6 +127,22 @@ fn resolved_action(rule: Option, default: Option) -> A rule.map_or_else(|| default.unwrap_or(AclAction::Allow), |v| v.action) } +/// The action the configuration alone says applies to a packet. +/// +/// The three steps above composed: first matching rule, else the peering's default, else allow. +/// Exported for `nf_fuzz`, which asks the same oracle the same question about a real packet -- so +/// that the network function is compared against this oracle rather than against a second copy of +/// it. +pub(crate) fn oracle_resolved_action( + overlay: &ValidatedOverlay, + packet: &PacketSummary, +) -> AclAction { + resolved_action( + oracle_lookup(overlay, packet), + oracle_default_action(overlay, packet.src_vni, packet.dst_vni), + ) +} + // ------------------------------------------------------------------------------------------------- // Properties. diff --git a/acl-filter/src/lib.rs b/acl-filter/src/lib.rs index 3e17f71453..d4fe2c6f40 100644 --- a/acl-filter/src/lib.rs +++ b/acl-filter/src/lib.rs @@ -26,6 +26,8 @@ mod fuzz; #[cfg(test)] mod fuzz_gen; #[cfg(test)] +mod nf_fuzz; +#[cfg(test)] mod tests; pub use access::{ diff --git a/acl-filter/src/nf_fuzz.rs b/acl-filter/src/nf_fuzz.rs new file mode 100644 index 0000000000..3e5b7ddd0a --- /dev/null +++ b/acl-filter/src/nf_fuzz.rs @@ -0,0 +1,342 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! The ACL properties, carried from the lookup to the network function. +//! +//! `fuzz.rs` already has the strongest oracle in this codebase: it evaluates the validated +//! configuration directly and compares that against the lowered tables, so a lowering mistake cannot +//! hide behind the thing it produced. What it does not touch is a packet. Every probe there is a +//! [`PacketSummary`] handed straight to `lookup`. +//! +//! Two pieces of production code sit between a packet and that summary, and neither had any +//! coverage from a generated configuration: +//! +//! * **`PacketSummary::try_from`**, which reads the five-tuple and the two discriminants out of the +//! headers. A summary is six fields, and a stage that read the destination where the source +//! belongs would pass every property in `fuzz.rs` -- they never build the packet it misreads. +//! * **`AclFilter::process_packet`**, which turns a verdict into a fate: `DoneReason::AclDropped`, +//! `invalidate_flows`, and the `is_overlay` gate deciding whether any of it happens. +//! +//! So this module re-points the existing generators rather than writing new ones. The +//! [`OverlaySpec`] and [`ProbeSpec`] are the same; what differs is that a probe becomes a packet and +//! the answer is read off the packet's fate rather than returned from a function. +//! +//! # Why the verdict is still not predicted here +//! +//! `oracle_verdict` is the config-semantics oracle from `fuzz.rs`, unchanged. This module does not +//! reimplement it -- it asks the same oracle the same question and checks that the *stage* agrees, +//! which makes this a differential test over the packet path rather than a second ACL. + +#![cfg(test)] + +use crate::fuzz::oracle_resolved_action; +use crate::fuzz_gen::{OverlaySpec, ProbeSpec}; +use crate::{AclFilter, AclFilterContext, AclFilterContextWriter, PacketSummary}; +use concurrency::sync::atomic::{AtomicUsize, Ordering}; +use config::external::overlay::acl::AclAction; +use net::buffer::TestBuffer; +use net::ip::{NextHeader, UnicastIpAddr}; +use net::packet::test_utils::{ + build_test_ipv4_packet_with_transport, build_test_ipv6_packet_with_transport, +}; +use net::packet::{DoneReason, Packet, VpcDiscriminant}; +use net::tcp::port::TcpPort; +use net::udp::UdpPort; +use pipeline::NetworkFunction; +use std::net::IpAddr; + +/// The fewest arriving probes any property may see before it is considered vacuous. +const MIN_REACHED: usize = 8; + +/// Probes per configuration. +const PROBES: usize = 8; + +/// Build a packet carrying a summary's five-tuple and discriminants. +/// +/// Returns `None` for a protocol with no port builder. TCP and UDP are what carry ports and so what +/// the port half of every ACL rule is about; a probe drawing ICMP or an arbitrary next header is +/// counted and skipped rather than approximated, since a packet whose headers do not match the +/// summary it came from would make every disagreement below meaningless. +fn packet_for(summary: &PacketSummary) -> Option> { + let (sport, dport) = summary.ports?; + let tcp = match summary.proto { + NextHeader::TCP => true, + NextHeader::UDP => false, + _ => return None, + }; + + let mut packet = match (summary.src_ip, summary.dst_ip) { + (IpAddr::V4(_), IpAddr::V4(_)) => { + build_test_ipv4_packet_with_transport(64, Some(summary.proto)).ok()? + } + (IpAddr::V6(_), IpAddr::V6(_)) => { + build_test_ipv6_packet_with_transport(64, Some(summary.proto)).ok()? + } + // The generator's `CrossVersion` stray produces these on purpose. There is no such packet + // to build, so the case belongs to the summary-level properties. + _ => return None, + }; + + packet + .set_ip_source(UnicastIpAddr::try_from(summary.src_ip).ok()?) + .ok()?; + packet.set_ip_destination(summary.dst_ip).ok()?; + if tcp { + packet + .set_tcp_source_port(TcpPort::new_checked(sport.max(1)).ok()?) + .ok()?; + packet + .set_tcp_destination_port(TcpPort::new_checked(dport.max(1)).ok()?) + .ok()?; + } else { + packet + .set_udp_source_port(UdpPort::new_checked(sport.max(1)).ok()?) + .ok()?; + packet + .set_udp_destination_port(UdpPort::new_checked(dport.max(1)).ok()?) + .ok()?; + } + + let meta = packet.meta_mut(); + meta.src_vpcd = Some(VpcDiscriminant::from_vni(summary.src_vni)); + meta.dst_vpcd = Some(VpcDiscriminant::from_vni(summary.dst_vni)); + meta.set_overlay(true); + meta.set_keep(true); + Some(packet) +} + +/// The summary a built packet actually carries, with its ports normalized the way the builder did. +fn expected_summary(summary: &PacketSummary) -> PacketSummary { + let mut expected = summary.clone(); + expected.ports = summary.ports.map(|(s, d)| (s.max(1), d.max(1))); + expected +} + +fn filter(built: &crate::fuzz_gen::BuiltOverlay) -> AclFilter { + let writer = AclFilterContextWriter::new(); + writer.store(AclFilterContext::for_test(&built.overlay)); + AclFilter::new("nf-fuzz-acl-filter", writer.get_reader()) +} + +/// How much of a run reached the code under test. +#[derive(Default)] +struct Tally { + drawn: AtomicUsize, + reached: AtomicUsize, + denied: AtomicUsize, +} + +impl Tally { + /// Assert the run was not vacuous. + /// + /// Both floors are **ratios**, not absolute counts. An absolute floor measures how fast the + /// machine was: a property reaching ten thousand probes on its own reaches a few hundred beside + /// nine hundred other tests under coverage instrumentation, and a floor tuned to the fast case + /// then fails for a reason unrelated to the code under test. + /// + /// The denial ratio matters as much as the arrival one and is easy to miss. A run that only ever + /// saw permits would pass every assertion below while the drop path -- the only path where the + /// stage does anything at all -- went entirely unexercised. + fn report(&self, what: &str) { + let (drawn, reached, denied) = ( + self.drawn.load(Ordering::Relaxed), + self.reached.load(Ordering::Relaxed), + self.denied.load(Ordering::Relaxed), + ); + println!("{what}: {reached}/{drawn} probes became packets, {denied} of them denied"); + assert!( + reached >= MIN_REACHED && reached * 4 >= drawn, + "only {reached} of {drawn} probes became packets, so the {what} assertion is barely \ + running" + ); + assert!( + denied * 20 >= reached, + "only {denied} of {reached} probes were denied, so the drop path is barely exercised \ + and this property is mostly checking that nothing happens" + ); + } +} + +/// The stage's verdict on a packet is the configuration's verdict on its five-tuple. +/// +/// The claim `fuzz.rs` makes about the tables, carried to where it is observable: a denied packet is +/// dropped and says `AclDropped`, a permitted one survives untouched. +/// +/// This is where the summary extraction is tested, and it is tested implicitly rather than by +/// inspection -- if `PacketSummary::try_from` read any of the six fields from the wrong place, the +/// stage would look up a different tuple from the one the oracle judged, and the two would disagree +/// on the probes where that field decides the answer. The generator's near-miss strays exist to make +/// those probes common. +#[test] +fn the_stage_agrees_with_the_configuration() { + let tally = Tally::default(); + + bolero::check!() + .with_type::<(OverlaySpec, [ProbeSpec; PROBES])>() + .for_each(|(overlay_spec, probe_specs)| { + let built = overlay_spec.build(); + let mut acl = filter(&built); + + for probe_spec in probe_specs { + tally.drawn.fetch_add(1, Ordering::Relaxed); + let summary = probe_spec.resolve(&built); + let Some(packet) = packet_for(&summary) else { + continue; + }; + + let want = oracle_resolved_action(&built.overlay, &summary); + let out: Vec<_> = acl.process(std::iter::once(packet)).collect(); + let got = out[0].get_done(); + + match want { + AclAction::Deny => { + assert_eq!( + got, + Some(DoneReason::AclDropped), + "the configuration denies {summary:?} and the stage let it through \ + with {got:?}\nspec: {overlay_spec:?}" + ); + tally.denied.fetch_add(1, Ordering::Relaxed); + } + AclAction::Allow => { + assert_eq!( + got, None, + "the configuration allows {summary:?} and the stage dropped it for \ + {got:?}\nspec: {overlay_spec:?}" + ); + } + } + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("stage verdict"); +} + +/// The five-tuple the stage reads back is the one the packet was built with. +/// +/// The previous property tests the extraction only where a misread field changes a verdict. This one +/// tests it directly, which catches the misread that happens to be harmless for the configuration +/// drawn -- a field read from the wrong place is a defect whether or not this particular ruleset +/// notices. +#[test] +fn the_summary_survives_the_round_trip_through_a_packet() { + let tally = Tally::default(); + + bolero::check!() + .with_type::<(OverlaySpec, [ProbeSpec; PROBES])>() + .for_each(|(overlay_spec, probe_specs)| { + let built = overlay_spec.build(); + + for probe_spec in probe_specs { + tally.drawn.fetch_add(1, Ordering::Relaxed); + let summary = probe_spec.resolve(&built); + let Some(packet) = packet_for(&summary) else { + continue; + }; + + let read = PacketSummary::try_from(&packet) + .unwrap_or_else(|e| panic!("a built packet did not yield a summary: {e:?}")); + let expected = expected_summary(&summary); + + assert_eq!( + (read.src_vni, read.dst_vni), + (expected.src_vni, expected.dst_vni), + "discriminants came back swapped or wrong\nspec: {overlay_spec:?}" + ); + assert_eq!( + (read.src_ip, read.dst_ip), + (expected.src_ip, expected.dst_ip), + "addresses came back swapped or wrong\nspec: {overlay_spec:?}" + ); + assert_eq!( + read.proto, expected.proto, + "protocol came back wrong\nspec: {overlay_spec:?}" + ); + assert_eq!( + read.ports, expected.ports, + "ports came back swapped or wrong\nspec: {overlay_spec:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + // The drop path is not this property's subject; borrow the floor. + tally.denied.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("summary round trip"); +} + +/// A packet with no discriminants is dropped, and says why. +/// +/// `PacketSummary::try_from` returns `DoneReason::Unroutable` for it, and that is the whole of what +/// the stage can do -- an ACL is indexed by the vpc pair, so a packet that names neither cannot be +/// judged at all. Letting it through would apply no policy to it whatsoever, which is the failure +/// this rules out. +#[test] +fn a_packet_with_no_discriminants_is_dropped() { + let tally = Tally::default(); + + bolero::check!() + .with_type::<(OverlaySpec, [ProbeSpec; PROBES])>() + .for_each(|(overlay_spec, probe_specs)| { + let built = overlay_spec.build(); + let mut acl = filter(&built); + + for probe_spec in probe_specs { + tally.drawn.fetch_add(1, Ordering::Relaxed); + let summary = probe_spec.resolve(&built); + let Some(mut packet) = packet_for(&summary) else { + continue; + }; + packet.meta_mut().dst_vpcd = None; + + let out: Vec<_> = acl.process(std::iter::once(packet)).collect(); + assert_eq!( + out[0].get_done(), + Some(DoneReason::Unroutable), + "a packet with no destination vpc was not refused\nspec: {overlay_spec:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + tally.denied.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("missing discriminant"); +} + +/// A packet that is not overlay traffic is left alone. +/// +/// The stage's gate. Underlay traffic is not indexed by a vpc pair and no ACL in the configuration +/// describes it, so applying one would be applying a policy to traffic it was never written for. +#[test] +fn underlay_traffic_is_not_judged() { + let tally = Tally::default(); + + bolero::check!() + .with_type::<(OverlaySpec, [ProbeSpec; PROBES])>() + .for_each(|(overlay_spec, probe_specs)| { + let built = overlay_spec.build(); + let mut acl = filter(&built); + + for probe_spec in probe_specs { + tally.drawn.fetch_add(1, Ordering::Relaxed); + let summary = probe_spec.resolve(&built); + let Some(mut packet) = packet_for(&summary) else { + continue; + }; + packet.meta_mut().set_overlay(false); + + let out: Vec<_> = acl.process(std::iter::once(packet)).collect(); + assert_eq!( + out[0].get_done(), + None, + "a packet that is not overlay traffic was judged by an overlay acl\nspec: \ + {overlay_spec:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + tally.denied.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("underlay gate"); +}