mirror of
https://github.com/norandom/OpenUltraSAST.git
synced 2026-11-13 09:48:18 +00:00
260 lines
11 KiB
Python
260 lines
11 KiB
Python
"""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}
|