feat(access-control-prover): 10.3 authority matching through promoted implications

This commit is contained in:
Marius Ciepluch
2026-10-29 19:11:30 +01:00
parent cf60e02804
commit 7eb491dc82
3 changed files with 164 additions and 13 deletions
+1 -1
View File
@@ -179,7 +179,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with
- _Requirements: 2.1, 2.2, 2.5, 2.6, 2.7, 11.1_
- _Boundary: Witness Matcher_
- _Depends: 7.2, 10.1_
- [ ] 10.3 Match authority and promoted implications
- [x] 10.3 Match authority and promoted implications
- Apply only promoted authority implications and preserve their evidence.
- Return NO for insufficient authority and UNKNOWN when compatibility cannot be decided.
- Done when stronger, weaker, unrelated and unknown authorities produce the expected relations.
@@ -1,17 +1,22 @@
"""Witness kind, scope and resource matching (task 10.2, Reqs 2.1, 2.2, 2.5-2.7, 11.1).
"""Witness kind, scope, resource and authority matching (tasks 10.2-10.3, Reqs 2.1, 2.2, 2.5-2.8, 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.
matches the kind, scope, resource and authority dimensions; dominance (task 10.1) joins
through the same algebra. Definite mismatches are NO, unresolved compatibility is UNKNOWN
(never a broad match, never a definite rejection), per Req 2.7. Authority implications come
only from promoted knowledge and their fact identifiers are preserved as evidence (Req 2.8).
"""
from .abstract_domain import (
AuthorityImplication,
AuthorityRef,
EvidenceRelation,
ResourceRef,
WitnessMatch,
authority_satisfies,
conjoin_dimensions,
parse_resource,
supporting_implications,
)
from .facts import OperationFact
from .operations import Discharge, Operation
@@ -19,17 +24,25 @@ 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."""
def match_witness(
witness: Discharge,
operation: Operation,
fact: OperationFact | None = None,
*,
required_authority: AuthorityRef | None = None,
implications: tuple[AuthorityImplication, ...] = (),
) -> WitnessMatch:
"""Match one witness against one operation on kind, scope, resource and authority."""
if witness.kind not in operation.requires:
return _match(EvidenceRelation.NO, EvidenceRelation.NO, witness, operation)
return _match(EvidenceRelation.NO, EvidenceRelation.NO, EvidenceRelation.UNKNOWN, witness, operation, ())
if _out_of_scope(witness, operation):
return _match(EvidenceRelation.NO, EvidenceRelation.NO, witness, operation)
return _match(EvidenceRelation.NO, EvidenceRelation.NO, EvidenceRelation.UNKNOWN, witness, operation, ())
resource_relation = _resource_relation(witness, operation, fact)
authority_relation, implication_ids = _authority_relation(witness, required_authority, implications)
relation = conjoin_dimensions(
(EvidenceRelation.MUST, resource_relation),
(EvidenceRelation.MUST, resource_relation, authority_relation),
)
return _match(relation, resource_relation, witness, operation)
return _match(relation, resource_relation, authority_relation, witness, operation, implication_ids)
def _out_of_scope(witness: Discharge, operation: Operation) -> bool:
@@ -75,20 +88,41 @@ def _alias_relation(witness_resource: ResourceRef, operation_resource: ResourceR
return EvidenceRelation.UNKNOWN
def _authority_relation(
witness: Discharge,
required_authority: AuthorityRef | None,
implications: tuple[AuthorityImplication, ...],
) -> tuple[EvidenceRelation, tuple[str, ...]]:
"""Decide the authority dimension (Req 2.5-2.8); preserve implication fact ids."""
if required_authority is None:
return EvidenceRelation.MUST, ()
held_authority = witness.authority
if held_authority is None or held_authority.is_unknown or required_authority.is_unknown:
return EvidenceRelation.UNKNOWN, ()
relation = authority_satisfies(held_authority, required_authority, implications)
used_ids = tuple(
f"implication:{implication.id}" for implication in supporting_implications(held_authority, required_authority, implications)
)
return relation, used_ids
def _match(
relation: EvidenceRelation,
resource_relation: EvidenceRelation,
authority_relation: EvidenceRelation,
witness: Discharge,
operation: Operation,
implication_ids: tuple[str, ...],
) -> WitnessMatch:
evidence = (
f"witness:{witness.fact_id}",
f"operation:{operation.fact_id}",
f"resource:{operation.resource or 'unknown'}",
*implication_ids,
)
return WitnessMatch(
relation=relation,
resource_relation=resource_relation,
authority_relation=EvidenceRelation.UNKNOWN, # task 10.3 owns authority matching
authority_relation=authority_relation,
evidence=evidence,
)
+118 -1
View File
@@ -2,6 +2,7 @@
from openultrasast.semantic.obligations.abstract_domain import (
UNKNOWN_RESOURCE,
AuthorityRef,
EvidenceRelation,
ResourceRef,
parse_resource,
@@ -20,6 +21,7 @@ def _witness(
scope: str = "statement",
function: str = "handle",
line: int | None = 3,
authority: AuthorityRef | None = None,
) -> Discharge:
return Discharge(
path=PATH,
@@ -30,6 +32,7 @@ def _witness(
provenance="call",
scope=scope,
resource=resource,
authority=authority,
)
@@ -62,7 +65,7 @@ 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
assert match.authority_relation is EvidenceRelation.MUST # no authority obligation: vacuous MUST (10.3)
def test_definite_resource_mismatch_is_no() -> None:
@@ -132,3 +135,117 @@ 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())
# --- Task 10.3: authority matching through promoted implications (Reqs 2.2, 2.5, 2.7, 2.8, 11.1) ---
def _authority_witness(authority: AuthorityRef | None) -> Discharge:
return _witness(resource=ResourceRef(kind="exact", values=("book",)), authority=authority)
def test_stronger_authority_via_promoted_implication_is_must_and_keeps_fact_id() -> None:
from openultrasast.semantic.obligations.abstract_domain import AuthorityImplication, AuthorityRef
witness = _authority_witness(AuthorityRef(values=("admin",)))
required = AuthorityRef(values=("supervisor",))
implications = (AuthorityImplication(id="php:admin-implies-supervisor", authority="admin", implies="supervisor"),)
match = match_witness(
witness,
_operation(),
required_authority=required,
implications=implications,
)
assert match.authority_relation is EvidenceRelation.MUST
assert "implication:php:admin-implies-supervisor" in match.evidence
def test_identity_authority_is_must() -> None:
from openultrasast.semantic.obligations.abstract_domain import AuthorityRef
match = match_witness(
_authority_witness(AuthorityRef(values=("admin",))),
_operation(),
required_authority=AuthorityRef(values=("admin",)),
)
assert match.authority_relation is EvidenceRelation.MUST
def test_weaker_authority_is_no() -> None:
from openultrasast.semantic.obligations.abstract_domain import AuthorityRef
match = match_witness(
_authority_witness(AuthorityRef(values=("user",))),
_operation(),
required_authority=AuthorityRef(values=("admin",)),
)
assert match.authority_relation is EvidenceRelation.NO
def test_unrelated_authority_is_no() -> None:
from openultrasast.semantic.obligations.abstract_domain import AuthorityRef
match = match_witness(
_authority_witness(AuthorityRef(values=("auditor",))),
_operation(),
required_authority=AuthorityRef(values=("admin",)),
)
assert match.authority_relation is EvidenceRelation.NO
def test_unknown_witness_authority_is_unknown() -> None:
from openultrasast.semantic.obligations.abstract_domain import AuthorityRef
match = match_witness(
_authority_witness(None),
_operation(),
required_authority=AuthorityRef(values=("admin",)),
)
assert match.authority_relation is EvidenceRelation.UNKNOWN
def test_unknown_required_authority_is_unknown() -> None:
from openultrasast.semantic.obligations.abstract_domain import AuthorityRef
match = match_witness(
_authority_witness(AuthorityRef(values=("admin",))),
_operation(),
required_authority=AuthorityRef(values=(), is_unknown=True),
)
assert match.authority_relation is EvidenceRelation.UNKNOWN
def test_multi_value_requirement_is_may_never_must() -> None:
from openultrasast.semantic.obligations.abstract_domain import AuthorityRef
match = match_witness(
_authority_witness(AuthorityRef(values=("admin",))),
_operation(),
required_authority=AuthorityRef(values=("admin", "guest")),
)
assert match.authority_relation is EvidenceRelation.MAY
def test_no_authority_requirement_is_vacuous_must() -> None:
from openultrasast.semantic.obligations.abstract_domain import AuthorityRef
match = match_witness(
_authority_witness(AuthorityRef(values=("admin",))),
_operation(),
required_authority=None,
)
assert match.authority_relation is EvidenceRelation.MUST
def test_overall_relation_conjoins_authority() -> None:
from openultrasast.semantic.obligations.abstract_domain import AuthorityRef
witness = _authority_witness(AuthorityRef(values=("user",)))
match = match_witness(
witness,
_operation(),
required_authority=AuthorityRef(values=("admin",)),
)
assert match.resource_relation is EvidenceRelation.MUST
assert match.authority_relation is EvidenceRelation.NO
assert match.relation is EvidenceRelation.NO