Skip to content

Refuse a policy that forbids what it requires (closes #322) - #387

Open
shubhamkataria2005 wants to merge 3 commits into
mainfrom
feat/322-policy-contradictions
Open

shubhamkataria2005 wants to merge 3 commits into
mainfrom
feat/322-policy-contradictions

Conversation

@shubhamkataria2005

Copy link
Copy Markdown
Collaborator

Closes #322 (US-30). My one task from #354.

What it does

A prohibition says traffic must be DENIED. A requirement says it must be PERMITTED. Two such rules over overlapping traffic on the same device and filter cannot both be satisfied — whichever way the network is configured, one of them reports a violation, and fixing it creates the other.

Before this the policy loaded cleanly and the scan ran. load_policy() now refuses it:

PolicyError: this policy contradicts itself, so no configuration could
satisfy it: rule 3 ('The LAN must not reach the finance server') forbids
what rule 7 ('Accounts must reach the finance server') requires on rtr-us5
filter acl_in: both describe src 10.10.10.64/26, dst 10.20.0.5/32,
dst ports 443

Against the acceptance criteria:

criterion
Pure logic over the policy file; no Batfish, no config ✅ no Batfish, Docker or Ollama; analysis/policy_conflicts.py imports only ipaddress and re
Reports the contradicting pair with both rule numbers and the overlap ✅ and the overlap is the intersection, not either rule restated
A contradiction blocks the scan ✅ raised from load_policy(), the gate every entry point goes through
#240's problem D ✅

The design decision I want reviewed hardest

Three answers, not two. Batfish header specifiers are a language — dstIps can read 0.0.0.0/0 \ (218.8.104.58, 10.20.0.5), ipProtocols can read !tcp. This module parses a deliberate subset and refuses to guess at the rest:

answer effect
overlap policy refused
no overlap loads
undecidable loads, and is reported on Policy.undecidable

The third is the whole safety argument. An undecidable pair is printed by the pipeline as warning:, never dropped, because treating "we could not compare these" as "these are fine" is F-4 arriving through the policy file.

The shipped docs/examples/policy.example.json proves it is not theoretical — it uses both set difference and a negated protocol, so it loads and reports two pairs it could not compare rather than a clean bill of health it has not earned.

An unmodelled query field makes a pair undecidable rather than being skipped, and that direction is deliberate: skipping a field would widen both header spaces and could invent an overlap that is not there, refusing a policy that is perfectly consistent. That is the failure I would most want someone to check me on.

What is deliberately not a contradiction

Two prohibitions over the same traffic are consistent — denying twice is denying — and so are two requirements. Rules on different devices or filters never collide. A rule's queries are a union, because policy_compliance fails the rule if any one fails.

The port case is the one worth seeing, because it is the real shape in the example file: 0-442,444-65535 against 443 is not an overlap, and a cruder check that noticed "both mention ports" would refuse a correct policy.

Mutation-tested rather than assumed

Each of the five mutations that matter fails the new tests:

undecidable collapses to "no overlap"      9 failed, 18 passed
unmodelled query fields ignored            2 failed, 25 passed
node/filter scope check dropped            2 failed, 25 passed
two prohibitions counted as a conflict     8 failed, 19 passed
overlap detail dropped from the message    1 failed, 26 passed

tests/test_suite_hygiene.py also earned its keep here — six of my first-draft tests asserted nothing and it named all six. They assert the positive property now.

Scope

policy_compliance only, because kind is its key and it is the only section whose rules can disagree about the same traffic this way. contradictions() takes entries and knows nothing about which section produced them, so another section gaining that shape is a call, not a rewrite.

Touches none of the three things #354 told me to stay out of: no web/, no analysis/checks/access_control.py, no tools/.

Verified

1848 passed, 42 skipped. ruff check . reports 8 errors, all pre-existing in docs/document-builds/ and identical on main — I left them alone, but they are in the folder rescued by #311 and someone may want them in a separate PR.

US-30. A `prohibition` says traffic must be DENIED; a `requirement` says it
must be PERMITTED. Two such rules over overlapping traffic on the same device
and filter cannot both be satisfied -- whichever way the network is
configured, one reports a violation, and fixing it creates the other.

Before this, that policy loaded cleanly and the scan ran. The user got a real
finding, fixed it, and got the opposite finding. Nothing said the rules were
at fault.

`load_policy()` now refuses it, naming both rules and the intersection:

    PolicyError: this policy contradicts itself, so no configuration could
    satisfy it: rule 3 ('The LAN must not reach the finance server') forbids
    what rule 7 ('Accounts must reach the finance server') requires on
    rtr-us5 filter acl_in: both describe src 10.10.10.64/26,
    dst 10.20.0.5/32, dst ports 443

The overlap is in the message because US-30 asks for it: naming only the pair
leaves the user diffing two header specifiers by eye.

Pure logic over the policy file. No Batfish, no Docker, no config.

PROVEN, NOT PRESUMED -- AND THE THIRD ANSWER

Batfish header specifiers are a language, not a list: `dstIps` can read
`0.0.0.0/0 \ (218.8.104.58, 10.20.0.5)` and `ipProtocols` can read `!tcp`.
analysis/policy_conflicts.py parses a deliberate subset and refuses to guess
at the rest, so every comparison has three answers:

    overlap        proven to share traffic      -> policy refused
    no overlap     proven disjoint              -> loads
    undecidable    outside the parsed subset    -> loads, and is REPORTED

The third one is the point. Undecidable pairs come out on
`Policy.undecidable` and the pipeline prints them as `warning:`, never drops
them. Treating "we could not compare these" as "these are fine" would be F-4
arriving through the policy file.

An unmodelled query field makes a pair undecidable rather than being skipped.
That direction is deliberate: skipping a field widens both header spaces and
could invent an overlap, refusing a policy that is consistent.

The shipped docs/examples/policy.example.json demonstrates it -- it uses both
set difference and a negated protocol, so it loads and reports two pairs it
could not compare, rather than a clean bill of health it has not earned.

MUTATION-TESTED RATHER THAN ASSUMED

Each of the five mutations that matter fails the new tests:

    undecidable collapses to "no overlap"        9 failed
    unmodelled query fields ignored              2 failed
    node/filter scope check dropped              2 failed
    two prohibitions counted as a conflict       8 failed
    overlap detail dropped from the message      1 failed

Scoped to `policy_compliance`, because `kind` is its key and it is the only
section whose rules can disagree about the same traffic this way.
`contradictions()` takes entries and knows nothing about the section, so
another section gaining that shape is a call, not a rewrite.

1848 passed, 42 skipped. ruff clean (the 8 pre-existing errors in
docs/document-builds/ are unchanged and also present on main).
@shubhamkataria2005

Copy link
Copy Markdown
Collaborator Author

@ARSH871-bot @SamikaPerera — gentle nudge, no rush. This closes #322, which was my one task from #354. It is clean against current main with CI green.

The thing most worth a reviewer's time is the third answer ("undecidable"). #324 now depends on it too: the corrected "never fires" definition I posted there today reuses policy_conflicts.overlap() from this PR.

@ARSH871-bot ARSH871-bot left a comment

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I reviewed ab9a784 in a detached worktree, and on scratch merges onto main dc93ccb (which now has #389) and onto #390. Everything below I re-ran; none of it is taken from the description.

What holds up

  • A proven contradiction is refused everywhere I tried. With your example file, python -m analysis.pipeline tests/fixtures/rtr-us5-secure --policy contra.json prints "Policy not loaded, so nothing was analysed." and then your message word for word. /api/policy returns 400 with the same text and stages nothing. Policy( is only built inside load_policy, so "the gate every entry point goes through" is true.
  • The before is real. On main the same file loads, and rtr-us5-secure reports PC-003 and PC-007.
  • No false refusals in the subset you parse. Adjacent /24s, 0-442 vs 443, different devices, different filters, udp vs tcp, two prohibitions and two requirements all load. I thought icmp-forbidden vs dstPorts-443-required was a false refusal, but Batfish's searchFilters(deny, dstIps=10.20.0.5, dstPorts=443) returned ICMP (type=8, code=0), so a ports-only space really does include ICMP and you're right to refuse it.
  • Numbers: 1848 passed / 42 skipped without Batfish, as you said. ruff shows the same 8 as main. Four of your five mutation counts reproduce exactly. "Undecidable collapses" gave me 5 or 10 depending on where it collapses, not 9, but it's caught either way.

Changes requested

  1. Protocol tokens are guessed — analysis/policy_conflicts.py:133-146. Anything not negated is taken as a protocol name. So "6", "tcp,udp" and ["tcp, udp"] never meet tcp/udp, and the pair loads as consistent with no warning. Batfish reads all three as real protocols: ipProtocols=["6"] returned a TCP (SYN) flow, and pybatfish splits "tcp,udp" into ['tcp','udp']. Repro:

    prohibition {"srcIps":"10.10.10.0/24","dstIps":"10.20.0.5","ipProtocols":["6"]}
    requirement {"srcIps":"10.10.10.64/26","dstIps":"10.20.0.0/16","ipProtocols":["tcp"],"dstPorts":"443"}
    

    This loads with undecidable == []. Swap "6" for "tcp" and it's refused. Scanned, PC-003 fires on the "6" rule with a TCP flow. That's "no contradiction" standing in for "didn't understand the token", which is the exact case your third answer exists for (overlap() says "Never guesses", line 226). Please split items on commas, map numbers or treat them as undecidable, and make anything outside a known name list undecidable.

  2. Filter scope is compared as raw strings — :242-243 and :268-269. ACL_IN vs acl_in is "different filter: cannot collide", silently. Batfish resolves ACL_IN, acl_in (trailing space), /acl_in/ and @in(GigabitEthernet0/0) all to acl_in on rtr-us5, while nonexistent raises. Repro: your example with the requirement's filter set to "ACL_IN" loads clean, and the scan reports both PC-003 and PC-007. Suggest comparing strip().casefold(). If two filters match only after normalising, or either uses specifier syntax (/ @ ( ,), report the pair as undecidable rather than skipping it. docs/policy-rules.md:374 ("never collide") needs the same qualifier. Node is fine as it is: a mis-cased node never runs.

  3. "Never dropped" holds on the CLI only — docs/policy-rules.md:396-397 and the PR body. /api/policy returns only renamed (web/main.py:2022). Uploading docs/examples/policy.example.json gives 200 with no mention of either pair, and python -m analysis.change_impact … policy.json doesn't print them either. So on the dashboard an undecidable pair is dropped silently. I know #354 kept you out of web/, so please change the wording to say the CLI prints them and the dashboard doesn't yet, and we'll open an issue for the UI. Also, deleting print(f"warning: {note}") at analysis/pipeline.py:886 fails no test. Please add one that runs pipeline.main() on the example policy and asserts two warning: lines.

Should-fix

  1. One unparseable field hides a disjoint parsed one — _parse(), :149-166. On the shipped example, rule 2 vs rule 4 says "could not be compared: ipProtocols=['!tcp']", but their dstIps are 10.20.0.5 and 218.8.104.58, which is provably disjoint on a field you do parse. So one of the two warnings the PR cites is wrong. Please compare field by field and return False as soon as any parsed field is disjoint. That can't invent an overlap, which is the direction you were worried about, because a conjunct only shrinks a space. If our own example produces a false warning, people will learn to skip the warnings.

Nits

  • overlap({"dstPorts":"1-100,50-200"},{"dstPorts":"60-70"}) gives dst ports 60-70,60-70.
  • The "Last, because…" ordering in load_policy isn't pinned. Moving the call above _assign_missing_numbers passes every test, and the message would then say "an unnumbered rule … an unnumbered rule". One test with no number fields would cover it.
  • tests/test_policy_contradictions.py:214 is relative to the current directory and fails when run from tests/. test_policy_example_is_valid.py anchors on Path(__file__).
  • The _COMPLEX comment mentions /, but the regex doesn't include it.
  • dstPorts: true is accepted as port 1.

Cross-PR: merges cleanly onto main dc93ccb and with #390. Without Batfish: main 1849/49, plus #387 1878/49, plus #390 1895/49. With Batfish: main 1885/13, plus #387 1914/13. No semantic overlap with #390. #389 loads through the same gate, so it refuses contradictions too.

Requesting changes for 1–3. Items 1 and 2 are your design's own rule applied to two places it missed, and both fixes are small.

…nings

Every item from @ARSH871-bot's review of ab9a784, each reproduced first.

1. Protocol tokens were guessed. Anything not negated was taken as a name,
   so "6", "tcp,udp" and ["tcp, udp"] never met tcp/udp and a real
   contradiction loaded as consistent. Batfish reads "6" as TCP. Protocols
   now come from a closed list -- tcp, udp, icmp by name or number -- with
   comma lists split the way pybatfish splits them. Anything else is
   undecidable, never a new protocol.

2. Filter scope compared raw strings, so ACL_IN vs acl_in was "different
   filter: cannot collide". Batfish resolves ACL_IN, "acl_in ", /acl_in/ and
   @in(...) to the same ACL. Filters that match only after strip/casefold,
   or that are specifiers (/ @ ( ,), now make the pair undecidable rather
   than skipped. Node is still compared exactly: a mis-cased node never runs.

3. "Never dropped" held on the CLI only. docs/policy-rules.md now says the
   pipeline and change_impact CLIs print each pair and the dashboard does
   not yet, pointing at #404. change_impact's CLI now prints them too, and
   two tests run both CLIs on the shipped example and count the warnings --
   deleting the pipeline's print used to fail nothing.

4. One unparseable field hid a disjoint parsed one. Comparison is now field
   by field: a query is a conjunction, so one provably disjoint field makes
   the pair disjoint whatever the others say. That cannot invent an overlap.
   The shipped example drops from two warnings to one; rule 2 vs rule 4 was
   false (10.20.0.5 vs 218.8.104.58).

Nits: overlapping port ranges are described once; a bool is not a port; the
"last, because" ordering in load_policy is pinned by a test with no numbers;
the example path is anchored on __file__; the _COMPLEX comment no longer
mentions "/".

Mutation-tested: unknown protocol accepted, commas not split, raw filter
compare, specifiers skipped, giving up at the first unparsed field, the
pipeline print removed, the check moved before numbering, and a bool port
each fail the tests. The "first unparsed field" mutant initially SURVIVED --
both disjoint-beats-unparsed tests put the disjoint field first in field
order -- so a test with the unparsed field first now pins it.

1932 passed, 13 skipped with Batfish running. ruff clean.
@shubhamkataria2005

Copy link
Copy Markdown
Collaborator Author

@ARSH871-bot — all of it is addressed in 8a190a3. I reproduced each item before fixing it, and under M-2 rule 1 your review is void now, so this needs a fresh look.

# your finding now
1 "6", "tcp,udp", ["tcp, udp"] load as consistent refused. Closed list (tcp/udp/icmp, plus 6/17/1), comma lists split like pybatfish does; anything else, e.g. "banana", is undecidable
2 ACL_IN vs acl_in skipped as "cannot collide" undecidable, and so are acl_in , /acl_in/ and @in(GigabitEthernet0/0). acl_out vs acl_in is still skipped. Node compared exactly, as you said
3 "never dropped" is CLI-only docs say exactly that and point to #404, which I opened for the dashboard. change_impact's CLI prints them too now, and two tests run both CLIs on the example and count the warning: lines
4 one unparsed field hides a disjoint one field by field now. The example drops from two warnings to one; rule 2 vs rule 4 was the false one

All five nits are done: ports described once, dstPorts: true is undecidable, the ordering is pinned by a test with no number fields, the example path is anchored on __file__, and the _COMPLEX comment is fixed.

One thing your review caught that I should have caught myself. When I mutation-tested fix 4, the "give up at the first unparsed field" mutant survived. Both of my disjoint-beats-unparsed tests put the disjoint field before the unparsed one in field order, so the early return never mattered. There's now a test with an unparsed srcIps ahead of a disjoint dstIps, and the mutant fails.

On your icmp note: thank you for checking that against Batfish before calling it a false refusal. A ports-only space does include ICMP, so it stays refused.

1932 passed, 13 skipped with Batfish running, merged with current main (dc93ccb). ruff clean.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

US-30 — Tell me if my own policy contradicts itself

2 participants