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/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/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/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/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/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 aab6266..ebcd64a 100644 --- a/docs/DECISIONS_REGISTER.md +++ b/docs/DECISIONS_REGISTER.md @@ -162,3 +162,8 @@ 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 **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) | 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 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/func_builders.py b/tests/func_builders.py new file mode 100644 index 0000000..0089a65 --- /dev/null +++ b/tests/func_builders.py @@ -0,0 +1,124 @@ +"""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" + + +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") + + +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} + + +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/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_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 new file mode 100644 index 0000000..8d253fd --- /dev/null +++ b/tests/unit/test_reachability_predicate.py @@ -0,0 +1,859 @@ +"""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, + egress_5432, + ingress_5432, + rule, + 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 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_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() 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() 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_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_cidr_ports.py b/tests/unit/test_verification_cidr_ports.py index a0387cd..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 @@ -136,6 +137,157 @@ 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 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_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_]+)+$") 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() 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(