Anabasis, Book 3 - Ἔστησαν ἀγνοοῦντες

ἔστησαν ἀγνοοῦντες εἰ διαβατέον εἴη τὸ νάπος - “they halted, not knowing whether the glen had to be crossed”

Book six, chapter five. The army is marching in three columns when the vanguard arrives at a large and difficult wooded glen, and there it stops. Why, one might reasonably ask, and the answer is less obvious than it looks: not because the enemy has been sighted, nor because the obstacle is insurmountable, but because nobody at the front can say whether this glen is an obstacle that needs dealing with at all; and so word is passed back down the line for the commanding officers to ride forward. Xenophon, who by this point in the narrative is reliably the last man to hear of anything, wonders what has halted the march, hears the order being relayed along the ranks, and rides up.

What follows is the part I am particularly fond of: Sophaenetus, the eldest of the generals, declares the question unworthy of deliberation. Xenophon disagrees, at some length, and the argument that ensues turns on whether they will have a ravine at their backs once the fighting begins. An army, in hostile country, has halted in order to hold a meeting about something it cannot adequately assess.

That conundrum sums up this post rather neatly. Two posts ago I set out what a firewall audit is for, and last time the algebra it runs on; neither had anything to say about what the tool ought to do upon reaching a rule it cannot safely assess, and, as luck would have it, many rulesets contain at least one such rule.

First and foremost: turning a ruleset into a set

I still owe this series a proper elaboration on how rules turn into sets, and it will be forthcoming. For the moment, an outline will have to do.

An nftables chain is evaluated first-match. The rules are applied to the packet in order; the first whose conditions hold and which carries a verdict decides the packet, while the verdictless ones, of which nftables has a fair few (counters, logging, marking), let evaluation proceed to the next. One therefore walks the chain a single time, carrying along the set of packets not yet decided, and at each rule intersects that set with whatever the rule matches. Packets in the intersection that meet an accept move into the chain’s accept set, those meeting a drop into its drop set, and packets the rule did not match at all remain undecided and are handed on to the next rule. When the chain is exhausted, whatever remains undecided falls to the base chain’s policy; jumps, on the other hand, recurse and hand a set back to their caller.

One nftables-specific detail matters rather more than its size suggests. The manual states that an accept verdict “ends the evaluation of the current base chain” and the packet “advances to the next base chain”, whereas a drop “immediately ends the evaluation of the whole ruleset”. To paraphrase: accept is local, drop is final. A packet must consequently be accepted by every base chain along its path and is dropped as soon as any of them renders a drop; along a given path, the accept sets intersect and the drop sets union. On a host where Docker, libvirt and one’s own table have each registered a base chain on forward or input - which describes rather a lot of hosts - this is the norm rather than the exception, and a tool that stops evaluating at the first accept it encounters is, for nftables, simply wrong.

After evaluation, one set per path and per address family remains: these are the packets the firewall accepts. Every compliance question thereafter is set algebra against that object, which was, as you may remember, the subject of the previous post.

That, at any rate, is the happy path, on which every rule can be evaluated deterministically. As ever, trouble begins the moment we leave it.

Is it a bird? Is it a plane? No, it’s a rate limit.

Consider the following rule, which is, frankly, nothing terribly exotic:

tcp dport 80 limit rate 10/second accept

Which packets does it accept? The candid answer is that the question is not well formed. The manual describes limit as matching “at a limited rate using a token bucket filter” and notes that “a rule using this statement will match until this limit is reached”, so whether the rule matches a given packet depends entirely on how many packets it has already waved through in the recent past, and for that the packet-space model of the last post possesses no vocabulary whatsoever. A packet is, if you’ll remember, a point in a space of 157 or more bits worth of boolean variables, and “how many came before” is not one of the axes. The phrase my code uses when it declines to decide one of these is that the match matches on packet history rather than packet content, which is the fact of the matter, put about as tersely as it can be.

limit, however, has company. quota conveys the same idea, stretched over a longer horizon. ct count counts parallel connections per key, and the manual’s own example for it describes a guard against SSH floods, something one would expect to find on plenty of hosts. osf fingerprints the sending operating system from the shape of the SYN - window size, MSS, the order of the options - a fact about a TCP stack somewhere else entirely. socket asks whether a local socket exists, numgen generates numbers, tproxy hands the packet off to a local service, and queue hands the verdict itself to a userspace program, after which whatever happens is the business of somebody’s daemon. And then there is the open-ended category: an expression emitted by a version of nft newer than the build doing the reading, which is not undecidable in principle but is undecidable by this program, and to whoever is holding the report that distinction is academic in nature.

One thing that does not belong on the list, though at first glance it looks as if it could: a dynamic set, of the kind CrowdSec fills and expires around the clock. The dump the tool reads carries that set’s contents at the instant of the dump, and the verdict concerns that very instant. Far from being a weakness, this is the point of evaluating live rulesets in the first place. You may recall the first post made rather a fuss about the ruleset in the kernel being a fact rather than an intent; the contents of a dynamic set at 02:14 are part of that fact, and the report states what was true at 02:14, as it should.

Your guess is as good as mine - and that’s not good enough

Two guesses are on offer, and both are catastrophic in precisely the same manner.

Guess that the limit lets packets through, and port 80 will be reported reachable. If the bucket happens to be empty, it is not, and you have sent some poor DevOps engineer off hunting for a blocker that sits squarely inside the firewall you assured them was fine.

Guess that the limit blocks, and port 80 will show as closed. Should the bucket still have tokens in it, the port is open, and a hole goes unnoticed.

The direction of the error is beside the point. What matters is that a PASS the tool earned and a PASS the tool made up are typographically identical, and no amount of diligence at the reading end will tell them apart. This is the failure mode the TU München group described for the previous generation of tools, and a point I raised in the first post: once the firewall exceeds the supported feature set, the tools either produce erroneous results or cannot continue. Erroneous results are a good deal worse than not continuing at all, because a silent failure looks exactly like confidence.

No guessing, then. That leaves the question of what to do instead, and the answer is to stop insisting on a single accept set.

Two sets, and the uncertainty band between them

The load-bearing work here was done by Diekmann and colleagues, who translate a real iptables ruleset into a simplified model one can reason about. Their move is to abstract over the primitives the model does not understand and - this is the part that matters - to do so in a chosen direction:

This algorithm leads to an approximation of the ruleset. It can either be an overapproximation which results in a more permissive ruleset, or an underapproximation, which results in a stricter ruleset.

Which is what buys them their Theorem 2:

Any packet dropped by the translated, overapproximated simple firewall ruleset is guaranteed to be dropped by the real-world firewall, for arbitrary γ, Γ, rs.

That bounds the error: if even the permissive reading of your ruleset drops a packet, the real firewall drops it too, and that is a fact you may take to the bank.

Anabasis carries both readings simultaneously, in a single pass, because once the algebra exists the second reading costs next to nothing. Every predicate in the analysis is not a set but a bracket around one:

struct TriPredicate
{
    Bdd                           over;
    Bdd                           under;
    std::vector<UnknownPrimitive> reasons;
};

over is what the rule might match, under what it cannot avoid matching, and the truth, as is the way of these things, lies somewhere between. Written as an inclusion, the invariant the whole program maintains reads under ⊆ real ⊆ over. For a match that can be decided the two coincide and nothing is lost; for one that cannot, over = everything and under = nothing, which is the most honest statement available: this could be any packet, and nothing further can be promised.

The operations propagate the bracket in the obvious way: intersection intersects the two bounds, union unions them. It is worth pausing over why that is sound rather than merely plausible, and the reason is monotonicity. Shrink either input to an intersection or a union and the output can only shrink, which is to say that for any monotone g whatsoever,

and the bracket survives the operation untouched. Feeding such an operation lower bounds therefore yields a lower bound, and upper bounds an upper. Complement is the exception, complement being about as far from monotone as an operation gets, and the code shows what it does to a bracket:

TriPredicate negate(TriPredicate operand)
{
    return {.over = ~operand.under, .under = ~operand.over, ...};
}

The bounds trade places. The most a rule can match, negated, is the least its negation can match. Anyone who has used interval arithmetic has encountered the application of this principle before, and for the same reason: negate an interval and its endpoints swap. Get this the wrong way round and your uncertainty band quietly inverts into a certainty band - the precise failure the entire apparatus exists to prevent - and negated matches are anything but rare in real rulesets.

The difference over - under is the set of packets whose fate genuinely is not settled by the ruleset as this program understands it. I call it the uncertainty band, and much of the design is built around it.

What this logic represents

Look at one packet rather than at sets and the bracket collapses to a single value with three possible states: the packet lies in under and is certainly matched; it lies outside over and certainly is not; or it sits in the band, and the ruleset as read simply does not render a deterministic verdict. That is the nature of a three-valued logic, and it has a pedigree. Kleene introduced it in 1938 in order to talk about partial recursive functions, where the third value represented a computation whose result is undefined, and he denoted the three values as t, f and u in 1952 for precisely that reason. His truth tables are the ones the bracket arithmetic reproduces: unknown-and-false is false, unknown-and-true is unknown, unknown-or-true is true, and the negation of unknown is unknown, which is negate above as seen from a single packet’s point of view.

Please do not misconstrue the third value to be a probability, for it is not. It does not mean “matched about half the time”, nor “we lean towards yes”; it means the question is not settled by the information available to us, and the tool declines to pretend otherwise. The distinction sounds pedantic right up until one recalls that Anabasis is a compliance tool and nothing else: if a verdict is uncertain in any way, the only honest course is to render none, and to surface that finding in the report.

The heart of the matter

A single rule’s bracket gets us nowhere on its own. The chain walk from the first section carries a set of undecided packets from rule to rule, and that set must now be a bracket as well, because a rule the tool could not decide does not merely leave its own verdict in doubt; it leaves in doubt which packets reach the next rule at all.

The mechanism is a single small function, and it is the one I would point to if asked where the heart of the application logic resides:

void consume(TriPredicate& remaining, const TriPredicate& taken)
{
    remaining = {.over  = remaining.over  - taken.under,
                 .under = remaining.under - taken.over};
}

To make the consume function easily understandable, you may read it as two sentences. A packet is certainly still undecided only if the rule certainly did not take it, so the lower bound of what remains loses everything the rule might have matched. A packet might still be undecided unless the rule certainly did take it, so the upper bound of what remains loses only what the rule matched for certain. Note which bound is subtracted from which. The lower bound of what remains loses the rule’s upper bound, the upper bound loses the rule’s lower, and that crossing is the whole trick: keep it and every set that comes out the far end of the walk, accepted, dropped, returned, still brackets the real one.

The agreeable consequence is that the two readings from Diekmann’s paper, the permissive and the strict, need not be computed as two separate evaluations with the unknowns flipped first one way and then the other, for the uniform bracket arithmetic yields both at once: accepted.over is the permissive reading, accepted.under the strict one, and a single pass over the same rules delivers both. A queue verdict is the one place the code has to make an exception, since the packet’s fate is not visible to my software; it therefore lands squarely in the upper bound of both the accept set and the drop set, and in the lower bound of neither.

How assertions are handled

Nor does the three-valued logic need to be threaded through the assertion layer by hand, for it is a property of the implementation itself.

Take deny, an assertion that some flow must not be accepted. You have the flow’s packets as a set; call it the scope. Two questions arise:

• scope ∩ under - packets that are accepted under the strictest reading. If this is non-empty, then since under ⊆ real, the real firewall accepts traffic the policy forbids. That is a hard failure, and it arrives with a witness packet, courtesy of Satisfy-one as outlined in the last post.
• scope ∩ over - packets that are accepted under the most permissive reading. If the first set was empty but this one is not, then whether the policy holds depends on something the analysis has declined to pass a final verdict upon; therefore our verdict must be inconclusive.
• If both are empty, then since real ⊆ over, no packet of the flow is accepted by the real firewall either, and the assertion passes soundly.

allow is the mirror image: scope - over is what is definitely refused, scope - under what might be. The judge in the code is a single function shared by both, because once the sets have been chosen correctly the three-way decision is identical, and the only thing separating one assertion kind from another is which two sets get passed to it.

Set out beside one another, the whole judge amounts to six expressions:

and a rule that reads off those two columns and nothing else: non-empty on the left is a failure, empty on the left yet not on the right is inconclusive, and empty on both is a pass one may stand behind. only I have not mentioned until now, and it is the one that states most directly what an audit is usually after - “nothing beyond these flows is reachable on this path” - but as the table shows, it is not a third mechanism at all, merely deny with the permitted flows subtracted before the question is put.

Here is how the machinery handles being run against a ruleset built to break it. The fixture contains a rate-limited web rule, an osf match, a tproxy statement, and an SMTP rule that rejects unconditionally. This is the report, with nothing omitted but the file path and the fingerprint lines:

Undecided
  [inconclusive] web-must-be-reachable (allow input, ip)
      the ruleset may refuse traffic the specification requires
      example: ip tcp 0.0.0.0:0 -> 0.0.0.0:80 ct state new iif <other>
      traffic: ct state new l4proto tcp dport 80
      packets: 3.4e+38
      decided by inet/filter/input handle 12: match cannot be decided statically [match(implicit) l4proto == 6 match dport == 80 gate limit (unknown) verdict accept]
      undecidable: limit: matches on packet history rather than packet content
      undecidable: osf:{"key": "name"} : expression has no modelled left-hand side
      undecidable: {"addr": "127.0.0.1", "port": 50080}: unmodelled statement 'tproxy'

Satisfied
  [pass] smtp-must-be-blocked (deny input, ip)
      no packet of this flow is accepted

Two things deserve notice. The first is that the SMTP assertion still passes: uncertainty is local, it does not seep into the rest of the report, and a rule the tool fully understands still yields a sound verdict on the very same run. The second circumstance to be aware of is that the inconclusive finding names the rule, by chain and handle, and names all three constructs that contributed to the inconclusive verdict, which carries a certain likeness to the generals being sent for, don’t you think? The tool is not shrugging off uncertainty; it is telling an engineer precisely where to look and what it was unable to read so as to enable a prompt manual assessment of the situation at hand.

The bill, once again

None of this comes free, and the most honest way to present it is to showcase the scenario in which it degenerates.

If a ruleset opens by rate limiting everything, then the strict reading of it drops every packet, and the accept set under that reading is empty. Every allow assertion turns inconclusive at a stroke. Diekmann’s group ran into exactly this on a real device, a NAS appliance, and wrote up the result with admirable bluntness:

If the firewall features some rate-limiting for all packets in the beginning, the underapproximation is naturally a drop-all ruleset because the rate-limiting could apply to all packets. According to our metric, such a ruleset is of no use (but the only sound solution).

The parenthesis is the whole argument in four words. A useless answer that is true beats a useful one that might not be, for a useless answer will bring scrutiny by the only engine which may, with deliberation, resolve such a conundrum: the human brain.

In practice it is nowhere near the catastrophe it seems to be, because real rulesets do not use rate limits as a catch-all, but apply them rather selectively. The production dump I keep testing against, the one from the first post with its 23,621-address blocklist, yields a clean bill of health: eleven assertions, eleven satisfied, nothing undecided. The machinery we spent this article elaborating on did not fire once - yet, it has to be available all the same, for the same reason your seatbelt stays fastened during the parts of the drive in which you do not crash.

One further distinction has to be made, and it’s one that took me a while to get right: not everything the tool cannot determine is an unknown match. The same production ruleset ends in a masquerade rule, and the report says as much:

Assumptions
  chain postrouting: masquerade computes its target per packet,
  so where the traffic ends up is not determined by the ruleset

Masquerading per se does not equal an uncertainty band, for masquerade happens after filtering and cannot alter a filter verdict in the first place. Rather, it is an assumption: something outside the model on which the verdict does not depend, but which the reader nonetheless deserves to know lay outside the model. Undecidable matches render findings inconclusive; assumptions get stated and the findings stand. Conflate the two and you either drown the report in doubt or conceal real gaps, which is why separate language exists for such cases.

Making “I don’t know” routable

An answer nobody can act upon is not much of an improvement on a wrong one, so inconclusive is a first-class outcome the whole way out of the program.

It has an exit code of its own, 2, sitting between violations at 1 and the assorted error conditions above it. By default an undecided assertion does not fail a run, since the common case is a rate limit on SSH in an otherwise unremarkable ruleset and nobody wants a red pipeline on that account. Pass --fail-on-inconclusive and it does, which is the setting for those who would sooner block a release than ship a policy nobody has actually verified.

In SARIF, the format the tool emits for code scanning platforms, these findings carry kind: review, which the specification defines as a result that “requires review by a human user to decide if it represents a problem”, with the note that the value is intended for “tools that are unable to check for certain conditions, but that wish to bring to the user’s attention the possibility that there might be a problem”. That is an apt description of this exact situation, written by people who had never heard of it, which is about as much as one can reasonably ask of a standard.

This is precisely why the three-valued logic is a crucial component of Anabasis in the first place; it isn’t meant to showcase epistemic humility or act as an ornament, but much rather to clearly designate findings denoted as “I could not determine this, here is the rule, here is why” as a work item with an owner rather than have said findings not surface and advertise a false sense of security.

The army halted at the glen, sent for the people who could decide, and upon deliberation and arguments being had, continued their march. It did not guess and march.

What is still missing

The accept set I gestured at in the second section deserves the full treatment it did not receive here: first-match semantics as a fold, jumps and gotos, what return does to a set, the base chain policy, and the genuinely awkward one, NAT, which is no filter at all but a function that rewrites packets in the middle of the path and consequently forces you to ask your question about a packet that no longer exists in its previous form.

However, night looms, and as such, this entry will postpone further elaboration on that topic in favor of the rest even our army requires. Stay tuned for Book 4!