From 73700e17500050f51bff95a48d70979d6740dd66 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 00:12:01 +0530 Subject: [PATCH 1/8] P5b step 0: record the P5a mini-gate verdict (PHASE_GATES) Co-Authored-By: Claude Sonnet 5.5 --- docs/PHASE_GATES.md | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/docs/PHASE_GATES.md b/docs/PHASE_GATES.md index e8ec6ff..efb1ac4 100644 --- a/docs/PHASE_GATES.md +++ b/docs/PHASE_GATES.md @@ -123,7 +123,22 @@ C-120(c) is decided (unresolved direction form is UNSUPPORTED) and is a P5 gate D4; C-130 before D5; C-137 to C-143 Proposed. ``` -## P5–P10 — NOT STARTED +## P5a — Verification, part 1 (security predicates) + +```text +P5a mini-gate: PASSED (external review, 29 Oct 2026; PR #21 at 247a6c6, merged before the +verdict, C-28 process lapse recorded a fourth time). Suite passes on Python 3.12 and 3.13 +(skipped=1); black, ruff and mypy clean. 60 of 60 SEC fixture cells equal expected.json (Claude +Code report); reviewer probes (about 40) found no unsound result other than C-150. +Carry-forward: (1) add CIDR boundary tests (one-address gap, uncovered last address, single-address +member advancing the cursor); three mutants of covers() survive; fix in P5b step 0 or P5b step 1, +no behaviour change. (2) C-150 Open: registry v1.1 amendment before D4, SEC-001/002 version bump, +oracle must match; limitation stated until then. (3) index_rules placeholder hazard: cleanup +with C-143 option B before D4. C-148 NOT_APPLICABLE question goes to the authors. C-144 to C-148 +Proposed; C-149, C-150 Open. C-120(c) verified in source; probe in the P5 gate. +``` + +## P5b–P10 — NOT STARTED ## Temporary exceptions From bb61d2878187733c16e84051e644072e92dd89fc Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 00:14:58 +0530 Subject: [PATCH 2/8] =?UTF-8?q?P5b=20step=201:=20CIDR=20boundary=20tests?= =?UTF-8?q?=20for=20covers()=20(registry=20=C2=A72.5,=20=C2=A73.3;=20C-146?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One missing address in the middle, the first or the last address uncovered, a single-address member at the cursor, consecutive single-address members tiling a network, and order and duplicates, for IPv4 and IPv6. Tests only; nothing under core/ changes. Scratch-copy proof (outside the repository): the three mutants named in the P5a verdict (first > cursor + 1; return cursor >= wanted.last; member.last > cursor) all survive the 12 existing verification test files (396 tests) and are all killed by the new tests. Co-Authored-By: Claude Sonnet 5.5 --- tests/unit/test_verification_cidr_ports.py | 91 ++++++++++++++++++++++ 1 file changed, 91 insertions(+) diff --git a/tests/unit/test_verification_cidr_ports.py b/tests/unit/test_verification_cidr_ports.py index a0387cd..4797e1c 100644 --- a/tests/unit/test_verification_cidr_ports.py +++ b/tests/unit/test_verification_cidr_ports.py @@ -136,6 +136,97 @@ def _brute_force(self, version: int, window: str, prefixes: range, seed: int) -> self.assertGreater(misses, 30) +class TestCoverageBoundaries(unittest.TestCase): + """P5a carry-forward 1: the edges of the sweep, where an off-by-one would hide. + + A target network ``T`` covers the addresses ``first..last``. Members are built by cutting that + range into CIDRs with ``summarize_address_range`` (input construction only: the expected answer + follows from which addresses are left out, never from ``covers``). For each family: + + * a set that leaves out exactly one address in the middle does not cover ``T``; adding that + address as a single-address member makes it cover; + * leaving out only the last address (or only the first) does not cover; adding it does; + * a single-address member (``/32``, ``/128``) at the cursor advances it: ``[x/32]`` covers + ``x/32``, consecutive single-address members cover the network they tile, and a single + address next to the target does not cover it; + * order and duplicates never change any of these answers. + """ + + TARGETS = ("10.0.0.0/24", "2001:db8::/120") + + @staticmethod + def cut(first: int, last: int, version: int) -> list[str]: + """The CIDRs that exactly tile the addresses first..last (empty when first > last).""" + if first > last: + return [] + make = ipaddress.IPv4Address if version == 4 else ipaddress.IPv6Address + return [str(net) for net in ipaddress.summarize_address_range(make(first), make(last))] + + @staticmethod + def single(value: int, version: int) -> str: + make = ipaddress.IPv4Address if version == 4 else ipaddress.IPv6Address + return f"{make(value)}/{32 if version == 4 else 128}" + + def each_family(self) -> list[tuple[str, int, int, int]]: + found = [] + for target in self.TARGETS: + net = ipaddress.ip_network(target) + found.append( + (target, net.version, int(net.network_address), int(net.broadcast_address)) + ) + return found + + def check_every_order(self, members: list[str], target: str, expected: bool) -> None: + rng = random.Random(len(members) * 31 + int(expected)) + variants = [members, [*members, *members]] + for _ in range(4): + shuffled = [*members, members[0]] if members else [] + rng.shuffle(shuffled) + variants.append(shuffled) + for variant in variants: + self.assertIs(covers(variant, target), expected, (target, variant)) + + def test_one_missing_address_in_the_middle(self) -> None: + for target, version, first, last in self.each_family(): + gap = first + (last - first) // 2 + 1 # not at an edge, not on a CIDR boundary + around = [*self.cut(first, gap - 1, version), *self.cut(gap + 1, last, version)] + with self.subTest(target=target): + self.check_every_order(around, target, False) + self.check_every_order([*around, self.single(gap, version)], target, True) + + def test_the_last_address_uncovered(self) -> None: + for target, version, first, last in self.each_family(): + short = self.cut(first, last - 1, version) + with self.subTest(target=target): + self.check_every_order(short, target, False) + self.check_every_order([*short, self.single(last, version)], target, True) + + def test_the_first_address_uncovered(self) -> None: + for target, version, first, last in self.each_family(): + short = self.cut(first + 1, last, version) + with self.subTest(target=target): + self.check_every_order(short, target, False) + self.check_every_order([self.single(first, version), *short], target, True) + + def test_a_single_address_member_advances_the_cursor(self) -> None: + for _target, version, first, _last in self.each_family(): + one = self.single(first + 5, version) + with self.subTest(family=version): + self.assertTrue(covers([one], one)) + self.assertFalse(covers([one], self.single(first + 6, version))) + self.assertFalse(covers([one], self.single(first + 4, version))) + + def test_consecutive_single_address_members_tile_a_network(self) -> None: + for _target, version, first, _last in self.each_family(): + bits = 30 if version == 4 else 126 + network = f"{ipaddress.ip_address(first)}/{bits}" + tiles = [self.single(first + offset, version) for offset in range(4)] + with self.subTest(family=version): + self.check_every_order(tiles, network, True) + self.check_every_order(tiles[:3], network, False) # the fourth is missing + self.check_every_order([tiles[0], tiles[1], tiles[3]], network, False) + + class TestCoverageOracle(unittest.TestCase): """The work package's oracle: the address space is cut into 64 blocks (the /6 networks), a CIDR of prefix length 1 to 6 is a run of consecutive blocks, and coverage is plain set containment of From 8cc729fa91fa8e0f1b115720b64be74cd1f69e93 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 00:19:41 +0530 Subject: [PATCH 3/8] =?UTF-8?q?P5b=20step=202:=20register=20rows=20C-151?= =?UTF-8?q?=20to=20C-154=20(Proposed),=20FUNC=20reason=20codes,=20R17=20se?= =?UTF-8?q?lf-test=20for=20the=20new=20modules=20(registry=20=C2=A76;=20C-?= =?UTF-8?q?151=20to=20C-154)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit C-151 boundary, entry and parameters; C-152 endpoint resolution across moves and indeterminate endpoints; C-153 rows 1 to 9 and the definitions they need (src_sg, self, partly covers, could satisfy, ADDR(S), M3, the R5 cases); C-154 assumptions, observations and the baseline list. Ten closed reason codes are added to the vocabulary. The R17 self-test names the two modules that step 3 and 4 add; it fails when R17 is broken (shown in a scratch copy). Co-Authored-By: Claude Sonnet 5.5 --- core/domain/verification.py | 11 ++++++++++ docs/DECISIONS_REGISTER.md | 4 ++++ .../contract/test_architecture_boundaries.py | 22 +++++++++++++++++++ tests/unit/test_verification_domain.py | 16 ++++++++++++++ 4 files changed, 53 insertions(+) diff --git a/core/domain/verification.py b/core/domain/verification.py index 6bb6f8a..1b842f0 100644 --- a/core/domain/verification.py +++ b/core/domain/verification.py @@ -119,6 +119,17 @@ class VerificationReason(StrEnum): CONSISTENCY_FINDING = "consistency.finding" VERIFIER_NOT_AVAILABLE = "verifier.not_available" VERIFIER_ERROR = "verifier.error" + # INV-FUNC-001 (C-151, C-153) + PARAMETERS_INVALID = "parameters.invalid" + ENDPOINT_ABSENT = "endpoint.absent" + PORT_MISMATCH = "port.mismatch" + VPC_MISMATCH = "vpc.mismatch" + PATH_MISSING = "path.missing" + COVERAGE_PARTIAL = "coverage.partial" + ROUTE_UNSUPPORTED = "route.unsupported" + INTERFACE_UNSUPPORTED = "interface.unsupported" + VALUE_UNSUPPORTED = "value.unsupported" + MODEL_UNSUPPORTED = "model.unsupported" # --- helpers -------------------------------------------------------------------------------------- diff --git a/docs/DECISIONS_REGISTER.md b/docs/DECISIONS_REGISTER.md index aab6266..814773e 100644 --- a/docs/DECISIONS_REGISTER.md +++ b/docs/DECISIONS_REGISTER.md @@ -162,3 +162,7 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-148 | P5a: baseline verification and types with no predicate | P4 emits a `RESOURCE` work item (class BASELINE) per CREATED resource. For a created `aws_security_group` or `aws_security_group_rule` the item runs `PIP(22)` and `PIP(5432)` and reports the clauses of the groups that resource contributes to; the item result is the worst of the two, restricted to those groups (the restriction narrows the observations only; it never turns another group's FAIL into PASS, which the invariant items still carry). A created `aws_db_instance`: the SEC-003 flag of that instance. A created resource of a relevant-unsupported type: UNSUPPORTED. A created resource inside an indeterminate (placeholder) block: UNKNOWN. **A created resource of any other type: PASS with `applicable = false`**, and the assumption `registry-v1.0 declares no baseline predicate for ` (Doc 08 §16; registry §2.7: every other unsupported type is declared irrelevant). **This is an explicit modelling assumption that the paper must state, not a proof. Flagged for the authors:** the alternative is a distinct NOT_APPLICABLE outcome that never counts as proof. **Step 5 details:** the verifier of a security-group or rule item is that of INV-SEC-001 in the definitions given, of a database item that of INV-SEC-003, of a not-applicable item the DAIL-internal `dail.verify.baseline` version `1` (not a registry §10 identity); a definition set without the invariant makes the item UNSUPPORTED `invariant.unknown`, never PASS. The relevant-unsupported list used is the security-group list of registry §2.7 (the INV-FUNC-001 list joins in P5b). A placeholder of any type is UNKNOWN with the new reason `resource.indeterminate`; an unreadable (UNSUPPORTED) security group, rule or database is UNSUPPORTED `rule.unsupported`; a work item naming a resource the candidate does not have is UNSUPPORTED `structural.finding` (and a structural finding). Observations: `resource`, `resource_type`, and `groups` and `predicates` (per port, per clause) for groups and rules, or `value` for a database. | Proposed (P5a) | | C-149 | P5a: the stored view does not say which field of a rule is unresolved (R1) | Registry §3.3 makes `possible4(g)` depend on a rule's IPv4 sources being unresolved and `possible6(g)` on its IPv6 sources, apart from the protocol and ports. The stored rule view (`security_attributes`) has `determinate` and `problems` (reason codes such as `variable.no_value`), but a reason does not name the field, and an unresolved list is stored as `[]`. So `func_unknown_dependency_unknown_v1` (an ingress rule on 5432 whose **source group** is unknown, expected clauses PASS and PASS) cannot be told from a rule with an unknown CIDR list by the view alone. **Resolution used:** for an `aws_security_group_rule` the verifier reads the rule's own `attributes` (C-112 encoding, which holds every configured argument) and derives, per field, whether it is unresolved: exact. For inline rules the stored blocks are in `attributes` too, but the view sorts them, so a rule cannot be paired with its block without redoing P3a's canonicalisation; the verifier takes the **union over the indeterminate blocks of one direction** of the family flags (IPv4 list unresolved, IPv6 list unresolved) and gives them to every indeterminate inline rule of that direction. This can only add UNKNOWN (never remove it); it differs from the registry text only for a group with two or more indeterminate inline blocks in one direction that are unresolved in different families, and then only at clause level unless a third block explains the first. No fixture or vector is affected. **Question for the authors:** accept this, or extend the P3a view (a P3a change) to record the unresolved fields per rule? | Open (found 28 Oct 2026; P5a) | | C-150 | P5a: registry §3.3 drops an indeterminate rule whose sources are known | Registry §3.3 defines `possible4(g)` as an indeterminate rule that could permit TCP/p **and** whose IPv4 sources are unresolved or include a prefix list (`possible6` likewise). A rule whose protocol or port is unresolved but whose IPv4 source is known, for example `from_port = var.p` with `cidr_blocks = ["0.0.0.0/0"]`, is indeterminate, could permit the port, but has resolved sources, so it is not `possible`, is not in `D(g)` (not determinate), and the registry text gives PASS although the rule may open the port to the internet. **Implemented verbatim** (work package: no reinterpretation), pinned by `TestRegistryGap` in `tests/unit/test_verification_public_ingress.py`, and the rule is reported in the observation `indeterminate_rules`. It is the one place where the registry text lets a PASS stand on a rule whose meaning is unresolved, against "uncertainty is never a pass" (CLAUDE.md). The independent oracle follows the same text, so the two would agree and both be unsound for this case. **Proposed amendment, for the authors:** `possible` also when the family's sources are known and non-empty (what C-146 already does for a rule with an unresolved direction); a new registry file and version bump under C-85. **Question: amend, or accept and state as a limitation?** | Open (found 28 Oct 2026; P5a step 4) | +| C-151 | P5b: FUNC verifier boundary, entry and parameters | `core/verification/reachability.py` (the predicate) and `core/verification/func_view.py` (the reader of the stored resources) import only the standard library and `core.domain`, like the rest of `core.verification` (contract rule R17, nothing loosened; the self-test now names both modules). The verifier is registered in `dispatch.DEFAULT_VERIFIERS` under `dispatch.REACHABILITY_CFG` = `("dail.verify.reachability_cfg", "1")`, read from the definition, not retyped; a pair that is missing from the table is still UNSUPPORTED `verifier.not_available`. Entry: `evaluate_reachability(definition, inputs) -> PredicateOutcome`. The endpoints are `definition.predicate["parameters"]` = `{S, D, port}`; a definition without text `S` and `D`, with `S == D`, or with `port != 5432` is UNSUPPORTED `parameters.invalid`, never PASS. An endpoint of the wrong type (S not an `aws_instance`, D not an `aws_db_instance`) is UNSUPPORTED `parameters.invalid`. A stored value the reader cannot read raises `ViewError`, which the engine turns into VERIFIER_ERROR; "cannot read" is never "absent". **Shared code:** the MIXED test (registry §2.6) moves from `public_ingress` to `views.group_is_mixed` and RETAINED-INLINE gets a direction parameter (`retention.inline_retention`, with `ingress_retention` as the same call for ingress), so FUNC reads the egress of `SG(S)` and the ingress of `SG(D)` with the one definition; `views.Rule` gains the flags `sources_unresolved` and `self_unresolved` (read like the family flags of C-149); `cidr.py` gains `overlaps`. The SEC results are unchanged and the whole SEC test suite is the check. New reason codes (closed vocabulary): `parameters.invalid`, `endpoint.absent`, `port.mismatch`, `vpc.mismatch`, `path.missing`, `coverage.partial`, `route.unsupported`, `interface.unsupported`, `value.unsupported`, `model.unsupported`. | Proposed (P5b) | +| C-152 | P5b: endpoint resolution across moves, and indeterminate endpoints | The bindings `S` and `D` are addresses of the **trusted** state (registry §6.1). A baseline resolves a binding by address in the candidate; an address that no candidate resource has is absent (row 1, FAIL, `endpoint.absent`). A candidate with a parent resolves it through the identity report (registry §2.3, moves followed): the match whose `trusted_resource_ref` is the binding; UNCHANGED, MODIFIED and REPLACED give the candidate resource of the match; **DELETED is absent** (row 1); **UNCERTAIN, a placeholder (unknown `count` or `for_each`, support status UNKNOWN) and a resource that is itself UNSUPPORTED are indeterminate**: UNKNOWN (row 4), never FAIL, never PASS. **Registry reading, flagged:** registry §2.4 would call an UNSUPPORTED endpoint resource UNSUPPORTED rather than UNKNOWN; the work package says UNKNOWN and both are lack of proof, so the work package is followed and the question goes to the reviewer. A candidate that has a parent but no identity report, or a report with no match for the binding while the parent has the resource, is UNSUPPORTED `identity.missing` (as in P5a). A binding that the parent does not have either is UNSUPPORTED `parameters.invalid` (the definitions and the trusted state disagree). **A created endpoint** (the candidate creates the resource at another address and the old one is DELETED) is FAIL by row 1: no heuristic match is made; only a `moved` block or an identity match ties a new address to the trusted one. The observation `endpoints` records, per binding, the trusted address, the match change type and the candidate address. | Proposed (P5b) | +| C-153 | P5b: rows 1 to 9 and the definitions they need | The rows of registry §6.4 are evaluated in order and the first that applies returns. Row 2 collects every cause it can evaluate, reports all of them in the observation `row2_causes` and names the reason by the first in this fixed order: relevant-unsupported type, M3 route, `propagating_vgws`, interface block, name-based `security_groups`, no `vpc_security_group_ids` or no `subnet_id`, MIXED, RETAINED-INLINE, `unresolved` direction form (C-120(c)), unsupported value or rule, other. **Definitions** (each with the registry text it makes precise): `SG(S)` and `SG(D)` are the groups that the `vpc_security_group_ids` of `S` and `D` reference; `src_sg(r)` is `source_security_groups` of the stored rule view (a reference gives the address of the group; a literal AWS id gives `EXTERNAL:` and matches no configured group), so "src_sg(r) contains a group in SG(D)" is a non-empty intersection of addresses; `self(r)` is the stored `self` flag and E6 needs `h in SG(S)`; the CIDR clauses use `cidr.covers` on the IPv4 sources of determinate rules that permit TCP/5432 (`ports.permits_tcp`), pooled over the groups of the side; **"partly covers"** (row 8) is `cidr.overlaps`: the pooled sources of rules that permit TCP/5432 intersect the target but do not contain it (interval arithmetic, no enumeration); `ADDR(S)` is `private_ip/32` if it resolves to an IPv4 address, else the `cidr_block` of the subnet of `S`; an unresolved subnet CIDR makes the clause unresolved. **"An indeterminate rule could satisfy" E5 or E6** (row 7): a rule of the side (an egress rule of a group in `SG(S)` for E5, an ingress rule of a group in `SG(D)` for E6, a rule with direction `None` for either, a rule of an `UNRESOLVED:*` pseudo-group, a rule resource that is an UNKNOWN placeholder) that is not determinate, is not unsupported, **could permit TCP/5432** (`ports.may_permit_tcp`, so an unresolved protocol or port counts) **and whose satisfying side could match**: its group sources are unresolved or could be the other side's groups, its IPv4 sources are unresolved, include a prefix list, or cover or partly cover the target, or (E6) its `self` is unresolved. **Counted:** an indeterminate rule with a resolved satisfying source and an unresolved port or protocol is counted (UNKNOWN), because the rule could supply the permission; this is the safe direction and it is the mirror of the gap of C-150 (where SEC `possible` text drops such a rule and can give PASS); here dropping it could give an unsound FAIL, so it is not dropped. When both E5 and E6 fail, row 7 applies if either failing condition could be satisfied by an indeterminate rule (registry text: "it"; the more cautious reading), then row 8. **Where the registry is silent (R5), UNSUPPORTED and listed as a spec gap:** a `vpc_id` of a group in `SG(D)`, of `S`'s subnet or of a route table that is a literal id rather than a reference to a configured `aws_vpc` (the VPC CIDR is then unknown); a literal AWS id in `vpc_security_group_ids`; `D` with neither `port` nor `engine`; a route table whose `vpc_id` is unresolved and that has an M3 candidate route or `propagating_vgws` (it may be the VPC of `D`); an unresolved or unsupported route destination or target in a route table of `VPC(D)`, a dynamic route expansion that cannot be fixed, an unsupported value of a field the path reads, an invalid `private_ip`. **Unresolved values (row 4):** an unresolved `vpc_security_group_ids`, group `vpc_id`, `subnet_id`, subnet `vpc_id` or an unresolved `D.port` (**gap:** registry row 4 names E3 and E4 but not E2; an unresolved E2 cannot be PASS, so it is UNKNOWN). **M3:** a route of a route table of `VPC(D)` whose IPv4 `cidr_block` lies inside the CIDR of that VPC and whose target is not `local` (`gateway_id = "local"` and no other target); IPv6-only routes are not read (M5); a route wider than the VPC CIDR never applies. Rows 3 and 5 FAIL only on resolved values. | Proposed (P5b) | +| C-154 | P5b: assumptions, observations and the baseline list | The result's `assumptions`, sorted: `IPv4 only`, `M1: RDS security groups and subnet group share one VPC (C-15, C-77, uncited)`, `M4: default network ACL assumed (no NACL type present)`, and `tolerated type: aws_db_subnet_group (C-15)` when that type is present. Closed observation keys: `row`, `reason`, `endpoints`, `port`, `path` (`S`, `subnet`, `vpc_s`, `sg_s`, `egress_rule`, `sg_d`, `ingress_rule`, `vpc_d`; a part that is not reached is null), `row2_causes`, `failing_conditions`, `indeterminate_rules`, `partial_coverage`, `relevant_unsupported`. `baseline.py`: the relevant-unsupported list of a created resource becomes the 26 types of registry §2.7 for INV-FUNC-001 (`core.domain.registry_v1.FUNC_RELEVANT_UNSUPPORTED`, which contains the three of the security list), so a created resource of any of them is UNSUPPORTED `type.relevant_unsupported`, not PASS with `applicable = false`; the predicate lists for INV-SEC-001/002 do not change. | Proposed (P5b) | diff --git a/tests/contract/test_architecture_boundaries.py b/tests/contract/test_architecture_boundaries.py index b14e4c2..276d590 100644 --- a/tests/contract/test_architecture_boundaries.py +++ b/tests/contract/test_architecture_boundaries.py @@ -588,6 +588,28 @@ def test_r17_allows_core_domain_itself_and_the_standard_library(self) -> None: with self.subTest(module=module, source=source.splitlines()[0]): self.assertNotIn("R17", self.rules_for(module, source)) + def test_r17_covers_the_functional_verifier_modules(self) -> None: + # C-151: the reachability verifier and its reader are under the same rule as the rest + for module in ("core.verification.reachability", "core.verification.func_view"): + for source in ( + "from core.terraform_model import security_rules\n", + "from core.dependency import build\n", + "from core.identity import engine\n", + "from core.impact import engine\n", + "from core.persistence import sqlite\n", + "import evidence.store\n", + ): + with self.subTest(module=module, source=source.strip(), allowed=False): + self.assertIn("R17", self.rules_for(module, source)) + for source in ( + "from core.domain.registry_v1 import FUNC_RELEVANT_UNSUPPORTED\n", + "from core.verification.views import read_security\n", + "from .cidr import covers, overlaps\n", + "import ipaddress\n", + ): + with self.subTest(module=module, source=source.strip(), allowed=True): + self.assertNotIn("R17", self.rules_for(module, source)) + def test_r17_applies_only_to_the_verification_engine(self) -> None: for module in ("core.impact.ok", "core.identity.ok", "core.application.ok"): self.assertNotIn("R17", self.rules_for(module, "from core.domain import hashing\n")) diff --git a/tests/unit/test_verification_domain.py b/tests/unit/test_verification_domain.py index 266f20a..5fe83aa 100644 --- a/tests/unit/test_verification_domain.py +++ b/tests/unit/test_verification_domain.py @@ -72,6 +72,22 @@ def test_the_aggregate_results_of_doc_09_s18(self) -> None: def test_the_construction_statuses(self) -> None: self.assertEqual({c.value for c in ConstructionStatus}, {"OK", "INVALID", "UNSUPPORTED"}) + def test_the_functional_predicate_reason_codes_of_c_151(self) -> None: + # C-151: the closed codes the reachability verifier reports, besides the P5a ones + wanted = { + "parameters.invalid", + "endpoint.absent", + "port.mismatch", + "vpc.mismatch", + "path.missing", + "coverage.partial", + "route.unsupported", + "interface.unsupported", + "value.unsupported", + "model.unsupported", + } + self.assertTrue(wanted <= {c.value for c in VerificationReason}) + def test_reason_codes_are_dotted_lower_case_text(self) -> None: for code in VerificationReason: self.assertRegex(code.value, r"^[a-z_]+(\.[a-z_]+)+$") From ef9d96eda39e39b1928e5cd7035192b6cd240d51 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 00:25:03 +0530 Subject: [PATCH 4/8] =?UTF-8?q?P5b=20step=203:=20readers=20for=20the=20INV?= =?UTF-8?q?-FUNC-001=20inputs=20(registry=20=C2=A76.2,=20=C2=A76.3,=20?= =?UTF-8?q?=C2=A76.6;=20C-151,=20C-153)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit func_view.py reads instance, database, subnet, VPC, group VPC and route table from the stored C-112 encoding into frozen views. A fact is absent, known, unknown or unsupported; a stored shape that cannot be read is a ViewError, never absent; a placeholder keeps its support status so it is not mistaken for a resource without the argument. Routes carry a destination state and a local/other/unresolved target; interface blocks and propagating_vgws are read as presence. Tests first (module not found), including every functional resource of every fixture. 13 deliberate breakages checked; two survivors got tests. Co-Authored-By: Claude Sonnet 5.5 --- core/verification/func_view.py | 381 ++++++++++++++++++++++++ tests/func_builders.py | 60 ++++ tests/unit/test_reachability_readers.py | 358 ++++++++++++++++++++++ 3 files changed, 799 insertions(+) create mode 100644 core/verification/func_view.py create mode 100644 tests/func_builders.py create mode 100644 tests/unit/test_reachability_readers.py diff --git a/core/verification/func_view.py b/core/verification/func_view.py new file mode 100644 index 0000000..2c81d0c --- /dev/null +++ b/core/verification/func_view.py @@ -0,0 +1,381 @@ +"""The verifier's reader of the INV-FUNC-001 inputs (registry §6.2, §6.3, §6.6; C-151, C-153). + +Typed, frozen views of the stored resources the reachability predicate reads: the instance ``S``, +the database ``D``, a subnet, a VPC, a security group's VPC and a route table. They are built on +``values.decode`` from ``Resource.attributes`` (the C-112 encoding keeps every configured argument), +so a field the registry's footprint (§6.6) names is always there to be read. + +**A fact is one of four things** (``Fact.state``): ``absent`` (the argument is not written, or is +an explicit null, which the provider reads as "not set"), ``known`` (a value; a reference is a known +``Ref``), ``unknown`` (it cannot be fixed from the configuration and variable values) and +``unsupported`` (a construct DAIL does not implement, or an argument written as a block where a +value is expected). A list is a known value even when an element is unresolved; ``items_of`` yields +the elements with the unresolved ones as ``Unknown`` or ``Unsupported`` objects. + +**A stored shape the reader cannot read raises ``ViewError``**; it is never "absent". A resource of +the wrong type is also a ``ViewError``. A placeholder (UNKNOWN support: its ``count`` or +``for_each`` could not be fixed) is read with an empty ``attributes``, so every fact is ``absent``; +the view keeps ``support`` so that the predicate never mistakes a placeholder for a resource +without the argument. + +Standard library and ``core.domain`` only. +""" + +from __future__ import annotations + +from collections.abc import Mapping +from dataclasses import dataclass +from typing import Any, Final + +from core.domain.enums import ResourceSupport +from core.domain.jsonvalue import thaw_json +from core.domain.resource import Resource +from core.verification.cidr import CidrError, Network, parse_network +from core.verification.values import ( + Argument, + SetValue, + Unknown, + Unsupported, + ValueDecodeError, + decode_argument, +) +from core.verification.views import ViewError + +ABSENT_STATE: Final = "absent" +KNOWN: Final = "known" +UNKNOWN_STATE: Final = "unknown" +UNSUPPORTED_STATE: Final = "unsupported" + +_INTERFACE_ARGUMENTS: Final = ("network_interface", "primary_network_interface") +_ROUTE_TARGETS: Final = ( + "gateway_id", + "nat_gateway_id", + "network_interface_id", + "transit_gateway_id", + "vpc_peering_connection_id", + "vpc_endpoint_id", + "egress_only_gateway_id", + "carrier_gateway_id", + "core_network_arn", + "local_gateway_id", + "instance_id", +) + + +@dataclass(frozen=True, slots=True) +class Fact: + state: str + value: Any = None + reason: str | None = None + + +ABSENT: Final = Fact(ABSENT_STATE) + + +def _fact_of_value(value: Any) -> Fact: + if value is None: + return ABSENT + if isinstance(value, Unknown): + return Fact(UNKNOWN_STATE, reason=value.reason) + if isinstance(value, Unsupported): + return Fact(UNSUPPORTED_STATE, reason=value.reason) + return Fact(KNOWN, value) + + +def _fact_of_argument(argument: Argument) -> Fact: + if argument.form != "ATTRIBUTE": + return Fact(UNSUPPORTED_STATE, reason="form.block") + return _fact_of_value(argument.value) + + +def _argument(encoded: object, where: str) -> Argument: + try: + return decode_argument(encoded) + except ValueDecodeError as error: + raise ViewError(f"{where}: {error}") from None + + +def items_of(fact: Fact) -> tuple[Any, ...]: + """The elements of a fact: none if absent, the one value if it is not a collection, and the + unresolved fact as one ``Unknown`` or ``Unsupported`` item.""" + if fact.state == ABSENT_STATE: + return () + if fact.state == UNKNOWN_STATE: + return (Unknown(fact.reason or ""),) + if fact.state == UNSUPPORTED_STATE: + return (Unsupported(fact.reason or ""),) + if isinstance(fact.value, tuple): + return fact.value + if isinstance(fact.value, SetValue): + return fact.value.items + return (fact.value,) + + +def _attributes(resource: Resource, expected_type: str) -> dict[str, Any]: + if resource.resource_type != expected_type: + raise ViewError(f"{resource.address}: a {resource.resource_type}, not an {expected_type}") + return dict(thaw_json(resource.attributes)) + + +def _read(attributes: Mapping[str, Any], name: str, owner: str) -> Fact: + if name not in attributes: + return ABSENT + return _fact_of_argument(_argument(attributes[name], f"{owner}.{name}")) + + +def _has_blocks(encoded: object, where: str) -> bool: + """Whether an argument that holds blocks (or a list of them) holds any, or might.""" + argument = _argument(encoded, where) + if argument.form != "ATTRIBUTE": + return bool(argument.blocks) or bool(argument.indeterminate) + value = argument.value + if value is None: + return False + if isinstance(value, Unknown | Unsupported): + return True + if isinstance(value, tuple): + return len(value) > 0 + if isinstance(value, SetValue): + return len(value.items) > 0 + return True + + +@dataclass(frozen=True, slots=True) +class InstanceView: + address: str + support: ResourceSupport + subnet_id: Fact + vpc_security_group_ids: Fact + security_groups: Fact + private_ip: Fact + interface_blocks: tuple[str, ...] + + +@dataclass(frozen=True, slots=True) +class DatabaseView: + address: str + support: ResourceSupport + port: Fact + engine: Fact + vpc_security_group_ids: Fact + + +@dataclass(frozen=True, slots=True) +class SubnetView: + address: str + support: ResourceSupport + vpc_id: Fact + cidr_block: Fact + + +@dataclass(frozen=True, slots=True) +class VpcView: + address: str + support: ResourceSupport + cidr_block: Fact + + +@dataclass(frozen=True, slots=True) +class GroupNetworkView: + address: str + support: ResourceSupport + vpc_id: Fact + + +def read_instance(resource: Resource) -> InstanceView: + attributes = _attributes(resource, "aws_instance") + owner = resource.address + return InstanceView( + address=owner, + support=resource.support_status, + subnet_id=_read(attributes, "subnet_id", owner), + vpc_security_group_ids=_read(attributes, "vpc_security_group_ids", owner), + security_groups=_read(attributes, "security_groups", owner), + private_ip=_read(attributes, "private_ip", owner), + interface_blocks=tuple( + name + for name in _INTERFACE_ARGUMENTS + if name in attributes and _has_blocks(attributes[name], f"{owner}.{name}") + ), + ) + + +def read_database(resource: Resource) -> DatabaseView: + attributes = _attributes(resource, "aws_db_instance") + owner = resource.address + return DatabaseView( + address=owner, + support=resource.support_status, + port=_read(attributes, "port", owner), + engine=_read(attributes, "engine", owner), + vpc_security_group_ids=_read(attributes, "vpc_security_group_ids", owner), + ) + + +def read_subnet(resource: Resource) -> SubnetView: + attributes = _attributes(resource, "aws_subnet") + owner = resource.address + return SubnetView( + address=owner, + support=resource.support_status, + vpc_id=_read(attributes, "vpc_id", owner), + cidr_block=_read(attributes, "cidr_block", owner), + ) + + +def read_vpc(resource: Resource) -> VpcView: + attributes = _attributes(resource, "aws_vpc") + return VpcView( + address=resource.address, + support=resource.support_status, + cidr_block=_read(attributes, "cidr_block", resource.address), + ) + + +def read_group_network(resource: Resource) -> GroupNetworkView: + attributes = _attributes(resource, "aws_security_group") + return GroupNetworkView( + address=resource.address, + support=resource.support_status, + vpc_id=_read(attributes, "vpc_id", resource.address), + ) + + +# --- route tables ------------------------------------------------------------------------------ + + +@dataclass(frozen=True, slots=True) +class RouteView: + """One route. ``state``: ``ipv4`` (a CIDR destination), ``ipv6_only``, ``unresolved`` (a + destination that cannot be fixed, or a prefix list) or ``unsupported``. ``target``: ``local`` + (``gateway_id = "local"`` and no other target), ``other`` (any other target, and also no target: + conservative), ``unresolved`` or ``unsupported``.""" + + state: str + destination: Network | None + target: str + + def sort_key(self) -> tuple[str, int, int, str]: + first = -1 if self.destination is None else self.destination.first + last = -1 if self.destination is None else self.destination.last + return (self.state, first, last, self.target) + + +@dataclass(frozen=True, slots=True) +class RouteTableView: + address: str + support: ResourceSupport + vpc_id: Fact + routes: tuple[RouteView, ...] + routes_unresolved: str | None # why the set of routes cannot be fixed, else None + propagating_vgws_present: bool + + +def _destination(fields: Mapping[str, Fact]) -> tuple[str, Network | None]: + prefix_list = fields["destination_prefix_list_id"] + cidr = fields["cidr_block"] + ipv6 = fields["ipv6_cidr_block"] + if prefix_list.state != ABSENT_STATE: + return "unresolved", None + if cidr.state == KNOWN: + try: + if not isinstance(cidr.value, str): + raise CidrError("not text") + return "ipv4", parse_network(cidr.value) + except CidrError: + return "unsupported", None + if cidr.state == UNKNOWN_STATE: + return "unresolved", None + if cidr.state == UNSUPPORTED_STATE: + return "unsupported", None + if ipv6.state == KNOWN: + return "ipv6_only", None + if ipv6.state == UNKNOWN_STATE: + return "unresolved", None + return "unsupported", None + + +def _target(fields: Mapping[str, Fact]) -> str: + present = {name: fields[name] for name in _ROUTE_TARGETS if fields[name].state != ABSENT_STATE} + gateway = present.get("gateway_id") + if ( + gateway is not None + and gateway.state == KNOWN + and gateway.value == "local" + and len(present) == 1 + ): + return "local" + if any(fact.state == UNSUPPORTED_STATE for fact in present.values()): + return "unsupported" + if any(fact.state == UNKNOWN_STATE for fact in present.values()): + return "unresolved" + return "other" + + +_ROUTE_FIELDS: Final = ( + "cidr_block", + "ipv6_cidr_block", + "destination_prefix_list_id", + *_ROUTE_TARGETS, +) + + +def _route(fields: Mapping[str, Fact]) -> RouteView: + state, destination = _destination(fields) + return RouteView(state, destination, _target(fields)) + + +def _routes(encoded: object, owner: str) -> tuple[tuple[RouteView, ...], str | None]: + where = f"{owner}.route" + argument = _argument(encoded, where) + found: list[RouteView] = [] + unresolved: str | None = None + if argument.form != "ATTRIBUTE": + for block in argument.blocks: + fields = { + name: ( + _fact_of_argument(block.arguments[name]) if name in block.arguments else ABSENT + ) + for name in _ROUTE_FIELDS + } + found.append(_route(fields)) + if argument.indeterminate: + unresolved = "route.expansion" + else: + value = argument.value + if value is None: + elements: tuple[Any, ...] = () + elif isinstance(value, Unknown | Unsupported): + return (), f"route.{value.reason}" + elif isinstance(value, tuple): + elements = value + elif isinstance(value, SetValue): + elements = value.items + else: + raise ViewError(f"{where}: a list of routes was expected") + for element in elements: + if isinstance(element, Unknown | Unsupported): + unresolved = f"route.{element.reason}" + elif isinstance(element, Mapping): + found.append( + _route({name: _fact_of_value(element.get(name)) for name in _ROUTE_FIELDS}) + ) + else: + raise ViewError(f"{where}: a route must be an object") + return tuple(sorted(found, key=RouteView.sort_key)), unresolved + + +def read_route_table(resource: Resource) -> RouteTableView: + attributes = _attributes(resource, "aws_route_table") + owner = resource.address + routes, unresolved = ( + _routes(attributes["route"], owner) if "route" in attributes else ((), None) + ) + return RouteTableView( + address=owner, + support=resource.support_status, + vpc_id=_read(attributes, "vpc_id", owner), + routes=routes, + routes_unresolved=unresolved, + propagating_vgws_present="propagating_vgws" in attributes, + ) diff --git a/tests/func_builders.py b/tests/func_builders.py new file mode 100644 index 0000000..522748b --- /dev/null +++ b/tests/func_builders.py @@ -0,0 +1,60 @@ +"""Builders for the INV-FUNC-001 tests (P5b): the canonical configuration and asserted text edits. + +Every F-vector is "a minimal configuration difference from the canonical topology" (registry §8). +The canonical text is the fixture ``canonical_regression/patch_safe`` (SSH fixed, path kept); an +edit is a replacement that is asserted to apply exactly once, so a no-op edit cannot pass silently. +Standard library plus ``core.*`` (tests may import every package). Not a test module. +""" + +from __future__ import annotations + +from collections.abc import Mapping +from pathlib import Path +from typing import Any + +from core.domain.jsonvalue import thaw_json +from core.domain.resource import Resource + +ROOT = Path(__file__).resolve().parents[1] +CANONICAL_PATH = ROOT / "fixtures" / "canonical_regression" / "patch_safe" / "main.tf" +SOURCE = "aws_instance.app" +DESTINATION = "aws_db_instance.database" + + +def canonical() -> str: + """The canonical configuration text (a PASS for INV-FUNC-001, registry F1).""" + return CANONICAL_PATH.read_text(encoding="utf-8") + + +def edit(text: str, old: str, new: str) -> str: + """Replace ``old`` by ``new``; the old text must occur exactly once.""" + count = text.count(old) + if count != 1: + raise AssertionError(f"the edit target occurs {count} times, not once: {old[:80]!r}") + return text.replace(old, new) + + +def edits(text: str, *pairs: tuple[str, str]) -> str: + for old, new in pairs: + text = edit(text, old, new) + return text + + +def with_attributes(resource: Resource, attributes: Mapping[str, Any]) -> Resource: + """The same resource with other stored ``attributes`` (hash recomputed): a damaged record.""" + return Resource.create( + address=resource.address, + resource_type=resource.resource_type, + logical_identity=thaw_json(resource.logical_identity), + attributes=attributes, + security_attributes=thaw_json(resource.security_attributes), + semantic_attributes=thaw_json(resource.semantic_attributes), + references=resource.references, + provenance=resource.provenance, + support_status=resource.support_status, + ) + + +def attribute(value: Any) -> dict[str, Any]: + """An ATTRIBUTE-form argument in the stored encoding.""" + return {"form": "ATTRIBUTE", "value": value} diff --git a/tests/unit/test_reachability_readers.py b/tests/unit/test_reachability_readers.py new file mode 100644 index 0000000..e6b246d --- /dev/null +++ b/tests/unit/test_reachability_readers.py @@ -0,0 +1,358 @@ +"""The reader of the INV-FUNC-001 inputs (P5b step 3; registry §6.2, §6.3, §6.6; C-151, C-153). + +Expected values are written by hand from the stored shape P3a writes (``Resource.attributes`` in the +C-112 encoding, dumped from the canonical fixture) and from the registry fields §6.6 lists as the +footprint: for ``S`` the ``subnet_id``, ``vpc_security_group_ids``, ``security_groups``, +``private_ip``, ``network_interface`` and ``primary_network_interface``; for ``D`` the +``vpc_security_group_ids``, ``port`` and ``engine``; for a subnet the ``vpc_id`` and ``cidr_block``; +for a VPC the ``cidr_block``; for a route table its routes and ``propagating_vgws``. + +A stored shape the reader cannot read raises ``ViewError``; it is never "absent". +""" + +from __future__ import annotations + +import unittest +from pathlib import Path + +from core.domain.enums import ResourceSupport +from core.terraform_model.normalization import normalize_directory +from core.verification.cidr import Network +from core.verification.func_view import ( + Fact, + items_of, + read_database, + read_group_network, + read_instance, + read_route_table, + read_subnet, + read_vpc, +) +from core.verification.values import Ref, Unknown, Unsupported +from core.verification.views import ViewError +from tests import fixture_catalog as fc +from tests.func_builders import attribute, canonical, with_attributes +from tests.identity_builders import NOW +from tests.security_builders import VARS, resources_of + +CANON = {r.address: r for r in resources_of(canonical())} +ABSENT = Fact("absent") + + +def one(text: str, address: str): # type: ignore[no-untyped-def] + return next(r for r in resources_of(text) if r.address == address) + + +def instance(body: str): # type: ignore[no-untyped-def] + text = VARS + f'resource "aws_instance" "s" {{\n ami = "ami-1"\n{body}}}\n' + return read_instance(one(text, "aws_instance.s")) + + +def table(body: str): # type: ignore[no-untyped-def] + text = VARS + f'resource "aws_route_table" "t" {{\n vpc_id = "vpc-1"\n{body}}}\n' + return read_route_table(one(text, "aws_route_table.t")) + + +def route(body: str): # type: ignore[no-untyped-def] + view = table(f" route {{\n{body} }}\n") + (found,) = view.routes + return found + + +class TestCanonicalResources(unittest.TestCase): + def test_the_instance(self) -> None: + view = read_instance(CANON["aws_instance.app"]) + self.assertEqual(view.address, "aws_instance.app") + self.assertEqual(view.support, ResourceSupport.SUPPORTED) + self.assertEqual(view.subnet_id, Fact("known", Ref("aws_subnet.app", "id"))) + self.assertEqual( + view.vpc_security_group_ids, Fact("known", (Ref("aws_security_group.app", "id"),)) + ) + self.assertEqual((view.security_groups, view.private_ip), (ABSENT, ABSENT)) + self.assertEqual(view.interface_blocks, ()) + + def test_the_database(self) -> None: + view = read_database(CANON["aws_db_instance.database"]) + self.assertEqual((view.port, view.engine), (ABSENT, Fact("known", "postgres"))) + self.assertEqual( + view.vpc_security_group_ids, Fact("known", (Ref("aws_security_group.db", "id"),)) + ) + + def test_subnet_vpc_and_group(self) -> None: + subnet = read_subnet(CANON["aws_subnet.app"]) + self.assertEqual(subnet.vpc_id, Fact("known", Ref("aws_vpc.main", "id"))) + self.assertEqual(subnet.cidr_block, Fact("known", "10.0.1.0/24")) + self.assertEqual(read_vpc(CANON["aws_vpc.main"]).cidr_block, Fact("known", "10.0.0.0/16")) + group = read_group_network(CANON["aws_security_group.db"]) + self.assertEqual(group.vpc_id, Fact("known", Ref("aws_vpc.main", "id"))) + + def test_the_route_table(self) -> None: + view = read_route_table(CANON["aws_route_table.public"]) + self.assertEqual(view.vpc_id, Fact("known", Ref("aws_vpc.main", "id"))) + self.assertFalse(view.propagating_vgws_present) + self.assertIsNone(view.routes_unresolved) + (found,) = view.routes + self.assertEqual(found.state, "ipv4") + self.assertEqual(found.destination, Network(4, 0, 2**32 - 1)) + self.assertEqual(found.target, "other") + + +class TestFacts(unittest.TestCase): + def test_a_literal(self) -> None: + self.assertEqual( + instance(' private_ip = "10.0.1.10"\n').private_ip, Fact("known", "10.0.1.10") + ) + self.assertEqual( + instance(' subnet_id = "subnet-1"\n').subnet_id, Fact("known", "subnet-1") + ) + + def test_name_based_groups(self) -> None: + view = instance(' security_groups = ["default"]\n') + self.assertEqual(view.security_groups, Fact("known", ("default",))) + + def test_a_value_that_cannot_be_fixed_is_unknown_with_its_reason(self) -> None: + fact = instance(" private_ip = var.u\n").private_ip + self.assertEqual((fact.state, fact.reason), ("unknown", "variable.no_value")) + + def test_an_explicit_null_is_not_set(self) -> None: + self.assertEqual(instance(" private_ip = null\n").private_ip, ABSENT) + + def test_a_list_with_an_unresolved_element_is_known_but_its_items_say_so(self) -> None: + text = ( + VARS + + 'resource "aws_security_group" "a" {}\n' + + 'resource "aws_instance" "s" {\n ami = "ami-1"\n' + + " vpc_security_group_ids = [aws_security_group.a.id, var.u]\n}\n" + ) + view = read_instance(one(text, "aws_instance.s")) + self.assertEqual(view.vpc_security_group_ids.state, "known") + items = items_of(view.vpc_security_group_ids) + self.assertEqual(items[0], Ref("aws_security_group.a", "id")) + self.assertIsInstance(items[1], Unknown) + + def test_a_list_that_cannot_be_fixed_is_unknown(self) -> None: + self.assertEqual( + instance(" vpc_security_group_ids = var.u\n").vpc_security_group_ids.state, "unknown" + ) + + def test_items_of_every_state(self) -> None: + self.assertEqual(items_of(ABSENT), ()) + self.assertEqual(items_of(Fact("known", "x")), ("x",)) + self.assertEqual(items_of(Fact("known", ("a", "b"))), ("a", "b")) + self.assertEqual(items_of(Fact("unknown", reason="r")), (Unknown("r"),)) + self.assertEqual(items_of(Fact("unsupported", reason="r")), (Unsupported("r"),)) + + def test_an_unsupported_value(self) -> None: + resource = CANON["aws_db_instance.database"] + damaged = with_attributes( + resource, + {"port": attribute({"$dail": "unsupported", "reason": "function.unsupported"})}, + ) + fact = read_database(damaged).port + self.assertEqual((fact.state, fact.reason), ("unsupported", "function.unsupported")) + + def test_an_argument_written_as_a_block_where_a_value_is_expected(self) -> None: + damaged = with_attributes( + CANON["aws_db_instance.database"], + {"engine": {"form": "BLOCKS", "blocks": [], "indeterminate": []}}, + ) + fact = read_database(damaged).engine + self.assertEqual((fact.state, fact.reason), ("unsupported", "form.block")) + + +class TestRoutes(unittest.TestCase): + def test_a_local_route(self) -> None: + found = route(' cidr_block = "10.0.0.0/16"\n gateway_id = "local"\n') + self.assertEqual((found.state, found.target), ("ipv4", "local")) + self.assertEqual(found.destination, Network(4, 10 << 24, (10 << 24) + 2**16 - 1)) + + def test_a_route_to_a_nat_gateway_or_an_interface_is_not_local(self) -> None: + for target in ('nat_gateway_id = "nat-1"', 'network_interface_id = "eni-1"'): + found = route(f' cidr_block = "10.0.2.0/24"\n {target}\n') + self.assertEqual(found.target, "other", target) + + def test_local_plus_another_target_is_not_local(self) -> None: + found = route( + ' cidr_block = "10.0.2.0/24"\n gateway_id = "local"\n' + ' nat_gateway_id = "nat-1"\n' + ) + self.assertEqual(found.target, "other") + + def test_a_route_without_a_target_is_treated_as_not_local(self) -> None: + self.assertEqual(route(' cidr_block = "10.0.2.0/24"\n').target, "other") + + def test_an_unresolved_target_is_unresolved_unless_it_is_surely_local(self) -> None: + self.assertEqual( + route(' cidr_block = "10.0.2.0/24"\n gateway_id = var.u\n').target, "unresolved" + ) + + def test_an_ipv6_only_route(self) -> None: + found = route(' ipv6_cidr_block = "::/0"\n gateway_id = "igw-1"\n') + self.assertEqual((found.state, found.destination), ("ipv6_only", None)) + + def test_a_prefix_list_destination_cannot_be_fixed(self) -> None: + found = route(' destination_prefix_list_id = "pl-1"\n gateway_id = "igw-1"\n') + self.assertEqual(found.state, "unresolved") + + def test_an_unresolved_or_invalid_destination(self) -> None: + self.assertEqual( + route(' cidr_block = var.u\n gateway_id = "igw-1"\n').state, "unresolved" + ) + self.assertEqual( + route(' cidr_block = "10.0.0.1/8"\n gateway_id = "igw-1"\n').state, "unsupported" + ) + + def test_a_route_without_any_destination(self) -> None: + self.assertEqual(route(' gateway_id = "igw-1"\n').state, "unsupported") + + def test_routes_are_read_in_a_fixed_order(self) -> None: + one_way = table( + ' route {\n cidr_block = "10.0.2.0/24"\n gateway_id = "local"\n }\n' + ' route {\n cidr_block = "0.0.0.0/0"\n gateway_id = "igw-1"\n }\n' + ) + other = table( + ' route {\n cidr_block = "0.0.0.0/0"\n gateway_id = "igw-1"\n }\n' + ' route {\n cidr_block = "10.0.2.0/24"\n gateway_id = "local"\n }\n' + ) + self.assertEqual(one_way.routes, other.routes) + self.assertEqual(len(one_way.routes), 2) + + def test_the_reader_orders_routes_whatever_order_it_is_given(self) -> None: + # P3a already stores routes in a canonical order; the reader does not rely on it + base = CANON["aws_route_table.public"] + wide = {"cidr_block": "0.0.0.0/0", "gateway_id": "igw-1"} + narrow = {"cidr_block": "10.0.2.0/24", "gateway_id": "local"} + views = [ + read_route_table(with_attributes(base, {"route": attribute(order)})) + for order in ([wide, narrow], [narrow, wide]) + ] + self.assertEqual(views[0].routes, views[1].routes) + self.assertEqual([r.target for r in views[0].routes], ["other", "local"]) + + def test_no_routes(self) -> None: + view = table("") + self.assertEqual((view.routes, view.routes_unresolved), ((), None)) + + def test_an_explicit_empty_route_list_and_one_that_cannot_be_fixed(self) -> None: + self.assertEqual(table(" route = []\n").routes, ()) + self.assertIsNotNone(table(" route = var.u\n").routes_unresolved) + + def test_a_dynamic_route_block_that_cannot_be_expanded(self) -> None: + body = ( + ' dynamic "route" {\n for_each = var.u\n content {\n' + ' cidr_block = "10.0.2.0/24"\n gateway_id = "local"\n }\n }\n' + ) + view = table(body) + self.assertEqual(view.routes, ()) + self.assertIsNotNone(view.routes_unresolved) + + def test_propagating_vgws_even_when_empty(self) -> None: + self.assertFalse(table("").propagating_vgws_present) + self.assertTrue(table(" propagating_vgws = []\n").propagating_vgws_present) + self.assertTrue(table(' propagating_vgws = ["vgw-1"]\n').propagating_vgws_present) + + +class TestInterfaceBlocks(unittest.TestCase): + def test_none(self) -> None: + self.assertEqual(instance("").interface_blocks, ()) + + def test_each_kind(self) -> None: + net = instance( + ' network_interface {\n device_index = 0\n network_interface_id = "eni-1"\n }\n' + ) + self.assertEqual(net.interface_blocks, ("network_interface",)) + primary = instance( + ' primary_network_interface {\n network_interface_id = "eni-1"\n }\n' + ) + self.assertEqual(primary.interface_blocks, ("primary_network_interface",)) + + def test_both_kinds_are_listed_in_a_fixed_order(self) -> None: + both = instance( + ' primary_network_interface {\n network_interface_id = "eni-1"\n }\n' + ' network_interface {\n device_index = 1\n network_interface_id = "eni-2"\n }\n' + ) + self.assertEqual(both.interface_blocks, ("network_interface", "primary_network_interface")) + + def test_a_dynamic_block_that_cannot_be_expanded_counts_as_present(self) -> None: + body = ( + ' dynamic "network_interface" {\n for_each = var.u\n content {\n' + ' device_index = 0\n network_interface_id = "eni-1"\n }\n }\n' + ) + self.assertEqual(instance(body).interface_blocks, ("network_interface",)) + + def test_a_value_that_cannot_be_fixed_counts_as_present(self) -> None: + # attribute form: `network_interface = var.u` might be any number of blocks + self.assertEqual( + instance(" network_interface = var.u\n").interface_blocks, ("network_interface",) + ) + + def test_an_empty_list_is_no_block(self) -> None: + self.assertEqual(instance(" network_interface = []\n").interface_blocks, ()) + + +class TestPlaceholdersAndErrors(unittest.TestCase): + def test_a_placeholder_is_read_with_its_support_status_so_it_is_not_taken_for_absent( + self, + ) -> None: + text = VARS + 'resource "aws_instance" "p" {\n count = var.u\n ami = "ami-1"\n}\n' + view = read_instance(one(text, "aws_instance.p")) + self.assertEqual(view.support, ResourceSupport.UNKNOWN) + + def test_a_stored_value_the_reader_cannot_read_is_an_error(self) -> None: + base = CANON["aws_instance.app"] + for bad in ( + {"subnet_id": {"form": "ATTRIBUTE"}}, + {"subnet_id": "plain"}, + {"subnet_id": attribute({"$dail": "weird"})}, + {"subnet_id": attribute({"$dail": "ref", "address": "a"})}, + {"private_ip": {"form": "WEIRD"}}, + ): + with self.subTest(bad=bad), self.assertRaises(ViewError): + read_instance(with_attributes(base, bad)) + + def test_a_resource_of_the_wrong_type_is_an_error(self) -> None: + with self.assertRaises(ViewError): + read_instance(CANON["aws_db_instance.database"]) + with self.assertRaises(ViewError): + read_route_table(CANON["aws_subnet.app"]) + with self.assertRaises(ViewError): + read_database(CANON["aws_instance.app"]) + + def test_a_damaged_route_table_is_an_error(self) -> None: + base = CANON["aws_route_table.public"] + for bad in ( + {"route": {"form": "WEIRD"}}, + {"route": {"form": "BLOCKS", "blocks": [{"type": "route"}], "indeterminate": []}}, + {"route": attribute(["not an object"])}, + {"route": attribute([{"cidr_block": {"$dail": "weird"}}])}, + ): + with self.subTest(bad=bad), self.assertRaises(ViewError): + read_route_table(with_attributes(base, bad)) + + +class TestEveryFixture(unittest.TestCase): + def test_every_functional_resource_of_every_fixture_can_be_read(self) -> None: + readers = { + "aws_instance": read_instance, + "aws_db_instance": read_database, + "aws_subnet": read_subnet, + "aws_vpc": read_vpc, + "aws_security_group": read_group_network, + "aws_route_table": read_route_table, + } + folders = {fx.data["config"] for fx in fc.load_all().values()} + folders |= {fx.data["parent"] for fx in fc.load_all().values() if fx.data.get("parent")} + read = 0 + for folder in sorted(folders): + outcome = normalize_directory(Path(fc.REPO_ROOT) / folder, None, now=NOW) + for resource in outcome.resources: + reader = readers.get(resource.resource_type) + if reader is not None: + with self.subTest(folder=folder, resource=resource.address): + self.assertEqual(reader(resource).address, resource.address) + read += 1 + self.assertGreater(read, 100) + + +if __name__ == "__main__": + unittest.main() From 66982dde00c82e0a1c3c578ff56b292d05a6e629 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 00:52:21 +0530 Subject: [PATCH 5/8] =?UTF-8?q?P5b=20step=204:=20the=20INV-FUNC-001=20pred?= =?UTF-8?q?icate,=20rows=201=20to=209=20(registry=20=C2=A76.2-=C2=A76.4,?= =?UTF-8?q?=20=C2=A78;=20C-151=20to=20C-154)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit reachability.py implements E1 to E7 and the first-row-wins table of §6.4: endpoints followed across moves through the identity report (a deleted one is absent, an uncertain or placeholder one is indeterminate), every row 2 cause collected and reported, rows 3 to 5 on resolved values only, E5 and E6 per rule, and rows 7 to 9 with "could satisfy" and "partly covers" as C-153 defines them. Vectors F1 to F20 are tests with the derivation written before the predicate. Shared code extended for it (SEC results unchanged, whole SEC suite rerun): views.group_is_mixed, retention.inline_retention with a direction, Rule.sources_unresolved / self_unresolved (a reference is a resolved source: values.has_unresolved), cidr.overlaps. A rule in an UNRESOLVED:* pseudo-group is determinate but may belong to a group of the side: a bug found by the tests and fixed before this commit. 26 deliberate breakages were each caught. C-153 corrected to per-rule coverage. Co-Authored-By: Claude Sonnet 5.5 --- core/verification/cidr.py | 15 + core/verification/public_ingress.py | 25 +- core/verification/reachability.py | 925 +++++++++++++++++++++ core/verification/retention.py | 23 +- core/verification/values.py | 8 + core/verification/views.py | 105 ++- docs/DECISIONS_REGISTER.md | 4 +- tests/func_builders.py | 45 + tests/reach_builders.py | 29 + tests/unit/test_reachability_predicate.py | 875 +++++++++++++++++++ tests/unit/test_reachability_vectors.py | 310 +++++++ tests/unit/test_verification_cidr_ports.py | 61 ++ tests/unit/test_verification_values.py | 39 + tests/unit/test_verification_views.py | 122 +++ 14 files changed, 2553 insertions(+), 33 deletions(-) create mode 100644 core/verification/reachability.py create mode 100644 tests/reach_builders.py create mode 100644 tests/unit/test_reachability_predicate.py create mode 100644 tests/unit/test_reachability_vectors.py diff --git a/core/verification/cidr.py b/core/verification/cidr.py index 083a095..b2df549 100644 --- a/core/verification/cidr.py +++ b/core/verification/cidr.py @@ -69,3 +69,18 @@ def covers(cidrs: Iterable[str], target: str) -> bool: if cursor > wanted.last: return True return cursor > wanted.last + + +def overlaps(cidrs: Iterable[str], target: str) -> bool: + """Whether some member shares at least one address with ``target`` (registry §6.4 row 8: a CIDR + that overlaps the target without covering it covers it "partly"). + + Same rules as ``covers``: one address family, an invalid member is an error, never ignored.""" + wanted = parse_network(target) + found = False + for text in cidrs: + member = parse_network(text) + if member.version != wanted.version: + raise CidrError("an overlap question mixes IPv4 and IPv6") + found = found or (member.first <= wanted.last and member.last >= wanted.first) + return found diff --git a/core/verification/public_ingress.py b/core/verification/public_ingress.py index 17e0307..d48b4b0 100644 --- a/core/verification/public_ingress.py +++ b/core/verification/public_ingress.py @@ -55,12 +55,12 @@ from core.verification.cidr import IPV4_ANY, IPV6_ANY, covers from core.verification.outcome import CLAUSE_IPV4, CLAUSE_IPV6, PredicateOutcome, combine from core.verification.ports import may_permit_tcp, permits_tcp -from core.verification.retention import BLOCK_FORMS, ingress_retention +from core.verification.retention import ingress_retention from core.verification.views import ( - ORIGIN_RULE_RESOURCE, GroupView, Rule, SecurityConfig, + group_is_mixed, read_security, ) @@ -122,23 +122,6 @@ class Analysis: outcome: PredicateOutcome -def _is_mixed(view: GroupView, rule_resources: Sequence[Rule]) -> bool: - """Registry §2.6 MIXED, with the conservative reading of a direction that cannot be fixed.""" - forms = view.forms - if forms is None or not rule_resources: - return False - if any(forms[name] in BLOCK_FORMS for name in ("ingress", "egress")): - return True - if any(forms[name] == "unresolved" for name in ("ingress", "egress")): - return True # whether inline blocks exist cannot be told - for name, direction in (("ingress", "INGRESS"), ("egress", "EGRESS")): - if forms[name] == "explicit_empty" and any( - rule.direction in (direction, None) for rule in rule_resources - ): - return True - return False - - def _could_expose(rule: Rule, port: int, family: tuple[str, str, str, str]) -> bool: """``possible`` for one indeterminate rule and one address family (registry §3.3).""" if not may_permit_tcp(rule.protocol, rule.from_port, rule.to_port, port): @@ -174,10 +157,8 @@ def _group_status( retention: VerificationReason | None, ) -> tuple[GroupStatus, bool]: """The status of one group, and whether it is MIXED.""" - directional = (*view.ingress, *view.egress, *view.unresolved_direction) - rule_resources = [rule for rule in directional if rule.origin == ORIGIN_RULE_RESOURCE] ingress_like = (*view.ingress, *view.unresolved_direction) - mixed = _is_mixed(view, rule_resources) + mixed = group_is_mixed(view) forms_unresolved = view.forms is not None and view.forms["ingress"] == "unresolved" reasons = [ reason diff --git a/core/verification/reachability.py b/core/verification/reachability.py new file mode 100644 index 0000000..7f7e634 --- /dev/null +++ b/core/verification/reachability.py @@ -0,0 +1,925 @@ +"""INV-FUNC-001: the application can reach the database on TCP/5432, ``REACH(S, D, 5432)``. + +Registry §6 (``dail.verify.reachability_cfg`` version 1; C-151 to C-154). The result is decided by +the first row of the table of §6.4 that applies: + + 1 S or D is absent (deleted, with no move) FAIL + 2 a relevant-unsupported type, an M3 route, name-based security groups, no groups or no + subnet, a MIXED or RETAINED-INLINE group, an interface block, ``propagating_vgws``, an + unsupported value or rule UNSUPPORTED + 3 E2 definitely false (the port, or the engine when there is no port) FAIL + 4 E3 or E4 needs a value that is unresolved, or an endpoint is indeterminate UNKNOWN + 5 E3 holds and VPC(S) differs from VPC(D) FAIL + 6 E5 and E6 hold with determinate rules PASS + 7 E5 or E6 fails, but an indeterminate rule could satisfy it UNKNOWN + 8 E5 or E6 fails, and a CIDR partly covers its target UNKNOWN + 9 otherwise FAIL + +so that a PASS needs every one of E1 to E7 and nothing that is unresolved can make a PASS: row 6 +uses determinate rules only. The definitions that make the rows precise (what ``src_sg`` is, +"partly covers", "could satisfy", ``ADDR(S)``, the M3 test) are in C-153, with the registry text +beside each; a case the registry does not decide is UNSUPPORTED and listed there as a spec gap +(R5). + +The endpoints are the bindings ``S`` and ``D`` of the definition: addresses of the trusted state, +followed across moves through the identity report (C-152). A PASS is a statement about +configuration prerequisites in this model, not about packets (registry §6.1). + +Standard library and ``core.domain`` only. +""" + +from __future__ import annotations + +import ipaddress +from collections.abc import Callable, Mapping +from dataclasses import dataclass, field +from typing import Any, Final + +from core.domain.enums import ChangeType, ResourceSupport, VerificationResult +from core.domain.invariant import Invariant +from core.domain.registry_v1 import FUNC_RELEVANT_UNSUPPORTED +from core.domain.resource import Resource +from core.domain.verification import VerificationReason +from core.verification.cidr import CidrError, Network, covers, overlaps, parse_network +from core.verification.func_view import ( + ABSENT_STATE, + KNOWN, + UNKNOWN_STATE, + UNSUPPORTED_STATE, + Fact, + RouteTableView, + items_of, + read_database, + read_group_network, + read_instance, + read_route_table, + read_subnet, + read_vpc, +) +from core.verification.inputs import VerificationInputs +from core.verification.outcome import PredicateOutcome +from core.verification.ports import may_permit_tcp, permits_tcp +from core.verification.retention import inline_retention +from core.verification.values import Ref, Unknown, Unsupported +from core.verification.views import ( + SECURITY_GROUP_TYPE, + GroupView, + Rule, + SecurityConfig, + group_is_mixed, + read_security, +) + +PORT: Final = 5432 +TOLERATED_TYPE: Final = "aws_db_subnet_group" +ASSUMPTIONS: Final = ( + "IPv4 only", + "M1: RDS security groups and subnet group share one VPC (C-15, C-77, uncited)", + "M4: default network ACL assumed (no NACL type present)", +) +TOLERATED_ASSUMPTION: Final = "tolerated type: aws_db_subnet_group (C-15)" + +P, F, U, S = ( + VerificationResult.PASS, + VerificationResult.FAIL, + VerificationResult.UNKNOWN, + VerificationResult.UNSUPPORTED, +) +R = VerificationReason + +# The fixed order of the row 2 causes; the first names the reason (C-153). +_RANK_TYPE, _RANK_ROUTE, _RANK_VGWS, _RANK_INTERFACE, _RANK_NAMES = 0, 1, 2, 3, 4 +_RANK_MISSING, _RANK_MIXED, _RANK_RETAINED, _RANK_FORMS, _RANK_VALUE, _RANK_MODEL = ( + 5, + 6, + 7, + 8, + 9, + 10, +) + + +@dataclass(frozen=True, slots=True) +class _Cause: + rank: int + code: VerificationReason + detail: str + + def sort_key(self) -> tuple[int, str, str]: + return (self.rank, self.code.value, self.detail) + + +@dataclass(frozen=True, slots=True) +class _Endpoint: + trusted: str + state: str # found | absent | indeterminate + resource: Resource | None + candidate: str | None + match: str + + +class _Finish(Exception): + """Raised to stop with a finished outcome (an early row, or an input that is not usable).""" + + def __init__(self, outcome: PredicateOutcome) -> None: + super().__init__("finished") + self.outcome = outcome + + +@dataclass(slots=True) +class _Sides: + """The groups of one side: configured group addresses, unresolved entries, causes found.""" + + groups: list[str] = field(default_factory=list) + unresolved: list[str] = field(default_factory=list) + + +def _coerce_port(fact: Fact) -> tuple[str, int | None]: + """The port as ``("value", n)``, or ``("absent" | "unresolved" | "unsupported", None)``.""" + if fact.state == ABSENT_STATE: + return "absent", None + if fact.state == UNKNOWN_STATE: + return "unresolved", None + if fact.state == UNSUPPORTED_STATE: + return "unsupported", None + value = fact.value + if isinstance(value, bool): + return "unsupported", None + if isinstance(value, int): + return "value", value + if isinstance(value, str) and value.isascii() and value.isdigit(): + return "value", int(value) + return "unsupported", None + + +class _Evaluation: + def __init__(self, definition: Invariant, inputs: VerificationInputs) -> None: + self.definition = definition + self.inputs = inputs + self.by_address = {r.address: r for r in inputs.candidate_resources} + self.parent = ( + None + if inputs.parent_resources is None + else {r.address: r for r in inputs.parent_resources} + ) + self.config: SecurityConfig = read_security(inputs.candidate_resources) + self.causes: list[_Cause] = [] + self.unresolved: list[str] = [] # why row 4 applies + self.endpoint_reasons: list[str] = [] + self.observations: dict[str, Any] = { + "row": 0, + "reason": None, + "detail": None, + "unresolved": [], + "endpoints": {}, + "port": PORT, + "path": { + "S": None, + "subnet": None, + "vpc_s": None, + "sg_s": None, + "egress_rule": None, + "sg_d": None, + "ingress_rule": None, + "vpc_d": None, + }, + "row2_causes": [], + "failing_conditions": [], + "indeterminate_rules": [], + "partial_coverage": [], + "relevant_unsupported": [], + } + tolerated = any(r.resource_type == TOLERATED_TYPE for r in inputs.candidate_resources) + self.assumptions = tuple( + sorted((*ASSUMPTIONS, *((TOLERATED_ASSUMPTION,) if tolerated else ()))) + ) + + # --- finishing ------------------------------------------------------------------------------- + + def finish( + self, result: VerificationResult, row: int, reason: VerificationReason | None + ) -> PredicateOutcome: + self.observations["row"] = row + self.observations["reason"] = None if reason is None else reason.value + self.observations["row2_causes"] = [ + {"cause": c.code.value, "detail": c.detail} + for c in sorted(self.causes, key=_Cause.sort_key) + ] + return PredicateOutcome(result, reason, None, self.observations, self.assumptions) + + def stop( + self, result: VerificationResult, row: int, reason: VerificationReason, detail: str + ) -> _Finish: + self.observations["detail"] = detail + return _Finish(self.finish(result, row, reason)) + + def cause(self, rank: int, code: VerificationReason, detail: str) -> None: + self.causes.append(_Cause(rank, code, detail)) + + # --- parameters and endpoints ---------------------------------------------------------------- + + def parameters(self) -> tuple[str, str]: + parameters = self.definition.predicate.get("parameters") + if not isinstance(parameters, Mapping): + raise self.stop(S, 0, R.PARAMETERS_INVALID, "parameters is not an object") + source, destination, port = parameters.get("S"), parameters.get("D"), parameters.get("port") + if not isinstance(source, str) or not isinstance(destination, str): + raise self.stop(S, 0, R.PARAMETERS_INVALID, "S and D must be text") + if not source.startswith("aws_instance.") or not destination.startswith("aws_db_instance."): + raise self.stop( + S, 0, R.PARAMETERS_INVALID, "S must be an aws_instance and D an aws_db_instance" + ) + if source == destination: + raise self.stop(S, 0, R.PARAMETERS_INVALID, "S and D must differ") + if isinstance(port, bool) or port != PORT: + raise self.stop(S, 0, R.PARAMETERS_INVALID, f"the port must be {PORT}") + return source, destination + + def resolve(self, binding: str, label: str) -> _Endpoint: + if self.parent is None: + resource = self.by_address.get(binding) + if resource is None: + return _Endpoint(binding, "absent", None, None, "BASELINE") + return self._found(binding, resource, "BASELINE") + if binding not in self.parent: + raise self.stop( + S, 0, R.PARAMETERS_INVALID, f"{label} {binding} is not in the trusted state" + ) + identity = self.inputs.identity + if identity is None: + raise self.stop(S, 0, R.IDENTITY_MISSING, "a parent without an identity report") + match = next( + (m for m in identity.resource_matches if m.trusted_resource_ref == binding), None + ) + if match is None: + raise self.stop( + S, 0, R.IDENTITY_MISSING, f"the identity report has no match for {binding}" + ) + kind = match.change_type + if kind is ChangeType.DELETED: + return _Endpoint(binding, "absent", None, None, kind.value) + if kind is ChangeType.UNCERTAIN: + return _Endpoint( + binding, "indeterminate", None, match.candidate_resource_ref, kind.value + ) + resource = self.by_address.get(match.candidate_resource_ref or "") + if resource is None: + raise self.stop( + S, 0, R.IDENTITY_MISSING, f"{binding} is matched to a resource the candidate lacks" + ) + return self._found(binding, resource, kind.value) + + def _found(self, binding: str, resource: Resource, match: str) -> _Endpoint: + if resource.support_status is not ResourceSupport.SUPPORTED: + return _Endpoint(binding, "indeterminate", None, resource.address, match) + return _Endpoint(binding, "found", resource, resource.address, match) + + # --- the groups, the subnet and the VPCs ----------------------------------------------------- + + def groups_of(self, fact: Fact, label: str) -> _Sides: + side = _Sides() + for item in items_of(fact): + if isinstance(item, Ref): + found = self.by_address.get(item.address) + if found is None or found.resource_type != SECURITY_GROUP_TYPE: + self.cause( + _RANK_MODEL, + R.MODEL_UNSUPPORTED, + f"{label}: {item.address} is not a configured security group", + ) + elif found.support_status is ResourceSupport.SUPPORTED: + side.groups.append(found.address) + else: + side.unresolved.append(f"{label}: {found.address} is a placeholder") + elif isinstance(item, Unknown): + side.unresolved.append(f"{label}: {item.reason}") + elif isinstance(item, Unsupported): + self.cause(_RANK_VALUE, R.VALUE_UNSUPPORTED, f"{label}: {item.reason}") + elif isinstance(item, str): + self.cause( + _RANK_MODEL, + R.MODEL_UNSUPPORTED, + f"{label}: the group id {item!r} is not a configured group", + ) + else: + self.cause( + _RANK_VALUE, R.VALUE_UNSUPPORTED, f"{label}: an entry that is not a group" + ) + side.groups = sorted(set(side.groups)) + return side + + def vpc_of(self, fact: Fact, label: str) -> str | None: + """The address of the configured VPC that a ``vpc_id`` references, else ``None`` (and the + cause or the unresolved reason is recorded).""" + if fact.state == ABSENT_STATE: + self.cause( + _RANK_MODEL, R.MODEL_UNSUPPORTED, f"{label}: no vpc_id (default VPC not modelled)" + ) + elif fact.state == UNKNOWN_STATE: + self.unresolved.append(f"{label}: vpc_id {fact.reason}") + elif fact.state == UNSUPPORTED_STATE: + self.cause(_RANK_VALUE, R.VALUE_UNSUPPORTED, f"{label}: vpc_id {fact.reason}") + elif isinstance(fact.value, Ref): + vpc = self.by_address.get(fact.value.address) + if vpc is None or vpc.resource_type != "aws_vpc": + self.cause( + _RANK_MODEL, R.MODEL_UNSUPPORTED, f"{label}: vpc_id is not a configured aws_vpc" + ) + elif vpc.support_status is not ResourceSupport.SUPPORTED: + self.unresolved.append(f"{label}: {vpc.address} is a placeholder") + else: + return vpc.address + else: + self.cause( + _RANK_MODEL, + R.MODEL_UNSUPPORTED, + f"{label}: vpc_id is a literal id, so the VPC CIDR is unknown", + ) + return None + + def network_of(self, vpc: str | None, label: str) -> Network | None: + if vpc is None: + return None + fact = read_vpc(self.by_address[vpc]).cidr_block + return self._cidr(fact, f"{label}: the CIDR of {vpc}") + + def _cidr(self, fact: Fact, label: str) -> Network | None: + if fact.state == KNOWN and isinstance(fact.value, str): + try: + return parse_network(fact.value) + except CidrError: + self.cause(_RANK_VALUE, R.VALUE_UNSUPPORTED, f"{label} is not a CIDR") + return None + if fact.state == UNKNOWN_STATE: + self.unresolved.append(f"{label} {fact.reason}") + elif fact.state == ABSENT_STATE: + self.cause(_RANK_MODEL, R.MODEL_UNSUPPORTED, f"{label} is not written") + else: + self.cause(_RANK_VALUE, R.VALUE_UNSUPPORTED, f"{label} {fact.reason}") + return None + + +def evaluate_reachability(definition: Invariant, inputs: VerificationInputs) -> PredicateOutcome: + """``REACH(S, D, 5432)`` for a candidate (no parent resources means a baseline).""" + run = _Evaluation(definition, inputs) + try: + return _decide(run) + except _Finish as done: + return done.outcome + + +# --- the rows ------------------------------------------------------------------------------------- + + +def _decide(run: _Evaluation) -> PredicateOutcome: + source, destination = run.parameters() + endpoints = {"S": run.resolve(source, "S"), "D": run.resolve(destination, "D")} + run.observations["endpoints"] = { + label: {"trusted": e.trusted, "candidate": e.candidate, "match": e.match} + for label, e in endpoints.items() + } + run.observations["relevant_unsupported"] = sorted( + r.address + for r in run.inputs.candidate_resources + if r.resource_type in FUNC_RELEVANT_UNSUPPORTED + ) + # row 1 + gone = [label for label, e in endpoints.items() if e.state == "absent"] + if gone: + raise run.stop(F, 1, R.ENDPOINT_ABSENT, f"absent: {', '.join(gone)}") + # row 2: every cause that can be evaluated, then the reason by the fixed order + s_end, d_end = endpoints["S"], endpoints["D"] + for label, endpoint in endpoints.items(): + if endpoint.state == "indeterminate": + run.endpoint_reasons.append( + f"{label} is {endpoint.match.lower()}: {endpoint.candidate or endpoint.trusted}" + ) + model = _Model(run, s_end, d_end) + model.collect_causes() + if run.causes: + first = min(run.causes, key=_Cause.sort_key) + raise _Finish(run.finish(S, 2, first.code)) + # row 3 + model.check_listener() + # row 4 + if run.endpoint_reasons or run.unresolved: + reason = R.RESOURCE_INDETERMINATE if run.endpoint_reasons else R.ATTRIBUTE_UNRESOLVED + run.observations["unresolved"] = sorted([*run.endpoint_reasons, *run.unresolved]) + raise _Finish(run.finish(U, 4, reason)) + # row 5 + if model.vpc_s != model.vpc_d: + raise run.stop( + F, 5, R.VPC_MISMATCH, f"VPC(S) {model.vpc_s} differs from VPC(D) {model.vpc_d}" + ) + return model.reach() + + +class _Model: + """The path from S to D: the facts the rows read, in the order the registry names them.""" + + def __init__(self, run: _Evaluation, s_end: _Endpoint, d_end: _Endpoint) -> None: + self.run = run + self.s_end, self.d_end = s_end, d_end + self.instance = read_instance(s_end.resource) if s_end.resource is not None else None + self.database = read_database(d_end.resource) if d_end.resource is not None else None + self.sg_s = _Sides() + self.sg_d = _Sides() + self.vpc_s: str | None = None + self.vpc_d: str | None = None + self.net_d: Network | None = None + self.addr_s: Network | None = None + self.subnet: str | None = None + self.loaded = False + + # --- row 2 ----------------------------------------------------------------------------------- + + def collect_causes(self) -> None: + run = self.run + types = run.observations["relevant_unsupported"] + if types: + run.cause(_RANK_TYPE, R.TYPE_RELEVANT_UNSUPPORTED, ", ".join(types)) + self._load() + self._groups_and_forms() + self._routes() + + def _load(self) -> None: + run, inst, db = self.run, self.instance, self.database + if inst is not None: + if inst.interface_blocks: + run.cause( + _RANK_INTERFACE, + R.INTERFACE_UNSUPPORTED, + f"{inst.address}: {', '.join(inst.interface_blocks)}", + ) + names = inst.security_groups + if names.state == KNOWN and not items_of(names): + pass # an explicit empty list uses no name-based group + elif names.state != ABSENT_STATE: + run.cause( + _RANK_NAMES, + R.MODEL_UNSUPPORTED, + f"{inst.address} uses name-based security_groups", + ) + self.sg_s = self._side(inst.vpc_security_group_ids, inst.address) + self._subnet(inst) + if db is not None: + self.sg_d = self._side(db.vpc_security_group_ids, db.address) + self._engine_and_port(db) + self.loaded = True + + def _side(self, fact: Fact, owner: str) -> _Sides: + run = self.run + if fact.state == ABSENT_STATE or (fact.state == KNOWN and not items_of(fact)): + run.cause( + _RANK_MISSING, + R.MODEL_UNSUPPORTED, + f"{owner} has no vpc_security_group_ids (default group not modelled)", + ) + return _Sides() + if fact.state == UNKNOWN_STATE: + run.unresolved.append(f"{owner}: vpc_security_group_ids {fact.reason}") + return _Sides() + return run.groups_of(fact, f"{owner}.vpc_security_group_ids") + + def _subnet(self, inst: Any) -> None: + run = self.run + fact = inst.subnet_id + if fact.state == ABSENT_STATE: + run.cause( + _RANK_MISSING, + R.MODEL_UNSUPPORTED, + f"{inst.address} has no subnet_id (default VPC not modelled)", + ) + elif fact.state == UNKNOWN_STATE: + run.unresolved.append(f"{inst.address}: subnet_id {fact.reason}") + elif fact.state == UNSUPPORTED_STATE: + run.cause(_RANK_VALUE, R.VALUE_UNSUPPORTED, f"{inst.address}: subnet_id {fact.reason}") + elif isinstance(fact.value, Ref): + found = run.by_address.get(fact.value.address) + if found is None or found.resource_type != "aws_subnet": + run.cause( + _RANK_MODEL, + R.MODEL_UNSUPPORTED, + f"{inst.address}: subnet_id is not a configured aws_subnet", + ) + elif found.support_status is not ResourceSupport.SUPPORTED: + run.unresolved.append(f"{inst.address}: {found.address} is a placeholder") + else: + self.subnet = found.address + view = read_subnet(found) + self.vpc_s = run.vpc_of(view.vpc_id, found.address) + else: + run.cause( + _RANK_MODEL, + R.MODEL_UNSUPPORTED, + f"{inst.address}: subnet_id is a literal id, not a configured subnet", + ) + + def _engine_and_port(self, db: Any) -> None: + run = self.run + kind, _ = _coerce_port(db.port) + engine = db.engine + if kind == "unsupported": + run.cause(_RANK_VALUE, R.VALUE_UNSUPPORTED, f"{db.address}: port") + if engine.state == UNSUPPORTED_STATE or ( + engine.state == KNOWN and not isinstance(engine.value, str) + ): + run.cause(_RANK_VALUE, R.VALUE_UNSUPPORTED, f"{db.address}: engine") + if kind == "absent" and engine.state == ABSENT_STATE: + run.cause( + _RANK_MODEL, + R.MODEL_UNSUPPORTED, + f"{db.address} has neither port nor engine (registry gap)", + ) + + def _groups_and_forms(self) -> None: + run = self.run + groups = run.config.groups + parent, identity = run.parent, run.inputs.identity + for label, side, direction in (("S", self.sg_s, "egress"), ("D", self.sg_d, "ingress")): + for address in side.groups: + view = groups.get(address) + if view is None: + continue + if group_is_mixed(view): + run.cause(_RANK_MIXED, R.GROUP_MIXED, f"{address} (SG({label}))") + forms = view.forms + if forms is not None and forms[direction] == "unresolved": + run.cause( + _RANK_FORMS, R.FORMS_UNRESOLVED, f"{address}: {direction} of SG({label})" + ) + if forms is not None and forms[direction] == "absent": + retention = inline_retention( + address, direction, parent=parent, identity=identity + ) + if retention is R.GROUP_RETAINED_INLINE: + run.cause( + _RANK_RETAINED, + R.GROUP_RETAINED_INLINE, + f"{address}: {direction} of SG({label})", + ) + elif retention is R.IDENTITY_MISSING: + run.cause( + _RANK_RETAINED, + R.IDENTITY_MISSING, + f"{address}: {direction} of SG({label})", + ) + for rule in _side_rules(view, direction): + if rule.unsupported: + run.cause( + _RANK_VALUE, + R.RULE_UNSUPPORTED, + f"{rule.source_address} ({rule.target})", + ) + for address, view in groups.items(): + if address.startswith("UNRESOLVED:"): + for rule in (*view.ingress, *view.egress, *view.unresolved_direction): + if rule.unsupported: + run.cause( + _RANK_VALUE, R.RULE_UNSUPPORTED, f"{rule.source_address} ({address})" + ) + + def _routes(self) -> None: + run = self.run + if self.d_end.resource is None: + return + groups_vpcs = [] + for address in self.sg_d.groups: + fact = read_group_network(run.by_address[address]).vpc_id + groups_vpcs.append(run.vpc_of(fact, f"SG(D) {address}")) + known = sorted({v for v in groups_vpcs if v is not None}) + if len(known) > 1: + run.cause( + _RANK_MODEL, + R.MODEL_UNSUPPORTED, + f"the groups of D are in different VPCs: {', '.join(known)} (M1)", + ) + elif len(known) == 1 and None not in groups_vpcs: + self.vpc_d = known[0] + self.net_d = run.network_of(self.vpc_d, "VPC(D)") + if self.net_d is None: + return # the VPC of D is not known, so the routes of M3 cannot be judged here + for resource in run.inputs.candidate_resources: + if resource.resource_type == "aws_route_table": + self._table(resource) + + def _table(self, resource: Resource) -> None: + run = self.run + if resource.support_status is not ResourceSupport.SUPPORTED: + run.cause( + _RANK_ROUTE, + R.ROUTE_UNSUPPORTED, + f"{resource.address} is a placeholder, it may be a route table of VPC(D)", + ) + return + table = read_route_table(resource) + ours = self._ours(table) + if ours == "no": + return + where = "" if ours == "yes" else " (its vpc_id is unresolved, it may be VPC(D)'s)" + if table.propagating_vgws_present: + run.cause( + _RANK_VGWS, R.ROUTE_UNSUPPORTED, f"{table.address} sets propagating_vgws{where}" + ) + if table.routes_unresolved is not None: + run.cause( + _RANK_ROUTE, + R.ROUTE_UNSUPPORTED, + f"{table.address}: its routes cannot be fixed ({table.routes_unresolved}){where}", + ) + assert self.net_d is not None + for route in table.routes: + if route.state == "ipv6_only": + continue + if route.state in ("unresolved", "unsupported"): + run.cause( + _RANK_ROUTE, + R.ROUTE_UNSUPPORTED, + f"{table.address}: a route whose destination is {route.state}{where}", + ) + continue + assert route.destination is not None + inside = ( + route.destination.first >= self.net_d.first + and route.destination.last <= self.net_d.last + ) + if inside and route.target != "local": + text = _network_text(route.destination) + run.cause( + _RANK_ROUTE, + R.ROUTE_UNSUPPORTED, + f"{table.address}: {text} is inside the VPC CIDR, target {route.target}{where}", + ) + + def _ours(self, table: RouteTableView) -> str: + fact = table.vpc_id + if fact.state == KNOWN: + return ( + "yes" if isinstance(fact.value, Ref) and fact.value.address == self.vpc_d else "no" + ) + if fact.state == ABSENT_STATE: + return "no" + return "maybe" # unresolved or unsupported: it may be the VPC of D + + # --- row 3 ----------------------------------------------------------------------------------- + + def check_listener(self) -> None: + db = self.database + if db is None: + return + run = self.run + kind, port = _coerce_port(db.port) + if kind == "value": + if port != PORT: + raise run.stop(F, 3, R.PORT_MISMATCH, f"{db.address}.port is {port}") + return + if kind == "unresolved": + run.unresolved.append(f"{db.address}: port {db.port.reason}") + return + engine = db.engine + if engine.state == UNKNOWN_STATE: + run.unresolved.append(f"{db.address}: engine {engine.reason}") + elif engine.state == KNOWN and str(engine.value).lower() != "postgres": + raise run.stop(F, 3, R.PORT_MISMATCH, f"{db.address}.engine is {engine.value}") + + # --- rows 6 to 9 ----------------------------------------------------------------------------- + + def reach(self) -> PredicateOutcome: + run, inst, config = self.run, self.instance, self.run.config + assert inst is not None and self.net_d is not None + self._source_address(inst) + if run.causes: # a private_ip or a subnet CIDR that is not an address or a CIDR + raise _Finish(run.finish(S, 2, min(run.causes, key=_Cause.sort_key).code)) + sg_s, sg_d = set(self.sg_s.groups), set(self.sg_d.groups) + target_d = _network_text(self.net_d) + target_s = None if self.addr_s is None else _network_text(self.addr_s) + out_rules = [(g, r) for g in sorted(sg_s) for r in config.groups[g].egress] + in_rules = [(h, r) for h in sorted(sg_d) for r in config.groups[h].ingress] + # E5 and E6 are stated per rule: v4(r) is the CIDR list of one rule, so coverage is not + # pooled across rules + e5 = _first( + out_rules, + lambda _g, r: bool(set(r.source_security_groups) & sg_d) + or covers(r.ipv4_sources, target_d), + ) + e6 = _first( + in_rules, + lambda h, r: bool(set(r.source_security_groups) & sg_s) + or (r.self_reference and h in sg_s) + or (target_s is not None and covers(r.ipv4_sources, target_s)), + ) + run.observations["path"].update( + { + "S": self.s_end.candidate, + "subnet": self.subnet, + "vpc_s": self.vpc_s, + "sg_s": sorted(sg_s), + "egress_rule": e5, + "sg_d": sorted(sg_d), + "ingress_rule": e6, + "vpc_d": self.vpc_d, + } + ) + if e5 is not None and e6 is not None: + return run.finish(P, 6, None) + failing = [name for name, found in (("E5", e5), ("E6", e6)) if found is None] + run.observations["failing_conditions"] = failing + sides = (sg_s, sg_d) + possible = self._possible(failing, sides, out_rules, in_rules, target_d, target_s) + if possible: + run.observations["indeterminate_rules"] = possible + only_groups = all(item["rule"] == "vpc_security_group_ids" for item in possible) + reason = R.ATTRIBUTE_UNRESOLVED if only_groups else R.RULE_INDETERMINATE + return run.finish(U, 7, reason) + partial = _partial(failing, out_rules, in_rules, target_d, target_s) + if partial: + run.observations["partial_coverage"] = partial + return run.finish(U, 8, R.COVERAGE_PARTIAL) + return run.finish(F, 9, R.PATH_MISSING) + + def _source_address(self, inst: Any) -> None: + """ADDR(S): ``private_ip/32`` if it resolves, else the CIDR of the subnet of S (§6.3).""" + run = self.run + fact = inst.private_ip + if fact.state == KNOWN: + try: + if not isinstance(fact.value, str): + raise ValueError("not text") + self.addr_s = parse_network(f"{ipaddress.IPv4Address(fact.value)}/32") + except ValueError: # not text, not an address (CidrError is a ValueError too) + run.cause( + _RANK_VALUE, + R.VALUE_UNSUPPORTED, + f"{inst.address}: private_ip is not an IPv4 address", + ) + return + if fact.state == UNSUPPORTED_STATE: + run.cause(_RANK_VALUE, R.VALUE_UNSUPPORTED, f"{inst.address}: private_ip {fact.reason}") + return + assert self.subnet is not None + cidr = read_subnet(run.by_address[self.subnet]).cidr_block + if cidr.state == KNOWN and isinstance(cidr.value, str): + try: + self.addr_s = parse_network(cidr.value) + except CidrError: + run.cause( + _RANK_VALUE, R.VALUE_UNSUPPORTED, f"{self.subnet}: cidr_block is not a CIDR" + ) + elif cidr.state == ABSENT_STATE: + run.cause(_RANK_MODEL, R.MODEL_UNSUPPORTED, f"{self.subnet}: cidr_block is not written") + elif cidr.state == UNSUPPORTED_STATE: + run.cause(_RANK_VALUE, R.VALUE_UNSUPPORTED, f"{self.subnet}: cidr_block {cidr.reason}") + # unresolved: ADDR(S) stays unknown, so E6 cannot be judged by a CIDR (see _possible) + + def _possible( + self, + failing: list[str], + sides: tuple[set[str], set[str]], + out_rules: list[tuple[str, Rule]], + in_rules: list[tuple[str, Rule]], + target_d: str, + target_s: str | None, + ) -> list[dict[str, Any]]: + """What could still supply the missing permission (row 7).""" + config = self.run.config + sg_s, sg_d = sides + found: list[dict[str, Any]] = [] + for condition in failing: + wanted = "EGRESS" if condition == "E5" else "INGRESS" + own = sg_s if condition == "E5" else sg_d + side = out_rules if condition == "E5" else in_rules + candidates: list[tuple[str | None, Rule]] = [ + (g, r) for g, r in side if not r.determinate and not r.unsupported + ] + for member in sorted(own): # a rule with no direction counts for every direction + candidates += [ + (member, r) + for r in config.groups[member].unresolved_direction + if not r.unsupported + ] + for address, view in sorted(config.groups.items()): # an unresolved target may be ours + if address.startswith("UNRESOLVED:"): + every = (*view.ingress, *view.egress, *view.unresolved_direction) + candidates += [ + (None, r) + for r in every + if r.direction in (wanted, None) and not r.unsupported + ] + for group, rule in candidates: + if may_permit_tcp( + rule.protocol, rule.from_port, rule.to_port, PORT + ) and _could_match(condition, group, rule, sg_s, sg_d, target_d, target_s): + found.append(_entry(condition, rule)) + found += [ + _entry(condition, None) + for address in config.unknown_resources + if address.startswith("aws_security_group_rule.") + ] + if ( + condition == "E6" and target_s is None + ): # ADDR(S) is not known: a CIDR cannot be judged + found += [ + _entry(condition, r, "ADDR(S) is not known") + for _, r in in_rules + if r.determinate + and permits_tcp(r.protocol, r.from_port, r.to_port, PORT) + and r.ipv4_sources + ] + if self.sg_s.unresolved: + found.append( + { + "condition": condition, + "rule": "vpc_security_group_ids", + "reasons": sorted(self.sg_s.unresolved), + } + ) + unique = {(i["condition"], i["rule"], tuple(i["reasons"])): i for i in found} + return [unique[key] for key in sorted(unique)] + + +# --- helpers -------------------------------------------------------------------------------------- + + +def _first(pairs: list[tuple[str, Rule]], holds: Callable[[str, Rule], bool]) -> str | None: + """The first determinate rule of the side that permits TCP/5432 and satisfies ``holds``.""" + for group, rule in pairs: + permitted = rule.determinate and permits_tcp( + rule.protocol, rule.from_port, rule.to_port, PORT + ) + if permitted and holds(group, rule): + return rule.source_address + return None + + +def _could_match( + condition: str, + group: str | None, + rule: Rule, + sg_s: set[str], + sg_d: set[str], + target_d: str, + target_s: str | None, +) -> bool: + """Whether an indeterminate rule (that could permit TCP/5432) could be the one E5 or E6 needs: + its satisfying side is unresolved, or resolved and matching, or only partly matching. A + resolved satisfying side beside an unresolved port or protocol counts (C-153).""" + if rule.sources_unresolved or rule.prefix_list_ids or rule.ipv4_unresolved: + return True + if condition == "E5": + return bool(set(rule.source_security_groups) & sg_d) or overlaps( + rule.ipv4_sources, target_d + ) + if rule.self_unresolved or (rule.self_reference and (group is None or group in sg_s)): + return True + if set(rule.source_security_groups) & sg_s: + return True + return target_s is None or overlaps(rule.ipv4_sources, target_s) + + +def _partial( + failing: list[str], + out_rules: list[tuple[str, Rule]], + in_rules: list[tuple[str, Rule]], + target_d: str, + target_s: str | None, +) -> list[dict[str, Any]]: + """Row 8: a CIDR of a rule that permits TCP/5432 overlaps the target without covering it.""" + found = [] + for condition in failing: + pairs, target = (out_rules, target_d) if condition == "E5" else (in_rules, target_s) + if target is None: + continue + for _, rule in pairs: + if ( + rule.determinate + and permits_tcp(rule.protocol, rule.from_port, rule.to_port, PORT) + and overlaps(rule.ipv4_sources, target) + ): + found.append( + {"condition": condition, "rule": rule.source_address, "target": target} + ) + return sorted(found, key=lambda item: (item["condition"], item["rule"])) + + +def _side_rules(view: GroupView, direction: str) -> tuple[Rule, ...]: + """The rules a side reads: the egress rules of SG(S) or the ingress rules of SG(D), and the + rules with no direction, which count for both.""" + return (view.egress if direction == "egress" else view.ingress) + view.unresolved_direction + + +def _network_text(network: Network) -> str: + cls = ipaddress.IPv4Network if network.version == 4 else ipaddress.IPv6Network + size = network.last - network.first + 1 + prefix = (32 if network.version == 4 else 128) - (size.bit_length() - 1) + return str(cls((network.first, prefix))) + + +def _entry(condition: str, rule: Rule | None, note: str | None = None) -> dict[str, Any]: + if rule is None: + return { + "condition": condition, + "rule": "placeholder", + "reasons": ["rule resource with an unknown count"], + } + reasons = [*rule.problems, *([note] if note else [])] + return {"condition": condition, "rule": rule.source_address, "reasons": reasons} diff --git a/core/verification/retention.py b/core/verification/retention.py index 9c6f640..d201dfa 100644 --- a/core/verification/retention.py +++ b/core/verification/retention.py @@ -32,9 +32,8 @@ from core.domain.identity import IdentityMatch, IdentityReport from core.domain.resource import Resource from core.domain.verification import VerificationReason -from core.verification.views import SECURITY_GROUP_TYPE, inline_form +from core.verification.views import BLOCK_FORMS, SECURITY_GROUP_TYPE, inline_form -BLOCK_FORMS = frozenset({"blocks", "dynamic", "mixed"}) _KEPT_FORMS = BLOCK_FORMS | {"unresolved"} @@ -71,14 +70,16 @@ def _unpaired_trusted(block: str, matches: tuple[IdentityMatch, ...]) -> list[st ] -def ingress_retention( +def inline_retention( address: str, + direction: str, *, parent: Mapping[str, Resource] | None, identity: IdentityReport | None, ) -> VerificationReason | None: - """``None`` when the group retains nothing, ``GROUP_RETAINED_INLINE`` when it keeps the parent's - inline ingress rules, ``IDENTITY_MISSING`` when that cannot be told.""" + """``None`` when the group retains nothing in ``direction`` (``ingress`` or ``egress``), + ``GROUP_RETAINED_INLINE`` when it keeps the parent's inline rules of that direction, + ``IDENTITY_MISSING`` when that cannot be told (registry §2.6, C-84).""" if parent is None: return None if identity is None: @@ -95,6 +96,16 @@ def ingress_retention( continue # a conflicting pairing of two types: not a group, nothing inline to keep if resource.support_status is not ResourceSupport.SUPPORTED: retained = True # a placeholder or unreadable group: cannot rule blocks out - elif inline_form(resource) in _KEPT_FORMS: + elif inline_form(resource, direction) in _KEPT_FORMS: retained = True return VerificationReason.GROUP_RETAINED_INLINE if retained else None + + +def ingress_retention( + address: str, + *, + parent: Mapping[str, Resource] | None, + identity: IdentityReport | None, +) -> VerificationReason | None: + """``inline_retention`` for the ingress direction (INV-SEC-001, INV-SEC-002).""" + return inline_retention(address, "ingress", parent=parent, identity=identity) diff --git a/core/verification/values.py b/core/verification/values.py index 3892aaa..5aa0a6d 100644 --- a/core/verification/values.py +++ b/core/verification/values.py @@ -177,6 +177,14 @@ def has_problem(value: object) -> bool: return first_problem(value) is not None +def has_unresolved(value: object) -> bool: + """Whether ``value`` is, or contains, an unknown or unsupported value. + + Unlike ``has_problem`` a reference counts as resolved: it names a configured resource (registry + §2.2), which is what a source security group normally is.""" + return any(isinstance(item, Unknown | Unsupported) for item in _walk(value)) + + def describe(problem: Unknown | Unsupported | Ref) -> str: """Short stable text of a problem value, for observations.""" if isinstance(problem, Ref): diff --git a/core/verification/views.py b/core/verification/views.py index aa23e66..b4bf523 100644 --- a/core/verification/views.py +++ b/core/verification/views.py @@ -49,6 +49,7 @@ decode_argument, describe, has_problem, + has_unresolved, ) INGRESS: Final = "INGRESS" @@ -83,6 +84,8 @@ _GROUP_KEYS: Final = frozenset({"forms", "inline_indeterminate", "inline_rules"}) _RULE_RESOURCE_KEYS: Final = frozenset({"rule", "target"}) _RULE_FIELDS: Final = ("cidr_blocks", "ipv6_cidr_blocks") +_SOURCE_FIELDS: Final = ("security_groups", "source_security_group_id") +BLOCK_FORMS: Final = frozenset({"blocks", "dynamic", "mixed"}) # "has inline blocks" (registry 2.6) class ViewError(ValueError): @@ -111,6 +114,8 @@ class Rule: problems: tuple[str, ...] ipv4_unresolved: bool = False ipv6_unresolved: bool = False + sources_unresolved: bool = False # the source (or destination) security group is unresolved + self_unresolved: bool = False def core_json(self) -> dict[str, Any]: """The fields that decide equivalence, as ``CanonicalSecurityRule.core_json`` has them.""" @@ -258,6 +263,57 @@ def _resource_families(attributes: Mapping[str, Any], owner: str) -> tuple[bool, return flags[0], flags[1] +def _unresolved_argument(argument: Argument | None) -> bool: + """Like ``_field_unresolved`` but a reference is resolved (source groups, ``self``).""" + if argument is None: + return False + if argument.form != "ATTRIBUTE": + return True + return has_unresolved(argument.value) + + +def _resource_extra(attributes: Mapping[str, Any], owner: str) -> tuple[bool, bool]: + """Exact flags of a rule resource: its source group and ``self`` (C-151).""" + sources = any( + _unresolved_argument(_argument(attributes[name], f"{owner}.{name}")) + for name in _SOURCE_FIELDS + if name in attributes + ) + own = "self" in attributes and _unresolved_argument( + _argument(attributes["self"], f"{owner}.self") + ) + return sources, own + + +def _direction_extra(encoded: object, owner: str, name: str) -> tuple[bool, bool]: + """For one direction of a group: whether some block leaves a source group, or ``self``, + unresolved (the union over the blocks, like the family flags of C-149).""" + if encoded is None: + return False, False + argument = _argument(encoded, f"{owner}.{name}") + sources = own = False + if argument.form == "ATTRIBUTE": + value = argument.value + elements: tuple[Any, ...] = () + if isinstance(value, tuple): + elements = value + elif isinstance(value, SetValue): + elements = value.items + for element in elements: + if isinstance(element, Mapping): + sources = sources or any( + has_problem(element.get(field)) for field in _SOURCE_FIELDS + ) + own = own or has_unresolved(element.get("self")) + return sources, own + for block in argument.blocks: + sources = sources or any( + _unresolved_argument(block.arguments.get(field)) for field in _SOURCE_FIELDS + ) + own = own or _unresolved_argument(block.arguments.get("self")) + return sources, own + + def _direction_details( encoded: object, owner: str, name: str ) -> tuple[bool, bool, tuple[str, ...]]: @@ -331,6 +387,7 @@ def _group_parts( details = { name: _direction_details(attributes.get(name), owner, name) for name, _ in DIRECTIONS } + extra = {name: _direction_extra(attributes.get(name), owner, name) for name, _ in DIRECTIONS} rules = [] for view in security["inline_rules"]: rule = read_rule(view, owner=owner) @@ -338,7 +395,13 @@ def _group_parts( raise _fail(owner, "an inline rule must be INLINE and have a direction") if not rule.determinate: name = "ingress" if rule.direction == INGRESS else "egress" - rule = replace(rule, ipv4_unresolved=details[name][0], ipv6_unresolved=details[name][1]) + rule = replace( + rule, + ipv4_unresolved=details[name][0], + ipv6_unresolved=details[name][1], + sources_unresolved=extra[name][0], + self_unresolved=extra[name][1], + ) rules.append(rule) blocks = {name: details[name][2] for name, _ in DIRECTIONS} return rules, MappingProxyType(dict(forms)), tuple(security["inline_indeterminate"]), blocks @@ -350,8 +413,16 @@ def _rule_of_resource(resource: Resource) -> Rule: if rule.origin != ORIGIN_RULE_RESOURCE: raise _fail(resource.address, "a rule resource's rule must be RULE_RESOURCE") if not rule.determinate: - v4, v6 = _resource_families(thaw_json(resource.attributes), resource.address) - rule = replace(rule, ipv4_unresolved=v4, ipv6_unresolved=v6) + attributes = thaw_json(resource.attributes) + v4, v6 = _resource_families(attributes, resource.address) + sources, own = _resource_extra(attributes, resource.address) + rule = replace( + rule, + ipv4_unresolved=v4, + ipv6_unresolved=v6, + sources_unresolved=sources, + self_unresolved=own, + ) return rule @@ -423,3 +494,31 @@ def inline_form(resource: Resource, direction: str = "ingress") -> str | None: return None forms = _group_parts(resource)[1] return forms[direction] + + +def group_is_mixed(view: GroupView) -> bool: + """Registry §2.6 MIXED (C-84), reading a direction that cannot be fixed conservatively. + + A configured group is MIXED when it has inline blocks (in either direction) and is also the + target of a rule resource, or when a direction is an explicit empty list and a rule resource + of that direction (or of an unresolved direction) targets it. If a direction cannot be fixed, + whether inline blocks exist cannot be told, so a rule resource makes it MIXED. A pseudo-group + has no inline form and is never MIXED.""" + forms = view.forms + rule_resources = [ + rule + for rule in (*view.ingress, *view.egress, *view.unresolved_direction) + if rule.origin == ORIGIN_RULE_RESOURCE + ] + if forms is None or not rule_resources: + return False + if any(forms[name] in BLOCK_FORMS for name in ("ingress", "egress")): + return True + if any(forms[name] == "unresolved" for name in ("ingress", "egress")): + return True + for name, direction in DIRECTIONS: + if forms[name] == "explicit_empty" and any( + rule.direction in (direction, None) for rule in rule_resources + ): + return True + return False diff --git a/docs/DECISIONS_REGISTER.md b/docs/DECISIONS_REGISTER.md index 814773e..70c5deb 100644 --- a/docs/DECISIONS_REGISTER.md +++ b/docs/DECISIONS_REGISTER.md @@ -164,5 +164,5 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-150 | P5a: registry §3.3 drops an indeterminate rule whose sources are known | Registry §3.3 defines `possible4(g)` as an indeterminate rule that could permit TCP/p **and** whose IPv4 sources are unresolved or include a prefix list (`possible6` likewise). A rule whose protocol or port is unresolved but whose IPv4 source is known, for example `from_port = var.p` with `cidr_blocks = ["0.0.0.0/0"]`, is indeterminate, could permit the port, but has resolved sources, so it is not `possible`, is not in `D(g)` (not determinate), and the registry text gives PASS although the rule may open the port to the internet. **Implemented verbatim** (work package: no reinterpretation), pinned by `TestRegistryGap` in `tests/unit/test_verification_public_ingress.py`, and the rule is reported in the observation `indeterminate_rules`. It is the one place where the registry text lets a PASS stand on a rule whose meaning is unresolved, against "uncertainty is never a pass" (CLAUDE.md). The independent oracle follows the same text, so the two would agree and both be unsound for this case. **Proposed amendment, for the authors:** `possible` also when the family's sources are known and non-empty (what C-146 already does for a rule with an unresolved direction); a new registry file and version bump under C-85. **Question: amend, or accept and state as a limitation?** | Open (found 28 Oct 2026; P5a step 4) | | C-151 | P5b: FUNC verifier boundary, entry and parameters | `core/verification/reachability.py` (the predicate) and `core/verification/func_view.py` (the reader of the stored resources) import only the standard library and `core.domain`, like the rest of `core.verification` (contract rule R17, nothing loosened; the self-test now names both modules). The verifier is registered in `dispatch.DEFAULT_VERIFIERS` under `dispatch.REACHABILITY_CFG` = `("dail.verify.reachability_cfg", "1")`, read from the definition, not retyped; a pair that is missing from the table is still UNSUPPORTED `verifier.not_available`. Entry: `evaluate_reachability(definition, inputs) -> PredicateOutcome`. The endpoints are `definition.predicate["parameters"]` = `{S, D, port}`; a definition without text `S` and `D`, with `S == D`, or with `port != 5432` is UNSUPPORTED `parameters.invalid`, never PASS. An endpoint of the wrong type (S not an `aws_instance`, D not an `aws_db_instance`) is UNSUPPORTED `parameters.invalid`. A stored value the reader cannot read raises `ViewError`, which the engine turns into VERIFIER_ERROR; "cannot read" is never "absent". **Shared code:** the MIXED test (registry §2.6) moves from `public_ingress` to `views.group_is_mixed` and RETAINED-INLINE gets a direction parameter (`retention.inline_retention`, with `ingress_retention` as the same call for ingress), so FUNC reads the egress of `SG(S)` and the ingress of `SG(D)` with the one definition; `views.Rule` gains the flags `sources_unresolved` and `self_unresolved` (read like the family flags of C-149); `cidr.py` gains `overlaps`. The SEC results are unchanged and the whole SEC test suite is the check. New reason codes (closed vocabulary): `parameters.invalid`, `endpoint.absent`, `port.mismatch`, `vpc.mismatch`, `path.missing`, `coverage.partial`, `route.unsupported`, `interface.unsupported`, `value.unsupported`, `model.unsupported`. | Proposed (P5b) | | C-152 | P5b: endpoint resolution across moves, and indeterminate endpoints | The bindings `S` and `D` are addresses of the **trusted** state (registry §6.1). A baseline resolves a binding by address in the candidate; an address that no candidate resource has is absent (row 1, FAIL, `endpoint.absent`). A candidate with a parent resolves it through the identity report (registry §2.3, moves followed): the match whose `trusted_resource_ref` is the binding; UNCHANGED, MODIFIED and REPLACED give the candidate resource of the match; **DELETED is absent** (row 1); **UNCERTAIN, a placeholder (unknown `count` or `for_each`, support status UNKNOWN) and a resource that is itself UNSUPPORTED are indeterminate**: UNKNOWN (row 4), never FAIL, never PASS. **Registry reading, flagged:** registry §2.4 would call an UNSUPPORTED endpoint resource UNSUPPORTED rather than UNKNOWN; the work package says UNKNOWN and both are lack of proof, so the work package is followed and the question goes to the reviewer. A candidate that has a parent but no identity report, or a report with no match for the binding while the parent has the resource, is UNSUPPORTED `identity.missing` (as in P5a). A binding that the parent does not have either is UNSUPPORTED `parameters.invalid` (the definitions and the trusted state disagree). **A created endpoint** (the candidate creates the resource at another address and the old one is DELETED) is FAIL by row 1: no heuristic match is made; only a `moved` block or an identity match ties a new address to the trusted one. The observation `endpoints` records, per binding, the trusted address, the match change type and the candidate address. | Proposed (P5b) | -| C-153 | P5b: rows 1 to 9 and the definitions they need | The rows of registry §6.4 are evaluated in order and the first that applies returns. Row 2 collects every cause it can evaluate, reports all of them in the observation `row2_causes` and names the reason by the first in this fixed order: relevant-unsupported type, M3 route, `propagating_vgws`, interface block, name-based `security_groups`, no `vpc_security_group_ids` or no `subnet_id`, MIXED, RETAINED-INLINE, `unresolved` direction form (C-120(c)), unsupported value or rule, other. **Definitions** (each with the registry text it makes precise): `SG(S)` and `SG(D)` are the groups that the `vpc_security_group_ids` of `S` and `D` reference; `src_sg(r)` is `source_security_groups` of the stored rule view (a reference gives the address of the group; a literal AWS id gives `EXTERNAL:` and matches no configured group), so "src_sg(r) contains a group in SG(D)" is a non-empty intersection of addresses; `self(r)` is the stored `self` flag and E6 needs `h in SG(S)`; the CIDR clauses use `cidr.covers` on the IPv4 sources of determinate rules that permit TCP/5432 (`ports.permits_tcp`), pooled over the groups of the side; **"partly covers"** (row 8) is `cidr.overlaps`: the pooled sources of rules that permit TCP/5432 intersect the target but do not contain it (interval arithmetic, no enumeration); `ADDR(S)` is `private_ip/32` if it resolves to an IPv4 address, else the `cidr_block` of the subnet of `S`; an unresolved subnet CIDR makes the clause unresolved. **"An indeterminate rule could satisfy" E5 or E6** (row 7): a rule of the side (an egress rule of a group in `SG(S)` for E5, an ingress rule of a group in `SG(D)` for E6, a rule with direction `None` for either, a rule of an `UNRESOLVED:*` pseudo-group, a rule resource that is an UNKNOWN placeholder) that is not determinate, is not unsupported, **could permit TCP/5432** (`ports.may_permit_tcp`, so an unresolved protocol or port counts) **and whose satisfying side could match**: its group sources are unresolved or could be the other side's groups, its IPv4 sources are unresolved, include a prefix list, or cover or partly cover the target, or (E6) its `self` is unresolved. **Counted:** an indeterminate rule with a resolved satisfying source and an unresolved port or protocol is counted (UNKNOWN), because the rule could supply the permission; this is the safe direction and it is the mirror of the gap of C-150 (where SEC `possible` text drops such a rule and can give PASS); here dropping it could give an unsound FAIL, so it is not dropped. When both E5 and E6 fail, row 7 applies if either failing condition could be satisfied by an indeterminate rule (registry text: "it"; the more cautious reading), then row 8. **Where the registry is silent (R5), UNSUPPORTED and listed as a spec gap:** a `vpc_id` of a group in `SG(D)`, of `S`'s subnet or of a route table that is a literal id rather than a reference to a configured `aws_vpc` (the VPC CIDR is then unknown); a literal AWS id in `vpc_security_group_ids`; `D` with neither `port` nor `engine`; a route table whose `vpc_id` is unresolved and that has an M3 candidate route or `propagating_vgws` (it may be the VPC of `D`); an unresolved or unsupported route destination or target in a route table of `VPC(D)`, a dynamic route expansion that cannot be fixed, an unsupported value of a field the path reads, an invalid `private_ip`. **Unresolved values (row 4):** an unresolved `vpc_security_group_ids`, group `vpc_id`, `subnet_id`, subnet `vpc_id` or an unresolved `D.port` (**gap:** registry row 4 names E3 and E4 but not E2; an unresolved E2 cannot be PASS, so it is UNKNOWN). **M3:** a route of a route table of `VPC(D)` whose IPv4 `cidr_block` lies inside the CIDR of that VPC and whose target is not `local` (`gateway_id = "local"` and no other target); IPv6-only routes are not read (M5); a route wider than the VPC CIDR never applies. Rows 3 and 5 FAIL only on resolved values. | Proposed (P5b) | -| C-154 | P5b: assumptions, observations and the baseline list | The result's `assumptions`, sorted: `IPv4 only`, `M1: RDS security groups and subnet group share one VPC (C-15, C-77, uncited)`, `M4: default network ACL assumed (no NACL type present)`, and `tolerated type: aws_db_subnet_group (C-15)` when that type is present. Closed observation keys: `row`, `reason`, `endpoints`, `port`, `path` (`S`, `subnet`, `vpc_s`, `sg_s`, `egress_rule`, `sg_d`, `ingress_rule`, `vpc_d`; a part that is not reached is null), `row2_causes`, `failing_conditions`, `indeterminate_rules`, `partial_coverage`, `relevant_unsupported`. `baseline.py`: the relevant-unsupported list of a created resource becomes the 26 types of registry §2.7 for INV-FUNC-001 (`core.domain.registry_v1.FUNC_RELEVANT_UNSUPPORTED`, which contains the three of the security list), so a created resource of any of them is UNSUPPORTED `type.relevant_unsupported`, not PASS with `applicable = false`; the predicate lists for INV-SEC-001/002 do not change. | Proposed (P5b) | +| C-153 | P5b: rows 1 to 9 and the definitions they need | The rows of registry §6.4 are evaluated in order and the first that applies returns. Row 2 collects every cause it can evaluate, reports all of them in the observation `row2_causes` and names the reason by the first in this fixed order: relevant-unsupported type, M3 route, `propagating_vgws`, interface block, name-based `security_groups`, no `vpc_security_group_ids` or no `subnet_id`, MIXED, RETAINED-INLINE, `unresolved` direction form (C-120(c)), unsupported value or rule, other. **Definitions** (each with the registry text it makes precise): `SG(S)` and `SG(D)` are the groups that the `vpc_security_group_ids` of `S` and `D` reference; `src_sg(r)` is `source_security_groups` of the stored rule view (a reference gives the address of the group; a literal AWS id gives `EXTERNAL:` and matches no configured group), so "src_sg(r) contains a group in SG(D)" is a non-empty intersection of addresses; `self(r)` is the stored `self` flag and E6 needs `h in SG(S)`; the CIDR clauses use `cidr.covers` on the IPv4 sources of **one** determinate rule that permits TCP/5432 (`ports.permits_tcp`): E5 and E6 say "exists r with ... v4(r) covers" and `v4(r)` is the CIDR list of a single rule, so two rules with half of the range each do not cover it (no pooling across rules; a test pins this); **"partly covers"** (row 8) is `cidr.overlaps`: the IPv4 sources of a determinate rule that permits TCP/5432 intersect the target, and (E5 or E6 failing) no rule covers it (interval arithmetic, no enumeration); `ADDR(S)` is `private_ip/32` if it resolves to an IPv4 address, else the `cidr_block` of the subnet of `S`; an unresolved subnet CIDR makes the clause unresolved. **"An indeterminate rule could satisfy" E5 or E6** (row 7): a rule of the side (an egress rule of a group in `SG(S)` for E5, an ingress rule of a group in `SG(D)` for E6, a rule with direction `None` for either, a rule of an `UNRESOLVED:*` pseudo-group, a rule resource that is an UNKNOWN placeholder) that is not determinate, is not unsupported, **could permit TCP/5432** (`ports.may_permit_tcp`, so an unresolved protocol or port counts) **and whose satisfying side could match**: its group sources are unresolved or could be the other side's groups, its IPv4 sources are unresolved, include a prefix list, or cover or partly cover the target, or (E6) its `self` is unresolved. **Counted:** an indeterminate rule with a resolved satisfying source and an unresolved port or protocol is counted (UNKNOWN), because the rule could supply the permission; this is the safe direction and it is the mirror of the gap of C-150 (where SEC `possible` text drops such a rule and can give PASS); here dropping it could give an unsound FAIL, so it is not dropped. When both E5 and E6 fail, row 7 applies if either failing condition could be satisfied by an indeterminate rule (registry text: "it"; the more cautious reading), then row 8. **Where the registry is silent (R5), UNSUPPORTED and listed as a spec gap:** a `vpc_id` of a group in `SG(D)`, of `S`'s subnet or of a route table that is a literal id rather than a reference to a configured `aws_vpc` (the VPC CIDR is then unknown); a literal AWS id in `vpc_security_group_ids`; `D` with neither `port` nor `engine`; a route table whose `vpc_id` is unresolved and that has an M3 candidate route or `propagating_vgws` (it may be the VPC of `D`); an unresolved or unsupported route destination or target in a route table of `VPC(D)`, a dynamic route expansion that cannot be fixed, an unsupported value of a field the path reads, an invalid `private_ip`. **Unresolved values (row 4):** an unresolved `vpc_security_group_ids`, group `vpc_id`, `subnet_id`, subnet `vpc_id` or an unresolved `D.port` (**gap:** registry row 4 names E3 and E4 but not E2; an unresolved E2 cannot be PASS, so it is UNKNOWN). **M3:** a route of a route table of `VPC(D)` whose IPv4 `cidr_block` lies inside the CIDR of that VPC and whose target is not `local` (`gateway_id = "local"` and no other target); IPv6-only routes are not read (M5); a route wider than the VPC CIDR never applies. Rows 3 and 5 FAIL only on resolved values. | Proposed (P5b) | +| C-154 | P5b: assumptions, observations and the baseline list | The result's `assumptions`, sorted: `IPv4 only`, `M1: RDS security groups and subnet group share one VPC (C-15, C-77, uncited)`, `M4: default network ACL assumed (no NACL type present)`, and `tolerated type: aws_db_subnet_group (C-15)` when that type is present. Closed observation keys (present on every path): `row`, `reason`, `detail`, `endpoints`, `port`, `unresolved` (why row 4 applies), `path` (`S`, `subnet`, `vpc_s`, `sg_s`, `egress_rule`, `sg_d`, `ingress_rule`, `vpc_d`; a part that is not reached is null), `row2_causes`, `failing_conditions`, `indeterminate_rules`, `partial_coverage`, `relevant_unsupported`. `baseline.py`: the relevant-unsupported list of a created resource becomes the 26 types of registry §2.7 for INV-FUNC-001 (`core.domain.registry_v1.FUNC_RELEVANT_UNSUPPORTED`, which contains the three of the security list), so a created resource of any of them is UNSUPPORTED `type.relevant_unsupported`, not PASS with `applicable = false`; the predicate lists for INV-SEC-001/002 do not change. | Proposed (P5b) | diff --git a/tests/func_builders.py b/tests/func_builders.py index 522748b..0d257dc 100644 --- a/tests/func_builders.py +++ b/tests/func_builders.py @@ -21,6 +21,51 @@ DESTINATION = "aws_db_instance.database" +APP_TO_DB = """resource "aws_security_group_rule" "app_to_db_5432" { + type = "ingress" + protocol = "tcp" + from_port = 5432 + to_port = 5432 + source_security_group_id = aws_security_group.app.id + security_group_id = aws_security_group.db.id +} +""" +APP_EGRESS = """resource "aws_security_group_rule" "app_egress_all" { + type = "egress" + protocol = "-1" + from_port = 0 + to_port = 0 + cidr_blocks = ["0.0.0.0/0"] + security_group_id = aws_security_group.app.id +} +""" +IGW_ROUTE = """ + route { + cidr_block = "0.0.0.0/0" + gateway_id = aws_internet_gateway.igw.id + } +""" +SOURCE_LINE = " source_security_group_id = aws_security_group.app.id\n" +SUBNET_LINE = " subnet_id = aws_subnet.app.id\n" +PUBLIC_IP_LINE = " associate_public_ip_address = true\n}" +DB_GROUP = """resource "aws_security_group" "db" { + name = "db" + description = "Database security group" + vpc_id = aws_vpc.main.id + egress = [] +} +""" +APP_GROUP = """resource "aws_security_group" "app" { + name = "app" + description = "Application security group" + vpc_id = aws_vpc.main.id + ingress = [] +} +""" +DB_SGS_LINE = " vpc_security_group_ids = [aws_security_group.db.id]\n" +APP_SGS_LINE = " vpc_security_group_ids = [aws_security_group.app.id]\n" + + def canonical() -> str: """The canonical configuration text (a PASS for INV-FUNC-001, registry F1).""" return CANONICAL_PATH.read_text(encoding="utf-8") diff --git a/tests/reach_builders.py b/tests/reach_builders.py new file mode 100644 index 0000000..5fa4f04 --- /dev/null +++ b/tests/reach_builders.py @@ -0,0 +1,29 @@ +"""The reachability verifier driven from Terraform text (P5b). Not a test module. + +Standard library plus ``core.*`` (tests may import every package; ``core.verification`` may not). +""" + +from __future__ import annotations + +from core.domain.invariant import Invariant +from core.verification.inputs import VerificationInputs +from core.verification.outcome import PredicateOutcome +from core.verification.reachability import evaluate_reachability +from tests.pipeline_builders import inputs_for + + +def inputs(text: str, parent: str | None = None) -> VerificationInputs: + """Inputs for a candidate text (and the pipeline of its parent text); no graphs are built.""" + return inputs_for(text, parent, with_graphs=False) + + +def definition(of: VerificationInputs) -> Invariant: + found = of.invariant("INV-FUNC-001", 1) + assert found is not None + return found + + +def evaluate(text: str, parent: str | None = None) -> PredicateOutcome: + """INV-FUNC-001 for a candidate text, with the identity of its parent text if it has one.""" + given = inputs(text, parent) + return evaluate_reachability(definition(given), given) diff --git a/tests/unit/test_reachability_predicate.py b/tests/unit/test_reachability_predicate.py new file mode 100644 index 0000000..37f51ce --- /dev/null +++ b/tests/unit/test_reachability_predicate.py @@ -0,0 +1,875 @@ +"""INV-FUNC-001, row by row (P5b step 4; registry §6.2, §6.3, §6.4; C-151 to C-154). + +Every expected value is derived by hand from the registry text on the canonical topology (see the +derivation in ``test_reachability_vectors.py``): E5 and E6 are stated per rule (``v4(r)`` is the +CIDR list of one rule, so coverage is not pooled across rules); row 7 is "an indeterminate rule +could satisfy it"; row 2 comes before rows 3 to 9 and row 1 before row 2. Where the registry is +silent the choice is UNSUPPORTED (R5) or the cautious reading, and the test says so. +""" + +from __future__ import annotations + +import dataclasses +import random +import unittest +from collections.abc import Callable +from typing import Any + +from core.domain.enums import VerificationResult +from core.domain.invariant import Invariant +from core.domain.jsonvalue import thaw_json +from core.domain.resource import Resource +from core.domain.verification import VerificationReason +from core.verification.inputs import VerificationInputs +from core.verification.outcome import PredicateOutcome +from core.verification.reachability import evaluate_reachability +from tests.func_builders import ( + APP_EGRESS, + APP_GROUP, + APP_SGS_LINE, + APP_TO_DB, + DB_GROUP, + DB_SGS_LINE, + PUBLIC_IP_LINE, + SUBNET_LINE, + attribute, + canonical, + edit, + edits, + with_attributes, +) +from tests.reach_builders import definition, evaluate, inputs + +P, F, U, S = ( + VerificationResult.PASS, + VerificationResult.FAIL, + VerificationResult.UNKNOWN, + VerificationResult.UNSUPPORTED, +) +R = VerificationReason +VAR = 'variable "u" {}\n' +TABLE = 'resource "aws_route_table" "public" {\n vpc_id = aws_vpc.main.id\n' +INGRESS_BLOCK = ( + '\n ingress {\n protocol = "tcp"\n from_port = 22\n to_port = 22\n' + ' cidr_blocks = ["10.0.0.0/8"]\n }\n' +) +EGRESS_BLOCK = ( + '\n egress {\n protocol = "-1"\n from_port = 0\n to_port = 0\n' + ' cidr_blocks = ["0.0.0.0/0"]\n }\n' +) + + +def rule( + name: str, kind: str, protocol: str, low: int, high: int, group: str, body: str = "" +) -> str: + """A rule resource in the style of the canonical file.""" + return ( + f'resource "aws_security_group_rule" "{name}" {{\n type = "{kind}"\n' + f' protocol = "{protocol}"\n from_port = {low}\n to_port = {high}\n' + f" security_group_id = aws_security_group.{group}.id\n{body}}}\n" + ) + + +def ingress_5432(name: str, body: str) -> str: + return rule(name, "ingress", "tcp", 5432, 5432, "db", body) + + +def egress_5432(name: str, body: str) -> str: + return rule(name, "egress", "tcp", 5432, 5432, "app", body) + + +def swap_ingress(body: str) -> str: + """The canonical text with ``app_to_db_5432`` replaced by another ingress rule on ``db``.""" + return edit(canonical(), APP_TO_DB, ingress_5432("ingress_x", body)) + + +def swap_egress(body: str) -> str: + return edit(canonical(), APP_EGRESS, egress_5432("egress_x", body)) + + +class Check(unittest.TestCase): + def check( + self, + outcome: PredicateOutcome, + result: VerificationResult, + row: int, + reason: VerificationReason | None, + ) -> None: + self.assertEqual( + (outcome.result, outcome.observations["row"], outcome.reason), + (result, row, reason), + outcome.observations, + ) + + +def replaced( + given: VerificationInputs, address: str, build: Callable[[Resource], Resource] +) -> VerificationInputs: + found = [build(r) if r.address == address else r for r in given.candidate_resources] + return dataclasses.replace(given, candidate_resources=tuple(found)) + + +def with_parameters(given: VerificationInputs, **parameters: Any) -> Invariant: + base = definition(given) + merged = {**thaw_json(base.predicate["parameters"]), **parameters} + merged = {key: value for key, value in merged.items() if value is not None} + return dataclasses.replace(base, predicate={**thaw_json(base.predicate), "parameters": merged}) + + +class TestParameters(Check): + def test_bad_parameters_are_unsupported_never_a_pass(self) -> None: + given = inputs(canonical()) + cases = { + "wrong port": {"port": 3306}, + "no port": {"port": None}, + "no source": {"S": None}, + "empty destination": {"D": ""}, + "same endpoint": {"S": "aws_instance.app", "D": "aws_instance.app"}, + "source of the wrong type": {"S": "aws_subnet.app"}, + "destination of the wrong type": {"D": "aws_instance.app"}, + "a number as the source": {"S": 7}, + } + for name, parameters in cases.items(): + with self.subTest(case=name): + outcome = evaluate_reachability(with_parameters(given, **parameters), given) + self.assertEqual((outcome.result, outcome.reason), (S, R.PARAMETERS_INVALID)) + + def test_parameters_that_are_not_an_object(self) -> None: + given = inputs(canonical()) + base = definition(given) + broken = dataclasses.replace( + base, predicate={"registry": "registry-v1.0", "parameters": "x"} + ) + outcome = evaluate_reachability(broken, given) + self.assertEqual((outcome.result, outcome.reason), (S, R.PARAMETERS_INVALID)) + + def test_a_binding_the_trusted_state_does_not_have(self) -> None: + given = inputs(canonical(), canonical()) + outcome = evaluate_reachability(with_parameters(given, S="aws_instance.ghost"), given) + self.assertEqual((outcome.result, outcome.reason), (S, R.PARAMETERS_INVALID)) + + +class TestEndpoints(Check): + MOVE = "\nmoved {\n from = aws_instance.app\n to = aws_instance.web\n}\n" + + def renamed(self) -> str: + text = canonical().replace('resource "aws_instance" "app"', 'resource "aws_instance" "web"') + self.assertNotEqual(text, canonical()) + return text + + def test_a_moved_source_is_followed(self) -> None: + outcome = evaluate(self.renamed() + self.MOVE, canonical()) + self.check(outcome, P, 6, None) + self.assertEqual(outcome.observations["path"]["S"], "aws_instance.web") + endpoint = outcome.observations["endpoints"]["S"] + self.assertEqual( + (endpoint["trusted"], endpoint["candidate"]), ("aws_instance.app", "aws_instance.web") + ) + self.assertIn(endpoint["match"], ("UNCHANGED", "MODIFIED")) + + def test_a_renamed_source_without_a_move_is_a_created_endpoint_and_the_old_one_is_gone( + self, + ) -> None: + # C-152: no heuristic match; DELETED is absent + outcome = evaluate(self.renamed(), canonical()) + self.check(outcome, F, 1, R.ENDPOINT_ABSENT) + self.assertEqual(outcome.observations["endpoints"]["S"]["match"], "DELETED") + + def test_a_moved_database_is_followed(self) -> None: + text = canonical().replace( + 'resource "aws_db_instance" "database"', 'resource "aws_db_instance" "db2"' + ) + text += "\nmoved {\n from = aws_db_instance.database\n to = aws_db_instance.db2\n}\n" + self.check(evaluate(text, canonical()), P, 6, None) + + def test_an_uncertain_endpoint_is_unknown_never_fail_or_pass(self) -> None: + # a placeholder (unknown count) is always UNCERTAIN in the identity report + text = VAR + edit( + canonical(), + 'resource "aws_instance" "app" {\n', + 'resource "aws_instance" "app" {\n count = var.u\n', + ) + outcome = evaluate(text, canonical()) + self.check(outcome, U, 4, R.RESOURCE_INDETERMINATE) + self.assertEqual(outcome.observations["endpoints"]["S"]["match"], "UNCERTAIN") + + def test_a_placeholder_endpoint_in_a_baseline_is_unknown(self) -> None: + text = VAR + edit( + canonical(), + 'resource "aws_instance" "app" {\n', + 'resource "aws_instance" "app" {\n count = var.u\n', + ) + self.check(evaluate(text), U, 4, R.RESOURCE_INDETERMINATE) + + def test_an_endpoint_that_is_itself_unsupported_is_unknown_by_c_152(self) -> None: + given = inputs(canonical()) + + def broken(resource: Resource) -> Resource: + return Resource.create( + address=resource.address, + resource_type=resource.resource_type, + logical_identity={}, + attributes={"$content": {"$dail": "unsupported", "reason": "limit.json_depth"}}, + security_attributes={}, + semantic_attributes={}, + references=(), + provenance=resource.provenance, + support_status=dataclasses.replace( + resource, support_status=resource.support_status + ).support_status.__class__.UNSUPPORTED, + ) + + outcome = evaluate_reachability( + definition(given), replaced(given, "aws_db_instance.database", broken) + ) + self.check(outcome, U, 4, R.RESOURCE_INDETERMINATE) + + def test_a_parent_without_an_identity_report_is_unsupported(self) -> None: + given = dataclasses.replace(inputs(canonical(), canonical()), identity=None) + outcome = evaluate_reachability(definition(given), given) + self.assertEqual((outcome.result, outcome.reason), (S, R.IDENTITY_MISSING)) + + def test_an_indexed_binding(self) -> None: + text = edit( + canonical(), + 'resource "aws_instance" "app" {\n', + 'resource "aws_instance" "app" {\n count = 1\n', + ) + given = inputs(text) + outcome = evaluate_reachability(with_parameters(given, S="aws_instance.app[0]"), given) + self.check(outcome, P, 6, None) + + def test_an_absent_source_in_a_baseline(self) -> None: + start = canonical().index('resource "aws_instance" "app"') + end = canonical().index('resource "aws_db_subnet_group"') + self.check(evaluate(canonical()[:start] + canonical()[end:]), F, 1, R.ENDPOINT_ABSENT) + + +class TestRowTwo(Check): + def test_row_one_comes_before_row_two(self) -> None: + start = canonical().index('resource "aws_db_subnet_group" "db"') + text = ( + canonical()[:start] + + '\nresource "aws_network_acl" "x" {\n vpc_id = aws_vpc.main.id\n}\n' + ) + self.check(evaluate(text), F, 1, R.ENDPOINT_ABSENT) + + def test_row_two_comes_before_row_three(self) -> None: + text = edit( + canonical(), + " publicly_accessible = false\n", + " publicly_accessible = false\n port = 3306\n", + ) + text += '\nresource "aws_network_acl" "x" {\n vpc_id = aws_vpc.main.id\n}\n' + self.check(evaluate(text), S, 2, R.TYPE_RELEVANT_UNSUPPORTED) + + def test_every_cause_is_reported_and_the_first_in_the_fixed_order_names_the_reason( + self, + ) -> None: + text = canonical() + '\nresource "aws_network_acl" "x" {\n vpc_id = aws_vpc.main.id\n}\n' + text = edit( + text, + PUBLIC_IP_LINE, + " associate_public_ip_address = true\n network_interface {\n device_index = 0\n" + ' network_interface_id = "eni-1"\n }\n}', + ) + outcome = evaluate(text) + self.check(outcome, S, 2, R.TYPE_RELEVANT_UNSUPPORTED) + self.assertEqual( + [c["cause"] for c in outcome.observations["row2_causes"]], + ["type.relevant_unsupported", "interface.unsupported"], + ) + self.assertEqual(outcome.observations["relevant_unsupported"], ["aws_network_acl.x"]) + + def test_name_based_security_groups(self) -> None: + text = edit( + canonical(), + PUBLIC_IP_LINE, + ' associate_public_ip_address = true\n security_groups = ["default"]\n}', + ) + self.check(evaluate(text), S, 2, R.MODEL_UNSUPPORTED) + + def test_an_empty_name_list_uses_nothing(self) -> None: + text = edit( + canonical(), + PUBLIC_IP_LINE, + " associate_public_ip_address = true\n security_groups = []\n}", + ) + self.check(evaluate(text), P, 6, None) + + def test_a_name_list_that_cannot_be_fixed_is_unsupported_by_r5(self) -> None: + text = VAR + edit( + canonical(), + PUBLIC_IP_LINE, + " associate_public_ip_address = true\n security_groups = var.u\n}", + ) + self.check(evaluate(text), S, 2, R.MODEL_UNSUPPORTED) + + def test_the_default_security_group_and_default_vpc_are_not_modelled(self) -> None: + for name, text in { + "S without a subnet": edit(canonical(), SUBNET_LINE, ""), + "S without groups": edit(canonical(), APP_SGS_LINE, ""), + "S with an empty group list": edit( + canonical(), APP_SGS_LINE, " vpc_security_group_ids = []\n" + ), + "D with an empty group list": edit( + canonical(), DB_SGS_LINE, " vpc_security_group_ids = []\n" + ), + }.items(): + with self.subTest(case=name): + self.check(evaluate(text), S, 2, R.MODEL_UNSUPPORTED) + + def test_a_mixed_group_of_either_side(self) -> None: + block = INGRESS_BLOCK + app_with_block = APP_GROUP.replace(" ingress = []\n", "") + app_with_block = app_with_block[: app_with_block.rindex("}")] + block + "}\n" + db_with_block = DB_GROUP[: DB_GROUP.rindex("}")] + block + "}\n" + for group, old, new in ( + ("db", DB_GROUP, db_with_block), + ("app", APP_GROUP, app_with_block), + ): + text = edit(canonical(), old, new) + with self.subTest(group=group): + outcome = evaluate(text) + self.check(outcome, S, 2, R.GROUP_MIXED) + + def test_a_group_outside_both_sides_may_be_mixed(self) -> None: + extra = ( + '\nresource "aws_security_group" "other" {\n vpc_id = aws_vpc.main.id\n' + + INGRESS_BLOCK.lstrip("\n") + + "}\n" + + rule("o", "ingress", "tcp", 80, 80, "other", ' cidr_blocks = ["10.0.0.0/8"]\n') + ) + self.check(evaluate(canonical() + extra), P, 6, None) + + def test_retained_inline_egress_of_the_source_group(self) -> None: + egress_block = EGRESS_BLOCK + parent = edits( + canonical(), + (APP_EGRESS, ""), + (APP_GROUP, APP_GROUP[: APP_GROUP.rindex("}")] + egress_block + "}\n"), + ) + outcome = evaluate(canonical(), parent) + self.check(outcome, S, 2, R.GROUP_RETAINED_INLINE) + self.assertIn("aws_security_group.app", outcome.observations["row2_causes"][0]["detail"]) + + def test_retention_of_the_other_direction_does_not_matter(self) -> None: + # S reads egress only: an ingress retained by the source group is not a cause + ingress_block = INGRESS_BLOCK + app_without = APP_GROUP.replace(" ingress = []\n", "") + parent = edit( + canonical(), APP_GROUP, app_without[: app_without.rindex("}")] + ingress_block + "}\n" + ) + self.check(evaluate(edit(canonical(), APP_GROUP, app_without), parent), P, 6, None) + # D reads ingress only: an egress retained by the database group is not a cause + egress_block = EGRESS_BLOCK + db_without = DB_GROUP.replace(" egress = []\n", "") + parent = edit( + canonical(), DB_GROUP, db_without[: db_without.rindex("}")] + egress_block + "}\n" + ) + self.check(evaluate(edit(canonical(), DB_GROUP, db_without), parent), P, 6, None) + + def test_a_direction_that_cannot_be_fixed_is_unsupported_not_no_rules(self) -> None: + # C-120(c): the egress of SG(S) and the ingress of SG(D) + db = VAR + edits( + canonical(), + (DB_GROUP, DB_GROUP.replace(" egress = []", " ingress = var.u")), + (APP_TO_DB, ""), + ) + self.check(evaluate(db), S, 2, R.FORMS_UNRESOLVED) + app = VAR + edits( + canonical(), + (APP_GROUP, APP_GROUP.replace(" ingress = []", " egress = var.u")), + (APP_EGRESS, ""), + ) + self.check(evaluate(app), S, 2, R.FORMS_UNRESOLVED) + + def test_an_unresolved_direction_beside_a_rule_resource_is_mixed_by_the_conservative_reading( + self, + ) -> None: + text = VAR + edit( + canonical(), APP_GROUP, APP_GROUP.replace(" ingress = []", " ingress = var.u") + ) + self.check(evaluate(text), S, 2, R.GROUP_MIXED) + + def test_an_unsupported_rule_of_a_group_on_either_side(self) -> None: + bad = rule("bad", "egress", "tcp", 80, 80, "app", ' cidr_blocks = ["10.0.0.1/8"]\n') + self.check(evaluate(canonical() + "\n" + bad), S, 2, R.RULE_UNSUPPORTED) + + def test_an_unsupported_rule_of_another_group_is_not_read(self) -> None: + other = '\nresource "aws_security_group" "other" {\n vpc_id = aws_vpc.main.id\n}\n' + text = ( + canonical() + + other + + rule("bad", "egress", "tcp", 80, 80, "other", ' cidr_blocks = ["10.0.0.1/8"]\n') + ) + self.check(evaluate(text), P, 6, None) + + def test_an_unsupported_engine_or_port(self) -> None: + given = inputs(canonical()) + for name in ("engine", "port"): + + def damage(resource: Resource, name: str = name) -> Resource: + attributes = thaw_json(resource.attributes) + attributes[name] = attribute( + {"$dail": "unsupported", "reason": "function.unsupported"} + ) + return with_attributes(resource, attributes) + + with self.subTest(argument=name): + outcome = evaluate_reachability( + definition(given), replaced(given, "aws_db_instance.database", damage) + ) + self.check(outcome, S, 2, R.VALUE_UNSUPPORTED) + + +class TestRoutes(Check): + def routed(self, route_block: str, table: str = TABLE) -> str: + return edit(canonical(), TABLE, table + route_block) + + def test_a_local_route_inside_the_vpc_is_fine(self) -> None: + block = ' route {\n cidr_block = "10.0.0.0/16"\n gateway_id = "local"\n }\n' + self.check(evaluate(self.routed(block)), P, 6, None) + + def test_a_non_local_route_equal_to_the_vpc_cidr_applies(self) -> None: + block = ' route {\n cidr_block = "10.0.0.0/16"\n gateway_id = "igw-1"\n }\n' + self.check(evaluate(self.routed(block)), S, 2, R.ROUTE_UNSUPPORTED) + + def test_a_route_wider_or_outside_never_applies(self) -> None: + for destination in ("10.0.0.0/8", "192.168.0.0/16", "0.0.0.0/1"): + block = ( + f' route {{\n cidr_block = "{destination}"\n' + ' nat_gateway_id = "nat-1"\n }\n' + ) + with self.subTest(destination=destination): + self.check(evaluate(self.routed(block)), P, 6, None) + + def test_an_ipv6_only_route_is_not_read(self) -> None: + block = ' route {\n ipv6_cidr_block = "fd00::/8"\n nat_gateway_id = "nat-1"\n }\n' + self.check(evaluate(self.routed(block)), P, 6, None) + + def test_a_route_table_of_another_vpc_is_not_ours(self) -> None: + other = ( + '\nresource "aws_vpc" "other" {\n cidr_block = "10.1.0.0/16"\n}\n' + '\nresource "aws_route_table" "elsewhere" {\n vpc_id = aws_vpc.other.id\n' + ' propagating_vgws = ["vgw-1"]\n route {\n cidr_block = "10.0.2.0/24"\n' + ' nat_gateway_id = "nat-1"\n }\n}\n' + ) + self.check(evaluate(canonical() + other), P, 6, None) + + def test_a_route_table_of_a_vpc_that_is_not_configured_is_not_ours(self) -> None: + other = ( + '\nresource "aws_route_table" "elsewhere" {\n vpc_id = "vpc-9"\n' + ' route {\n cidr_block = "10.0.2.0/24"\n nat_gateway_id = "nat-1"\n }\n}\n' + ) + self.check(evaluate(canonical() + other), P, 6, None) + + def test_a_route_table_whose_vpc_cannot_be_fixed_may_be_ours(self) -> None: + # registry silent (R5): UNSUPPORTED when it has an M3 route or propagating_vgws + table = ( + VAR + '\nresource "aws_route_table" "maybe" {\n vpc_id = var.u\n' + ' route {\n cidr_block = "10.0.2.0/24"\n nat_gateway_id = "nat-1"\n }\n}\n' + ) + self.check(evaluate(table + canonical()), S, 2, R.ROUTE_UNSUPPORTED) + harmless = ( + VAR + '\nresource "aws_route_table" "maybe" {\n vpc_id = var.u\n' + ' route {\n cidr_block = "0.0.0.0/0"\n nat_gateway_id = "nat-1"\n }\n}\n' + ) + self.check(evaluate(harmless + canonical()), P, 6, None) + + def test_a_destination_target_or_expansion_that_cannot_be_fixed(self) -> None: + cases = { + "destination": ' route {\n cidr_block = var.u\n nat_gateway_id = "nat-1"\n }\n', + "target": ' route {\n cidr_block = "10.0.2.0/24"\n gateway_id = var.u\n }\n', + "prefix list": ( + ' route {\n destination_prefix_list_id = "pl-1"\n' + ' nat_gateway_id = "nat-1"\n }\n' + ), + "expansion": ( + ' dynamic "route" {\n for_each = var.u\n content {\n' + ' cidr_block = "10.0.2.0/24"\n nat_gateway_id = "nat-1"\n }\n }\n' + ), + } + for name, block in cases.items(): + with self.subTest(case=name): + self.check(evaluate(VAR + self.routed(block)), S, 2, R.ROUTE_UNSUPPORTED) + + def test_propagating_vgws_of_our_table_even_empty(self) -> None: + self.check(evaluate(self.routed(" propagating_vgws = []\n")), S, 2, R.ROUTE_UNSUPPORTED) + + def test_the_causes_say_which_route(self) -> None: + block = ' route {\n cidr_block = "10.0.2.0/24"\n nat_gateway_id = "nat-1"\n }\n' + outcome = evaluate(self.routed(block)) + (cause,) = outcome.observations["row2_causes"] + self.assertEqual(cause["cause"], "route.unsupported") + self.assertIn("aws_route_table.public", cause["detail"]) + self.assertIn("10.0.2.0/24", cause["detail"]) + + +class TestRowsThreeToFive(Check): + def with_db(self, line: str) -> str: + return edit( + canonical(), + " publicly_accessible = false\n", + " publicly_accessible = false\n" + line, + ) + + def test_the_listener_port(self) -> None: + cases = [ + (" port = 5432\n", P, 6, None), + (' port = "5432"\n', P, 6, None), + (" port = 5433\n", F, 3, R.PORT_MISMATCH), + (" port = 5432\n # engine stays postgres\n", P, 6, None), + ] + for line, result, row, reason in cases: + with self.subTest(line=line): + self.check(evaluate(self.with_db(line)), result, row, reason) + + def test_the_port_wins_over_the_engine(self) -> None: + text = edit( + self.with_db(" port = 5432\n"), + ' engine = "postgres"', + ' engine = "mysql"', + ) + self.check(evaluate(text), P, 6, None) + + def test_another_engine_without_a_port_is_definitely_not_postgres(self) -> None: + text = edit(canonical(), '"postgres"', '"mysql"') + self.check(evaluate(text), F, 3, R.PORT_MISMATCH) + + def test_neither_port_nor_engine_is_a_registry_gap(self) -> None: + text = edit(canonical(), ' engine = "postgres"\n', "") + self.check(evaluate(text), S, 2, R.MODEL_UNSUPPORTED) + + def test_an_unresolved_listener_is_unknown_by_the_gap_reading(self) -> None: + # registry row 4 names E3 and E4, not E2; an unresolved E2 cannot be a PASS + self.check(evaluate(VAR + self.with_db(" port = var.u\n")), U, 4, R.ATTRIBUTE_UNRESOLVED) + text = VAR + edit(canonical(), '"postgres"', "var.u") + self.check(evaluate(text), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_row_three_comes_before_row_four(self) -> None: + text = VAR + edit( + self.with_db(" port = 3306\n"), SUBNET_LINE, " subnet_id = var.u\n" + ) + self.check(evaluate(text), F, 3, R.PORT_MISMATCH) + + def test_values_that_cannot_be_fixed_are_unknown(self) -> None: + cases = { + "D groups": edit(canonical(), DB_SGS_LINE, " vpc_security_group_ids = var.u\n"), + "D group vpc": edit( + canonical(), DB_GROUP, DB_GROUP.replace("aws_vpc.main.id", "var.u") + ), + "S subnet": edit(canonical(), SUBNET_LINE, " subnet_id = var.u\n"), + "subnet vpc": edit( + canonical(), + 'resource "aws_subnet" "app" {\n vpc_id = aws_vpc.main.id\n', + 'resource "aws_subnet" "app" {\n vpc_id = var.u\n', + ), + } + for name, text in cases.items(): + with self.subTest(case=name): + self.check(evaluate(VAR + text), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_row_four_comes_before_row_five(self) -> None: + far = ( + '\nresource "aws_vpc" "other" {\n cidr_block = "10.1.0.0/16"\n}\n' + '\nresource "aws_subnet" "far" {\n vpc_id = aws_vpc.other.id\n' + ' cidr_block = "10.1.1.0/24"\n}\n' + ) + text = edits( + canonical(), + (SUBNET_LINE, " subnet_id = aws_subnet.far.id\n"), + (DB_SGS_LINE, " vpc_security_group_ids = var.u\n"), + ) + self.check(evaluate(VAR + text + far), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_things_outside_the_model_are_unsupported_by_r5(self) -> None: + other = '\nresource "aws_vpc" "other" {\n cidr_block = "10.1.0.0/16"\n}\n' + ( + '\nresource "aws_security_group" "away" {\n vpc_id = aws_vpc.other.id\n}\n' + ) + cases = { + "D groups in two VPCs": edit( + canonical(), + DB_SGS_LINE, + " vpc_security_group_ids = " + "[aws_security_group.db.id, aws_security_group.away.id]\n", + ) + + other, + "a literal group id on D": edit( + canonical(), DB_SGS_LINE, ' vpc_security_group_ids = ["sg-123"]\n' + ), + "a literal VPC id on a D group": edit( + canonical(), DB_GROUP, DB_GROUP.replace("aws_vpc.main.id", '"vpc-123"') + ), + "a literal subnet id on S": edit( + canonical(), SUBNET_LINE, ' subnet_id = "subnet-123"\n' + ), + "an invalid private_ip": edit( + canonical(), + PUBLIC_IP_LINE, + ' associate_public_ip_address = true\n private_ip = "not-an-ip"\n}', + ), + } + for name, text in cases.items(): + with self.subTest(case=name): + self.assertEqual(evaluate(text).result, S, name) + + +class TestRowsSixToNine(Check): + def test_e5_by_the_destination_group(self) -> None: + text = swap_egress(" source_security_group_id = aws_security_group.db.id\n") + outcome = evaluate(text) + self.check(outcome, P, 6, None) + self.assertEqual( + outcome.observations["path"]["egress_rule"], "aws_security_group_rule.egress_x" + ) + + def test_e5_by_a_cidr_list_that_covers_the_vpc_as_a_union(self) -> None: + text = swap_egress(' cidr_blocks = ["10.0.0.0/17", "10.0.128.0/17"]\n') + self.check(evaluate(text), P, 6, None) + + def test_the_port_range_decides_whether_a_rule_counts(self) -> None: + cases = [ + ("tcp", 5000, 6000, P, 6), + ("tcp", 5433, 5433, F, 9), + ("tcp", 5432, 5432, P, 6), + ("udp", 5432, 5432, F, 9), + ("-1", 0, 0, P, 6), + ] + for protocol, low, high, result, row in cases: + text = edit( + canonical(), + APP_EGRESS, + rule( + "egress_x", + "egress", + protocol, + low, + high, + "app", + ' cidr_blocks = ["0.0.0.0/0"]\n', + ), + ) + with self.subTest(protocol=protocol, low=low, high=high): + outcome = evaluate(text) + self.assertEqual((outcome.result, outcome.observations["row"]), (result, row)) + + def test_coverage_is_per_rule_not_pooled(self) -> None: + # E5 says v4(r) covers CIDR(VPC(D)) for one rule r: two rules with a half each do not + halves = egress_5432("half_a", ' cidr_blocks = ["10.0.0.0/17"]\n') + egress_5432( + "half_b", ' cidr_blocks = ["10.0.128.0/17"]\n' + ) + outcome = evaluate(edit(canonical(), APP_EGRESS, halves)) + self.check(outcome, U, 8, R.COVERAGE_PARTIAL) # each half partly covers the VPC + + def test_e6_by_the_group_of_the_source(self) -> None: + self.check(evaluate(canonical()), P, 6, None) + + def test_e6_by_self_needs_the_group_to_be_one_of_the_source(self) -> None: + self_rule = ingress_5432("db_self", " self = true\n") + both = DB_SGS_LINE.replace("[aws_security_group.db.id]", "[aws_security_group.db.id]") + text = edit(canonical(), APP_TO_DB, self_rule) + self.check(evaluate(text), F, 9, R.PATH_MISSING) # db is not a group of S + in_both = edit( + text, + APP_SGS_LINE, + " vpc_security_group_ids = " + "[aws_security_group.app.id, aws_security_group.db.id]\n", + ) + self.check(evaluate(in_both), P, 6, None) + self.assertEqual(both, DB_SGS_LINE) + + def test_e6_by_a_cidr_around_a_private_ip(self) -> None: + text = swap_ingress(' cidr_blocks = ["10.0.1.0/25"]\n') + inside = edit( + text, + PUBLIC_IP_LINE, + ' associate_public_ip_address = true\n private_ip = "10.0.1.10"\n}', + ) + outside = edit( + text, + PUBLIC_IP_LINE, + ' associate_public_ip_address = true\n private_ip = "10.0.1.200"\n}', + ) + self.check(evaluate(inside), P, 6, None) + self.check(evaluate(outside), F, 9, R.PATH_MISSING) # one address is covered or it is not + + def test_an_unresolved_private_ip_falls_back_to_the_subnet(self) -> None: + text = VAR + edit( + swap_ingress(' cidr_blocks = ["10.0.1.0/25"]\n'), + PUBLIC_IP_LINE, + " associate_public_ip_address = true\n private_ip = var.u\n}", + ) + self.check(evaluate(text), U, 8, R.COVERAGE_PARTIAL) + + def test_ipv6_is_not_modelled(self) -> None: + self.check(evaluate(swap_ingress(' ipv6_cidr_blocks = ["::/0"]\n')), F, 9, R.PATH_MISSING) + self.check(evaluate(swap_egress(' ipv6_cidr_blocks = ["::/0"]\n')), F, 9, R.PATH_MISSING) + + def test_a_disjoint_cidr_is_not_a_partial_cover(self) -> None: + self.check( + evaluate(swap_ingress(' cidr_blocks = ["10.0.3.0/24"]\n')), F, 9, R.PATH_MISSING + ) + + def test_row_seven_an_unresolved_source_group_could_satisfy_e6(self) -> None: + text = VAR + swap_ingress(" source_security_group_id = var.u\n") + outcome = evaluate(text) + self.check(outcome, U, 7, R.RULE_INDETERMINATE) + (item,) = outcome.observations["indeterminate_rules"] + self.assertEqual( + (item["condition"], item["rule"]), ("E6", "aws_security_group_rule.ingress_x") + ) + + def test_row_seven_counts_a_resolved_source_with_an_unresolved_port(self) -> None: + # R3: the mirror of the gap of C-150. The rule could supply the permission, so it is not + # dropped (dropping it could turn a possible PASS into an unsound FAIL). Pinned. + broken = rule( + "ingress_x", + "ingress", + "tcp", + 5432, + 5432, + "db", + " source_security_group_id = aws_security_group.app.id\n", + ).replace("from_port = 5432", "from_port = var.u") + self.check(evaluate(VAR + edit(canonical(), APP_TO_DB, broken)), U, 7, R.RULE_INDETERMINATE) + + def test_row_seven_ignores_an_indeterminate_rule_that_cannot_satisfy(self) -> None: + elsewhere = '\nresource "aws_security_group" "other" {\n vpc_id = aws_vpc.main.id\n}\n' + broken = rule( + "ingress_x", + "ingress", + "tcp", + 5432, + 5432, + "db", + " source_security_group_id = aws_security_group.other.id\n", + ).replace("from_port = 5432", "from_port = var.u") + self.check( + evaluate(VAR + edit(canonical(), APP_TO_DB, broken) + elsewhere), F, 9, R.PATH_MISSING + ) + + def test_row_seven_a_rule_of_a_pseudo_group_with_an_unresolved_target(self) -> None: + loose = ( + 'resource "aws_security_group_rule" "loose" {\n type = "ingress"\n protocol = "tcp"\n' + " from_port = 5432\n to_port = 5432\n security_group_id = var.u\n" + " source_security_group_id = aws_security_group.app.id\n}\n" + ) + self.check(evaluate(VAR + edit(canonical(), APP_TO_DB, loose)), U, 7, R.RULE_INDETERMINATE) + external = loose.replace("var.u", '"sg-0123"') + self.check(evaluate(edit(canonical(), APP_TO_DB, external)), F, 9, R.PATH_MISSING) + + def test_row_seven_a_rule_resource_that_is_a_placeholder(self) -> None: + text = VAR + edit( + canonical(), + 'resource "aws_security_group_rule" "app_to_db_5432" {\n', + 'resource "aws_security_group_rule" "app_to_db_5432" {\n count = var.u\n', + ) + self.check(evaluate(text), U, 7, R.RULE_INDETERMINATE) + + def test_row_seven_a_rule_whose_type_cannot_be_fixed(self) -> None: + # a rule of unknown direction counts for both directions; the database group must not + # declare an explicit empty egress, or the rule would make it MIXED (next test) + text = VAR + edits( + canonical(), + (' type = "ingress"\n', " type = var.u\n"), + (DB_GROUP, DB_GROUP.replace(" egress = []\n", "")), + ) + self.check(evaluate(text), U, 7, R.RULE_INDETERMINATE) + + def test_a_rule_of_unknown_direction_on_a_group_with_an_explicit_empty_egress_is_mixed( + self, + ) -> None: + # the rule might be an egress rule on a group that declares `egress = []` (registry §2.6, + # read as for INV-SEC-001/002): row 2, which comes before row 7 + text = VAR + edit( + canonical(), + ' type = "ingress"\n', + " type = var.u\n", + ) + self.check(evaluate(text), S, 2, R.GROUP_MIXED) + + def test_row_seven_a_prefix_list(self) -> None: + self.check( + evaluate(swap_ingress(' prefix_list_ids = ["pl-1"]\n')), U, 7, R.RULE_INDETERMINATE + ) + + def test_row_seven_an_unresolved_group_of_the_source(self) -> None: + text = VAR + edits( + canonical(), + (APP_TO_DB, ""), + (APP_SGS_LINE, " vpc_security_group_ids = [aws_security_group.app.id, var.u]\n"), + ) + self.check(evaluate(text), U, 7, R.ATTRIBUTE_UNRESOLVED) + + def test_an_unresolved_group_does_not_spoil_a_pass_that_already_holds(self) -> None: + text = VAR + edit( + canonical(), + APP_SGS_LINE, + " vpc_security_group_ids = [aws_security_group.app.id, var.u]\n", + ) + self.check(evaluate(text), P, 6, None) + + def test_row_seven_comes_before_row_eight(self) -> None: + both = ingress_5432("narrow", ' cidr_blocks = ["10.0.1.0/25"]\n') + ingress_5432( + "loose", " source_security_group_id = var.u\n" + ) + self.check(evaluate(VAR + edit(canonical(), APP_TO_DB, both)), U, 7, R.RULE_INDETERMINATE) + + def test_row_seven_applies_when_either_failing_condition_could_be_satisfied(self) -> None: + # E5 fails for good (no egress); E6 could be satisfied. Cautious reading of "it": UNKNOWN + text = VAR + edits( + canonical(), + (APP_EGRESS, ""), + (APP_TO_DB, ingress_5432("loose", " source_security_group_id = var.u\n")), + ) + outcome = evaluate(text) + self.check(outcome, U, 7, R.RULE_INDETERMINATE) + self.assertEqual(outcome.observations["failing_conditions"], ["E5", "E6"]) + + def test_both_conditions_failing_without_any_possibility_is_row_nine(self) -> None: + text = edits(canonical(), (APP_EGRESS, ""), (APP_TO_DB, "")) + outcome = evaluate(text) + self.check(outcome, F, 9, R.PATH_MISSING) + self.assertEqual(outcome.observations["failing_conditions"], ["E5", "E6"]) + + +class TestOrderAndOutcome(Check): + def test_resource_order_does_not_change_the_outcome(self) -> None: + given = inputs(canonical()) + base = evaluate_reachability(definition(given), given) + rng = random.Random(20261029) + resources = list(given.candidate_resources) + for _ in range(6): + rng.shuffle(resources) + shuffled = dataclasses.replace(given, candidate_resources=tuple(resources)) + self.assertEqual(evaluate_reachability(definition(shuffled), shuffled), base) + + def test_the_observations_are_plain_json(self) -> None: + import json + + for text in ( + canonical(), + edit(canonical(), APP_TO_DB, ""), + canonical() + '\nresource "aws_default_vpc" "d" {}\n', + ): + json.dumps(dict(evaluate(text).observations)) + + def test_no_clauses_and_a_fixed_key_set(self) -> None: + outcome = evaluate(canonical()) + self.assertIsNone(outcome.clauses) + keys = ( + "row reason detail endpoints port path row2_causes unresolved failing_conditions " + "indeterminate_rules partial_coverage relevant_unsupported" + ).split() + self.assertEqual(sorted(outcome.observations), sorted(keys)) + # the same keys on every path, not only on the one that happens to set them + for text in ( + edit(canonical(), APP_TO_DB, ""), + canonical() + '\nresource "aws_default_vpc" "d" {}\n', + ): + self.assertEqual(sorted(evaluate(text).observations), sorted(keys)) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/unit/test_reachability_vectors.py b/tests/unit/test_reachability_vectors.py new file mode 100644 index 0000000..ed81fe4 --- /dev/null +++ b/tests/unit/test_reachability_vectors.py @@ -0,0 +1,310 @@ +"""INV-FUNC-001: the conformance vectors F1 to F20 (P5b step 4; registry §6.3, §6.4, §8; C-151..). + +HAND DERIVATION, written before the predicate existed and before any run. The base is the canonical +configuration (fixture ``patch_safe``): VPC ``main`` 10.0.0.0/16; subnets ``app`` 10.0.1.0/24, +``db_a`` 10.0.2.0/24, ``db_b`` 10.0.3.0/24; route table ``public`` with 0.0.0.0/0 -> igw; group +``app`` (``ingress = []``, egress by the rule ``app_egress_all``: ``-1`` to 0.0.0.0/0); group ``db`` +(``egress = []``, ingress by the rule ``app_to_db_5432``: tcp 5432 from group ``app``); instance +``app`` (subnet ``app``, groups [app]); database ``database`` (engine postgres, no port, groups +[db]); a tolerated ``aws_db_subnet_group``. Bindings: S = aws_instance.app and +D = aws_db_instance.database. + +Canonical: no row 1 (both exist); no row 2 cause (no relevant-unsupported type; the only route is +wider than the VPC CIDR; no ``propagating_vgws``; no interface block; no ``security_groups``; both +have ``vpc_security_group_ids`` and ``S`` a ``subnet_id``; ``app`` has an explicit-empty ingress and +an egress rule, ``db`` an explicit-empty egress and an ingress rule, so neither is MIXED; a baseline +has no RETAINED-INLINE group); E2 holds (no port, engine postgres); E3: ``db`` is in VPC main; E4: +subnet ``app`` is in VPC main, so VPC(S) = VPC(D); E5: ``app_egress_all`` permits TCP/5432 and +0.0.0.0/0 covers 10.0.0.0/16; E6: ``app_to_db_5432`` permits 5432 and its source group ``app`` is in +SG(S). Row 6. + + F1 no edit. As above. registry PASS, row 6 + F2 rule app_to_db_5432 removed. E6 fails, nothing indeterminate FAIL, row 9 + or partial. + F3 ingress tcp 5432 from 10.0.1.0/24 instead of the group. PASS, row 6 + ADDR(S) = subnet 10.0.1.0/24, which the CIDR covers. + F4 as F3, S in subnet db_b 10.0.3.0/24. The CIDR does not touch FAIL, row 9 + 10.0.3.0/24. + F5 rule app_egress_all removed. Out(app) is empty, E5 fails. FAIL, row 9 + F6 egress only tcp 5432 to 10.0.2.0/24. E5 fails; the CIDR UNKNOWN, row 8 + partly covers the VPC CIDR. + F7 route 10.0.2.0/24 -> network_interface_id. Inside the VPC UNSUPPORTED, row 2 + CIDR and not local. + F8 route 0.0.0.0/0 -> igw removed. That route never applied PASS, row 6 + (wider than the VPC CIDR). + F9 an aws_network_acl. Relevant-unsupported type. UNSUPPORTED, row 2 + F10 D removed (a baseline; and a parent that had D: DELETED). FAIL, row 1 + F11 D.port = 3306. E2 definitely false. FAIL, row 3 + F12 D without vpc_security_group_ids. Default group not modelled. UNSUPPORTED, row 2 + F13 ingress from 10.0.1.0/25, S.private_ip unset. ADDR(S) = UNKNOWN, row 8 + 10.0.1.0/24 is only partly covered. + F13b as F13 with S.private_ip = 10.0.1.10. ADDR(S) = 10.0.1.10/32, PASS, row 6 + inside the /25. + F14 S in a subnet of a second VPC. E3 holds, VPC(S) != VPC(D). FAIL, row 5 + F15 the aws_db_subnet_group is present (the canonical has it). PASS, row 6 + Tolerated; the assumption is recorded. + F16 S has a network_interface block (C-78). UNSUPPORTED, row 2 + F17 a route table of VPC(D) sets propagating_vgws = [] (C-78). UNSUPPORTED, row 2 + F18 an aws_vpc_security_group_vpc_association. UNSUPPORTED, row 2 + F19 parent: db has an inline ingress block; candidate: the db UNSUPPORTED, row 2 + ingress argument absent (RETAINED-INLINE, C-84). + F20 an aws_default_vpc. Relevant-unsupported type. UNSUPPORTED, row 2 + +In every line the right-hand column is also the registry's answer in section 8 (F13 has two). + +The fixtures with a non-trivial FUNC result, derived the same way from their diff against the +canonical text: ``func_unknown_dependency`` (the source group of ``app_to_db_5432`` is a variable +without a value: E6 fails with determinate rules, an indeterminate rule could satisfy it) row 7 +UNKNOWN; ``func_unsupported_relationship`` (an ``aws_network_acl``) row 2 UNSUPPORTED; +``rds_deleted_dependency`` (D deleted, with a parent) row 1 FAIL; ``ec2_rds_5432_break`` (app +``egress = []``, no egress rule) row 9 FAIL; ``patch_regression`` (rule ``app_to_db_5432`` removed) +row 9 FAIL. The 20-fixture test compares all of them with ``expected.json`` in step 6. +""" + +from __future__ import annotations + +import unittest +from typing import Any + +from core.domain.enums import VerificationResult +from core.domain.verification import VerificationReason +from core.verification.outcome import PredicateOutcome +from tests.func_builders import ( + APP_EGRESS, + APP_TO_DB, + DB_GROUP, + IGW_ROUTE, + PUBLIC_IP_LINE, + SOURCE_LINE, + SUBNET_LINE, + canonical, + edit, + edits, +) +from tests.reach_builders import evaluate + +P, F, U, S = ( + VerificationResult.PASS, + VerificationResult.FAIL, + VerificationResult.UNKNOWN, + VerificationResult.UNSUPPORTED, +) +R = VerificationReason + + +class Vectors(unittest.TestCase): + def check( + self, + outcome: PredicateOutcome, + result: VerificationResult, + row: int, + reason: VerificationReason | None, + ) -> None: + self.assertEqual( + (outcome.result, outcome.observations["row"], outcome.reason), (result, row, reason) + ) + + def test_the_canonical_text_is_what_the_derivation_assumes(self) -> None: + text = canonical() + for part in (APP_TO_DB, APP_EGRESS, IGW_ROUTE, SOURCE_LINE, SUBNET_LINE, DB_GROUP): + self.assertEqual(text.count(part), 1, part[:60]) + + def test_f1_canonical(self) -> None: + outcome = evaluate(canonical()) + self.check(outcome, P, 6, None) + self.assertIsNone(outcome.clauses) + + def test_f2_the_database_rule_removed(self) -> None: + self.check(evaluate(edit(canonical(), APP_TO_DB, "")), F, 9, R.PATH_MISSING) + + def test_f3_ingress_from_the_app_subnet(self) -> None: + text = edit(canonical(), SOURCE_LINE, ' cidr_blocks = ["10.0.1.0/24"]\n') + self.check(evaluate(text), P, 6, None) + + def test_f4_the_same_rule_with_the_instance_in_another_subnet(self) -> None: + text = edits( + canonical(), + (SOURCE_LINE, ' cidr_blocks = ["10.0.1.0/24"]\n'), + (SUBNET_LINE, " subnet_id = aws_subnet.db_b.id\n"), + ) + self.check(evaluate(text), F, 9, R.PATH_MISSING) + + def test_f5_no_egress_at_all(self) -> None: + self.check(evaluate(edit(canonical(), APP_EGRESS, "")), F, 9, R.PATH_MISSING) + + def test_f6_egress_only_to_a_database_subnet(self) -> None: + narrow = """resource "aws_security_group_rule" "app_egress_all" { + type = "egress" + protocol = "tcp" + from_port = 5432 + to_port = 5432 + cidr_blocks = ["10.0.2.0/24"] + security_group_id = aws_security_group.app.id +} +""" + outcome = evaluate(edit(canonical(), APP_EGRESS, narrow)) + self.check(outcome, U, 8, R.COVERAGE_PARTIAL) + + def test_f7_an_intra_vpc_route_to_a_network_interface(self) -> None: + extra = ( + IGW_ROUTE + + '\n route {\n cidr_block = "10.0.2.0/24"\n' + + ' network_interface_id = "eni-0123"\n }\n' + ) + self.check(evaluate(edit(canonical(), IGW_ROUTE, extra)), S, 2, R.ROUTE_UNSUPPORTED) + + def test_f8_the_internet_gateway_route_removed(self) -> None: + self.check(evaluate(edit(canonical(), IGW_ROUTE, "")), P, 6, None) + + def test_f9_a_network_acl(self) -> None: + text = canonical() + '\nresource "aws_network_acl" "x" {\n vpc_id = aws_vpc.main.id\n}\n' + self.check(evaluate(text), S, 2, R.TYPE_RELEVANT_UNSUPPORTED) + + def test_f10_the_database_deleted(self) -> None: + # a baseline without D, and a candidate whose parent had it (identity: DELETED) + db_start = canonical().index('resource "aws_db_subnet_group" "db"') + gone = canonical()[:db_start] + self.check(evaluate(gone), F, 1, R.ENDPOINT_ABSENT) + self.check(evaluate(gone, canonical()), F, 1, R.ENDPOINT_ABSENT) + + def test_f11_the_database_listens_elsewhere(self) -> None: + text = edit( + canonical(), + " publicly_accessible = false\n", + " publicly_accessible = false\n port = 3306\n", + ) + self.check(evaluate(text), F, 3, R.PORT_MISMATCH) + + def test_f12_the_database_without_security_groups(self) -> None: + text = edit(canonical(), " vpc_security_group_ids = [aws_security_group.db.id]\n", "") + self.check(evaluate(text), S, 2, R.MODEL_UNSUPPORTED) + + def test_f13_a_partly_covering_ingress_without_a_private_ip(self) -> None: + text = edit(canonical(), SOURCE_LINE, ' cidr_blocks = ["10.0.1.0/25"]\n') + self.check(evaluate(text), U, 8, R.COVERAGE_PARTIAL) + + def test_f13b_the_same_with_a_private_ip_inside_the_range(self) -> None: + text = edits( + canonical(), + (SOURCE_LINE, ' cidr_blocks = ["10.0.1.0/25"]\n'), + ( + PUBLIC_IP_LINE, + " associate_public_ip_address = true\n" + ' private_ip = "10.0.1.10"\n}', + ), + ) + self.check(evaluate(text), P, 6, None) + + def test_f14_the_instance_in_a_second_vpc(self) -> None: + text = edit(canonical(), SUBNET_LINE, " subnet_id = aws_subnet.far.id\n") + text += ( + '\nresource "aws_vpc" "other" {\n cidr_block = "10.1.0.0/16"\n}\n' + '\nresource "aws_subnet" "far" {\n vpc_id = aws_vpc.other.id\n' + ' cidr_block = "10.1.1.0/24"\n availability_zone = "us-east-1a"\n}\n' + ) + self.check(evaluate(text), F, 5, R.VPC_MISMATCH) + + def test_f15_the_tolerated_subnet_group_is_recorded(self) -> None: + outcome = evaluate(canonical()) + self.check(outcome, P, 6, None) + self.assertIn("tolerated type: aws_db_subnet_group (C-15)", outcome.assumptions) + without = canonical()[: canonical().index('resource "aws_db_subnet_group" "db"')] + without += canonical()[canonical().index('resource "aws_db_instance" "database"') :] + without = without.replace( + " db_subnet_group_name = aws_db_subnet_group.db.name\n", "" + ) + self.assertNotIn( + "tolerated type: aws_db_subnet_group (C-15)", evaluate(without).assumptions + ) + + def test_f16_an_interface_block_on_the_instance(self) -> None: + block = ( + " associate_public_ip_address = true\n" + " network_interface {\n device_index = 0\n" + ' network_interface_id = "eni-0123"\n }\n}' + ) + outcome = evaluate(edit(canonical(), PUBLIC_IP_LINE, block)) + self.check(outcome, S, 2, R.INTERFACE_UNSUPPORTED) + + def test_f17_propagating_vgws_even_empty(self) -> None: + old = 'resource "aws_route_table" "public" {\n vpc_id = aws_vpc.main.id\n' + outcome = evaluate(edit(canonical(), old, old + " propagating_vgws = []\n")) + self.check(outcome, S, 2, R.ROUTE_UNSUPPORTED) + + def test_f18_a_security_group_vpc_association(self) -> None: + text = canonical() + ( + '\nresource "aws_vpc_security_group_vpc_association" "x" {\n' + " security_group_id = aws_security_group.app.id\n" + " vpc_id = aws_vpc.main.id\n}\n" + ) + self.check(evaluate(text), S, 2, R.TYPE_RELEVANT_UNSUPPORTED) + + def test_f19_the_database_group_keeps_its_inline_ingress(self) -> None: + inline = DB_GROUP.replace( + " egress = []\n", + ' egress = []\n\n ingress {\n protocol = "tcp"\n' + " from_port = 5432\n to_port = 5432\n" + " security_groups = [aws_security_group.app.id]\n }\n", + ) + parent = edits(canonical(), (APP_TO_DB, ""), (DB_GROUP, inline)) + outcome = evaluate(canonical(), parent) + self.check(outcome, S, 2, R.GROUP_RETAINED_INLINE) + causes = [item["cause"] for item in outcome.observations["row2_causes"]] + self.assertEqual(causes, ["group.retained_inline"]) + self.assertIn("aws_security_group.db", outcome.observations["row2_causes"][0]["detail"]) + + def test_f20_a_default_vpc(self) -> None: + self.check( + evaluate(canonical() + '\nresource "aws_default_vpc" "d" {}\n'), + S, + 2, + R.TYPE_RELEVANT_UNSUPPORTED, + ) + + +def observed(outcome: PredicateOutcome) -> dict[str, Any]: + return dict(outcome.observations) + + +class TestTheEvaluatedPath(unittest.TestCase): + def test_the_pass_records_the_path_the_registry_asks_for(self) -> None: + obs = observed(evaluate(canonical())) + self.assertEqual(obs["port"], 5432) + self.assertEqual( + dict(obs["path"]), + { + "S": "aws_instance.app", + "subnet": "aws_subnet.app", + "vpc_s": "aws_vpc.main", + "sg_s": ["aws_security_group.app"], + "egress_rule": "aws_security_group_rule.app_egress_all", + "sg_d": ["aws_security_group.db"], + "ingress_rule": "aws_security_group_rule.app_to_db_5432", + "vpc_d": "aws_vpc.main", + }, + ) + self.assertEqual(obs["failing_conditions"], []) + self.assertEqual(obs["row2_causes"], []) + + def test_the_failing_condition_is_named(self) -> None: + self.assertEqual( + observed(evaluate(edit(canonical(), APP_TO_DB, "")))["failing_conditions"], ["E6"] + ) + self.assertEqual( + observed(evaluate(edit(canonical(), APP_EGRESS, "")))["failing_conditions"], ["E5"] + ) + + def test_the_assumptions_are_a_sorted_closed_list(self) -> None: + self.assertEqual( + evaluate(canonical()).assumptions, + ( + "IPv4 only", + "M1: RDS security groups and subnet group share one VPC (C-15, C-77, uncited)", + "M4: default network ACL assumed (no NACL type present)", + "tolerated type: aws_db_subnet_group (C-15)", + ), + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/unit/test_verification_cidr_ports.py b/tests/unit/test_verification_cidr_ports.py index 4797e1c..954980b 100644 --- a/tests/unit/test_verification_cidr_ports.py +++ b/tests/unit/test_verification_cidr_ports.py @@ -19,6 +19,7 @@ CidrError, Network, covers, + overlaps, parse_network, ) from core.verification.ports import PortsError, may_permit_tcp, permits_tcp @@ -227,6 +228,66 @@ def test_consecutive_single_address_members_tile_a_network(self) -> None: self.check_every_order([tiles[0], tiles[1], tiles[3]], network, False) +class TestOverlaps(unittest.TestCase): + """``overlaps``: some member shares at least one address with the target (registry §6.4 row 8 + asks whether a CIDR *partly* covers a target: it overlaps without covering).""" + + def test_by_hand(self) -> None: + table = [ + (["10.0.1.0/25"], "10.0.1.0/24", True), # inside the target + (["10.0.1.0/24"], "10.0.1.0/25", True), # around the target + (["10.0.2.0/24"], "10.0.1.0/24", False), # next door + (["10.0.1.0/24"], "10.0.2.0/24", False), # the other neighbour + (["10.0.0.255/32"], "10.0.0.0/24", True), # shares only the last address + (["10.0.0.0/32"], "10.0.0.0/24", True), # shares only the first address + (["10.0.1.0/32"], "10.0.0.0/24", False), # one address beyond the last + (["9.255.255.255/32"], "10.0.0.0/24", False), # one address before the first + ([], "10.0.0.0/24", False), + (["10.9.0.0/16", "10.0.0.128/25"], "10.0.0.0/24", True), # one of several + (["2001:db8::/121"], "2001:db8::/120", True), + (["2001:db8::100/120"], "2001:db8::/120", False), + (["::/0"], "2001:db8::/120", True), + ] + for members, target, expected in table: + with self.subTest(members=members, target=target): + self.assertIs(overlaps(members, target), expected) + + def test_a_family_mix_or_an_invalid_member_is_an_error(self) -> None: + with self.assertRaises(CidrError): + overlaps(["::/0"], "10.0.0.0/24") + with self.assertRaises(CidrError): + overlaps(["nonsense"], "10.0.0.0/24") + + def test_covering_implies_overlapping_and_not_the_reverse(self) -> None: + self.assertTrue( + covers(["10.0.0.0/16"], "10.0.1.0/24") and overlaps(["10.0.0.0/16"], "10.0.1.0/24") + ) + self.assertTrue(overlaps(["10.0.1.0/25"], "10.0.1.0/24")) + self.assertFalse(covers(["10.0.1.0/25"], "10.0.1.0/24")) + + def test_agrees_with_the_block_oracle(self) -> None: + oracle = TestCoverageOracle() + for version, seed in ((4, 11), (6, 12)): + rng = random.Random(seed) + hits = misses = 0 + for _ in range(600): + members, union = [], set() + for _ in range(rng.randint(0, 4)): + prefix = rng.randint(1, 6) + index = rng.randrange(2**prefix) + members.append(oracle.text(version, prefix, index)) + union |= oracle.blocks(prefix, index) + prefix = rng.randint(1, 6) + index = rng.randrange(2**prefix) + wanted = oracle.blocks(prefix, index) + got = overlaps(members, oracle.text(version, prefix, index)) + self.assertIs(got, bool(wanted & union), (members, prefix, index)) + hits += bool(wanted & union) + misses += not (wanted & union) + self.assertGreater(hits, 40) + self.assertGreater(misses, 40) + + class TestCoverageOracle(unittest.TestCase): """The work package's oracle: the address space is cut into 64 blocks (the /6 networks), a CIDR of prefix length 1 to 6 is a run of consecutive blocks, and coverage is plain set containment of diff --git a/tests/unit/test_verification_values.py b/tests/unit/test_verification_values.py index 7fb9bea..49bcdff 100644 --- a/tests/unit/test_verification_values.py +++ b/tests/unit/test_verification_values.py @@ -24,6 +24,7 @@ decode_argument, first_problem, has_problem, + has_unresolved, ) @@ -175,6 +176,44 @@ def test_a_deep_value_does_not_overflow_the_stack(self) -> None: self.assertTrue(has_problem(value)) +class TestUnresolved(unittest.TestCase): + """``has_unresolved``: unknown or unsupported anywhere. A reference is a *resolved* value (it + names a configured resource), unlike in ``has_problem``, which counts it as not fixed.""" + + def test_a_reference_is_resolved(self) -> None: + ref = Ref("aws_security_group.app", "id") + for value in ( + ref, + (ref,), + SetValue((ref, "x")), + decode({"k": [{"$dail": "ref", "address": "a.b", "attribute": "id"}]}), + ): + with self.subTest(value=value): + self.assertFalse(has_unresolved(value)) + self.assertTrue(has_problem(value)) + + def test_unknown_and_unsupported_are_found_anywhere(self) -> None: + for value in ( + Unknown("r"), + Unsupported("r"), + ("x", Unknown("r")), + SetValue((Unsupported("r"),)), + decode({"k": [{"$dail": "unknown", "reason": "r"}]}), + ): + with self.subTest(value=value): + self.assertTrue(has_unresolved(value)) + + def test_plain_values_are_resolved(self) -> None: + for value in ("x", 1, None, ("a", ("b",)), Decimal("1.5")): + self.assertFalse(has_unresolved(value)) + + def test_a_deep_value_does_not_overflow_the_stack(self) -> None: + value: object = Unknown("deep") + for _ in range(5000): + value = (value,) + self.assertTrue(has_unresolved(value)) + + class TestArgument(unittest.TestCase): def test_attribute_form(self) -> None: got = decode_argument({"form": "ATTRIBUTE", "value": ["10.0.0.0/8"]}) diff --git a/tests/unit/test_verification_views.py b/tests/unit/test_verification_views.py index 223b8fe..e7ec158 100644 --- a/tests/unit/test_verification_views.py +++ b/tests/unit/test_verification_views.py @@ -270,6 +270,128 @@ def test_every_group_is_indexed_even_without_rules(self) -> None: self.assertEqual(index["aws_security_group.a"].ingress, ()) +class TestSourceAndSelfFlags(unittest.TestCase): + """P5b (C-151): which *other* fields of an indeterminate rule are unresolved, for INV-FUNC-001 + (E5 and E6 look at the source group and at ``self``). Read like the family flags of C-149.""" + + BASE = ' type = "ingress"\n protocol = "tcp"\n from_port = 5432\n to_port = 5432\n' + + def rule(self, body: str) -> views.Rule: + (found,) = view_of(VARS + group() + rule_resource(self.BASE + body)).ingress + return found + + def test_an_unresolved_source_group(self) -> None: + found = self.rule(" source_security_group_id = var.u\n") + self.assertTrue(found.sources_unresolved) + self.assertFalse(found.self_unresolved or found.ipv4_unresolved or found.ipv6_unresolved) + + def test_an_unresolved_self(self) -> None: + found = self.rule(" self = var.u\n") + self.assertTrue(found.self_unresolved) + self.assertFalse(found.sources_unresolved) + + def test_a_reference_to_a_group_is_a_resolved_source(self) -> None: + line = " source_security_group_id = aws_security_group.other.id" + chr(10) + text = VARS + group() + group(name="other") + rule_resource(self.BASE + line) + (found,) = views.index_rules(resources_of(text))[APP].ingress + self.assertTrue(found.determinate) + self.assertFalse(found.sources_unresolved) + self.assertEqual(found.source_security_groups, ("aws_security_group.other",)) + + def test_a_reference_beside_an_unresolved_entry_is_still_unresolved(self) -> None: + body = ( + ' ingress {\n protocol = "tcp"\n from_port = 1\n to_port = 1\n' + " security_groups = [aws_security_group.other.id, var.u]\n }" + ) + text = VARS + group(name="other") + group(body) + (found,) = views.index_rules(resources_of(text))[APP].ingress + self.assertFalse(found.determinate) + self.assertTrue(found.sources_unresolved) + + def test_a_resolved_rule_is_never_flagged(self) -> None: + found = self.rule(' cidr_blocks = ["10.0.0.0/8"]\n self = true\n') + self.assertFalse(found.sources_unresolved or found.self_unresolved) + + def test_a_cidr_list_alone_is_not_a_source_group(self) -> None: + found = self.rule(" cidr_blocks = var.u\n") + self.assertTrue(found.ipv4_unresolved) + self.assertFalse(found.sources_unresolved) + + def test_inline_blocks_use_the_union_of_their_direction(self) -> None: + text = VARS + group( + ' ingress {\n protocol = "tcp"\n from_port = 5432\n to_port = 5432\n' + " security_groups = [var.u]\n }\n" + ' ingress {\n protocol = "tcp"\n from_port = 22\n to_port = 22\n' + " self = var.u\n }\n" + ' ingress {\n protocol = "tcp"\n from_port = 80\n to_port = 80\n' + ' cidr_blocks = ["10.0.0.0/8"]\n }\n' + ) + rules = view_of(text).ingress + indeterminate = [r for r in rules if not r.determinate] + self.assertEqual(len(indeterminate), 2) + for ( + found + ) in indeterminate: # the stored blocks are sorted: a rule is not paired with its block + self.assertTrue(found.sources_unresolved and found.self_unresolved) + (determinate,) = (r for r in rules if r.determinate) + self.assertFalse(determinate.sources_unresolved or determinate.self_unresolved) + + def test_flags_are_per_direction(self) -> None: + text = VARS + group( + ' egress {\n protocol = "tcp"\n from_port = 1\n to_port = 1\n self = var.u\n }\n' + ' ingress {\n protocol = "tcp"\n from_port = 1\n to_port = 1\n' + " cidr_blocks = var.u\n }\n" + ) + view = view_of(text) + self.assertTrue(view.egress[0].self_unresolved) + self.assertFalse(view.ingress[0].self_unresolved) + + +class TestGroupIsMixed(unittest.TestCase): + """The MIXED test of registry §2.6 (C-84), shared by the SEC and the FUNC verifiers.""" + + def mixed(self, text: str) -> bool: + return views.group_is_mixed(view_of(VARS + text)) + + def test_inline_blocks_and_a_rule_resource(self) -> None: + text = group( + ' ingress {\n protocol = "tcp"\n from_port = 22\n to_port = 22\n }' + ) + rule_resource( + ' type = "ingress"\n protocol = "tcp"\n from_port = 1\n to_port = 1\n' + ) + self.assertTrue(self.mixed(text)) + + def test_inline_blocks_alone_or_rule_resources_alone(self) -> None: + blocks = group(' egress {\n protocol = "-1"\n from_port = 0\n to_port = 0\n }') + self.assertFalse(self.mixed(blocks)) + only_rules = group() + rule_resource( + ' type = "ingress"\n protocol = "tcp"\n from_port = 1\n to_port = 1\n' + ) + self.assertFalse(self.mixed(only_rules)) + + def test_explicit_empty_with_a_rule_of_the_same_direction_only(self) -> None: + ingress_rule = rule_resource( + ' type = "ingress"\n protocol = "tcp"\n from_port = 1\n to_port = 1\n' + ) + self.assertTrue(self.mixed(group(" ingress = []\n") + ingress_rule)) + self.assertFalse(self.mixed(group(" egress = []\n") + ingress_rule)) + + def test_a_direction_that_cannot_be_fixed_with_a_rule_resource(self) -> None: + text = group(" egress = var.u\n") + rule_resource( + ' type = "ingress"\n protocol = "tcp"\n from_port = 1\n to_port = 1\n' + ) + self.assertTrue(self.mixed(text)) + self.assertFalse(self.mixed(group(" egress = var.u\n"))) + + def test_a_pseudo_group_is_never_mixed(self) -> None: + text = rule_resource( + ' type = "ingress"\n protocol = "tcp"\n from_port = 1\n to_port = 1\n', + target='"sg-1"', + ) + index = views.index_rules(resources_of(text)) + self.assertFalse(views.group_is_mixed(index["EXTERNAL:sg-1"])) + + class TestOtherTypes(unittest.TestCase): def test_other_resources_have_no_rules(self) -> None: for resource in resources_of( From dc6260f68473cbf0de6c4f7e3d8f19455d7a7989 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 00:57:34 +0530 Subject: [PATCH 6/8] =?UTF-8?q?P5b=20step=205:=20register=20INV-FUNC-001?= =?UTF-8?q?=20in=20the=20dispatch=20table,=20extend=20the=20baseline=20lis?= =?UTF-8?q?t,=20replace=20the=20interim=20assertions=20(registry=20=C2=A72?= =?UTF-8?q?.7,=20=C2=A76.7;=20C-151,=20C-154)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit dail.verify.reachability_cfg v1 is in DEFAULT_VERIFIERS; a pair the table does not have is still UNSUPPORTED verifier.not_available (one test keeps that, with the pair removed). A created resource of any of the 26 relevant-unsupported types is UNSUPPORTED in the baseline. The interim "FUNC is UNSUPPORTED" assertions are replaced by stronger ones: the engine's FUNC result of all 20 fixtures equals expected.json, the aggregate over all four invariants follows expected.json, the safe repair aggregates to PASS and the repair that breaks the database path to FAIL from the engine's own records, and without the functional result nothing passes. The cost metric now counts the functional verifier (6 runs on a full work set, not 5). Tests first: the rewritten tests were shown failing before the verifier was registered. Co-Authored-By: Claude Sonnet 5.5 --- core/verification/__init__.py | 4 +- core/verification/baseline.py | 10 +-- core/verification/dispatch.py | 8 ++- core/verification/engine.py | 5 +- tests/unit/test_verification_baseline.py | 13 ++++ tests/unit/test_verification_engine.py | 67 ++++++++++++++++---- tests/unit/test_verification_fixtures.py | 79 +++++++++++++++++++----- 7 files changed, 150 insertions(+), 36 deletions(-) diff --git a/core/verification/__init__.py b/core/verification/__init__.py index ed783e3..e08e525 100644 --- a/core/verification/__init__.py +++ b/core/verification/__init__.py @@ -4,12 +4,14 @@ sufficiency and freshness, aggregation), registry-v1.0 §2-§5 (the predicates). Built in P5a (C-144 to C-150): the structural and consistency gate, the security predicates (INV-SEC-001, INV-SEC-002, INV-SEC-003), baseline verification of created resources and the engine. -INV-FUNC-001 is built in P5b; until then it is UNSUPPORTED ``verifier.not_available``, never PASS. +INV-FUNC-001 (reachability) is built in P5b (C-151 to C-154); a verifier pair that the dispatch +table does not have is UNSUPPORTED ``verifier.not_available``, never PASS. values, views the verifier's own reader of the stored security view (C-112, C-149) cidr, ports interval-union coverage and the port logic of registry §2.5, §3.3 retention RETAINED-INLINE: the parent counterpart, through the identity report public_ingress PIP(22) and PIP(5432) rds_public_flag INV-SEC-003 + reachability INV-FUNC-001, REACH(S, D, 5432) func_view its reader of the inputs structural the mandatory STRUCTURAL and CONSISTENCY items (closed finding codes) baseline the RESOURCE items P4 emits for created resources dispatch the table from a definition's verifier id and version to a function diff --git a/core/verification/baseline.py b/core/verification/baseline.py index 5e2041c..90de9ee 100644 --- a/core/verification/baseline.py +++ b/core/verification/baseline.py @@ -9,8 +9,9 @@ groups. The restriction only narrows what is reported; it never turns another group's FAIL into a PASS, which the invariant items still carry. * A created ``aws_db_instance`` runs INV-SEC-003 for that instance. -* A created resource of a relevant-unsupported type (registry §2.7, the security-group list) is - UNSUPPORTED, even as a placeholder (R5). +* A created resource of a relevant-unsupported type (registry §2.7: the 26 types of + INV-FUNC-001, which contain the three of the security list; C-154) is UNSUPPORTED, even as a + placeholder (R5). * A created placeholder (an unknown ``count`` or ``for_each``) is UNKNOWN. * Any other type is PASS with ``applicable = false`` and the assumption that the registry declares no baseline predicate for it. **This is a modelling assumption, not a proof** (C-148, flagged for @@ -29,11 +30,12 @@ from typing import Any, Final from core.domain.enums import ResourceSupport, VerificationResult +from core.domain.registry_v1 import FUNC_RELEVANT_UNSUPPORTED from core.domain.resource import Resource from core.domain.verification import VerificationReason from core.verification.inputs import VerificationInputs from core.verification.outcome import CLAUSE_IPV4, CLAUSE_IPV6, combine -from core.verification.public_ingress import RELEVANT_UNSUPPORTED, GroupStatus, analyse +from core.verification.public_ingress import GroupStatus, analyse from core.verification.rds_public_flag import DB_INSTANCE_TYPE, instance_state from core.verification.views import ( SECURITY_GROUP_RULE_TYPE, @@ -146,7 +148,7 @@ def verify_baseline(address: str, inputs: VerificationInputs) -> BaselineOutcome return BaselineOutcome( S, R.INVARIANT_UNKNOWN, _base(resource), (), True, *BASELINE_VERIFIER ) - if kind in RELEVANT_UNSUPPORTED: + if kind in FUNC_RELEVANT_UNSUPPORTED: return BaselineOutcome(S, R.TYPE_RELEVANT_UNSUPPORTED, _base(resource), (), True, *ids) if resource.support_status is ResourceSupport.UNKNOWN: return BaselineOutcome(U, R.RESOURCE_INDETERMINATE, _base(resource), (), True, *ids) diff --git a/core/verification/dispatch.py b/core/verification/dispatch.py index 4645b4c..ea936f4 100644 --- a/core/verification/dispatch.py +++ b/core/verification/dispatch.py @@ -3,8 +3,8 @@ The definition of an invariant names its verifier (``verifier_id``, ``verifier_version``, registry §10) and its parameters (``predicate.parameters``). The table maps that pair to a function ``(definition, inputs) -> PredicateOutcome``. A pair the table does not have is not an error of the -engine: the item is UNSUPPORTED ``verifier.not_available``, never PASS. INV-FUNC-001 is such a pair -until P5b adds its verifier. +engine: the item is UNSUPPORTED ``verifier.not_available``, never PASS (P5a had no entry for +INV-FUNC-001, so that was its answer; P5b registers ``dail.verify.reachability_cfg``). The table is data so that a test can inject a verifier that raises, or one that returns something that is not an outcome, and watch the engine fail closed. @@ -23,13 +23,14 @@ from core.verification.outcome import PredicateOutcome from core.verification.public_ingress import evaluate_public_ingress from core.verification.rds_public_flag import evaluate_rds_public_flag +from core.verification.reachability import evaluate_reachability Verifier = Callable[[Invariant, VerificationInputs], PredicateOutcome] VerifierTable = Mapping[tuple[str, str], Verifier] PUBLIC_INGRESS: Final = ("dail.verify.public_ingress", "1") RDS_PUBLIC_FLAG: Final = ("dail.verify.rds_public_flag", "1") -REACHABILITY_CFG: Final = ("dail.verify.reachability_cfg", "1") # P5b; not in the table yet +REACHABILITY_CFG: Final = ("dail.verify.reachability_cfg", "1") def _port(definition: Invariant) -> int: @@ -59,5 +60,6 @@ def rds_public_flag(_definition: Invariant, inputs: VerificationInputs) -> Predi { PUBLIC_INGRESS: public_ingress, RDS_PUBLIC_FLAG: rds_public_flag, + REACHABILITY_CFG: evaluate_reachability, } ) diff --git a/core/verification/engine.py b/core/verification/engine.py index cc59aa8..b5b0e77 100644 --- a/core/verification/engine.py +++ b/core/verification/engine.py @@ -15,8 +15,9 @@ * Malformed inputs (``VerificationInputError``) stop the run before any item runs. * A construction status that is not OK makes every invariant and baseline item UNSUPPORTED ``construction.invalid``; no predicate runs (registry §2.8). -* An invariant the definitions do not have is UNSUPPORTED ``invariant.unknown``; a verifier the - table does not have (INV-FUNC-001 until P5b) is UNSUPPORTED ``verifier.not_available``. +* An invariant the definitions do not have is UNSUPPORTED ``invariant.unknown``; a verifier pair + the table does not have is UNSUPPORTED ``verifier.not_available`` (the table of P5b has the three + registry verifiers). ``verifier_invocations`` counts verifier executions: the predicates, the baseline checks and the two gates, including executions that raised. Items answered without running a verifier are not counted. diff --git a/tests/unit/test_verification_baseline.py b/tests/unit/test_verification_baseline.py index d4b1114..6faa148 100644 --- a/tests/unit/test_verification_baseline.py +++ b/tests/unit/test_verification_baseline.py @@ -13,6 +13,7 @@ import unittest from core.domain.enums import ResourceSupport, VerificationResult +from core.domain.registry_v1 import FUNC_RELEVANT_UNSUPPORTED from core.domain.resource import Resource from core.domain.verification import VerificationReason from core.verification.baseline import verify_baseline @@ -146,6 +147,18 @@ def test_a_relevant_unsupported_resource_is_unsupported(self) -> None: (item.result, item.reason, item.applicable), (S, R.TYPE_RELEVANT_UNSUPPORTED, True) ) + def test_every_functional_relevant_unsupported_type_is_unsupported_when_created(self) -> None: + # C-154: the 26 types of registry §2.7 for INV-FUNC-001, not only the security list's three + self.assertEqual(len(FUNC_RELEVANT_UNSUPPORTED), 26) + for kind in sorted(FUNC_RELEVANT_UNSUPPORTED): + text = OLD + f'resource "{kind}" "x" {{\n}}\n' + with self.subTest(type=kind): + item = baseline(f"{kind}.x", text) + self.assertEqual( + (item.result, item.reason, item.applicable), + (S, R.TYPE_RELEVANT_UNSUPPORTED, True), + ) + def test_an_unrelated_type_passes_but_says_it_is_not_applicable(self) -> None: text = OLD + 'resource "aws_vpc" "v" {\n cidr_block = "10.0.0.0/16"\n}\n' item = baseline("aws_vpc.v", text) diff --git a/tests/unit/test_verification_engine.py b/tests/unit/test_verification_engine.py index eaddd32..08d01d3 100644 --- a/tests/unit/test_verification_engine.py +++ b/tests/unit/test_verification_engine.py @@ -2,8 +2,10 @@ Doc 09 §3-§18, §30, §37, §41; registry §2.4, §2.8, §2.10; C-144 to C-148. Expected values are derived by hand: a clean group passes the three security invariants, a public SSH group fails -INV-SEC-001 only, INV-FUNC-001 is UNSUPPORTED ``verifier.not_available`` until P5b, and the two -gate items run on every candidate. +INV-SEC-001 only, INV-FUNC-001 is answered by its own verifier (a configuration without the two +endpoints fails it at row 1; the canonical topology passes it at row 6), a verifier pair the table +does not have is UNSUPPORTED ``verifier.not_available``, and the two gate items run on every +candidate. """ from __future__ import annotations @@ -51,6 +53,7 @@ from core.verification.outcome import PredicateOutcome from core.verification.views import ViewError from tests.domain_builders import uid +from tests.func_builders import canonical from tests.impact_builders import baseline_work from tests.pipeline_builders import ( CANDIDATE_STATE, @@ -77,6 +80,8 @@ CLEAN = sg(body=inline("ingress", "tcp", 443, 443, ["10.0.0.0/8"])) OPEN = sg(body=inline("ingress", "tcp", 22, 22, ["0.0.0.0/0"])) KEY_PUBLIC_INGRESS = ("dail.verify.public_ingress", "1") +KEY_RDS_PUBLIC_FLAG = ("dail.verify.rds_public_flag", "1") +KEY_REACHABILITY = ("dail.verify.reachability_cfg", "1") def items(*invariants: str) -> list[VerificationWorkItem]: @@ -162,13 +167,44 @@ def test_a_public_ssh_group_fails_only_inv_sec_001(self) -> None: self.assertIs(found["INVARIANT:INV-SEC-002:1"].result, P) self.assertIs(found["INVARIANT:INV-SEC-003:1"].result, P) - def test_the_functional_invariant_is_unsupported_never_pass_until_p5b(self) -> None: + def test_the_functional_invariant_is_answered_by_its_own_verifier(self) -> None: + # P5b: a configuration without the two endpoints fails at row 1 (the protected endpoint is + # gone), whatever its security groups say for text in (CLEAN, OPEN): func = by_target(run(text))["INVARIANT:INV-FUNC-001:1"] - self.assertEqual((func.result, func.reason), (S, R.VERIFIER_NOT_AVAILABLE)) + self.assertEqual((func.result, func.reason), (F, R.ENDPOINT_ABSENT)) + self.assertEqual(func.observations["row"], 1) + self.assertEqual((func.verifier_id, func.verifier_version), KEY_REACHABILITY) + self.assertEqual( + (func.evidence_level, func.verification_class.value), ("L1", "FUNCTIONAL") + ) self.assertIsNone(func.clauses) self.assertIsNone(func.error) + def test_on_the_canonical_topology_the_functional_invariant_passes(self) -> None: + report = run(canonical(), inputs=inputs_for(canonical())) + func = by_target(report)["INVARIANT:INV-FUNC-001:1"] + self.assertEqual((func.result, func.reason, func.observations["row"]), (P, None, 6)) + self.assertIn("M4: default network ACL assumed (no NACL type present)", func.assumptions) + self.assertEqual(func.evidence["result"], "PASS") + self.assertIn("§6", func.evidence["predicate"]) + for name in (SEC1, SEC2, SEC3): + self.assertIs(by_target(report)[f"INVARIANT:{name}:1"].result, P, name) + + def test_a_verifier_pair_the_table_does_not_have_is_still_not_available(self) -> None: + table = {k: v for k, v in DEFAULT_VERIFIERS.items() if k != KEY_REACHABILITY} + report = run(canonical(), inputs=inputs_for(canonical()), verifiers=table) + func = by_target(report)["INVARIANT:INV-FUNC-001:1"] + self.assertEqual((func.result, func.reason), (S, R.VERIFIER_NOT_AVAILABLE)) + self.assertIsNone(func.error) + # three security verifiers and the two gates ran; the functional item did not run one + self.assertEqual(report.verifier_invocations, 5) + + def test_the_default_table_has_the_three_registry_verifiers(self) -> None: + self.assertEqual( + set(DEFAULT_VERIFIERS), {KEY_PUBLIC_INGRESS, KEY_RDS_PUBLIC_FLAG, KEY_REACHABILITY} + ) + def test_every_result_carries_its_metadata(self) -> None: report = run(CLEAN) found = by_target(report) @@ -196,14 +232,13 @@ def test_the_summary_and_the_cost_metric(self) -> None: thaw_json(report.summary["by_class"]), { "CONSISTENCY": {"PASS": 1}, - "FUNCTIONAL": {"UNSUPPORTED": 1}, + "FUNCTIONAL": {"FAIL": 1}, "SECURITY": {"PASS": 3}, "STRUCTURAL": {"PASS": 1}, }, ) - # three security verifiers and the two gates ran; the functional item was answered - # without running a verifier - self.assertEqual(report.verifier_invocations, 5) + # the three security verifiers, the functional verifier and the two gates ran + self.assertEqual(report.verifier_invocations, 6) def test_the_mandatory_gate_runs_even_when_the_impact_report_is_empty(self) -> None: report = run(CLEAN, work=[]) @@ -295,7 +330,7 @@ def boom(_definition: Invariant, _inputs: VerificationInputs) -> PredicateOutcom self.assertIsNone(item.clauses) # the other verifiers are not affected, and the failed runs are still invocations self.assertIs(found["INVARIANT:INV-SEC-003:1"].result, P) - self.assertEqual(report.verifier_invocations, 5) + self.assertEqual(report.verifier_invocations, 6) def test_a_verifier_error_is_never_a_fail_or_a_pass(self) -> None: def boom(_definition: Invariant, _inputs: VerificationInputs) -> PredicateOutcome: @@ -425,9 +460,17 @@ def test_security_unknown(self) -> None: ) self.assertIs(self.verdict(text), AggregateResult.INSUFFICIENT_PROOF) - def test_unsupported_verifier_with_the_functional_invariant_is_never_a_pass(self) -> None: - # the interim: with INV-FUNC-001 required, a clean candidate is INSUFFICIENT_PROOF - self.assertIs(self.verdict(CLEAN, FOUR), AggregateResult.INSUFFICIENT_PROOF) + def test_a_missing_functional_verifier_is_never_a_pass(self) -> None: + # with INV-FUNC-001 required and no verifier for it, even a sound candidate is + # INSUFFICIENT_PROOF + table = {k: v for k, v in DEFAULT_VERIFIERS.items() if k != KEY_REACHABILITY} + verdict = self.verdict(canonical(), FOUR, verifiers=table) + self.assertIs(verdict, AggregateResult.INSUFFICIENT_PROOF) + + def test_the_functional_result_counts_in_the_aggregate(self) -> None: + self.assertIs(self.verdict(canonical(), FOUR), AggregateResult.PASS) + # no endpoints: INV-FUNC-001 fails at row 1, so the aggregate fails + self.assertIs(self.verdict(CLEAN, FOUR), AggregateResult.FAIL) def test_a_verifier_exception_is_insufficient_proof(self) -> None: def boom(_definition: Invariant, _inputs: VerificationInputs) -> PredicateOutcome: diff --git a/tests/unit/test_verification_fixtures.py b/tests/unit/test_verification_fixtures.py index 1e2d669..29203dd 100644 --- a/tests/unit/test_verification_fixtures.py +++ b/tests/unit/test_verification_fixtures.py @@ -6,9 +6,10 @@ external reviewer from registry-v1.0, not computed): the result of INV-SEC-001, INV-SEC-002 and INV-SEC-003, and the IPv4 and IPv6 clauses of the first two. -INV-FUNC-001 is not implemented in P5a. The interim assertion is that it is UNSUPPORTED -``verifier.not_available`` and never PASS; P5b replaces it. For the same reason the aggregate with -INV-FUNC-001 required is INSUFFICIENT_PROOF, never PASS, unless a security result already FAILs. +INV-FUNC-001 (P5b) is compared with ``expected.json`` in the same way. The aggregate over all four +invariants (Doc 09 §18) is FAIL if any expected result is FAIL, PASS if all four are PASS, and +INSUFFICIENT_PROOF otherwise (an expected UNKNOWN or UNSUPPORTED). It is computed from the engine's +own records, never taken from a constant. """ from __future__ import annotations @@ -88,15 +89,24 @@ def test_security_results_and_clauses_equal_expected_json(self) -> None: else: self.assertIsNone(item.clauses) - def test_the_functional_invariant_is_unsupported_and_never_pass_for_now(self) -> None: - for fixture_id in fixtures(): + def test_the_functional_result_equals_expected_json(self) -> None: + for fixture_id, fx in fixtures().items(): + with self.subTest(fixture=fixture_id): + _, report = world(fixture_id) + func = next(i for i in report.results if i.target_id == f"INVARIANT:{FUNC}:1") + self.assertEqual(func.result.value, expected(fx, FUNC)["result"]) + self.assertIsNone(func.clauses) + self.assertNotEqual(func.reason, VerificationReason.VERIFIER_NOT_AVAILABLE) + self.assertIsNone(func.error) + + def test_the_functional_invariant_is_never_a_pass_unless_expected_json_says_so(self) -> None: + for fixture_id, fx in fixtures().items(): + if expected(fx, FUNC)["result"] == "PASS": + continue with self.subTest(fixture=fixture_id): _, report = world(fixture_id) func = next(i for i in report.results if i.target_id == f"INVARIANT:{FUNC}:1") - self.assertEqual( - (func.result, func.reason), - (VerificationResult.UNSUPPORTED, VerificationReason.VERIFIER_NOT_AVAILABLE), - ) + self.assertIsNot(func.result, VerificationResult.PASS) def test_the_mandatory_gate_passes_on_every_sound_candidate(self) -> None: for fixture_id in fixtures(): @@ -153,15 +163,56 @@ def test_security_aggregate_follows_expected_json(self) -> None: with self.subTest(fixture=fixture_id): self.assertIs(self.verdict(fixture_id, SEC), hand) - def test_with_the_functional_invariant_required_nothing_passes_for_now(self) -> None: - # the interim: INV-FUNC-001 is UNSUPPORTED, so the aggregate is never PASS; a security - # FAIL still makes it FAIL + def test_the_aggregate_over_all_four_invariants_follows_expected_json(self) -> None: for fixture_id, fx in fixtures().items(): - wanted = [expected(fx, name)["result"] for name in SEC] - hand = AggregateResult.FAIL if "FAIL" in wanted else AggregateResult.INSUFFICIENT_PROOF + wanted = [expected(fx, name)["result"] for name in (*SEC, FUNC)] + if "FAIL" in wanted: + hand = AggregateResult.FAIL + elif set(wanted) == {"PASS"}: + hand = AggregateResult.PASS + else: + hand = AggregateResult.INSUFFICIENT_PROOF with self.subTest(fixture=fixture_id): self.assertIs(self.verdict(fixture_id, (*SEC, FUNC)), hand) +class TestCanonicalTransitions(unittest.TestCase): + """The canonical scenario (CLAUDE.md): a candidate that fixes SSH and keeps the path is + promotable, one that fixes SSH and breaks EC2 -> RDS must be rejected. Doc 09 §18, from the + engine's own records.""" + + SAFE = "canonical_safe_repair_promote_v1" + BREAKS = "canonical_security_repair_breaks_function_reject_v1" + + def verdict(self, fixture_id: str, *, without_functional: bool = False) -> AggregateResult: + inputs, report = world(fixture_id) + needs = required_for(inputs, [invariant_item(name) for name in (*SEC, FUNC)]) + results = [ + r + for r in report.results + if not (without_functional and r.target_id == f"INVARIANT:{FUNC}:1") + ] + return aggregate(results, needs, candidate_hash=report.candidate_hash) + + def test_the_safe_repair_aggregates_to_pass(self) -> None: + self.assertIs(self.verdict(self.SAFE), AggregateResult.PASS) + + def test_the_repair_that_breaks_the_database_path_aggregates_to_fail(self) -> None: + self.assertIs(self.verdict(self.BREAKS), AggregateResult.FAIL) + inputs, report = world(self.BREAKS) + by_id = {r.target_id: r for r in report.results} + # the security invariants hold; it is the functional one that fails (row 9: no ingress rule) + for name in SEC: + self.assertIs(by_id[f"INVARIANT:{name}:1"].result, VerificationResult.PASS) + func = by_id[f"INVARIANT:{FUNC}:1"] + self.assertEqual((func.result, func.observations["row"]), (VerificationResult.FAIL, 9)) + + def test_without_the_functional_result_nothing_passes(self) -> None: + # a missing required result is INSUFFICIENT_PROOF, never PASS (Doc 09 §18) + self.assertIs( + self.verdict(self.SAFE, without_functional=True), AggregateResult.INSUFFICIENT_PROOF + ) + + if __name__ == "__main__": unittest.main() From 68c4ffc90ad3d3840f0707f7d7b487596f81a362 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 01:09:56 +0530 Subject: [PATCH 7/8] =?UTF-8?q?P5b=20step=206:=20FUNC=20properties,=20the?= =?UTF-8?q?=20four=20P5=20gate=20probes,=20shared=20rule=20helpers=20(regi?= =?UTF-8?q?stry=20=C2=A76.3,=20=C2=A76.4;=20Doc=2015=20=C2=A712.2;=20C-151?= =?UTF-8?q?=20to=20C-154)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit test_reachability_properties.py: all 270 configurations of a determinate family against an oracle written in the test (plain ipaddress arithmetic, hand-derived in its docstring), then seeded random properties (order independence; added permission is monotone; irrelevant types change nothing; anything outside the model is UNSUPPORTED; indeterminate, partial or unsupported input is never a PASS), and demonstrations that each checker fails on a broken verifier. test_p5_gate_probes.py: (a) the unresolved direction form, (b) every verifier fault is VERIFIER_ERROR for each of the three verifiers, (c) stale hashes and versions are never sufficient, (d) the canonical scenario through the real fixtures: PASS and FAIL. Mutation checks (scratch copy outside the repository): 36 breakages of the functional verifier, the dispatch table, the baseline list and the boundary, all caught. Co-Authored-By: Claude Sonnet 5.5 --- tests/func_builders.py | 19 + tests/unit/test_p5_gate_probes.py | 328 +++++++++++++++ tests/unit/test_reachability_predicate.py | 22 +- tests/unit/test_reachability_properties.py | 441 +++++++++++++++++++++ 4 files changed, 791 insertions(+), 19 deletions(-) create mode 100644 tests/unit/test_p5_gate_probes.py create mode 100644 tests/unit/test_reachability_properties.py diff --git a/tests/func_builders.py b/tests/func_builders.py index 0d257dc..0089a65 100644 --- a/tests/func_builders.py +++ b/tests/func_builders.py @@ -103,3 +103,22 @@ def with_attributes(resource: Resource, attributes: Mapping[str, Any]) -> Resour def attribute(value: Any) -> dict[str, Any]: """An ATTRIBUTE-form argument in the stored encoding.""" return {"form": "ATTRIBUTE", "value": value} + + +def rule( + name: str, kind: str, protocol: str, low: int, high: int, group: str, body: str = "" +) -> str: + """A rule resource in the style of the canonical file.""" + return ( + f'resource "aws_security_group_rule" "{name}" {{\n type = "{kind}"\n' + f' protocol = "{protocol}"\n from_port = {low}\n to_port = {high}\n' + f" security_group_id = aws_security_group.{group}.id\n{body}}}\n" + ) + + +def ingress_5432(name: str, body: str) -> str: + return rule(name, "ingress", "tcp", 5432, 5432, "db", body) + + +def egress_5432(name: str, body: str) -> str: + return rule(name, "egress", "tcp", 5432, 5432, "app", body) diff --git a/tests/unit/test_p5_gate_probes.py b/tests/unit/test_p5_gate_probes.py new file mode 100644 index 0000000..330e8e3 --- /dev/null +++ b/tests/unit/test_p5_gate_probes.py @@ -0,0 +1,328 @@ +"""The four P5 gate probes (P5b step 6; Doc 15 §12.2; C-120(c), Doc 09 §11, §18, §30, §37). + +The reviewer repeats these. Each is the executable form of one sentence: + +(a) the ``unresolved`` direction form (C-120(c)) is UNSUPPORTED for every invariant that reads that + direction, never "no rules": the ingress of any group for INV-SEC-001 and INV-SEC-002, the + egress of ``SG(S)`` and the ingress of ``SG(D)`` for INV-FUNC-001; +(b) every verifier fault becomes VERIFIER_ERROR, never FAIL and never PASS, for each of the three + verifiers, whether it raises or reads a stored view that is not the shape P3a writes; +(c) a stale or mismatched candidate hash, invariant version or verifier version is never + sufficient, whatever the result says; +(d) the full pipeline on the canonical scenario: the SSH fix that keeps the path aggregates to + PASS, the SSH fix that breaks EC2 -> RDS to FAIL. +""" + +from __future__ import annotations + +import dataclasses +import unittest +from typing import Any + +from core.domain.enums import VerificationResult +from core.domain.jsonvalue import thaw_json +from core.domain.verification import ( + AggregateResult, + VerificationReason, + VerificationResultRecord, + aggregate, + sufficient, +) +from core.verification.dispatch import ( + DEFAULT_VERIFIERS, + PUBLIC_INGRESS, + RDS_PUBLIC_FLAG, + REACHABILITY_CFG, +) +from core.verification.engine import run_work_set +from tests.func_builders import ( + APP_EGRESS, + APP_GROUP, + APP_TO_DB, + DB_GROUP, + canonical, + edit, + edits, + with_attributes, +) +from tests.pipeline_builders import ( + counting_ids, + fixed_clock, + inputs_for, + invariant_item, + required_for, +) +from tests.security_builders import with_security +from tests.unit.test_verification_fixtures import world + +P, F, S, E = ( + VerificationResult.PASS, + VerificationResult.FAIL, + VerificationResult.UNSUPPORTED, + VerificationResult.VERIFIER_ERROR, +) +R = VerificationReason +NAMES = ("INV-SEC-001", "INV-SEC-002", "INV-SEC-003", "INV-FUNC-001") +VAR = 'variable "u" {}\n' + + +def run(text: str, **overrides: Any) -> dict[str, VerificationResultRecord]: + given = overrides.pop("given", None) or inputs_for(text) + report = run_work_set( + [invariant_item(name) for name in NAMES], + given, + clock=fixed_clock(), + ids=counting_ids(), + **overrides, + ) + return {item.target_id: item for item in report.results} + + +def item(found: dict[str, VerificationResultRecord], name: str) -> VerificationResultRecord: + return found[f"INVARIANT:{name}:1"] + + +class TestProbeA(unittest.TestCase): + """The unresolved direction form is UNSUPPORTED, never "no rules".""" + + def test_the_ingress_of_the_database_group(self) -> None: + # nothing targets the group by a rule resource, so it is not MIXED; its ingress is unknown + text = VAR + edits( + canonical(), + (DB_GROUP, DB_GROUP.replace(" egress = []", " ingress = var.u")), + (APP_TO_DB, ""), + ) + found = run(text) + for name in ("INV-SEC-001", "INV-SEC-002", "INV-FUNC-001"): + with self.subTest(invariant=name): + self.assertEqual( + (item(found, name).result, item(found, name).reason), (S, R.FORMS_UNRESOLVED) + ) + # INV-SEC-003 reads no security group: unaffected + self.assertIs(item(found, "INV-SEC-003").result, P) + + def test_the_egress_of_the_application_group_matters_to_the_functional_invariant_only( + self, + ) -> None: + text = VAR + edits( + canonical(), + (APP_GROUP, APP_GROUP.replace(" ingress = []", " egress = var.u")), + (APP_EGRESS, ""), + ) + found = run(text) + self.assertEqual( + (item(found, "INV-FUNC-001").result, item(found, "INV-FUNC-001").reason), + (S, R.FORMS_UNRESOLVED), + ) + # the security predicates read ingress: the egress of a group is not read + self.assertIs(item(found, "INV-SEC-001").result, P) + + def test_an_unresolved_direction_is_never_read_as_no_rules(self) -> None: + # with no rules at all the database group would make the functional invariant FAIL + # (row 9); an unresolved ingress must not be taken for "no rules" + text = VAR + edits( + canonical(), + (DB_GROUP, DB_GROUP.replace(" egress = []", " ingress = var.u")), + (APP_TO_DB, ""), + ) + func = item(run(text), "INV-FUNC-001") + self.assertIsNot(func.result, F) + self.assertIsNot(func.result, P) + + +class TestProbeB(unittest.TestCase): + """Every verifier fault is VERIFIER_ERROR, never FAIL and never PASS.""" + + KEYS = {"INV-SEC-001": PUBLIC_INGRESS, "INV-SEC-002": PUBLIC_INGRESS, + "INV-SEC-003": RDS_PUBLIC_FLAG, "INV-FUNC-001": REACHABILITY_CFG} # fmt: skip + + def test_a_verifier_that_raises(self) -> None: + for name, key in self.KEYS.items(): + + def boom(_definition: object, _inputs: object) -> object: + raise RuntimeError("boom") + + table = {**DEFAULT_VERIFIERS, key: boom} + found = run(canonical(), verifiers=table) + with self.subTest(invariant=name): + self.assertEqual( + (item(found, name).result, item(found, name).reason), (E, R.VERIFIER_ERROR) + ) + self.assertEqual(dict(item(found, name).error or {})["type"], "RuntimeError") + + def test_a_stored_view_that_is_not_the_shape_p3a_writes(self) -> None: + given = inputs_for(canonical()) + by_address = {r.address: r for r in given.candidate_resources} + + def swapped(address: str, damaged: Any) -> Any: + rest = [r for r in given.candidate_resources if r.address != address] + return dataclasses.replace(given, candidate_resources=(*rest, damaged)) + + cases = { + "the instance attributes (INV-FUNC-001 only)": ( + swapped( + "aws_instance.app", + with_attributes( + by_address["aws_instance.app"], {"subnet_id": {"form": "ATTRIBUTE"}} + ), + ), + {"INV-FUNC-001"}, + ), + "the database security view (INV-SEC-003 only)": ( + swapped( + "aws_db_instance.database", + with_security(by_address["aws_db_instance.database"], {"surprise": 1}), + ), + {"INV-SEC-003"}, + ), + "a group security view (the group readers: SEC-001, SEC-002, FUNC-001)": ( + swapped( + "aws_security_group.db", with_security(by_address["aws_security_group.db"], {}) + ), + {"INV-SEC-001", "INV-SEC-002", "INV-FUNC-001"}, + ), + } + for label, (damaged, hit) in cases.items(): + found = run("", given=damaged) + for name in NAMES: + with self.subTest(case=label, invariant=name): + if name in hit: + self.assertEqual( + (item(found, name).result, item(found, name).reason), + (E, R.VERIFIER_ERROR), + ) + self.assertEqual(dict(item(found, name).error or {})["type"], "ViewError") + else: + self.assertIsNot(item(found, name).result, E) + + def test_an_error_is_not_evidence_of_a_property(self) -> None: + def boom(_definition: object, _inputs: object) -> object: + raise RuntimeError("boom") + + found = run(canonical(), verifiers={**DEFAULT_VERIFIERS, REACHABILITY_CFG: boom}) + given = inputs_for(canonical()) + report_results = list(found.values()) + verdict = aggregate( + report_results, + required_for(given, [invariant_item(n) for n in NAMES]), + candidate_hash=given.candidate_state_hash, + ) + self.assertIs(verdict, AggregateResult.INSUFFICIENT_PROOF) + + +class TestProbeC(unittest.TestCase): + """A stale or mismatched hash or version is never sufficient.""" + + def setUp(self) -> None: + self.given = inputs_for(canonical()) + self.found = run(canonical(), given=self.given) + + def args(self, name: str) -> dict[str, Any]: + definition = self.given.invariant(name, 1) + assert definition is not None + return { + "target_id": f"INVARIANT:{name}:1", + "candidate_hash": self.given.candidate_state_hash, + "invariant_id": name, + "invariant_version": 1, + "verifier_id": definition.verifier_id, + "verifier_version": definition.verifier_version, + } + + def test_a_sound_pass_is_sufficient_for_its_own_requirement_only(self) -> None: + for name in NAMES: + with self.subTest(invariant=name): + self.assertIs(item(self.found, name).result, P) + self.assertTrue(sufficient(item(self.found, name), **self.args(name))) + + def test_each_mismatch_makes_it_insufficient(self) -> None: + for name in NAMES: + record = item(self.found, name) + for field, other in ( + ("candidate_hash", "b" * 64), + ("invariant_version", 2), + ("verifier_version", "2"), + ("verifier_id", "someone.else"), + ("target_id", "INVARIANT:INV-OTHER-001:1"), + ): + with self.subTest(invariant=name, field=field): + self.assertFalse(sufficient(record, **{**self.args(name), field: other})) + + def test_a_stale_set_of_results_never_aggregates_to_pass(self) -> None: + needs = required_for(self.given, [invariant_item(n) for n in NAMES]) + results = list(self.found.values()) + self.assertIs( + aggregate(results, needs, candidate_hash=self.given.candidate_state_hash), + AggregateResult.PASS, + ) + self.assertIs( + aggregate(results, needs, candidate_hash="b" * 64), AggregateResult.INSUFFICIENT_PROOF + ) + for name in NAMES: + stale = [ + ( + dataclasses.replace(r, candidate_hash="b" * 64) + if r.target_id.endswith(f"{name}:1") + else r + ) + for r in results + ] + with self.subTest(stale=name): + self.assertIs( + aggregate(stale, needs, candidate_hash=self.given.candidate_state_hash), + AggregateResult.INSUFFICIENT_PROOF, + ) + + def test_a_stale_fail_does_not_count_as_a_fail_either(self) -> None: + # Doc 09 §30: a result for another candidate is never reused, whatever it says + text = edit(canonical(), APP_TO_DB, "") + given = inputs_for(text) + found = run(text, given=given) + self.assertIs(item(found, "INV-FUNC-001").result, F) + needs = required_for(given, [invariant_item("INV-FUNC-001")]) + self.assertIs( + aggregate(list(found.values()), needs, candidate_hash=given.candidate_state_hash), + AggregateResult.FAIL, + ) + self.assertIs( + aggregate(list(found.values()), needs, candidate_hash="c" * 64), + AggregateResult.INSUFFICIENT_PROOF, + ) + + +class TestProbeD(unittest.TestCase): + """The canonical scenario through the whole pipeline (the real fixtures).""" + + def verdict(self, fixture_id: str) -> AggregateResult: + given, report = world(fixture_id) + needs = required_for(given, [invariant_item(n) for n in NAMES]) + return aggregate(report.results, needs, candidate_hash=report.candidate_hash) + + def test_the_trusted_state_has_public_ssh_open(self) -> None: + _, report = world("canonical_baseline_eligible_v1") + sec1 = next(r for r in report.results if r.target_id == "INVARIANT:INV-SEC-001:1") + func = next(r for r in report.results if r.target_id == "INVARIANT:INV-FUNC-001:1") + self.assertIs(sec1.result, F) # SSH is open to the internet + self.assertIs(func.result, P) # and the path to the database works + + def test_the_ssh_fix_that_keeps_the_path_aggregates_to_pass(self) -> None: + self.assertIs(self.verdict("canonical_safe_repair_promote_v1"), AggregateResult.PASS) + + def test_the_ssh_fix_that_breaks_the_path_aggregates_to_fail(self) -> None: + self.assertIs( + self.verdict("canonical_security_repair_breaks_function_reject_v1"), + AggregateResult.FAIL, + ) + _, report = world("canonical_security_repair_breaks_function_reject_v1") + sec1 = next(r for r in report.results if r.target_id == "INVARIANT:INV-SEC-001:1") + self.assertIs(sec1.result, P) # the SSH hole is fixed; the database path is what failed + + def test_every_record_of_the_scenario_round_trips_and_states_its_own_result(self) -> None: + _, report = world("canonical_safe_repair_promote_v1") + for record in report.results: + self.assertEqual(VerificationResultRecord.from_dict(record.to_dict()), record) + self.assertEqual(thaw_json(record.evidence)["result"], record.result.value) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/unit/test_reachability_predicate.py b/tests/unit/test_reachability_predicate.py index 37f51ce..8d253fd 100644 --- a/tests/unit/test_reachability_predicate.py +++ b/tests/unit/test_reachability_predicate.py @@ -36,6 +36,9 @@ canonical, edit, edits, + egress_5432, + ingress_5432, + rule, with_attributes, ) from tests.reach_builders import definition, evaluate, inputs @@ -59,25 +62,6 @@ ) -def rule( - name: str, kind: str, protocol: str, low: int, high: int, group: str, body: str = "" -) -> str: - """A rule resource in the style of the canonical file.""" - return ( - f'resource "aws_security_group_rule" "{name}" {{\n type = "{kind}"\n' - f' protocol = "{protocol}"\n from_port = {low}\n to_port = {high}\n' - f" security_group_id = aws_security_group.{group}.id\n{body}}}\n" - ) - - -def ingress_5432(name: str, body: str) -> str: - return rule(name, "ingress", "tcp", 5432, 5432, "db", body) - - -def egress_5432(name: str, body: str) -> str: - return rule(name, "egress", "tcp", 5432, 5432, "app", body) - - def swap_ingress(body: str) -> str: """The canonical text with ``app_to_db_5432`` replaced by another ingress rule on ``db``.""" return edit(canonical(), APP_TO_DB, ingress_5432("ingress_x", body)) diff --git a/tests/unit/test_reachability_properties.py b/tests/unit/test_reachability_properties.py new file mode 100644 index 0000000..7c0eb07 --- /dev/null +++ b/tests/unit/test_reachability_properties.py @@ -0,0 +1,441 @@ +"""INV-FUNC-001 on generated topologies (P5b step 6; registry §6.3, §6.4; C-151 to C-154). + +Part one is **exhaustive** over a family of fully determinate topologies, against an oracle written +in this file with plain ``ipaddress`` arithmetic and the table of §6.4 (no code of +``core.verification``): 6 egress variants x 5 ingress variants x 3 private-IP variants x 3 +placements of the instance, 270 configurations. The oracle is hand-derived in its docstring. + +Part two is seeded ``random`` (stdlib), five seeds: the result does not depend on the order of the +resources; adding a matching allow rule never turns PASS into non-PASS and never turns UNKNOWN into +FAIL; resources of irrelevant types change nothing; an intra-VPC non-local route, a type of the +relevant-unsupported list, ``propagating_vgws`` or an interface block always gives UNSUPPORTED; and +every indeterminate, partial or unsupported input is UNKNOWN, UNSUPPORTED or FAIL, never PASS (the +executable form of "unknown and unsupported cases do not become PASS"). + +Part three shows that the checkers themselves fail when a rule is broken. +""" + +from __future__ import annotations + +import dataclasses +import ipaddress +import random +import unittest +from collections.abc import Callable + +from core.domain.enums import VerificationResult +from core.domain.registry_v1 import FUNC_RELEVANT_UNSUPPORTED +from core.verification.outcome import PredicateOutcome +from core.verification.reachability import evaluate_reachability +from tests.func_builders import ( + APP_EGRESS, + APP_TO_DB, + DB_SGS_LINE, + IGW_ROUTE, + PUBLIC_IP_LINE, + SOURCE_LINE, + SUBNET_LINE, + canonical, + edit, + egress_5432, + ingress_5432, + rule, +) +from tests.reach_builders import definition, inputs + +P, F, U, S = ( + VerificationResult.PASS, + VerificationResult.FAIL, + VerificationResult.UNKNOWN, + VerificationResult.UNSUPPORTED, +) +SEEDS = (20261029, 1, 7, 424242, 99991) +VAR = 'variable "u" {}\n' +FAR = ( + '\nresource "aws_vpc" "other" {\n cidr_block = "10.1.0.0/16"\n}\n' + '\nresource "aws_subnet" "far" {\n vpc_id = aws_vpc.other.id\n' + ' cidr_block = "10.1.1.0/24"\n availability_zone = "us-east-1a"\n}\n' +) + +EGRESS = { + "all": APP_EGRESS, + "vpc": egress_5432("e", ' cidr_blocks = ["10.0.0.0/16"]\n'), + "dbsubnet": egress_5432("e", ' cidr_blocks = ["10.0.2.0/24"]\n'), + "other_port": rule("e", "egress", "tcp", 5433, 5433, "app", ' cidr_blocks = ["0.0.0.0/0"]\n'), + "none": "", + "to_db": egress_5432("e", " source_security_group_id = aws_security_group.db.id\n"), +} +INGRESS = { + "group": APP_TO_DB, + "app_subnet": ingress_5432("i", ' cidr_blocks = ["10.0.1.0/24"]\n'), + "half": ingress_5432("i", ' cidr_blocks = ["10.0.1.0/25"]\n'), + "other": ingress_5432("i", ' cidr_blocks = ["10.0.9.0/24"]\n'), + "none": "", +} +PRIVATE_IP = (None, "10.0.1.10", "10.0.1.200") +PLACEMENT = ("app", "db_b", "far") +SUBNET_CIDR = {"app": "10.0.1.0/24", "db_b": "10.0.3.0/24"} +INGRESS_CIDR = {"app_subnet": "10.0.1.0/24", "half": "10.0.1.0/25", "other": "10.0.9.0/24"} + + +def build(egress: str, ingress: str, ip: str | None, placement: str) -> str: + text = edit(canonical(), APP_EGRESS, EGRESS[egress]) + text = edit(text, APP_TO_DB, INGRESS[ingress]) + if placement == "db_b": + text = edit(text, SUBNET_LINE, " subnet_id = aws_subnet.db_b.id\n") + elif placement == "far": + text = edit(text, SUBNET_LINE, " subnet_id = aws_subnet.far.id\n") + FAR + if ip is not None: + text = edit( + text, + PUBLIC_IP_LINE, + f' associate_public_ip_address = true\n private_ip = "{ip}"\n}}', + ) + return text + + +def oracle( + egress: str, ingress: str, ip: str | None, placement: str +) -> tuple[VerificationResult, int]: + """Registry §6.4 for this family, by hand. Every rule is determinate and there is no + unsupported construct, so rows 1 to 4 never apply and row 5 is the instance in another VPC. + + E5 holds for a ``-1`` rule to the internet, a TCP/5432 rule whose CIDR is the whole VPC + 10.0.0.0/16, or one whose destination group is the database group; it fails with a partial + cover for 10.0.2.0/24 (inside the VPC but not all of it) and with no cover for another port or + no rule. ADDR(S) is private_ip/32 if set, else the subnet CIDR. E6 holds for the app group as + source, or a CIDR that contains ADDR(S); it is partial when the CIDR overlaps ADDR(S) without + containing it, which a single address cannot do. Row 8 if a failing condition is partial, + else row 9; row 6 if both hold.""" + if placement == "far": + return F, 5 + e5 = egress in ("all", "vpc", "to_db") + e5_partial = egress == "dbsubnet" + address = ipaddress.ip_network(f"{ip}/32" if ip else SUBNET_CIDR[placement]) + if ingress == "group": + e6, e6_partial = True, False + elif ingress == "none": + e6, e6_partial = False, False + else: + net = ipaddress.ip_network(INGRESS_CIDR[ingress]) + e6 = address.subnet_of(net) + e6_partial = (not e6) and net.overlaps(address) + if e5 and e6: + return P, 6 + if (not e5 and e5_partial) or (not e6 and e6_partial): + return U, 8 + return F, 9 + + +def evaluate(text: str, shuffle: int | None = None) -> PredicateOutcome: + given = inputs(text) + if shuffle is not None: + resources = list(given.candidate_resources) + random.Random(shuffle).shuffle(resources) + given = dataclasses.replace(given, candidate_resources=tuple(resources)) + return evaluate_reachability(definition(given), given) + + +Evaluator = Callable[[str, int | None], PredicateOutcome] + + +class TestAgainstTheOracle(unittest.TestCase): + def test_every_configuration_of_the_family(self) -> None: + seen: dict[tuple[VerificationResult, int], int] = {} + total = 0 + for egress in EGRESS: + for ingress in INGRESS: + for ip in PRIVATE_IP: + for placement in PLACEMENT: + want = oracle(egress, ingress, ip, placement) + outcome = evaluate(build(egress, ingress, ip, placement)) + got = (outcome.result, outcome.observations["row"]) + with self.subTest(egress=egress, ingress=ingress, ip=ip, at=placement): + self.assertEqual(got, want) + seen[want] = seen.get(want, 0) + 1 + total += 1 + self.assertEqual(total, 6 * 5 * 3 * 3) + # the family reaches every row it can: the check is not vacuous in any direction + self.assertEqual({row for _, row in seen}, {5, 6, 8, 9}) + self.assertTrue(all(count >= 5 for count in seen.values()), seen) + + +# --- part two: properties ------------------------------------------------------------------------- + + +def random_text(rng: random.Random) -> str: + return build( + rng.choice(list(EGRESS)), + rng.choice(list(INGRESS)), + rng.choice(PRIVATE_IP), + rng.choice(("app", "app", "db_b")), + ) + + +def key(outcome: PredicateOutcome) -> tuple[VerificationResult, object, object, object]: + obs = outcome.observations + return (outcome.result, obs["row"], outcome.reason, tuple(obs["failing_conditions"])) + + +def order_violations(evaluator: Evaluator, seed: int, cases: int = 12) -> list[str]: + rng = random.Random(seed) + bad = [] + for _ in range(cases): + text = random_text(rng) + base = key(evaluator(text, None)) + for shuffle in (1, 2, 3): + if key(evaluator(text, shuffle)) != base: + bad.append(text) + break + return bad + + +NOISE = ( + '\nresource "aws_internet_gateway" "spare" {\n vpc_id = aws_vpc.main.id\n}\n', + '\nresource "aws_subnet" "spare" {\n vpc_id = aws_vpc.main.id\n cidr_block = "10.0.7.0/24"\n' + ' availability_zone = "us-east-1c"\n}\n', + '\nresource "aws_security_group" "spare" {\n vpc_id = aws_vpc.main.id\n}\n' + + rule("spare_rule", "ingress", "tcp", 22, 22, "spare", ' cidr_blocks = ["10.0.0.0/8"]\n'), + '\nresource "aws_vpc" "spare" {\n cidr_block = "10.9.0.0/16"\n}\n' + '\nresource "aws_route_table" "spare" {\n vpc_id = aws_vpc.spare.id\n' + ' propagating_vgws = ["vgw-1"]\n route {\n cidr_block = "10.9.1.0/24"\n' + ' nat_gateway_id = "nat-1"\n }\n}\n', + '\nresource "aws_route_table_association" "spare" {\n subnet_id = aws_subnet.db_a.id\n' + " route_table_id = aws_route_table.public.id\n}\n", +) + + +def noise_violations(evaluator: Evaluator, seed: int, cases: int = 10) -> list[str]: + rng = random.Random(seed) + bad = [] + for _ in range(cases): + text = random_text(rng) + added = text + "".join(rng.sample(NOISE, rng.randint(1, 3))) + if key(evaluator(text, None)) != key(evaluator(added, None)): + bad.append(text) + return bad + + +ALLOW_EGRESS = ( + egress_5432("extra", ' cidr_blocks = ["10.0.0.0/16"]\n'), + egress_5432("extra", " source_security_group_id = aws_security_group.db.id\n"), + rule("extra", "egress", "-1", 0, 0, "app", ' cidr_blocks = ["0.0.0.0/0"]\n'), + rule("extra", "egress", "tcp", 80, 80, "app", ' cidr_blocks = ["10.0.0.0/16"]\n'), +) +ALLOW_INGRESS = ( + ingress_5432("extra", " source_security_group_id = aws_security_group.app.id\n"), + ingress_5432("extra", ' cidr_blocks = ["10.0.1.0/24"]\n'), + rule("extra", "ingress", "tcp", 22, 22, "db", ' cidr_blocks = ["10.0.0.0/8"]\n'), +) +INDETERMINATE = ( + ingress_5432("extra", " source_security_group_id = var.u\n"), + egress_5432("extra", " source_security_group_id = var.u\n"), +) + + +def monotone_violations(evaluator: Evaluator, seed: int, cases: int = 16) -> list[str]: + """Adding a determinate allow rule on S's egress or D's ingress never turns PASS into + non-PASS and never turns UNKNOWN into FAIL; adding an indeterminate rule keeps PASS.""" + rng = random.Random(seed) + bad = [] + for _ in range(cases): + text = random_text(rng) + before = evaluator(text, None).result + for extra in (rng.choice(ALLOW_EGRESS), rng.choice(ALLOW_INGRESS)): + after = evaluator(VAR + text + extra, None).result + if before is P and after is not P: + bad.append(text) + if before is U and after is F: + bad.append(text) + if before is P and evaluator(VAR + text + rng.choice(INDETERMINATE), None).result is not P: + bad.append(text) + return bad + + +TABLE_HEAD = 'resource "aws_route_table" "public" {\n vpc_id = aws_vpc.main.id\n' +PUBLIC_IP = " associate_public_ip_address = true\n" +NACL = '\nresource "aws_network_acl" "n" {\n vpc_id = aws_vpc.main.id\n}\n' +INTRA_ROUTE = ' route {\n cidr_block = "10.0.2.0/24"\n nat_gateway_id = "nat-1"\n }\n' +INTERFACE = ( + " network_interface {\n device_index = 0\n" ' network_interface_id = "eni-1"\n }\n' +) + +Transform = Callable[[str], str] + + +def unsupported_triggers(kind: str) -> dict[str, Transform]: + """Edits that put a configuration outside the model, whatever else it says (row 2).""" + return { + "an intra-VPC non-local route": lambda t: edit(t, IGW_ROUTE, IGW_ROUTE + INTRA_ROUTE), + "propagating_vgws": lambda t: edit(t, TABLE_HEAD, TABLE_HEAD + " propagating_vgws = []\n"), + f"a {kind}": lambda t: t + f'\nresource "{kind}" "x" {{\n}}\n', + "an interface block": lambda t: edit(t, PUBLIC_IP, PUBLIC_IP + INTERFACE), + } + + +def unsupported_violations(evaluator: Evaluator, seed: int, cases: int = 12) -> list[str]: + rng = random.Random(seed) + bad = [] + for _ in range(cases): + text = random_text(rng) + kind = rng.choice(sorted(FUNC_RELEVANT_UNSUPPORTED)) + for label, transform in unsupported_triggers(kind).items(): + outcome = evaluator(transform(text), None) + if outcome.result is not S or outcome.observations["row"] != 2: + bad.append(f"{label}: {text[:40]!r}") + return bad + + +# Edits of the canonical text after which no PASS may be reported: an unresolved or partial or +# unsupported fact on the path (each one removes the determinate support for a PASS or sits ahead +# of it in the table). +POISONS: dict[str, Transform] = { + "D groups unknown": lambda t: edit(t, DB_SGS_LINE, " vpc_security_group_ids = var.u\n"), + "S subnet unknown": lambda t: edit(t, SUBNET_LINE, " subnet_id = var.u\n"), + "port unknown": lambda t: edit( + t, + " publicly_accessible = false\n", + " publicly_accessible = false\n port = var.u\n", + ), + "engine unknown": lambda t: edit( + t, ' engine = "postgres"\n', " engine = var.u\n" + ), + "source group unknown": lambda t: edit(t, SOURCE_LINE, " source_security_group_id = var.u\n"), + "ingress prefix list": lambda t: edit(t, SOURCE_LINE, ' prefix_list_ids = ["pl-1"]\n'), + "destination partly covered": lambda t: edit( + t, APP_EGRESS, egress_5432("e", ' cidr_blocks = ["10.0.2.0/24"]\n') + ), + "a network acl": lambda t: t + NACL, + "name-based groups": lambda t: edit( + t, PUBLIC_IP, PUBLIC_IP + ' security_groups = ["default"]\n' + ), + "no subnet": lambda t: edit(t, SUBNET_LINE, ""), + "an interface block": lambda t: edit(t, PUBLIC_IP, PUBLIC_IP + INTERFACE), + "an intra-VPC route": lambda t: edit(t, IGW_ROUTE, IGW_ROUTE + INTRA_ROUTE), +} + + +def never_pass_violations(evaluator: Evaluator, seed: int, cases: int = 4) -> list[str]: + rng = random.Random(seed) + bad = [] + for label, transform in POISONS.items(): + for _ in range(cases): + noise = "".join(rng.sample(NOISE, rng.randint(0, 2))) + outcome = evaluator(VAR + transform(canonical()) + noise, None) + if outcome.result is P: + bad.append(label) + return bad + + +class TestProperties(unittest.TestCase): + def test_the_order_of_the_resources_never_changes_the_outcome(self) -> None: + for seed in SEEDS: + self.assertEqual(order_violations(evaluate, seed), [], f"seed {seed}") + + def test_the_order_of_a_cidr_list_never_changes_the_outcome(self) -> None: + # within one rule a CIDR list is a union (registry 2.5): two halves cover the VPC CIDR + # (E5 holds, row 6) whichever comes first; a list that leaves a half out is partial (row 8) + cases = ( + (["10.0.0.0/17", "10.0.128.0/17"], P, 6), + (["10.0.128.0/17", "10.0.0.0/17"], P, 6), + (["10.0.0.0/17", "10.0.0.0/18"], U, 8), + (["10.0.0.0/18", "10.0.0.0/17"], U, 8), + ) + for order, result, row in cases: + body = f" cidr_blocks = {order!r}\n".replace("'", '"') + text = edit(canonical(), APP_EGRESS, egress_5432("halves", body)) + outcome = evaluate(text) + with self.subTest(order=order): + self.assertEqual((outcome.result, outcome.observations["row"]), (result, row)) + + def test_irrelevant_resources_change_nothing(self) -> None: + for seed in SEEDS: + self.assertEqual(noise_violations(evaluate, seed), [], f"seed {seed}") + + def test_adding_permission_is_monotone(self) -> None: + for seed in SEEDS: + self.assertEqual(monotone_violations(evaluate, seed), [], f"seed {seed}") + + def test_anything_outside_the_model_is_unsupported(self) -> None: + for seed in SEEDS: + self.assertEqual(unsupported_violations(evaluate, seed), [], f"seed {seed}") + + def test_indeterminate_partial_or_unsupported_input_is_never_a_pass(self) -> None: + for seed in SEEDS: + self.assertEqual(never_pass_violations(evaluate, seed), [], f"seed {seed}") + + def test_every_poison_is_a_real_change(self) -> None: + for label, transform in POISONS.items(): + with self.subTest(poison=label): + self.assertNotEqual(transform(canonical()), canonical()) + + +# --- part three: the checkers can fail ---------------------------------------------------------- + + +def replaced(outcome: PredicateOutcome, **fields: object) -> PredicateOutcome: + return dataclasses.replace(outcome, **fields) # type: ignore[arg-type] + + +class TestTheCheckersCanFail(unittest.TestCase): + """A property checker that cannot fail proves nothing: break the verifier and watch it fail.""" + + def test_the_oracle_check_catches_a_changed_row(self) -> None: + def row_eight_as_fail(text: str, shuffle: int | None) -> PredicateOutcome: + outcome = evaluate(text, shuffle) + return replaced(outcome, result=F) if outcome.observations["row"] == 8 else outcome + + caught = 0 + for egress in EGRESS: + for ingress in INGRESS: + outcome = row_eight_as_fail(build(egress, ingress, None, "app"), None) + got = (outcome.result, outcome.observations["row"]) + caught += got != oracle(egress, ingress, None, "app") + self.assertGreater(caught, 0) + + def test_the_order_check_catches_an_order_dependent_verifier(self) -> None: + def drops_the_last_resource(text: str, shuffle: int | None) -> PredicateOutcome: + given = inputs(text) + resources = list(given.candidate_resources) + if shuffle is not None: + random.Random(shuffle).shuffle(resources) + resources = resources[:-1] + given = dataclasses.replace(given, candidate_resources=tuple(resources)) + return evaluate_reachability(definition(given), given) + + self.assertGreater(sum(len(order_violations(drops_the_last_resource, s)) for s in SEEDS), 0) + + def test_the_noise_check_catches_a_verifier_that_reads_irrelevant_resources(self) -> None: + def nervous(text: str, shuffle: int | None) -> PredicateOutcome: + outcome = evaluate(text, shuffle) + return replaced(outcome, result=S) if "spare" in text else outcome + + self.assertGreater(sum(len(noise_violations(nervous, s)) for s in SEEDS), 0) + + def test_the_monotone_check_catches_a_non_monotone_verifier(self) -> None: + def forgetful(text: str, shuffle: int | None) -> PredicateOutcome: + outcome = evaluate(text, shuffle) + crowded = text.count('resource "aws_security_group_rule"') > 2 + return replaced(outcome, result=F) if crowded and outcome.result is P else outcome + + self.assertGreater(sum(len(monotone_violations(forgetful, s)) for s in SEEDS), 0) + + def test_the_unsupported_check_catches_a_verifier_that_ignores_a_trigger(self) -> None: + def ignores_types(text: str, shuffle: int | None) -> PredicateOutcome: + outcome = evaluate(text, shuffle) + if outcome.reason is not None and outcome.reason.value == "type.relevant_unsupported": + return replaced(outcome, result=P) + return outcome + + self.assertGreater(sum(len(unsupported_violations(ignores_types, s)) for s in SEEDS), 0) + + def test_the_never_pass_check_catches_unknown_read_as_pass(self) -> None: + def optimistic(text: str, shuffle: int | None) -> PredicateOutcome: + outcome = evaluate(text, shuffle) + return replaced(outcome, result=P) if outcome.result is U else outcome + + self.assertGreater(sum(len(never_pass_violations(optimistic, s)) for s in SEEDS), 0) + + +if __name__ == "__main__": + unittest.main() From 3e09c10c483eb163294ce4c019714e61573b46eb Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 01:11:51 +0530 Subject: [PATCH 8/8] =?UTF-8?q?P5b=20step=207:=20register=20row=20C-155=20?= =?UTF-8?q?(Open),=20the=20cases=20registry=20section=206=20leaves=20to=20?= =?UTF-8?q?v1.1=20(registry=20=C2=A76.3,=20=C2=A76.4;=20C-150=20to=20C-154?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Twelve points that the registry text does not decide and that this package settled conservatively (R5): E2 in row 4, the "it" of row 7, "could satisfy", the UNSUPPORTED endpoint resource, rules of unknown direction, pseudo-groups, literal ids, M1, M3, per-rule coverage, the src_sg of an egress rule and ADDR(S). Open until the authors decide. Co-Authored-By: Claude Sonnet 5.5 --- docs/DECISIONS_REGISTER.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/DECISIONS_REGISTER.md b/docs/DECISIONS_REGISTER.md index 70c5deb..ebcd64a 100644 --- a/docs/DECISIONS_REGISTER.md +++ b/docs/DECISIONS_REGISTER.md @@ -166,3 +166,4 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-152 | P5b: endpoint resolution across moves, and indeterminate endpoints | The bindings `S` and `D` are addresses of the **trusted** state (registry §6.1). A baseline resolves a binding by address in the candidate; an address that no candidate resource has is absent (row 1, FAIL, `endpoint.absent`). A candidate with a parent resolves it through the identity report (registry §2.3, moves followed): the match whose `trusted_resource_ref` is the binding; UNCHANGED, MODIFIED and REPLACED give the candidate resource of the match; **DELETED is absent** (row 1); **UNCERTAIN, a placeholder (unknown `count` or `for_each`, support status UNKNOWN) and a resource that is itself UNSUPPORTED are indeterminate**: UNKNOWN (row 4), never FAIL, never PASS. **Registry reading, flagged:** registry §2.4 would call an UNSUPPORTED endpoint resource UNSUPPORTED rather than UNKNOWN; the work package says UNKNOWN and both are lack of proof, so the work package is followed and the question goes to the reviewer. A candidate that has a parent but no identity report, or a report with no match for the binding while the parent has the resource, is UNSUPPORTED `identity.missing` (as in P5a). A binding that the parent does not have either is UNSUPPORTED `parameters.invalid` (the definitions and the trusted state disagree). **A created endpoint** (the candidate creates the resource at another address and the old one is DELETED) is FAIL by row 1: no heuristic match is made; only a `moved` block or an identity match ties a new address to the trusted one. The observation `endpoints` records, per binding, the trusted address, the match change type and the candidate address. | Proposed (P5b) | | C-153 | P5b: rows 1 to 9 and the definitions they need | The rows of registry §6.4 are evaluated in order and the first that applies returns. Row 2 collects every cause it can evaluate, reports all of them in the observation `row2_causes` and names the reason by the first in this fixed order: relevant-unsupported type, M3 route, `propagating_vgws`, interface block, name-based `security_groups`, no `vpc_security_group_ids` or no `subnet_id`, MIXED, RETAINED-INLINE, `unresolved` direction form (C-120(c)), unsupported value or rule, other. **Definitions** (each with the registry text it makes precise): `SG(S)` and `SG(D)` are the groups that the `vpc_security_group_ids` of `S` and `D` reference; `src_sg(r)` is `source_security_groups` of the stored rule view (a reference gives the address of the group; a literal AWS id gives `EXTERNAL:` and matches no configured group), so "src_sg(r) contains a group in SG(D)" is a non-empty intersection of addresses; `self(r)` is the stored `self` flag and E6 needs `h in SG(S)`; the CIDR clauses use `cidr.covers` on the IPv4 sources of **one** determinate rule that permits TCP/5432 (`ports.permits_tcp`): E5 and E6 say "exists r with ... v4(r) covers" and `v4(r)` is the CIDR list of a single rule, so two rules with half of the range each do not cover it (no pooling across rules; a test pins this); **"partly covers"** (row 8) is `cidr.overlaps`: the IPv4 sources of a determinate rule that permits TCP/5432 intersect the target, and (E5 or E6 failing) no rule covers it (interval arithmetic, no enumeration); `ADDR(S)` is `private_ip/32` if it resolves to an IPv4 address, else the `cidr_block` of the subnet of `S`; an unresolved subnet CIDR makes the clause unresolved. **"An indeterminate rule could satisfy" E5 or E6** (row 7): a rule of the side (an egress rule of a group in `SG(S)` for E5, an ingress rule of a group in `SG(D)` for E6, a rule with direction `None` for either, a rule of an `UNRESOLVED:*` pseudo-group, a rule resource that is an UNKNOWN placeholder) that is not determinate, is not unsupported, **could permit TCP/5432** (`ports.may_permit_tcp`, so an unresolved protocol or port counts) **and whose satisfying side could match**: its group sources are unresolved or could be the other side's groups, its IPv4 sources are unresolved, include a prefix list, or cover or partly cover the target, or (E6) its `self` is unresolved. **Counted:** an indeterminate rule with a resolved satisfying source and an unresolved port or protocol is counted (UNKNOWN), because the rule could supply the permission; this is the safe direction and it is the mirror of the gap of C-150 (where SEC `possible` text drops such a rule and can give PASS); here dropping it could give an unsound FAIL, so it is not dropped. When both E5 and E6 fail, row 7 applies if either failing condition could be satisfied by an indeterminate rule (registry text: "it"; the more cautious reading), then row 8. **Where the registry is silent (R5), UNSUPPORTED and listed as a spec gap:** a `vpc_id` of a group in `SG(D)`, of `S`'s subnet or of a route table that is a literal id rather than a reference to a configured `aws_vpc` (the VPC CIDR is then unknown); a literal AWS id in `vpc_security_group_ids`; `D` with neither `port` nor `engine`; a route table whose `vpc_id` is unresolved and that has an M3 candidate route or `propagating_vgws` (it may be the VPC of `D`); an unresolved or unsupported route destination or target in a route table of `VPC(D)`, a dynamic route expansion that cannot be fixed, an unsupported value of a field the path reads, an invalid `private_ip`. **Unresolved values (row 4):** an unresolved `vpc_security_group_ids`, group `vpc_id`, `subnet_id`, subnet `vpc_id` or an unresolved `D.port` (**gap:** registry row 4 names E3 and E4 but not E2; an unresolved E2 cannot be PASS, so it is UNKNOWN). **M3:** a route of a route table of `VPC(D)` whose IPv4 `cidr_block` lies inside the CIDR of that VPC and whose target is not `local` (`gateway_id = "local"` and no other target); IPv6-only routes are not read (M5); a route wider than the VPC CIDR never applies. Rows 3 and 5 FAIL only on resolved values. | Proposed (P5b) | | C-154 | P5b: assumptions, observations and the baseline list | The result's `assumptions`, sorted: `IPv4 only`, `M1: RDS security groups and subnet group share one VPC (C-15, C-77, uncited)`, `M4: default network ACL assumed (no NACL type present)`, and `tolerated type: aws_db_subnet_group (C-15)` when that type is present. Closed observation keys (present on every path): `row`, `reason`, `detail`, `endpoints`, `port`, `unresolved` (why row 4 applies), `path` (`S`, `subnet`, `vpc_s`, `sg_s`, `egress_rule`, `sg_d`, `ingress_rule`, `vpc_d`; a part that is not reached is null), `row2_causes`, `failing_conditions`, `indeterminate_rules`, `partial_coverage`, `relevant_unsupported`. `baseline.py`: the relevant-unsupported list of a created resource becomes the 26 types of registry §2.7 for INV-FUNC-001 (`core.domain.registry_v1.FUNC_RELEVANT_UNSUPPORTED`, which contains the three of the security list), so a created resource of any of them is UNSUPPORTED `type.relevant_unsupported`, not PASS with `applicable = false`; the predicate lists for INV-SEC-001/002 do not change. | Proposed (P5b) | +| C-155 | P5b: cases that registry §6 does not decide, settled conservatively here, for registry v1.1 | Implementing INV-FUNC-001 exactly as §6.3 and §6.4 left these open; each was settled by the work package's rule R5 (UNSUPPORTED, or the cautious reading) and is listed in C-152 and C-153. The authors should confirm or amend them together with C-150 in registry v1.1 (a new file under C-85, with the version bump of the invariants whose results change). **(1) Row 4 and E2.** Row 4 names E3 and E4 but not E2; an unresolved `D.port`, or an unresolved `D.engine` when there is no port, is UNKNOWN here (row 4), because an unresolved E2 cannot be a PASS and no other row fits. **(2) Row 7, "it".** When both E5 and E6 fail and an indeterminate rule could satisfy only one of them, row 7 is UNKNOWN here (the more cautious reading; the precise reading would be FAIL, since both are needed). **(3) "Could satisfy".** An indeterminate rule with a resolved satisfying side beside an unresolved port or protocol counts as one that could satisfy (UNKNOWN), unlike the SEC `possible` text of C-150, which drops it. **(4) Row 2 and an UNSUPPORTED endpoint resource.** The work package says UNKNOWN (C-152); §2.4 would call it UNSUPPORTED. **(5) Rules of unknown direction.** A rule resource whose `type` is unresolved counts as a rule of every direction: it can satisfy E5 or E6 (row 7) and makes a group that declares an explicit empty list MIXED (row 2). **(6) A pseudo-group with an unresolved target.** Its rules are determinate but may belong to a group of `SG(S)` or `SG(D)`; they count for row 7. **(7) Literal ids.** A literal AWS id as a `vpc_id`, as an entry of `vpc_security_group_ids` or as a `subnet_id` is UNSUPPORTED (the VPC CIDR or the rules of that group are not known). **(8) M1.** Groups of `D` in two VPCs, and `D` with neither `port` nor `engine`, are UNSUPPORTED. **(9) M3.** A route table whose `vpc_id` cannot be fixed, a placeholder route table, a route whose destination or target cannot be fixed, a prefix-list destination and a dynamic route expansion that cannot be fixed make the result UNSUPPORTED when they could belong to `VPC(D)`; an IPv6-only route is not read (M5); a route with no target is treated as non-local. **(10) E5 and E6 per rule.** `v4(r)` is the CIDR list of one rule, so two rules with half of the range each do not cover it; the registry text does not say that explicitly. **(11) `src_sg` of an egress rule** is read as the group named in `security_groups` or `source_security_group_id` of that egress rule (a destination group), as AWS does. **(12) `ADDR(S)`** with an unresolved `private_ip` falls back to the subnet CIDR, and an unresolved subnet CIDR leaves E6 undecidable by a CIDR (row 7). | Open (found 29 Oct 2026; P5b) |