diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index f8f9164..9aa3491 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -87,7 +87,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with - Done when exhaustive table tests and algebraic law tests pass for every relation pair. - _Requirements: 11.1, 11.6, 11.7_ - _Boundary: Abstract Evidence Domain_ -- [ ] 7.2 Add resource abstract values and operation-fact fields +- [x] 7.2 Add resource abstract values and operation-fact fields - Represent exact resources, finite alias sets, request-global scope and unknown resources. - Extend operation facts to state when a request-global guard is sufficient. - Done when resource parsing and joins distinguish exact, alias, global and unknown fixtures. diff --git a/src/openultrasast/semantic/obligations/abstract_domain.py b/src/openultrasast/semantic/obligations/abstract_domain.py index 2245431..51fb895 100644 --- a/src/openultrasast/semantic/obligations/abstract_domain.py +++ b/src/openultrasast/semantic/obligations/abstract_domain.py @@ -1,19 +1,25 @@ -"""Evidence relations and the completeness value (access-control-prover, Req 11.1, 11.6, 11.7). +"""Evidence relations, the completeness value and resource abstract values (access-control-prover). + +Covers Req 2.1, 2.5, 2.6, 2.7, 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 from being used for the wrong quantifier: ``join_alternatives`` merges evidence from alternative call targets or control paths, ``conjoin_dimensions`` combines one witness's kind, scope, resource, authority and dominance dimensions, and ``aggregate_witnesses`` asks whether any witness definitely governs one -obligation. Every operation is deterministic, pure and independent of target names; join never converts +obligation. ``ResourceRef`` abstracts one resource binding into an exact token, a finite alias set, +request-global scope or an unknown value; ``join_resources`` unions alias sets finitely, lets +request-global scope absorb concrete bindings and never lets an unresolvable value resolve. Every +operation is deterministic, pure and independent of target names; join never converts ``MAY`` or ``UNKNOWN`` into ``MUST`` or ``NO``, so losing precision cannot manufacture a verdict. """ from __future__ import annotations -from collections.abc import Iterable, Mapping +from collections.abc import Iterable, Mapping, Sequence from dataclasses import dataclass from enum import Enum +from typing import Literal class EvidenceRelation(Enum): @@ -38,6 +44,70 @@ class Completeness: object.__setattr__(self, "reasons", tuple(dict.fromkeys(self.reasons))) +_RESOURCE_KINDS = ("exact", "aliases", "request_global", "unknown") + + +@dataclass(frozen=True) +class ResourceRef: + """The abstract value of one resource binding (design, "Abstract evidence domain"; Req 2.1, 2.5, 2.6, 2.7, 11.1). + + ``exact`` binds one named resource, ``aliases`` binds a finite set of them, ``request_global`` binds the + whole request without resource equality, and ``unknown`` is an unresolvable or unbounded binding. Values + are deduplicated and sorted, so equal bindings are equal however they were constructed; a misshapen kind + or arity fails loud rather than degrading silently. + """ + + kind: Literal["exact", "aliases", "request_global", "unknown"] + values: tuple[str, ...] = () + + def __post_init__(self) -> None: + if self.kind not in _RESOURCE_KINDS: + raise ValueError(f"unknown resource kind: {self.kind!r}") + tokens = sorted(set(self.values)) + if self.kind == "exact" and len(tokens) != 1: + raise ValueError(f"exact resource needs exactly one token: {self.values!r}") + if self.kind == "aliases" and not tokens: + raise ValueError("alias set needs at least one token") + if self.kind in ("request_global", "unknown") and tokens: + raise ValueError(f"{self.kind} resource binds no tokens: {self.values!r}") + object.__setattr__(self, "values", tuple(tokens)) + + +REQUEST_GLOBAL_RESOURCE = ResourceRef(kind="request_global") +UNKNOWN_RESOURCE = ResourceRef(kind="unknown") + + +def parse_resource(binding: str | Sequence[str] | None) -> ResourceRef: + """Parse one resource binding from fact or IR evidence into its abstract value. + + A single identifier token is ``exact``, a finite token collection is a finite alias set, and ``None`` + (no binding could be resolved) is ``unknown``; anything misshapen raises instead of quietly degrading. + """ + if binding is None: + return UNKNOWN_RESOURCE + tokens = (binding,) if isinstance(binding, str) else tuple(binding) + if not tokens or not all(isinstance(token, str) and token for token in tokens): + raise ValueError(f"misshapen resource binding: {binding!r}") + kind: Literal["exact", "aliases"] = "exact" if isinstance(binding, str) else "aliases" + return ResourceRef(kind=kind, values=tokens) + + +def join_resources(left: ResourceRef, right: ResourceRef) -> ResourceRef: + """Join resource bindings from alternative paths or call targets. + + Alias sets join by finite union and identical exact tokens stay exact; request-global scope absorbs any + concrete binding because it already covers every resource in the request (Req 2.6), and an unbounded or + unresolvable value joins to ``unknown`` so losing precision cannot manufacture an exact match (Req 2.7, 11.1). + """ + if left.kind == "unknown" or right.kind == "unknown": + return UNKNOWN_RESOURCE + if left.kind == "request_global" or right.kind == "request_global": + return REQUEST_GLOBAL_RESOURCE + if left.kind == right.kind == "exact" and left.values == right.values: + return left + return ResourceRef(kind="aliases", values=left.values + right.values) + + _ALTERNATIVE_JOIN: Mapping[tuple[EvidenceRelation, EvidenceRelation], EvidenceRelation] = { (EvidenceRelation.MUST, EvidenceRelation.MUST): EvidenceRelation.MUST, (EvidenceRelation.MUST, EvidenceRelation.NO): EvidenceRelation.MAY, diff --git a/src/openultrasast/semantic/obligations/facts.py b/src/openultrasast/semantic/obligations/facts.py index 4a37965..48100e6 100644 --- a/src/openultrasast/semantic/obligations/facts.py +++ b/src/openultrasast/semantic/obligations/facts.py @@ -22,7 +22,18 @@ SENSITIVITIES = ("low", "medium", "high") DEFAULT_OBLIGATION_FACTS_DIR = Path(__file__).resolve().parents[2] / "ruleset" / "obligations" _OPERATION_FIELDS = frozenset( - {"id", "kind", "calls", "resource_arg", "requires", "sensitivity", "query_document_arg", "handlers", "framework"} + { + "id", + "kind", + "calls", + "resource_arg", + "requires", + "sensitivity", + "query_document_arg", + "handlers", + "framework", + "request_global_kinds", + } ) _DISCHARGER_FIELDS = frozenset( {"id", "kind", "calls", "decorators", "identity_sources", "constraint_params", "request_sources", "permissive_values"} @@ -50,6 +61,9 @@ class OperationFact: query_document_arg: int | None = None handlers: tuple[str, ...] = () framework: str | None = None + # Requirement 2.6 (access-control-prover): discharger kinds a request-global witness may discharge for + # this operation at request scope, without resource equality. Declared by the fact, never inferred. + request_global_kinds: tuple[str, ...] = () @dataclass(frozen=True) @@ -97,48 +111,7 @@ def _load_obligation_facts_uncached(directory: Path | None = None) -> Obligation language = str(payload.get("language") or path.stem) versions.append(str(payload.get("version", "1"))) for row in _rows(payload.get("operation"), path): - _only_fields(row, _OPERATION_FIELDS, path) - kind = str(row.get("kind", "")) - if kind not in OPERATION_KINDS: - raise ObligationFactsError(f"{path}: operation {row.get('id')!r} has unknown kind {kind!r}") - requires = _strings(row.get("requires"), "requires", path) - for item in requires: - if item not in DISCHARGER_KINDS: - raise ObligationFactsError(f"{path}: operation {row.get('id')!r} requires unknown discharger kind {item!r}") - sensitivity = str(row.get("sensitivity", "medium")) - if sensitivity not in SENSITIVITIES: - raise ObligationFactsError(f"{path}: operation {row.get('id')!r} has unknown sensitivity {sensitivity!r}") - resource_arg = row.get("resource_arg") - if resource_arg is not None and not isinstance(resource_arg, int): - raise ObligationFactsError(f"{path}: operation {row.get('id')!r} resource_arg must be an integer") - document_arg = row.get("query_document_arg") - if document_arg is not None and (not isinstance(document_arg, int) or document_arg < 1): - raise ObligationFactsError(f"{path}: operation {row.get('id')!r} query_document_arg must be a positive integer") - handlers = _strings(row.get("handlers"), "handlers", path) - framework = row.get("framework") - if framework is not None and (not isinstance(framework, str) or not framework): - raise ObligationFactsError("invalid operation framework") - if handlers and framework is None: - raise ObligationFactsError("handler operation needs a framework") - for pattern in handlers: - try: - re.compile(pattern) - except re.error as exc: - raise ObligationFactsError(type(exc).__name__) from exc - operations.append( - OperationFact( - id=str(row["id"]), - kind=kind, - language=language, - calls=_strings(row.get("calls"), "calls", path), - resource_arg=resource_arg, - requires=requires, - sensitivity=sensitivity, - query_document_arg=document_arg, - handlers=handlers, - framework=framework, - ) - ) + operations.append(_operation_fact(row, path, language)) for row in _rows(payload.get("discharger"), path): _only_fields(row, _DISCHARGER_FIELDS, path) kind = str(row.get("kind", "")) @@ -160,6 +133,64 @@ def _load_obligation_facts_uncached(directory: Path | None = None) -> Obligation return ObligationFacts(version=versions[0] if versions else "1", operations=tuple(operations), dischargers=tuple(dischargers)) +def _operation_fact(row: dict[str, object], path: Path, language: str) -> OperationFact: + """Validate one operation row against the closed sets and parse it; any unknown kind or field fails loud.""" + _only_fields(row, _OPERATION_FIELDS, path) + kind = str(row.get("kind", "")) + if kind not in OPERATION_KINDS: + raise ObligationFactsError(f"{path}: operation {row.get('id')!r} has unknown kind {kind!r}") + requires = _strings(row.get("requires"), "requires", path) + for item in requires: + if item not in DISCHARGER_KINDS: + raise ObligationFactsError(f"{path}: operation {row.get('id')!r} requires unknown discharger kind {item!r}") + sensitivity = str(row.get("sensitivity", "medium")) + if sensitivity not in SENSITIVITIES: + raise ObligationFactsError(f"{path}: operation {row.get('id')!r} has unknown sensitivity {sensitivity!r}") + request_global_kinds = _strings(row.get("request_global_kinds"), "request_global_kinds", path) + for item in request_global_kinds: + if item not in DISCHARGER_KINDS: + raise ObligationFactsError(f"{path}: operation {row.get('id')!r} request_global_kinds names unknown discharger kind {item!r}") + handler_patterns, handler_framework = _handler_shape(row, path) + return OperationFact( + id=str(row["id"]), + kind=kind, + language=language, + calls=_strings(row.get("calls"), "calls", path), + resource_arg=_optional_int(row, "resource_arg", path, positive=False), + requires=requires, + sensitivity=sensitivity, + query_document_arg=_optional_int(row, "query_document_arg", path, positive=True), + handlers=handler_patterns, + framework=handler_framework, + request_global_kinds=request_global_kinds, + ) + + +def _optional_int(row: dict[str, object], field: str, path: Path, *, positive: bool) -> int | None: + value = row.get(field) + if value is None: + return None + if not isinstance(value, int) or (positive and value < 1): + requirement = "a positive integer" if positive else "an integer" + raise ObligationFactsError(f"{path}: operation {row.get('id')!r} {field} must be {requirement}") + return value + + +def _handler_shape(row: dict[str, object], path: Path) -> tuple[tuple[str, ...], str | None]: + handler_patterns = _strings(row.get("handlers"), "handlers", path) + framework = row.get("framework") + if framework is not None and (not isinstance(framework, str) or not framework): + raise ObligationFactsError("invalid operation framework") + if handler_patterns and framework is None: + raise ObligationFactsError("handler operation needs a framework") + for pattern in handler_patterns: + try: + re.compile(pattern) + except re.error as exc: + raise ObligationFactsError(type(exc).__name__) from exc + return handler_patterns, framework + + def _rows(value: object, path: Path) -> list[dict[str, object]]: if value is None: return [] diff --git a/tests/test_obligation_resource_domain.py b/tests/test_obligation_resource_domain.py new file mode 100644 index 0000000..b3532bb --- /dev/null +++ b/tests/test_obligation_resource_domain.py @@ -0,0 +1,222 @@ +"""access-control-prover task 7.2: resource abstract values and operation-fact sufficiency fields (offline). + +Exact resources, finite alias sets, request-global scope and unknown resources per the design's "Abstract +evidence domain" section (Req 2.1, 2.5, 2.6, 2.7, 11.1), plus the additive operation-fact field that declares +a request-global witness kind sufficient at request scope (Req 2.6). +""" + +from __future__ import annotations + +import itertools +from pathlib import Path + +import pytest + + +def _resource_fixtures(): + from openultrasast.semantic.obligations.abstract_domain import ( + REQUEST_GLOBAL_RESOURCE, + UNKNOWN_RESOURCE, + ResourceRef, + ) + + return ( + ResourceRef(kind="exact", values=("book",)), + ResourceRef(kind="exact", values=("volume",)), + ResourceRef(kind="aliases", values=("book", "volume")), + ResourceRef(kind="aliases", values=("volume", "shelf")), + REQUEST_GLOBAL_RESOURCE, + UNKNOWN_RESOURCE, + ) + + +_OPERATION_TOML = """version = "1" +language = "python" + +[[operation]] +id = "orm-read" +kind = "protected_read" +calls = ["filter_by"] +requires = ["identity_constraint"] +sensitivity = "high" +request_global_kinds = ["path_guard"] +""" + + +def test_parse_resource_single_token_is_exact() -> None: + from openultrasast.semantic.obligations.abstract_domain import ResourceRef, parse_resource + + binding = parse_resource("book") + assert binding == ResourceRef(kind="exact", values=("book",)) + assert binding.kind == "exact" + assert binding.values == ("book",) + + +def test_parse_resource_token_collection_is_a_finite_alias_set() -> None: + from openultrasast.semantic.obligations.abstract_domain import ResourceRef, parse_resource + + binding = parse_resource(["volume", "book", "volume"]) + assert binding == ResourceRef(kind="aliases", values=("book", "volume")) + + +def test_parse_resource_without_a_binding_is_unknown() -> None: + from openultrasast.semantic.obligations.abstract_domain import UNKNOWN_RESOURCE, parse_resource + + binding = parse_resource(None) + assert binding == UNKNOWN_RESOURCE + assert binding.kind == "unknown" + assert binding.values == () + + +def test_request_global_resource_binds_the_whole_request() -> None: + from openultrasast.semantic.obligations.abstract_domain import REQUEST_GLOBAL_RESOURCE + + assert REQUEST_GLOBAL_RESOURCE.kind == "request_global" + assert REQUEST_GLOBAL_RESOURCE.values == () + + +def test_resource_kinds_distinguish_exact_alias_global_and_unknown() -> None: + # Req 2.7, 11.1: the four grades stay distinct; an unknown binding never collapses onto a concrete one. + from openultrasast.semantic.obligations.abstract_domain import ( + REQUEST_GLOBAL_RESOURCE, + UNKNOWN_RESOURCE, + parse_resource, + ) + + grades = {parse_resource("book"), parse_resource(["book"]), REQUEST_GLOBAL_RESOURCE, UNKNOWN_RESOURCE} + assert {resource.kind for resource in grades} == {"exact", "aliases", "request_global", "unknown"} + + +def test_alias_values_are_normalized_deterministically() -> None: + from openultrasast.semantic.obligations.abstract_domain import ResourceRef + + forward = ResourceRef(kind="aliases", values=("volume", "book", "volume")) + backward = ResourceRef(kind="aliases", values=("book", "volume")) + assert forward == backward + assert hash(forward) == hash(backward) + assert len({forward, backward}) == 1 + + +def test_resource_ref_fails_loud_on_misshapen_kinds_and_arities() -> None: + from openultrasast.semantic.obligations.abstract_domain import ResourceRef + + with pytest.raises(ValueError, match="sometimes"): + ResourceRef(kind="sometimes", values=("book",)) + with pytest.raises(ValueError, match="exact"): + ResourceRef(kind="exact") + with pytest.raises(ValueError, match="exact"): + ResourceRef(kind="exact", values=("book", "volume")) + with pytest.raises(ValueError, match="alias"): + ResourceRef(kind="aliases", values=()) + with pytest.raises(ValueError, match="request_global"): + ResourceRef(kind="request_global", values=("book",)) + + +def test_parse_resource_rejects_misshapen_bindings() -> None: + from openultrasast.semantic.obligations.abstract_domain import parse_resource + + with pytest.raises(ValueError): + parse_resource("") + with pytest.raises(ValueError): + parse_resource(()) + with pytest.raises(ValueError): + parse_resource(["book", ""]) + + +def test_join_resources_keeps_identical_exact_tokens_exact() -> None: + from openultrasast.semantic.obligations.abstract_domain import ResourceRef, join_resources + + binding = ResourceRef(kind="exact", values=("book",)) + assert join_resources(binding, ResourceRef(kind="exact", values=("book",))) == binding + + +def test_join_resources_merges_different_exact_tokens_into_an_alias_set() -> None: + # Req 2.5: a different resource never collapses onto one exact binding; it widens to the finite alias set. + from openultrasast.semantic.obligations.abstract_domain import ResourceRef, join_resources + + joined = join_resources( + ResourceRef(kind="exact", values=("book",)), + ResourceRef(kind="exact", values=("volume",)), + ) + assert joined == ResourceRef(kind="aliases", values=("book", "volume")) + + +def test_join_resources_adds_exact_tokens_into_alias_sets() -> None: + from openultrasast.semantic.obligations.abstract_domain import ResourceRef, join_resources + + joined = join_resources( + ResourceRef(kind="exact", values=("shelf",)), + ResourceRef(kind="aliases", values=("book", "volume")), + ) + assert joined == ResourceRef(kind="aliases", values=("book", "shelf", "volume")) + + +def test_join_resources_unions_alias_sets_to_their_superset() -> None: + from openultrasast.semantic.obligations.abstract_domain import ResourceRef, join_resources + + subset = ResourceRef(kind="aliases", values=("book",)) + superset = ResourceRef(kind="aliases", values=("book", "volume")) + assert join_resources(subset, superset) == superset + assert join_resources(superset, subset) == superset + disjoint = join_resources(subset, ResourceRef(kind="aliases", values=("volume",))) + assert disjoint == ResourceRef(kind="aliases", values=("book", "volume")) + + +def test_join_resources_request_global_absorbs_concrete_bindings() -> None: + # Req 2.6: request-global scope already covers every resource in the request. + from openultrasast.semantic.obligations.abstract_domain import ( + REQUEST_GLOBAL_RESOURCE, + ResourceRef, + join_resources, + ) + + for concrete in ( + ResourceRef(kind="exact", values=("book",)), + ResourceRef(kind="aliases", values=("book", "volume")), + ): + assert join_resources(concrete, REQUEST_GLOBAL_RESOURCE) == REQUEST_GLOBAL_RESOURCE + assert join_resources(REQUEST_GLOBAL_RESOURCE, concrete) == REQUEST_GLOBAL_RESOURCE + assert join_resources(REQUEST_GLOBAL_RESOURCE, REQUEST_GLOBAL_RESOURCE) == REQUEST_GLOBAL_RESOURCE + + +def test_join_resources_unknown_absorbs_every_fixture() -> None: + # Req 2.7, 11.1: an unresolvable binding stays unresolvable; joining cannot manufacture precision. + from openultrasast.semantic.obligations.abstract_domain import UNKNOWN_RESOURCE, join_resources + + for other in _resource_fixtures(): + assert join_resources(other, UNKNOWN_RESOURCE) == UNKNOWN_RESOURCE, other + assert join_resources(UNKNOWN_RESOURCE, other) == UNKNOWN_RESOURCE, other + + +def test_join_resources_is_commutative_and_idempotent_over_fixtures() -> None: + from openultrasast.semantic.obligations.abstract_domain import join_resources + + fixtures = _resource_fixtures() + for left, right in itertools.product(fixtures, repeat=2): + assert join_resources(left, right) == join_resources(right, left), (left, right) + for resource in fixtures: + assert join_resources(resource, resource) == resource, resource + + +def test_operation_fact_declares_request_global_sufficient_kinds(tmp_path: Path) -> None: + from openultrasast.semantic.obligations.facts import load_obligation_facts + + (tmp_path / "python.toml").write_text(_OPERATION_TOML) + (row,) = load_obligation_facts(tmp_path).operations + assert row.request_global_kinds == ("path_guard",) + + +def test_operation_fact_without_sufficiency_declares_none(tmp_path: Path) -> None: + from openultrasast.semantic.obligations.facts import load_obligation_facts + + (tmp_path / "python.toml").write_text(_OPERATION_TOML.replace('request_global_kinds = ["path_guard"]\n', "")) + (row,) = load_obligation_facts(tmp_path).operations + assert row.request_global_kinds == () + + +def test_operation_fact_rejects_unknown_request_global_kind(tmp_path: Path) -> None: + from openultrasast.semantic.obligations.facts import ObligationFactsError, load_obligation_facts + + (tmp_path / "python.toml").write_text(_OPERATION_TOML.replace('["path_guard"]', '["vibes"]')) + with pytest.raises(ObligationFactsError, match="vibes"): + load_obligation_facts(tmp_path)