From 03807f4ddd42b639b120f5165da2317d3fe3adbb Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Thu, 29 Oct 2026 15:23:43 +0100 Subject: [PATCH] feat(access-control-prover): task 7.4 - judgment, trace and coverage contracts with abstract state --- .kiro/specs/access-control-prover/tasks.md | 2 +- src/openultrasast/hunt/prover.py | 5 + .../semantic/obligations/abstract_domain.py | 86 +++++- .../semantic/obligations/trace.py | 99 ++++++- tests/test_obligation_judgment.py | 259 ++++++++++++++++++ 5 files changed, 444 insertions(+), 7 deletions(-) create mode 100644 tests/test_obligation_judgment.py diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index 4277649..376ec94 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -101,7 +101,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with - _Requirements: 2.1, 2.2, 2.5, 2.7, 2.8, 11.1_ - _Boundary: Authority Domain_ - _Depends: 7.1_ -- [ ] 7.4 Extend judgment, trace and coverage contracts with abstract state +- [x] 7.4 Extend judgment, trace and coverage contracts with abstract state - Add three-way judgments, completeness and evidence relations without changing legacy defaults. - Add canonical serialization for resource and authority relations and all incompleteness reasons. - Done when old trace fixtures remain stable in legacy mode and new fixtures round-trip all abstract fields. diff --git a/src/openultrasast/hunt/prover.py b/src/openultrasast/hunt/prover.py index 69cb782..cd2bccd 100644 --- a/src/openultrasast/hunt/prover.py +++ b/src/openultrasast/hunt/prover.py @@ -15,6 +15,7 @@ from ..semantic.cfg import ControlContext, FunctionCfg from ..semantic.cst import parse_function_nodes from ..semantic.facts import load_facts from ..semantic.ir import FileIR, FunctionIR, trailing_name +from ..semantic.obligations.abstract_domain import PairJudgmentCounts from ..semantic.obligations.cfg_dominance import CfgDominance from ..semantic.obligations.check import _on_caller_hop, _relevant, _route_path, check_obligations from ..semantic.obligations.enforcement import witnesses @@ -36,6 +37,10 @@ class Coverage: operations_checked: int operations_discharged: int unchecked_by_reason: dict[str, int] + # Requirement 7.1/7.6 (access-control-prover): three-way pair judgment totals, additive and zero + # until the prover opts into abstract judgment (task 10.6). Indeterminate pairs are counted + # neither clean nor discharged. + pair_judgments: PairJudgmentCounts = PairJudgmentCounts() @dataclass(frozen=True) diff --git a/src/openultrasast/semantic/obligations/abstract_domain.py b/src/openultrasast/semantic/obligations/abstract_domain.py index b6e57ba..2d41f70 100644 --- a/src/openultrasast/semantic/obligations/abstract_domain.py +++ b/src/openultrasast/semantic/obligations/abstract_domain.py @@ -1,6 +1,6 @@ """Evidence relations, the completeness value, resource and authority abstract values (access-control-prover). -Covers Req 2.1, 2.2, 2.5, 2.6, 2.7, 2.8, 11.1, 11.6, 11.7. +Covers Req 2.1, 2.2, 2.5, 2.6, 2.7, 2.8, 7.1, 7.2, 7.5, 7.6, 9.1, 9.2, 9.6, 11.1, 11.6, 11.7. ``EvidenceRelation`` is the abstract evidence domain: definite presence (``MUST``), definite absence (``NO``), possibility (``MAY``) and unknown (``UNKNOWN``). Three separate operations keep one table @@ -22,7 +22,7 @@ operation is deterministic, pure and independent of target names; join never con from __future__ import annotations -from collections import deque +from collections import Counter, deque from collections.abc import Iterable, Mapping, Sequence from dataclasses import dataclass from enum import Enum @@ -37,6 +37,18 @@ class EvidenceRelation(Enum): UNKNOWN = "unknown" +class PairJudgment(Enum): + """The three-way judgment of one examined pair (design, "Abstract evidence domain"; Req 4.1-4.3, 9.2). + + Degraded evidence can reduce a pair to ``INDETERMINATE`` but can never manufacture + ``UNGUARDED`` or ``DISCHARGED``. + """ + + UNGUARDED = "unguarded" + DISCHARGED = "discharged" + INDETERMINATE = "indeterminate" + + @dataclass(frozen=True) class Completeness: """What the analysis could not decide; reasons are stage-prefixed strings, deduplicated in order. @@ -352,3 +364,73 @@ def join_completeness(left: Completeness, right: Completeness) -> Completeness: is_complete=left.is_complete and right.is_complete, reasons=left.reasons + right.reasons, ) + + +@dataclass(frozen=True) +class WitnessMatch: + """One witness's match relations for one obligation (design, "Witness matching and judgment"; Req 9.1). + + ``relation`` is the conjoined kind/scope/dominance verdict, ``resource_relation`` and + ``authority_relation`` are the resource and authority compatibility relations, and ``evidence`` + names the supporting fact identifiers (for example the authority implications used, Req 2.8). + """ + + relation: EvidenceRelation + resource_relation: EvidenceRelation + authority_relation: EvidenceRelation + evidence: tuple[str, ...] + + +@dataclass(frozen=True) +class PathJudgment: + """The abstract judgment of one examined path (design, "Witness matching and judgment"; Req 9.1, 11.4). + + ``missing`` names every required obligation with no governing witness; ``completeness`` carries + each incompleteness reason of the path (Req 7.5) and ``matches`` holds one row per witness + examined. Computing these values is task 10.4; this is the contract they must fill. + """ + + judgment: PairJudgment + missing: tuple[str, ...] + completeness: Completeness + matches: tuple[WitnessMatch, ...] + + +@dataclass(frozen=True) +class PairJudgmentCounts: + """Pair judgment totals for failure-visible coverage (Req 7.1, 7.6). + + ``indeterminate`` is a first-class count: an indeterminate pair is included in neither + ``unguarded`` nor ``discharged``, so a degraded instrument cannot read as a clean bill of health. + """ + + unguarded: int = 0 + discharged: int = 0 + indeterminate: int = 0 + + def examined(self) -> int: + """Examined pairs overall; the indeterminate rate is reported against this total (Req 7.6).""" + return self.unguarded + self.discharged + self.indeterminate + + +def count_pair_judgments(judgments: Iterable[PairJudgment]) -> PairJudgmentCounts: + """Count the three pair judgments separately over one examined population (Req 7.1, 7.6).""" + counts = Counter(judgments) + return PairJudgmentCounts( + unguarded=counts[PairJudgment.UNGUARDED], + discharged=counts[PairJudgment.DISCHARGED], + indeterminate=counts[PairJudgment.INDETERMINATE], + ) + + +def reason_counts(completeness_values: Iterable[Completeness]) -> dict[str, int]: + """Aggregate every incompleteness reason across examined pairs (Req 7.2, 7.5). + + Each pair contributes one count per distinct reason (``Completeness`` already deduplicates within + one value), so a reason two pairs share counts twice and no pair's reason is lost. Keys are + sorted, so the aggregate is deterministic however the pairs were ordered. + """ + counts: Counter[str] = Counter() + for value in completeness_values: + counts.update(value.reasons) + return dict(sorted(counts.items())) diff --git a/src/openultrasast/semantic/obligations/trace.py b/src/openultrasast/semantic/obligations/trace.py index 768bf32..e411c12 100644 --- a/src/openultrasast/semantic/obligations/trace.py +++ b/src/openultrasast/semantic/obligations/trace.py @@ -7,10 +7,20 @@ import json import re from collections.abc import Mapping, Sequence from dataclasses import asdict, dataclass, replace +from enum import Enum from typing import Any from ..cfg import ControlContext from ..ir import FileIR, FunctionIR, trailing_name +from .abstract_domain import ( + AuthorityRef, + Completeness, + EvidenceRelation, + PairJudgment, + PathJudgment, + ResourceRef, + WitnessMatch, +) from .cfg_dominance import describe, operation_context from .dominance import Dominance from .facts import ObligationFacts @@ -38,6 +48,73 @@ class Hop: forwarded: tuple[str, ...] +@dataclass(frozen=True) +class AbstractTraceState: + """The abstract evidence a prover-mode trace carries beyond the legacy verdict (Req 9.1, 9.2, 9.6). + + ``path_judgment`` is the three-way judgment with its missing kinds, every incompleteness reason + and the per-witness match relations; ``resource`` and ``authority`` are the operation's abstract + values and ``resource_relation``/``authority_relation`` the pair-level compatibility relations. + The state is absent from legacy traces, which stay byte-stable (task 7.4). + """ + + path_judgment: PathJudgment + resource: ResourceRef + authority: AuthorityRef + resource_relation: EvidenceRelation + authority_relation: EvidenceRelation + + +def _enum_json_value(value: Any) -> str: + """The canonical JSON encoding of a relation or judgment: its value string.""" + if isinstance(value, Enum): + return str(value.value) + raise TypeError(f"not canonically serializable: {type(value).__name__}") + + +def _parse_path_judgment(payload: Mapping[str, Any]) -> PathJudgment: + """Rebuild one ``PathJudgment`` from its canonical JSON (round-trip half of Req 9.5).""" + completeness_payload = payload["completeness"] + return PathJudgment( + judgment=PairJudgment(payload["judgment"]), + missing=tuple(payload["missing"]), + completeness=Completeness( + is_complete=bool(completeness_payload["is_complete"]), + reasons=tuple(completeness_payload["reasons"]), + ), + matches=tuple( + WitnessMatch( + relation=EvidenceRelation(match["relation"]), + resource_relation=EvidenceRelation(match["resource_relation"]), + authority_relation=EvidenceRelation(match["authority_relation"]), + evidence=tuple(match["evidence"]), + ) + for match in payload["matches"] + ), + ) + + +def parse_abstract_state(payload: Mapping[str, Any]) -> AbstractTraceState: + """Rebuild the abstract trace state from its canonical JSON record. + + The inverse of the canonical encoding: value strings name relations and judgments again, field + dicts become ``ResourceRef``/``AuthorityRef`` values and every incompleteness reason is kept. + Anything outside the closed vocabularies fails loud rather than degrading to a quieter value. + """ + resource_payload = payload["resource"] + authority_payload = payload["authority"] + return AbstractTraceState( + path_judgment=_parse_path_judgment(payload["path_judgment"]), + resource=ResourceRef(kind=resource_payload["kind"], values=tuple(resource_payload["values"])), + authority=AuthorityRef( + values=tuple(authority_payload["values"]), + is_unknown=bool(authority_payload["is_unknown"]), + ), + resource_relation=EvidenceRelation(payload["resource_relation"]), + authority_relation=EvidenceRelation(payload["authority_relation"]), + ) + + @dataclass(frozen=True) class Trace: entry_kind: str @@ -54,14 +131,24 @@ class Trace: dominating: tuple[str, ...] missing: str | None operation_context: ControlContext = ControlContext() + # Opt-in abstract evidence (task 7.4): absent (None) in legacy mode, so legacy serialization is + # byte-stable; set only by the prover's abstract judgment path (task 10.6). + abstract_state: AbstractTraceState | None = None def record(self) -> dict[str, Any]: - """Return JSON values with keys sorted recursively, retaining sequence order.""" - result: dict[str, Any] = json.loads(json.dumps(asdict(self), sort_keys=True)) - return result + """Return JSON values with keys sorted recursively, retaining sequence order. + + The abstract state is omitted entirely when unset, so a legacy trace's record keeps its exact + historical shape; when set, relations and judgments encode as their value strings. + """ + payload = asdict(self) + if payload["abstract_state"] is None: + del payload["abstract_state"] + record: dict[str, Any] = json.loads(json.dumps(payload, sort_keys=True, default=_enum_json_value)) + return record def text(self) -> str: - """Emit entry, hops, operation, later guards and verdict in that order.""" + """Emit entry, hops, operation, later guards, verdict and, when present, the abstract state.""" record = self.record() components = [("entry", {key: record[key] for key in ("entry_kind", "boundary", "access", "parameters")})] components.extend(("hop", hop) for hop in record["hops"]) @@ -69,6 +156,8 @@ class Trace: components.append(("operation", {key: record[key] for key in operation_keys})) components.extend(("guard_after", guard) for guard in record["guards_after"]) components.append(("verdict", {key: record[key] for key in ("requires", "dominating", "missing")})) + if "abstract_state" in record: + components.append(("abstract", record["abstract_state"])) return "\n".join(f"{label} {json.dumps(value, sort_keys=True, separators=(',', ':'))}" for label, value in components) @@ -168,6 +257,7 @@ def build_trace( dominating: tuple[str, ...], missing: str | None, access: str | None = None, + abstract_state: AbstractTraceState | None = None, ) -> Trace: """Build one trace without changing the checker's verdict or coverage.""" texts = {file: text for file, (_, text) in irs.items()} @@ -244,4 +334,5 @@ def build_trace( tuple(sorted(dominating)), missing, operation_context(dominance, operation), + abstract_state, ) diff --git a/tests/test_obligation_judgment.py b/tests/test_obligation_judgment.py new file mode 100644 index 0000000..98c3e42 --- /dev/null +++ b/tests/test_obligation_judgment.py @@ -0,0 +1,259 @@ +"""access-control-prover task 7.4: judgment, trace and coverage contracts with abstract state (offline). + +Three-way pair judgments, completeness and evidence relations as contracts, and their canonical +serialization, per the design's "Abstract evidence domain" and "Witness matching and judgment" +sections and Req 7.1, 7.2, 7.5, 7.6, 9.1, 9.2, 9.6. Legacy trace and coverage shapes stay byte-stable +unless the caller opts into the abstract state. +""" + +from __future__ import annotations + +import json +from types import SimpleNamespace +from typing import TYPE_CHECKING + +from openultrasast.semantic.ir import parse_python_ast +from openultrasast.semantic.obligations.dominance import OrderDominance +from openultrasast.semantic.obligations.facts import ObligationFacts, OperationFact +from openultrasast.semantic.obligations.operations import Operation +from openultrasast.semantic.obligations.paths import PathRecord +from openultrasast.semantic.obligations.trace import build_trace + +if TYPE_CHECKING: + from openultrasast.semantic.obligations.trace import AbstractTraceState, Trace + +_LEGACY_TRACE_KEYS = { + "entry_kind", + "boundary", + "access", + "parameters", + "hops", + "operation_kind", + "fact_id", + "operation_line", + "arguments", + "guards_after", + "requires", + "dominating", + "missing", + "operation_context", +} + + +def _abstract_state() -> AbstractTraceState: + from openultrasast.semantic.obligations.abstract_domain import ( + AuthorityRef, + Completeness, + EvidenceRelation, + PairJudgment, + PathJudgment, + ResourceRef, + WitnessMatch, + ) + from openultrasast.semantic.obligations.trace import AbstractTraceState + + return AbstractTraceState( + path_judgment=PathJudgment( + judgment=PairJudgment.UNGUARDED, + missing=("path_guard",), + completeness=Completeness( + False, + ("resolution:ambiguous_call", "matching:unknown_resource", "matching:unknown_authority"), + ), + matches=(WitnessMatch(EvidenceRelation.MUST, EvidenceRelation.MAY, EvidenceRelation.NO, ("implication:admin_role",)),), + ), + resource=ResourceRef(kind="exact", values=("doc:1",)), + authority=AuthorityRef(values=("admin",)), + resource_relation=EvidenceRelation.MAY, + authority_relation=EvidenceRelation.UNKNOWN, + ) + + +def _trace(abstract_state: AbstractTraceState | None = None) -> Trace: + from openultrasast.semantic.obligations.trace import Trace + + return Trace( + entry_kind="route", + boundary="http_request", + access="unknown", + parameters=("item",), + hops=(), + operation_kind="protected_read", + fact_id="read", + operation_line=2, + arguments=(("item", "request_input"),), + guards_after=(), + requires=("path_guard",), + dominating=(), + missing=None, + abstract_state=abstract_state, + ) + + +def test_pair_judgment_is_exactly_the_three_way_vocabulary() -> None: + # Req 4.1-4.3 vocabulary: a pair is unguarded, discharged or indeterminate (design, PairJudgment). + from openultrasast.semantic.obligations.abstract_domain import PairJudgment + + assert [judgment.value for judgment in PairJudgment] == ["unguarded", "discharged", "indeterminate"] + + +def test_witness_match_and_path_judgment_carry_the_design_fields() -> None: + from openultrasast.semantic.obligations.abstract_domain import ( + Completeness, + EvidenceRelation, + PairJudgment, + PathJudgment, + WitnessMatch, + ) + + match = WitnessMatch(EvidenceRelation.MUST, EvidenceRelation.NO, EvidenceRelation.MAY, ("witness:guard",)) + judgment = PathJudgment(PairJudgment.DISCHARGED, (), Completeness(True), (match,)) + assert (judgment.judgment, judgment.missing, judgment.matches) == (PairJudgment.DISCHARGED, (), (match,)) + assert judgment.completeness == Completeness(True) + assert hash(judgment) == hash(PathJudgment(PairJudgment.DISCHARGED, (), Completeness(True), (match,))) + + +def test_count_pair_judgments_reports_each_way_separately() -> None: + # Req 7.1, 7.6: unguarded, discharged and indeterminate pairs are counted separately; an + # indeterminate pair is included in neither the unguarded nor the discharged count. + from openultrasast.semantic.obligations.abstract_domain import PairJudgment, PairJudgmentCounts, count_pair_judgments + + counts = count_pair_judgments([PairJudgment.UNGUARDED, PairJudgment.INDETERMINATE, PairJudgment.INDETERMINATE, PairJudgment.DISCHARGED]) + assert counts == PairJudgmentCounts(unguarded=1, discharged=1, indeterminate=2) + assert counts.examined() == 4 + assert count_pair_judgments([]) == PairJudgmentCounts() + + +def test_reason_counts_aggregates_every_reason_by_pair() -> None: + # Req 7.2, 7.5: every incompleteness reason is preserved once per pair and aggregated in coverage. + from openultrasast.semantic.obligations.abstract_domain import Completeness, reason_counts + + counts = reason_counts( + [ + Completeness(False, ("resolution:ambiguous_call", "matching:unknown_resource")), + Completeness(False, ("resolution:ambiguous_call", "dominance:cfg_unavailable")), + Completeness(True), + ] + ) + assert counts == {"resolution:ambiguous_call": 2, "dominance:cfg_unavailable": 1, "matching:unknown_resource": 1} + assert list(counts) == sorted(counts) + + +def test_legacy_trace_omits_abstract_state_from_record_and_text() -> None: + record = _trace().record() + assert "abstract_state" not in record + assert set(record) == _LEGACY_TRACE_KEYS + assert json.loads(json.dumps(record)) == record + text = _trace().text() + assert [line.split(" ", 1)[0] for line in text.splitlines()] == ["entry", "operation", "verdict"] + assert _trace().record() == record and _trace().text() == text + + +def test_abstract_state_round_trips_all_fields_through_canonical_json() -> None: + from openultrasast.semantic.obligations.trace import parse_abstract_state + + state = _abstract_state() + record = _trace(abstract_state=state).record() + assert json.loads(json.dumps(record)) == record + assert parse_abstract_state(record["abstract_state"]) == state + assert _trace(abstract_state=state).record() == record + + +def test_canonical_value_encoding_names_every_domain_value_stably() -> None: + # EvidenceRelation and PairJudgment encode as their value strings; ResourceRef, AuthorityRef and + # Completeness encode as sorted field dicts, so the canonical form is deterministic (Req 9.5). + payload = _trace(abstract_state=_abstract_state()).record()["abstract_state"] + assert list(payload) == sorted(payload) + assert payload["path_judgment"]["judgment"] == "unguarded" + assert payload["path_judgment"]["completeness"] == { + "is_complete": False, + "reasons": ["resolution:ambiguous_call", "matching:unknown_resource", "matching:unknown_authority"], + } + assert payload["path_judgment"]["matches"] == [ + {"authority_relation": "no", "evidence": ["implication:admin_role"], "relation": "must", "resource_relation": "may"} + ] + assert payload["resource"] == {"kind": "exact", "values": ["doc:1"]} + assert payload["authority"] == {"is_unknown": False, "values": ["admin"]} + assert payload["resource_relation"] == "may" + assert payload["authority_relation"] == "unknown" + + +def test_abstract_text_appends_one_deterministic_abstract_component() -> None: + legacy = _trace().text() + extended = _trace(abstract_state=_abstract_state()).text() + assert extended.startswith(legacy) + lines = extended.splitlines() + assert lines[-1].startswith("abstract ") + assert json.loads(lines[-1][len("abstract ") :]) == _trace(abstract_state=_abstract_state()).record()["abstract_state"] + assert extended == _trace(abstract_state=_abstract_state()).text() + + +def test_every_incompleteness_reason_survives_the_round_trip() -> None: + # Req 7.2's reason vocabulary, including unknown resource and unknown authority, is preserved in + # the trace (Req 7.5, 9.6) rather than folded into a quieter summary. + from dataclasses import replace + + from openultrasast.semantic.obligations.abstract_domain import Completeness + from openultrasast.semantic.obligations.trace import parse_abstract_state + + reasons = ( + "recognition:framework_unrecognised", + "resolution:unresolved_call", + "resolution:ambiguous_call", + "summary:exploration_cutoff", + "dominance:cfg_unavailable", + "matching:unknown_resource", + "matching:unknown_authority", + "judgment:analysis_exception", + ) + state = _abstract_state() + state = replace(state, path_judgment=replace(state.path_judgment, completeness=Completeness(False, reasons))) + parsed = parse_abstract_state(_trace(abstract_state=state).record()["abstract_state"]) + assert parsed.path_judgment.completeness.reasons == reasons + assert parsed.path_judgment.completeness.is_complete is False + + +def test_parse_abstract_state_rejects_unknown_judgment_values() -> None: + import pytest + + from openultrasast.semantic.obligations.trace import parse_abstract_state + + payload = _trace(abstract_state=_abstract_state()).record()["abstract_state"] + payload["path_judgment"]["judgment"] = "probably_fine" + with pytest.raises(ValueError): + parse_abstract_state(payload) + + +def test_build_trace_carries_abstract_state_as_an_opt_in_argument() -> None: + text = "def entry(item):\n read(item)\n" + ir = parse_python_ast("app.py", text) + facts = ObligationFacts("1", (OperationFact("read", "protected_read", "python", ("read",), None, ("path_guard",), "high"),), ()) + result = build_trace( + path=PathRecord((("app.py::entry", None),), "app.py::entry", True), + entry=SimpleNamespace(kind="route", trust_boundary="http_request", access_level="unknown"), + operation=Operation("app.py", 2, "entry", "protected_read", "read", None, ("path_guard",)), + irs={"app.py": (ir, text)}, + facts=facts, + witnesses=(), + dominance=OrderDominance({"app.py": text}), + dominating=(), + missing="path_guard", + abstract_state=_abstract_state(), + ) + assert result.abstract_state == _abstract_state() + assert result.record()["abstract_state"]["path_judgment"]["judgment"] == "unguarded" + + +def test_coverage_counts_pair_judgments_without_changing_legacy_fields() -> None: + # Req 7.1, 7.6: the coverage contract gains the three pair judgment counts additively; the + # legacy constructor call and fields stay valid and the record stays pure JSON. + from dataclasses import asdict + + from openultrasast.hunt.prover import Coverage + from openultrasast.semantic.obligations.abstract_domain import PairJudgmentCounts + + coverage = Coverage({"python": 1}, {}, 1, 1, 0, 1, 1, {"parse_failed": 1}) + assert coverage.pair_judgments == PairJudgmentCounts() + serialized = asdict(coverage) + assert json.loads(json.dumps(serialized)) == serialized + assert serialized["pair_judgments"] == {"unguarded": 0, "discharged": 0, "indeterminate": 0}