Anabasis, Book 4 - ὁ δʼ ἑρμηνεὺς εἶπε περσιστὶ

ὁ δʼ ἑρμηνεὺς εἶπε περσιστὶ ὅτι παρὰ βασιλέως πορεύονται πρὸς τὸν σατράπην - “the interpreter said, in Persian, that they were on their way from the King to the satrap”

Book four, chapter five. The army has just come through the worst of the Armenian snow, the men are dropping from hunger, and with the sun about to set, Cheirisophus and the vanguard reach a village. Outside the stockade he runs into women and girls drawing water at the fountain, who ask, reasonably enough, who on earth these people are – whereupon the interpreter answers for him, in Persian: they are on their way from the King to the satrap. The women tell him the satrap isn’t home but a parasang farther on, and since it’s late, everyone troops inside with the water carriers to see the headman.

It’s an easy line to skate over, and that is rather the point of it. Ten thousand Greek mercenaries who have spent the past year fighting the King’s army get waved into a Persian village because, by the time the question reaches the people at the gate, the answer has already been rephrased into something the gate’s guardians will deem acceptable. Nobody at the fountain ever heard the original; what they heard was the interpreter.

This is the post I’ve now put off twice, somewhat to my own embarrassment: how a ruleset actually becomes a set. The previous two entries only needed the rough outline of that mechanism and made do with a sketch, whereas this one owes you the machinery – and it ends with the interpreter, because the awkward part of that machinery, the part that took me longest to get right, is that the packet a filter chain passes judgement on is quite often not the packet that arrived.

The mechanics of folding

An nftables chain is a list of rules, and a rule is a list of statements: some matches, possibly a few things that happen along the way (a counter, a log line, a mark being set), and at most one verdict. The manual’s phrasing is that verdicts, along with “statements that imply a verdict (like reject or the NAT statements)”, “end the evaluation of any later statements in their respective rules”. A rule without a verdict, then, is a rule that looks at the packet and hands it on – which sounds trivial until you notice how much of a real ruleset consists of exactly that.

Evaluating a chain on a set of packets is merely an extension of that principle, and it’s a fold in the ordinary functional sense. You carry a set – call it remaining – of packets nobody has decided on yet, which starts out as everything that entered the chain, and then, for each rule in order:

• intersect remaining with whatever the rule matches;
• if the rule carries a verdict, move that intersection into the set the verdict specifies, accepted or dropped, and take it out of remaining;
• if it doesn’t, move nothing, since the rule only observed the packet;
• either way, packets the rule didn’t match are untouched and continue to the next rule.

When the chain runs out, whatever is left in remaining has fallen through, and the base chain’s policy gets the last word.

As a state transition that is rather smaller than the code implementing it: carry a triple of accepted, dropped and still undecided, and a rule with match set P bearing an accept verdict takes it to

with drop doing the same thing into D, and a rule bearing no verdict leaving all three exactly as it found them. FIREMAN wrote very nearly this two decades ago for access lists; what follows below is that arrangement with nftables’ chain calls left as recursion rather than flattened, and with every one of those three sets a bracket rather than a set.

Since last time, every set in that description is really a bracket rather than a set, and “take it out of remaining” is the representation of the consume function from the previous post, with its deliberately crossed subtraction. I won’t go over that again; what matters here is that the fold below is written once, over brackets, and produces the permissive and the strict reading of the chain in a single pass, and nothing in the rest of this post needs to be aware that unknowns exist at all.

Here’s the loop, minus the obligatory bookkeeping:

TriPredicate remaining = std::move(incoming);

for (const ir::RuleId id : ruleset_->chain(chain).rules)
{
    const ir::Rule&     rule      = ruleset_->rule(id);
    const TriPredicate& predicate = predicateOf(rule);
    const TriPredicate  matched   = meet(remaining, predicate);

    effects_.push_back(RuleEffect{ ... .reaching = remaining.over, .matched = matched.over ... });

    if (const ir::Verdict* verdict = ir::verdictOf(rule))
    {
        applyVerdict(*verdict, id, matched, out, remaining);
    }
}

out.returned = unite(out.returned, remaining);

One detail deserves a sentence, because at first glance it looks like waste: the loop visits every rule even once remaining has emptied, at which point nothing can possibly reach the rules that follow. That is deliberate. A rule which the rules above it have rendered unreachable is exactly what the anomaly analysis wants to report later on, and it can only report what the evaluation bothered to write down – which is what the RuleEffect line does, one entry per rule, recording what reached it and what it matched.

The last line is worth a glance too. Whatever survives the chain is neither accepted nor dropped but returned, and that word is about to carry a good deal more weight than it looks capable of.

Jump, goto, and the ambiguity of return

A jump calls another chain, and so does a goto; the difference between them is a single fact about the call stack, which the manual states more plainly than most documentation manages:

A jump verdict causes the current position to be stored in the call stack of chains and evaluation to continue at the beginning of the called regular chain. […] When the end of the called chain is reached, an implicit return verdict is issued.

A goto verdict is equal to jump except that the current position is not stored in the call stack of chains.

And then the part that catches people unawares:

A return verdict ends the evaluation of the current chain, pops the most recently added position from the call stack of chains and causes evaluation to continue after that position. When there’s no position to pop (which is the case when the current chain is either the base chain or a regular chain that was reached solely via goto verdicts) it ends the evaluation of the current base chain (and any regular chains called from it) using the base chain’s policy as implicit verdict.

So return means two different things depending on how you got there. After a jump, returning means carry on with the next rule of the caller; after a goto there is no caller to carry on with, so returning means fall through to the base chain’s policy. A chain that ends in an innocent-looking return, or simply ends, therefore behaves in two entirely different ways depending on whether the rule that reached it said jump or goto – and I have seen, on a real host, a goto written where a jump was meant, with a drop policy quietly eating everything the called chain hadn’t explicitly accepted.

In the evaluator this boils down to one argument. A called chain hands back the set of packets that returned from it, and the caller has to decide where that set goes:

[&](const ir::Jump& jump)   { return descend(jump.target, remaining); },
[&](const ir::Goto& target) { return descend(target.target, out.returned); },

After a jump, the returned packets are united back into remaining and the fold carries on with the next rule; after a goto, they go into out.returned, which is the set the base chain’s policy will eventually decide. Two lines that differ in a single argument, and that argument is the entire semantic distance between the two verdicts. Once the base chain itself finishes, returned is folded into accepted or dropped according to the policy, and that’s the last thing that ever happens to a chain.

Then there’s the verdict map. vmap is the third way of branching and the one that looks least like a rule; the manual describes it as working “analogous to the map statement, but contains verdicts as values”, and its own example is the canonical one, ip protocol vmap { tcp : jump tcp-chain, udp : jump udp-chain, icmp : jump icmp-chain }. Semantically it’s a disjoint case split, so the evaluator treats each entry as a small rule in its own right – intersect the matched set with the entry’s key, apply the entry’s verdict to that slice, consume the slice from what is still pending, next entry. Because the keys of a map are disjoint by construction, their order makes no difference to the answer; it does mean, though, that a vmap with fifty entries costs you fifty small folds rather than one large one.

Beware of the hooks

So much for a single chain. A packet on the input path meets several, and this is where nftables parts company with the instincts most of us brought over from iptables.

I quoted the load-bearing sentence last time: an accept “ends the evaluation of the current base chain” and the packet “advances to the next base chain”, while a drop “immediately ends the evaluation of the whole ruleset”. The manual draws the conclusion itself:

Thus a packet is ultimately accepted if and only if no (matching) rule or base chain policy issues a drop verdict.

Which, for sets rather than packets, is a single line, taken over the base chains a packet meets on a given path:

Accept is conjunctive and drop disjunctive, and that asymmetry is the whole of the instinct one has to unlearn.

The path evaluator is therefore nothing more than the same fold applied a second time, one level up – the accept set that comes out of one base chain is the incoming set of the next. Where several base chains sit on the same hook, they run in order of priority, lowest first. Two chains with the same priority are a problem the dump can’t settle, because the kernel runs them in registration order and the JSON doesn’t record it; rather than pretend to know, the tool orders them by name and says so in the report, as an assumption.

Two further things can sit on a hook, and neither is a chain the tool can read:

• A chain from a family the analysis doesn’t model – arp or netdev, say. This one is passed over, and the report gets a line noting that a base chain in an unmodelled family filters this hook and was not analysed whatsoever.
• A chain in a modelled family whose verdicts can’t be derived. This one can’t simply be skipped, because skipping it would amount to a silent claim that it drops nothing.

For the second case the evaluator treats the chain as a filter that might accept anything and is certain to accept nothing:

if (!step.modelled)
{
    outcome.dropped.over   = outcome.dropped.over | outcome.accepted.over;
    outcome.accepted.under = space_->empty();
    continue;
}

The upper bound of what’s dropped grows to include everything that reached the chain, while the lower bound of what’s accepted collapses to nothing. That’s last post’s bracket applied to a whole chain rather than a single match, and the upshot is that a chain the tool doesn’t understand renders the path inconclusive rather than wrong – which, as before, is the only honest option available to us.

At the end of the path you hold, per address family, the set of packets the filter chains do accept. And that would be the end of the story, had the filter chains actually seen the packet that arrived - but what if that’s not the case ?

The interpreter

Quite often they haven’t. Destination NAT runs at the prerouting hook, before the routing decision and therefore before input and forward, and a dnat statement is, in the manual’s words, one of the “verdict-like statements that imply accept”: it rewrites the destination, ends the nat chain, and sends the packet on its way wearing a new address. Everything that happens afterwards happens to the rewritten packet - the filter chain that later says ip daddr 10.0.0.5 tcp dport 80 accept isn’t being coy about the public address, for it has never heard of it. It’s answering the interpreter to the best of its abilities.

The question a specification asks, meanwhile, is about the wire. “Can anything outside reach tcp/8080 on the public address” is a claim about packets as they arrive on the interface, because that’s what an auditor can see and what an attacker can send. The two have to be joined somehow, and that joining is the part of this project that gave me the most trouble for the least code.

The literature already had the right frame, and it comes from Header Space Analysis, the Stanford work I touched on in the second post. Their claim is that “all networking boxes can be modeled as Transformers with a Transfer Function”, a function from a header to a set of headers, and that a header rewrite in particular “can be represented by a masking AND followed by a rewrite OR”. They say in so many words that “a Network Address Translator (NAT) box can also be modeled using a rewrite operator”, and, decisively for my purposes, they define the operation you need in order to go the other way:

Range Inverse: Reachability and loop detection computation requires working backwards from a range to determine what input (header, port) pairs could have produced it.

On decision diagrams that inverse comes down to two operations I already had lying around. Constrain the set to what the rule writes, then forget the variables it overwrites; in the kernel’s vocabulary that’s a conjunction followed by an existential quantification over the rewritten field’s bits:

narrowed = narrowed & space_->fieldEq(ir::FieldId::DstAddr, *rewrite.address);
...
return space_->wrap(space_->kernel().exists(narrowed.id(), rewritten));

Put as a question, the code is asking: which packets, once their destination has been overwritten with 10.0.0.5, end up inside this set? Intersect the set with daddr == 10.0.0.5 and what remains describes packets whose other coordinates are right; then quantify the destination bits away, because the packet that arrived may have carried any destination whatsoever – the rule was going to overwrite it regardless. What’s left is the set of arriving packets whose rewritten form lands in the set you started from. That’s the range inverse, on a bit space, in two lines.

The direction matters, and it’s the one thing I got wrong on the first go-round. You could push the question forward through the rewrite and ask the filter chains about the translated flow; it’s simpler to write, yet the answers it yields are about the wrong packet. The witness that came back would have 10.0.0.5:80 in it, an address the attacker never sent and the auditor will never see on the wire. Pulling the answer back through the inverse instead means the filter chains are asked exactly what they know about the translated packet, while the result is expressed in terms of what actually arrived. Every witness is a wire packet, every region lies on the wire, and thusly, a stage: post-nat in a specification is the explicit opt-in for those who genuinely want to talk in translated terms – container port publishing being the usual culprit.

The bracket does survives the inverse, and to fully understand the implications of that, we need to take a closer look. Not every packet gets rewritten - a packet no dnat rule matches passes through untouched, and one that a rule might match, on some uncertain condition, might or might not. So the preimage starts from the translated bracket with the rewritten packets removed, and it removes them in the crossed manner you would - by now - expect:

packet::TriPredicate out{.over  = translated.over  - mustRewrite,
                         .under = translated.under - mayRewrite,
                         .reasons = translated.reasons};

A packet no rule certainly rewrites may still arrive untouched, so the upper bound keeps it; a packet some rule may rewrite isn’t certainly untouched, so the lower bound lets it go. Then, rule by rule, each rewrite contributes its inverse image – the may-matched set intersected with the inverse of the upper bound goes into over, the must-matched set intersected with the inverse of the lower bound into under. And a rule whose target isn’t a constant at all, dnat to ip saddr map { … } say, sends the packet somewhere the ruleset doesn’t name; it contributes to the upper bound only, since such a packet may be accepted and is never certainly accepted. It’s the unknown from the previous post, incorporated by a different kind of rule.

Let’s take it for a spin

Here’s the whole thing running against a ruleset built to show it off. Two tables: a nat table whose prerouting chain rewrites 203.0.113.10:8080 to 10.0.0.5:80, and a filter table whose input chain drops by default and accepts exactly ip daddr 10.0.0.5 tcp dport 80. Two assertions, both about the public address on the wire, both deny. The report, with the file path and fingerprint lines cut:

Violations
  [fail] nothing-reaches-8080-on-the-public-address (deny input, ip)
      traffic the specification forbids is accepted
      example: ip tcp 0.0.0.0:0 -> 203.0.113.10:8080 ct state new iif <other>
      traffic: ct state new l4proto tcp daddr 203.0.113.10 dport 8080
      packets: 7.92e+28
      decided by ip/nat/prerouting handle 2: translate [match daddr == 3405803786 match(implicit) l4proto == 6 match dport == 8080 nat {"addr":"10.0.0.5","port":80}]
      decided by ip/filter/input handle 2: accept [match daddr == 167772165 match(implicit) l4proto == 6 match dport == 80 verdict accept]

Satisfied
  [pass] nothing-reaches-80-on-the-public-address (deny input, ip)
      no packet of this flow is accepted

Look at what the first finding is stating. The filter chain never contained the string 8080, yet the witness packet carries it anyway, because the witness is a wire packet and the wire is where 8080 lives. The trace names both rules in the order the packet met them – translation first, accept second, which is to say the interpreter and only then the gate. The second assertion passes: port 80 on the public address is blocked, despite the only accept rule in the entire ruleset saying dport 80, because a wire packet to 203.0.113.10:80 isn’t rewritten, reaches the filter with its public destination intact, matches nothing, and falls to the policy. The rule that mentions port 80 is reachable only through the rule that mentions 8080. A person reading those two rules cold would be prone to misinterpretation of the findings, so reading the findings requires understanding the ruleset.

(The numeric address is an artifact of the current, intermediate build state)

Where this leaves us

A ruleset is now a set, or rather a bracket around one, per path and per family. The fold turns a chain into accepted and dropped; the path composition intersects the chains a packet meets; and the inverse of the NAT transfer pulls the answer back onto the wire, so that question and answer are finally about the same packet. Jumps, gotos, returns and verdict maps are all in there, and so is the one thing nftables does for which most of us still carry the wrong instinct over from iptables, namely that accept is never the last word to be said about a packet.

What every report in this series has carried, though, is a line I’ve so far declined to explain:

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

The ruleset decides what happens to a packet that reaches a chain. Whether the packet reaches the chain at all is decided by the machine: by whether it forwards, by what its reverse-path filter discards before any rule gets a look at it, by whether a frame switched across a bridge ever meets the ip hooks in the first place. None of that is in the dump, all of it potentially changes the answer, and a compliance tool that ignores it is auditing a firewall that doesn’t exist. The details of that distinction and how we’ll address it will be deliberated upon in Book 5 - so stay tuned for my next update!