Anabasis, Book 5 - Οὐκ ἄβατόν ἐστι τὸ ὄρος

οὐκ ἄβατόν ἐστι τὸ ὄρος, ἀλλὰ νέμεται αἰξὶ καὶ βουσίν - “the mountain is not impassable, but is grazed by goats and cattle”

Book four, chapter six. The army has arrived at a pass held against it, and Cheirisophus and Xenophon are having one of their needling exchanges about which of their cities produces the better thieves, when Xenophon volunteers to take the rear division after supper and seize the mountain. What piqued my interest is the sentence with which he justifies the plan. He has guides, he says, because the light troops laid an ambush and caught some of the cut-purses trailing the column; and from those men he has learnt that the mountain is not impassable but is grazed by goats and cattle, so that once they hold any part of it the pack animals will get across too.

What settles the question is worth dwelling on. It isn’t the map, because there is none; it isn’t the orders, which are silent on the subject; and it certainly isn’t anything visible from where the army stands, since from down there the whole ridge looks every bit as impassable as the one Cheirisophus had pointed at five chapters earlier. Whether the ground can be crossed is settled by evidence gathered from outside the column altogether, and the evidence is goats: livestock graze up there, therefore the terrain is passable, therefore the mules will manage.

Every report this tool has printed over the preceding four posts has carried a line I have so far walked straight past:

Assumptions
  the input path: the host's routing table, forwarding switches, reverse-path
  filtering and bridge netfilter state were not read, so every packet was taken
  to be deliverable and forwardable

That is the tool admitting it has, indeed, not bothered to go looking for the goats.

What the ruleset cannot tell you

The previous post established how a ruleset becomes a set - the fold over the chain, the composition along a path, the inverse of the NAT transfer - and all of it answers a single question, which is narrower than it looks. The chains decide what happens to the packets that reach them. Whether a packet reaches them at all is settled earlier, in a place the ruleset has no vocabulary for, and until now, wasn’t incorporated into any decision either.

Take a forward chain that accepts everything, on a host where net.ipv4.ip_forward is zero. Every rule in it is dead - not shadowed, not redundant in the sense the anomaly analysis means, just never consulted, because the kernel discarded the packet at the routing decision long before the forward hook was ever a possibility. An audit that reads only the ruleset will report that this host forwards web traffic, and it will be confidently wrong, embarrassingly so.

The only good news is that the list of things in this category is quite short. The routing table decides which destinations are delivered locally, which are forwarded and out of which interface, and which are dropped outright because somebody installed a blackhole route. A mere four switches decide the rest:

• the global forwarding sysctl,
• the per-interface one,
• the reverse-path filter, and
• whether bridged frames are shown to the ip hooks at all.

nft -j list ruleset contains not one word about any of that truth.

So the tool reads a second input alongside the ruleset, and the docstring on the probe elaborates on the part that matters:

Runs ip -j for the tables and reads /proc/sys and /sys/class/net for the switches, in the network namespace of the calling process - the same one whose ruleset nft reports, which is what makes the two halves of the answer belong together.

The namespace is anything but a minor detail. A ruleset dumped in one namespace and a routing table read in another describe two different machines, and combining them yields an answer about a host that does not exist as described. Given how much of modern Linux is containerized, that is a mistake with no shortage of opportunities to occur.

The routing table, as sets

The forwarding information base answers exactly one question - where does a packet with this address go - and the analysis surfaces it in four shapes: which addresses this host answers for itself, which it can route at all, which interface a given address leaves by, and what a fib expression inside the ruleset evaluates to. All four are the same relation with a different field substituted, so it gets built once, over the address and interface variables the packet space already carries. Nothing here widens the diagram: no new variables, and prefix matches are the shape decision diagrams are best at, as the second post laid out at some length.

Longest-prefix match is what makes this a relation rather than a union. A route doesn’t decide the packets it covers; it decides the packets that no more specific route claims. The construction therefore walks the table sorted by descending prefix length, with each prefix contributing itself minus everything longer that lies inside it. Two routes, 10.0.0.0/24 dev lan and 10.0.0.1 dev lo, don’t overlap in the relation even though one address sits inside the other’s prefix, because the host route has been subtracted from the network route before the network route contributes anything at all.

One design decision in here deserves being in the spotlight, for it’s about testing rather than routing. A ruleset can perform its own routing lookup with the fib expression - which is, as it happens, the only way to write a reverse-path check for IPv6, where the kernel offers no sysctl whatsoever. The obvious implementation would have the symbolic evaluator and the concrete packet interpreter each work out for themselves what fib saddr . iif oif exists means. The code deliberately refuses to, and the comment on it explains the reasoning behind that:

Both engines ask this one object rather than each deriving the meaning of fib for itself: a differential test between two views of the same model proves nothing if the views disagree about what the rule says; any disagreement must concern the answer and only the answer.

Two implementations that independently misread the same expression will agree with each other perfectly while both being wrong, and a differential test between them will cheerfully report success. Sharing the definition and differing only in how it is applied is what makes any disagreement informative.

Shape is not admission

This is the distinction that caused me a most repetitive headache, and it is remarkably easy to get backwards, as it happens. I’ll elaborate on the specifics:

A flow in a specification is named on a path: path: forward means forwarded traffic, path: input means traffic delivered to this host. That much has to constrain the question, because it’s what the question means - a packet on the input path has an incoming interface and no outgoing one, a forwarded packet has both. The tool therefore reads every flow within its path’s shape, and a question about the input path is a question about locally delivered packets, whatever else may be true.

What must not constrain the question is whether the host actually carries such packets. The two live in separate fields for precisely that reason:

/// @brief The packets the host actually carries on this path.
///
/// The shape narrowed by what the machine does - forwarding switched
/// off, a destination it does not answer for, a source its reverse-path
/// check refuses.  Deliberately *not* used to narrow the question: a
/// requirement that traffic flow is not met by the host declining to
/// carry it, and folding the two together would report exactly that
/// case as satisfied.
packet::Bdd admitted;

Fold shape and admission together and the arithmetic silently fails to encode any meaning. Let me rephrase the matter with an example: An allow assertion says traffic must get through. Were the question narrowed to what the host admits, a host that forwards nothing would pose an empty question; an empty question is vacuously satisfied, and so the report would cheerfully certify that web traffic traverses a machine with forwarding switched off. The admission set is therefore conjoined onto the accept set, after the chains have run, and never onto the flow being asked about. A requirement is only met if traffic actually does flow.

The upside of keeping the gates apart rather than collapsing them into one conjunction is that a counterexample can say which gate, specifically, it failed. “The ruleset dropped it” and “it was never forwarded in the first place” are different findings with different owners, and very different solutions indeed.

The reverse path, and some more sysctl

Source validation is the switch most likely to surprise, so it’s the prime example for demonstration.

The concept comes from RFC 3704, Ingress Filtering for Multihomed Networks, BCP 84, from 2004. It defines strict reverse path forwarding as looking the source address up in the FIB and passing the packet only if it arrived on the interface that would be used to send traffic back to that source, and loose reverse path forwarding as the weaker relative that “checks only for the existence of a route (even a default route, if applicable), not where the route points to”. Linux implements both, and the kernel documentation labels them by the same names: value 1 is “Strict mode as defined in RFC3704 Strict Reverse Path”, value 2 is loose, value 0 is no validation.

Here, then, comes the sentence that makes this worth modelling rather than assuming:

The max value from conf/{all,interface}/rp_filter is used when doing source validation on the {interface}.

The maximum. Not the interface value, not the global one, and emphatically not the stricter of the two - because in this encoding 2 is loose and 1 is strict, so the numeric maximum of a strict global setting and a loose interface setting is the loose one. Set net.ipv4.conf.all.rp_filter = 1, congratulate yourself on having hardened the machine, and any interface left at 2 is still running loose validation. The enum in the host model carries the kernel’s own numbering for exactly this reason, with the inversion written down beside it, because the moment somebody sorts these by “strictness” the bug becomes permanent.

Written out, with rᵢ standing for whatever check the mode in force on interface i performs:

A packet survives if the check belonging to the interface it actually arrived on holds of it, every other interface’s clause being vacuously true. Which is also where the trap becomes legible rather than merely surprising: moving from strict to loose replaces “routes back the way it came” with the distinctly weaker “routes back at all”, and off is weaker still. Note, though, that the numbering does not follow that ordering anywhere else: off is the weakest check and carries the smallest value, so the maximum of off and strict is strict and does strengthen the interface. It is only across the strict-against-loose pair, which is precisely the pair one actually configures, that the larger number is the weaker predicate - which is the whole reason these three cannot be sorted by anything resembling strictness.

Here’s what modelling it buys you. The ruleset below is as permissive as a ruleset gets - a forward chain with policy accept and a rule that accepts everything - and the host is the router fixture: a LAN on 10.0.0.0/24 behind lan, an uplink on wan. The assertion says that packets claiming a LAN source must not be forwarded when they arrive from the uplink, which is the textbook anti-spoofing requirement:

- id: spoofed-lan-addresses-from-the-uplink-are-refused
  kind: deny
  flow: {family: ip, path: forward, proto: tcp, iif: [wan], src: [lan], dport: [80]}

With rp_filter at 1 on that host:

Satisfied
  [pass] lan-may-reach-the-world (allow forward, ip)
      every packet of this flow is accepted
  [pass] spoofed-lan-addresses-from-the-uplink-are-refused (deny forward, ip)
      no packet of this flow is accepted

0 failed, 0 undecided, 2 satisfied, 0 not applicable

Now change one number. Same ruleset, byte for byte; same routing table, byte for byte; rp_filter set to 0:

Violations
  [fail] spoofed-lan-addresses-from-the-uplink-are-refused (deny forward, ip)
      traffic the specification forbids is accepted
      example: ip tcp 10.0.0.0:0 -> 10.0.0.0:80 ct state new iif wan oif lan
      traffic: ct state new iif wan l4proto tcp saddr 10.0.0.0/24 dport 80
      packets: 1.89e+31
      decided by ip/filter/forward handle 2: accept [verdict accept]

1 failed, 0 undecided, 1 satisfied, 0 not applicable

The anti-spoofing property held on the first host without a single rule enforcing it, and it was lost on the second without a single rule changing. No tool that reads only nft list ruleset can possibly tell those two machines apart, and the difference between them is whether a stranger can inject packets spoofing your own network’s addresses.

The witness, incidentally, is about the clearest statement of the problem one could ask for: a TCP packet with source 10.0.0.0 arriving on wan and leaving on lan.

Switching is a path, not a corner of forwarding

The last of the four switches is the one I would have gotten wrong had I not been aware of that particular intricacy of linux networking from configuring my own dedicated server.

The one word which most accurately describes my mindset on networking is “determinism”. If I can get away with banning any daemon like libvirt or docker from interfering with nftables, that’s exactly what I am doing, and thus, on my personal server, br_netfilter is very much disabled, the bridge table is hand-rolled, as is the ip table, and neither docker nor libvirt are allowed to interfere with what I’ve decreed the firewall shall encode. The particularities of L2 and L3 networking aren’t lost on me, which is exactly why I was adamant in my desire to ensure that this here software handles such cases with the grace and correctness I expect from it.

You may be aware that a frame that a bridge switches between two of its own ports never reaches the routing decision, and it follows that none of the machinery above applies to it - not the route lookup, not ip_forward, not the reverse-path check. On a virtualisation host that forwards nothing whatsoever, the virtual machines still chatter to each other all day long, and a model in which the forward hook is unreachable has precisely nothing to say about any of that traffic.

So switched frames get a path of their own, with a shape and no admission gate, and the shape spells out what being on it means: an incoming port, a different outgoing port, and both of them ports of the same bridge. Two facts underwrite that, and both were checked against a kernel rather than reasoned about - a bridge never returns a frame to the port it arrived on, and two bridges never switch between each other’s ports.

Whether those frames also meet the ip hooks is what br_netfilter decides, per namespace and per bridge. Where it’s loaded and enabled, the ip chains join the bridged path interleaved with the bridge ones rather than running before or after them, because br_netfilter calls each ip hook from inside the bridge hook of the same name: bridge prerouting, ip prerouting, bridge forward, ip forward, and so on down the line. Where the bridges on one host disagree about the setting, the ip chains are on the path but don’t decide every frame on it, and that is neither of the two clean answers. Including them would let a deny pass on filtering that may never happen; excluding them would let an allow pass on filtering that does. Only the three-valued reading from the third post is sound in both directions, which is a testament to the fact that the uncertainty band was never built for rate limits alone.

The demonstration for this one is the same permissive ruleset as before, an ip forward chain accepting everything, against a virtualisation host with six bridges and no br_netfilter loaded:

Violations
  [fail] the-forward-chain-filters-switched-frames (deny bridged, ip)
      traffic the specification forbids is accepted
      example: ip tcp 0.0.0.0:0 -> 0.0.0.0:80 ct state new iif eno1 oif vmtap0
      traffic: ct state new l4proto tcp dport 80
      packets: 8.17e+39

There is no “decided by” line on that finding, and its absence is the whole content of it. No rule decided this traffic, because no chain on that path ever saw it. The forward chain the operator is relying on to filter inter-VM traffic filters exactly nothing, and the witness names two ports of the same bridge to say so.

One more reduction lives in this corner and earns a paragraph because it kept the packet space narrow. A ruleset can match on ibrname and obrname, the bridge a frame’s port belongs to. The obvious modelling is two more symbolic fields, which would have widened every packet space in the program - including all the paths on which a bridge means nothing at all - and would then have had to be tied back to the interface fields anyway. But a port belongs to exactly one bridge, so naming a bridge is just naming the set of its ports:

Measured on a kernel, a rule matching ibrname "br0" decided exactly the frames that iif in br0’s two ports decided between them. No new variables, no widening, and the fact that the substitution is only available when a host was actually read is correct rather than unfortunate: which ports belong to which bridge is a fact about the machine, and a run that read no machine has no business answering it.

The host nobody read

Which brings us to the assumption in the report, and to the one place where this tool knowingly assumes something.

The host model carries its provenance - observed on this machine, captured from a file taken beside the ruleset dump, or assumed. An assumed host forwards everything, answers for every address, validates no source, and shows every bridged frame to the ip hooks. That is no neutral default; it is, quite deliberately, the most permissive machine that could exist.

The third post argued at some length that a compliance tool must never guess, so this deserves a defence, which simply is that it isn’t the same kind of decision. An undecidable match leaves a specific packet’s fate genuinely open, and the uncertainty band exists to carry that forward soundly. An unread host is a different animal: treating the four switches as unknown would widen every single forward and input assertion into inconclusive, all at once, and produce a report in which nothing is decided and no reader can act on anything. That isn’t sound humility so much as a refusal to answer dressed up as an answer.

What the assumed host does instead is make the ruleset’s own filtering the only thing standing between the traffic and the host - the worst case for the ruleset, which is after all what an audit is about. And it says so, in every report, on every path walked that way. The assumption is stated, which, as the third post concluded, is the entire difference between an assumption and a guess.

What it costs

The temptation with all of this is to assume a routing table costs about as much as a ruleset. It doesn’t, not even close, and the ratio is the useful number rather than the absolute, so here is a measurement in which both halves hail from the same run on the same machine: building the relation for the recorded host’s own table, twenty routes, and asking it three questions costs 3.5 µs, against 61.6 ms for one cold evaluation of that host’s input path, which yields a ratio of roughly 1:17.000

It also scales far past anything a host will plausibly carry. Four thousand and ninety-six routes, all /24, cost 2.9 ms. Growth fits N log N at 11 % RMS across three decades, because the per-length loop accumulates a cover whose diagram grows well below linearly - the prefixes of a real table share structure, which is precisely the property the second post said decision diagrams exploit. The bridge topology of a host with sixty-four bridges costs 72 µs.

One expectation in there was wrong, and measuring is how I found out. I had assumed that spreading the same four thousand routes across every available prefix length would cost more than stacking them all at /24, since each length’s contribution is that length’s prefixes minus everything longer. It’s three times cheaper: 0.93 ms against 2.9. The work is proportional to the accumulated cover rather than to the number of subtractions, and a table that uses many lengths holds fewer prefixes at each of them. I’ve had my expectations disproven by measurements in this series often enough by now to have stopped being surprised; it was unexpected nonetheless.

Where this leaves us

The tool now reads two things: what the kernel is filtering, and what the machine underneath it will carry. The filter chains supply the verdict, the routing relation and the four switches supply the question, the two meet at a single conjunction after the chains have run, and every path that was walked on assumptions says which ones.

Which raises the question this series has been quietly accumulating for five posts. Every one of the claims above - that accept is local and drop final, that a bridge never returns a frame to its own ingress port, that ibrname counts exactly the frames its ports count, that nft keeps an ethertype comparison positive under negation - is a claim about what a kernel does. I’ve cited a manual for some of them and written “measured on a kernel” for others, and you have had to take that on trust.

You shouldn’t have to. Book six is about the machinery that spares you from it: a differential test harness that takes the model’s answer, builds the same ruleset inside a throwaway network namespace on a real kernel, fires real packets at it, traces them, and compares. It refuses to run as root, it has caught me being wrong more than once, and the most interesting failure it ever produced was the time the harness itself broke in a way that looked exactly like the test passing.