From f700b99637ee72c285c193f3dc6d427f3d6e7e0c Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Thu, 29 Oct 2026 19:17:37 +0100 Subject: [PATCH] feat(access-control-prover): 10.4 one judgment per path --- .kiro/specs/access-control-prover/tasks.md | 2 +- .../semantic/obligations/judgment.py | 68 ++++++++ tests/test_pair_judgment.py | 154 ++++++++++++++++++ 3 files changed, 223 insertions(+), 1 deletion(-) create mode 100644 src/openultrasast/semantic/obligations/judgment.py create mode 100644 tests/test_pair_judgment.py diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index d10acfd..d89beae 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -186,7 +186,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with - _Requirements: 2.2, 2.5, 2.7, 2.8, 11.1_ - _Boundary: Witness Matcher_ - _Depends: 7.3, 10.1_ -- [ ] 10.4 Compute one judgment per complete or diagnostic path +- [x] 10.4 Compute one judgment per complete or diagnostic path - Conjoin witness dimensions, aggregate witnesses per obligation and apply the mixed-obligation rule. - Emit discharged only for all-MUST, indeterminate for any MAY/UNKNOWN, and unguarded for at least one NO. - Done when MUST/NO, MAY/NO, UNKNOWN and empty-witness fixtures match the specified truth table. diff --git a/src/openultrasast/semantic/obligations/judgment.py b/src/openultrasast/semantic/obligations/judgment.py new file mode 100644 index 0000000..1e16050 --- /dev/null +++ b/src/openultrasast/semantic/obligations/judgment.py @@ -0,0 +1,68 @@ +"""Task 10.4 -- one judgment per path (Reqs 4.1-4.3, 11.2-11.4). + +A witness governs an obligation only when every required relation is MUST. +With complete evidence and no governing witness for a required kind the path +is unguarded; any MAY or UNKNOWN among required relations, or an incomplete +path enumeration, makes it indeterminate. Engine module: no target names. +""" + +from collections.abc import Mapping + +from .abstract_domain import ( + Completeness, + EvidenceRelation, + PairJudgment, + PathJudgment, + WitnessMatch, + aggregate_witnesses, +) +from .cfg_dominance import DominanceEvidence +from .operations import Operation + + +def judgment_for_path( + operation: Operation, + matches_by_kind: Mapping[str, tuple[tuple[WitnessMatch, DominanceEvidence], ...]], + completeness: Completeness, + *, + discovery_complete: bool = True, +) -> PathJudgment: + """Conjoin witness and dominance evidence per kind and judge the path.""" + matches = tuple(dict.fromkeys(match for pairs in matches_by_kind.values() for match, _ in pairs)) + if not completeness.is_complete: + return PathJudgment(PairJudgment.INDETERMINATE, (), completeness, matches) + relations_by_kind = {kind: _kind_relation(pairs, discovery_complete) for kind, pairs in matches_by_kind.items()} + judgment, missing = _mixed_obligation(relations_by_kind) + return PathJudgment(judgment, missing, completeness, matches) + + +def _conjoined(pair: tuple[WitnessMatch, DominanceEvidence]) -> EvidenceRelation: + match, dominance = pair + if match.relation is EvidenceRelation.NO or dominance.relation is EvidenceRelation.NO: + return EvidenceRelation.NO + if match.relation is EvidenceRelation.MUST and dominance.relation is EvidenceRelation.MUST: + return EvidenceRelation.MUST + return EvidenceRelation.UNKNOWN + + +def _kind_relation(pairs: tuple[tuple[WitnessMatch, DominanceEvidence], ...], discovery_complete: bool) -> EvidenceRelation: + if not pairs: + return EvidenceRelation.NO if discovery_complete else EvidenceRelation.UNKNOWN + return aggregate_witnesses(tuple(_conjoined(pair) for pair in pairs), discovery_complete=True) + + +def _mixed_obligation( + relations_by_kind: Mapping[str, EvidenceRelation], +) -> tuple[PairJudgment, tuple[str, ...]]: + absent_kinds = sorted(kind for kind, relation in relations_by_kind.items() if relation is EvidenceRelation.NO) + undecidable = any( + relation is not EvidenceRelation.MUST and relation is not EvidenceRelation.NO for relation in relations_by_kind.values() + ) + if undecidable: + return PairJudgment.INDETERMINATE, () + if absent_kinds: + return PairJudgment.UNGUARDED, tuple(absent_kinds) + return PairJudgment.DISCHARGED, () + + +__all__ = ["judgment_for_path"] diff --git a/tests/test_pair_judgment.py b/tests/test_pair_judgment.py new file mode 100644 index 0000000..4bf5b45 --- /dev/null +++ b/tests/test_pair_judgment.py @@ -0,0 +1,154 @@ +"""Task 10.4 -- one judgment per path (Reqs 4.1-4.3, 11.2-11.4). + +Fixtures build WitnessMatch and DominanceEvidence directly; the truth table +pinned here is the design's: a witness governs only when every dimension is +MUST; one definite NO with the rest definite makes the path unguarded; any +MAY or UNKNOWN among required relations makes it indeterminate. +""" + +import pytest + +from openultrasast.semantic.obligations.abstract_domain import ( + Completeness, + EvidenceRelation, + PairJudgment, + WitnessMatch, +) +from openultrasast.semantic.obligations.cfg_dominance import DominanceEvidence +from openultrasast.semantic.obligations.judgment import judgment_for_path +from openultrasast.semantic.obligations.operations import Operation + +PATH = "src/C.java" + + +def _operation() -> Operation: + return Operation(PATH, 4, "handle", "protected_read", "f:op", "book", ("path_guard", "ownership_check")) + + +def _match(relation: EvidenceRelation) -> WitnessMatch: + return WitnessMatch( + relation=relation, + resource_relation=EvidenceRelation.MUST, + authority_relation=EvidenceRelation.MUST, + evidence=("witness:f:guard", "operation:f:op"), + ) + + +def _dominance(relation: EvidenceRelation) -> DominanceEvidence: + return DominanceEvidence(relation=relation, guard_effect="throws") + + +def _complete() -> Completeness: + return Completeness(is_complete=True) + + +def _matches_by_kind( + path_guard: tuple[tuple[WitnessMatch, DominanceEvidence], ...], + ownership_check: tuple[tuple[WitnessMatch, DominanceEvidence], ...], +) -> dict[str, tuple[tuple[WitnessMatch, DominanceEvidence], ...]]: + return {"path_guard": path_guard, "ownership_check": ownership_check} + + +def test_must_and_no_produce_unguarded_with_missing_kind() -> None: + judgment = judgment_for_path( + _operation(), + _matches_by_kind(((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),), ()), + _complete(), + ) + assert judgment.judgment is PairJudgment.UNGUARDED + assert judgment.missing == ("ownership_check",) + + +def test_all_must_produces_discharged() -> None: + pairs = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),) + judgment = judgment_for_path(_operation(), _matches_by_kind(pairs, pairs), _complete()) + assert judgment.judgment is PairJudgment.DISCHARGED + assert judgment.missing == () + + +def test_may_and_no_produce_indeterminate() -> None: + judgment = judgment_for_path( + _operation(), + _matches_by_kind( + ((_match(EvidenceRelation.MAY), _dominance(EvidenceRelation.MUST)),), + (), + ), + _complete(), + ) + assert judgment.judgment is PairJudgment.INDETERMINATE + + +def test_unknown_match_relation_produces_indeterminate() -> None: + judgment = judgment_for_path( + _operation(), + _matches_by_kind( + ((_match(EvidenceRelation.UNKNOWN), _dominance(EvidenceRelation.MUST)),), + (), + ), + _complete(), + ) + assert judgment.judgment is PairJudgment.INDETERMINATE + + +def test_unknown_dominance_produces_indeterminate() -> None: + judgment = judgment_for_path( + _operation(), + _matches_by_kind( + ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.UNKNOWN)),), + (), + ), + _complete(), + ) + assert judgment.judgment is PairJudgment.INDETERMINATE + + +def test_empty_witnesses_with_complete_discovery_are_unguarded() -> None: + judgment = judgment_for_path(_operation(), _matches_by_kind((), ()), _complete()) + assert judgment.judgment is PairJudgment.UNGUARDED + assert judgment.missing == ("ownership_check", "path_guard") + + +def test_empty_witnesses_without_discovery_are_indeterminate() -> None: + judgment = judgment_for_path(_operation(), _matches_by_kind((), ()), _complete(), discovery_complete=False) + assert judgment.judgment is PairJudgment.INDETERMINATE + + +def test_incomplete_path_completeness_is_indeterminate() -> None: + pairs = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),) + judgment = judgment_for_path( + _operation(), + _matches_by_kind(pairs, pairs), + Completeness(is_complete=False, reasons=("resolution:no_candidate",)), + ) + assert judgment.judgment is PairJudgment.INDETERMINATE + + +def test_matches_are_carried_in_the_judgment() -> None: + must_pair = (_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)) + judgment = judgment_for_path(_operation(), _matches_by_kind((must_pair,), (must_pair,)), _complete()) + assert judgment.matches == (_match(EvidenceRelation.MUST),) + assert judgment.matches[0].evidence == ("witness:f:guard", "operation:f:op") + + +def test_judgment_is_deterministic() -> None: + pairs = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),) + first = judgment_for_path(_operation(), _matches_by_kind(pairs, ()), _complete()) + second = judgment_for_path(_operation(), _matches_by_kind(pairs, ()), _complete()) + assert first == second + + +def test_empty_requires_with_no_witnesses_is_discharged() -> None: + operation = Operation(PATH, 4, "handle", "protected_read", "f:op", "book", ()) + judgment = judgment_for_path(operation, {}, _complete()) + assert judgment.judgment is PairJudgment.DISCHARGED + + +def test_no_witness_for_one_kind_only_reports_that_kind() -> None: + must_pair = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),) + judgment = judgment_for_path(_operation(), _matches_by_kind(must_pair, ()), _complete()) + assert judgment.judgment is PairJudgment.UNGUARDED + assert judgment.missing == ("ownership_check",) + + +if __name__ == "__main__": # pragma: no cover + pytest.main([__file__, "-q"])