diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index 99e30e9..507f407 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -172,7 +172,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with - _Requirements: 10.1, 10.2, 10.3, 10.4, 10.5, 10.6, 10.7_ - _Boundary: CFG Dominance_ - _Depends: 7.1_ -- [ ] 10.2 Match witness kind, scope and resource +- [x] 10.2 Match witness kind, scope and resource - Apply request-global sufficiency only when the operation fact declares it. - Return NO for definite mismatch and UNKNOWN for unresolved resource compatibility. - Done when same-resource, alias, global, mismatch and unknown fixtures match the design algebra. diff --git a/src/openultrasast/semantic/obligations/operations.py b/src/openultrasast/semantic/obligations/operations.py index df2c993..a26fd82 100644 --- a/src/openultrasast/semantic/obligations/operations.py +++ b/src/openultrasast/semantic/obligations/operations.py @@ -12,12 +12,16 @@ from __future__ import annotations import re from collections.abc import Mapping, Sequence from dataclasses import dataclass +from typing import TYPE_CHECKING from ..facts import SemanticFacts from ..ir import FileIR, FunctionIR, trailing_name from .facts import DischargerFact, ObligationFacts from .shapes import _call_matches, _constraint_provenance, _is_literal, _operations, _permissive +if TYPE_CHECKING: + from .abstract_domain import AuthorityRef, ResourceRef + SCOPES = ("decorator", "router", "statement", "hop") @@ -42,6 +46,10 @@ class Discharge: provenance: str scope: str # SCOPES detail: str = "" # identifier only: the decorator or call name that witnessed the discharge + # Requirement 2.2 (access-control-prover): the resource identity and authority a witness binds. + # None means the binding was not established (unknown), matching the abstract domain's unknown grades. + resource: ResourceRef | None = None + authority: AuthorityRef | None = None def find_operations( diff --git a/src/openultrasast/semantic/obligations/witness.py b/src/openultrasast/semantic/obligations/witness.py new file mode 100644 index 0000000..814122f --- /dev/null +++ b/src/openultrasast/semantic/obligations/witness.py @@ -0,0 +1,94 @@ +"""Witness kind, scope and resource matching (task 10.2, Reqs 2.1, 2.2, 2.5-2.7, 11.1). + +A witness governs an obligation only when every required dimension is MUST. This module +matches the kind, scope and resource dimensions; authority matching (task 10.3) and +dominance (task 10.1) join through the same algebra. Definite mismatches are NO, unresolved +compatibility is UNKNOWN (never a broad match, never a definite rejection), per Req 2.7. +""" + +from .abstract_domain import ( + EvidenceRelation, + ResourceRef, + WitnessMatch, + conjoin_dimensions, + parse_resource, +) +from .facts import OperationFact +from .operations import Discharge, Operation + +_WHOLE_HANDLER_SCOPES = frozenset({"decorator", "router"}) + + +def match_witness(witness: Discharge, operation: Operation, fact: OperationFact | None = None) -> WitnessMatch: + """Match one witness against one operation on kind, scope and resource.""" + if witness.kind not in operation.requires: + return _match(EvidenceRelation.NO, EvidenceRelation.NO, witness, operation) + if _out_of_scope(witness, operation): + return _match(EvidenceRelation.NO, EvidenceRelation.NO, witness, operation) + resource_relation = _resource_relation(witness, operation, fact) + relation = conjoin_dimensions( + (EvidenceRelation.MUST, resource_relation), + ) + return _match(relation, resource_relation, witness, operation) + + +def _out_of_scope(witness: Discharge, operation: Operation) -> bool: + same_function = (witness.path, witness.function) == (operation.path, operation.function) + if witness.scope in _WHOLE_HANDLER_SCOPES: + return not same_function + if witness.scope == "hop": + return False + return not same_function + + +def _resource_relation(witness: Discharge, operation: Operation, fact: OperationFact | None) -> EvidenceRelation: + witness_resource = witness.resource + if witness_resource is None: + return EvidenceRelation.UNKNOWN + if witness_resource.kind == "request_global": + if fact is not None and witness.kind in fact.request_global_kinds: + return EvidenceRelation.MUST + return EvidenceRelation.UNKNOWN + operation_resource = parse_resource(operation.resource) + if operation_resource.kind == "unknown": + return EvidenceRelation.UNKNOWN + if witness_resource.kind == "unknown": + return EvidenceRelation.UNKNOWN + if witness_resource.kind == "exact": + return _exact_relation(witness_resource, operation_resource) + return _alias_relation(witness_resource, operation_resource) + + +def _exact_relation(witness_resource: ResourceRef, operation_resource: ResourceRef) -> EvidenceRelation: + if operation_resource.kind == "exact": + if witness_resource.values == operation_resource.values: + return EvidenceRelation.MUST + return EvidenceRelation.NO + return _alias_relation(witness_resource, operation_resource) + + +def _alias_relation(witness_resource: ResourceRef, operation_resource: ResourceRef) -> EvidenceRelation: + if set(witness_resource.values) & set(operation_resource.values): + return EvidenceRelation.MAY + if witness_resource.kind == "exact" and operation_resource.kind == "exact": + return EvidenceRelation.NO + return EvidenceRelation.UNKNOWN + + +def _match( + relation: EvidenceRelation, + resource_relation: EvidenceRelation, + witness: Discharge, + operation: Operation, +) -> WitnessMatch: + evidence = ( + f"witness:{witness.fact_id}", + f"operation:{operation.fact_id}", + f"resource:{operation.resource or 'unknown'}", + ) + return WitnessMatch( + relation=relation, + resource_relation=resource_relation, + authority_relation=EvidenceRelation.UNKNOWN, # task 10.3 owns authority matching + evidence=evidence, + ) diff --git a/tests/test_witness_matching.py b/tests/test_witness_matching.py new file mode 100644 index 0000000..fdbeb78 --- /dev/null +++ b/tests/test_witness_matching.py @@ -0,0 +1,134 @@ +"""Witness kind, scope and resource matching (task 10.2, Reqs 2.1, 2.2, 2.5-2.7, 11.1).""" + +from openultrasast.semantic.obligations.abstract_domain import ( + UNKNOWN_RESOURCE, + EvidenceRelation, + ResourceRef, + parse_resource, +) +from openultrasast.semantic.obligations.facts import OperationFact +from openultrasast.semantic.obligations.operations import Discharge, Operation +from openultrasast.semantic.obligations.witness import match_witness + +PATH = "src/C.java" + + +def _witness( + *, + resource: ResourceRef | None = None, + kind: str = "path_guard", + scope: str = "statement", + function: str = "handle", + line: int | None = 3, +) -> Discharge: + return Discharge( + path=PATH, + line=line, + function=function, + kind=kind, + fact_id="java:authorize", + provenance="call", + scope=scope, + resource=resource, + ) + + +def _operation(*, resource: str | None = "book", requires: tuple[str, ...] = ("path_guard",)) -> Operation: + return Operation( + path=PATH, + line=4, + function="handle", + kind="protected_read", + fact_id="java:protected-read", + resource=resource, + requires=requires, + ) + + +def _fact(*, request_global_kinds: tuple[str, ...] = ("path_guard",)) -> OperationFact: + return OperationFact( + id="protected-read", + kind="protected_read", + language="java", + calls=("read",), + resource_arg=1, + requires=("path_guard",), + sensitivity="confidential", + request_global_kinds=request_global_kinds, + ) + + +def test_same_resource_exact_match_is_must() -> None: + match = match_witness(_witness(resource=parse_resource("book")), _operation(resource="book"), _fact()) + assert match.resource_relation is EvidenceRelation.MUST + assert match.relation is EvidenceRelation.MUST + assert match.authority_relation is EvidenceRelation.UNKNOWN + + +def test_definite_resource_mismatch_is_no() -> None: + match = match_witness(_witness(resource=parse_resource("volume")), _operation(resource="book"), _fact()) + assert match.resource_relation is EvidenceRelation.NO + assert match.relation is EvidenceRelation.NO + + +def test_alias_overlap_is_may() -> None: + alias_set = ResourceRef(kind="aliases", values=("book", "volume")) + match = match_witness(_witness(resource=alias_set), _operation(resource="book"), _fact()) + assert match.resource_relation is EvidenceRelation.MAY + assert match.relation is EvidenceRelation.MAY + + +def test_request_global_witness_with_declared_kind_is_must() -> None: + match = match_witness( + _witness(resource=ResourceRef(kind="request_global", values=())), + _operation(), + _fact(request_global_kinds=("path_guard",)), + ) + assert match.resource_relation is EvidenceRelation.MUST + assert match.relation is EvidenceRelation.MUST + + +def test_request_global_witness_without_declaration_is_unknown_never_no() -> None: + match = match_witness( + _witness(resource=ResourceRef(kind="request_global", values=())), + _operation(), + _fact(request_global_kinds=()), + ) + assert match.resource_relation is EvidenceRelation.UNKNOWN + assert match.relation is EvidenceRelation.UNKNOWN + without_fact = match_witness(_witness(resource=ResourceRef(kind="request_global", values=())), _operation(), None) + assert without_fact.resource_relation is EvidenceRelation.UNKNOWN + + +def test_unknown_witness_resource_is_unknown() -> None: + match = match_witness(_witness(resource=UNKNOWN_RESOURCE), _operation(resource="book"), _fact()) + assert match.resource_relation is EvidenceRelation.UNKNOWN + assert match.relation is EvidenceRelation.UNKNOWN + + +def test_unknown_operation_resource_is_unknown() -> None: + match = match_witness(_witness(resource=parse_resource("book")), _operation(resource=None), _fact()) + assert match.resource_relation is EvidenceRelation.UNKNOWN + + +def test_kind_not_required_is_no() -> None: + match = match_witness(_witness(kind="ownership_check"), _operation(requires=("path_guard",)), _fact()) + assert match.relation is EvidenceRelation.NO + + +def test_scoped_witness_on_other_function_is_no() -> None: + match = match_witness(_witness(scope="router", function="other", line=None), _operation(), _fact()) + assert match.relation is EvidenceRelation.NO + + +def test_evidence_carries_fact_ids_and_resource_tokens() -> None: + match = match_witness(_witness(resource=parse_resource("book")), _operation(resource="book"), _fact()) + assert "witness:java:authorize" in match.evidence + assert "operation:java:protected-read" in match.evidence + assert "resource:book" in match.evidence + + +def test_matching_is_deterministic() -> None: + witness = _witness(resource=parse_resource("book")) + operation = _operation(resource="book") + assert match_witness(witness, operation, _fact()) == match_witness(witness, operation, _fact())