Block isolation breaches and bind frozen replay to scheduled steps
Assistant: codex Assistant-Model: gpt-6-astra Assistant-Session: 01a0e76f-be98-7ae3-965d-e0b31290a4c4
This commit is contained in:
parent
a8bb787d12
commit
9cdade2116
10 changed files with 229 additions and 14 deletions
|
|
@ -244,3 +244,30 @@ Validation for this follow-up: initial reproduction had 20 failures and two
|
||||||
passing controls; full suite **327 passed**. The final dynamic-dependency and
|
passing controls; full suite **327 passed**. The final dynamic-dependency and
|
||||||
strict-postcondition additions passed **32 boundary checks**, including four
|
strict-postcondition additions passed **32 boundary checks**, including four
|
||||||
new cases. These counts overlap; they are not separate independent samples.
|
new cases. These counts overlap; they are not separate independent samples.
|
||||||
|
|
||||||
|
## Isolation and repeated-action replay follow-up (2026-09-28)
|
||||||
|
|
||||||
|
Recorded actor isolation violations now stop the runner before further actions
|
||||||
|
or judgments. Unreached scheduled assertions become INCONCLUSIVE; prior observed
|
||||||
|
product failures remain FAIL. The framework finding remains separate S3 evidence,
|
||||||
|
so it does not add or rewrite product claims. Isolation is examined at entry and
|
||||||
|
after each action. Classification requires all these checks to be present, S3,
|
||||||
|
and free of violations; crystallization inherits that gate. Older packs with
|
||||||
|
only an entry check need rerunning before automatic acceptance. Canary checks
|
||||||
|
remain a diagnostic at those boundaries, not proof against arbitrary memory
|
||||||
|
access or transient leaks inside a driver.
|
||||||
|
|
||||||
|
Runner dispatch now passes step identity to drivers that expose `realize_step`.
|
||||||
|
Composite drivers forward it while ordinary action-only drivers keep their
|
||||||
|
existing interface. Frozen replay selects by step and verifies the action name;
|
||||||
|
repeated names no longer overwrite different targets. Unknown/mismatched steps,
|
||||||
|
duplicate frozen step ids and ambiguous action-only calls cannot send a request.
|
||||||
|
Unambiguous action-only calls remain supported. Replay has no advancing cursor,
|
||||||
|
so the same driver can run the schedule repeatedly.
|
||||||
|
|
||||||
|
Regression coverage includes entry/mid-run/final-action leaks, otherwise passing
|
||||||
|
packs with invalid isolation evidence, distinct targets for repeated actions
|
||||||
|
through direct and composite dispatch, driver reuse and invalid frozen lookup.
|
||||||
|
Decision: `e8fabf6e-3e5e-424e-9a60-152bf3dec641`.
|
||||||
|
|
||||||
|
Validation: the complete suite passed **343 tests** (153.67 seconds).
|
||||||
|
|
|
||||||
|
|
@ -10,3 +10,4 @@ file is a pointer table, not a second source of truth.
|
||||||
| TD-WP-0003 T04/T05/T08 | Python claims, concept removal and not-ready assessment | `d80734d1-01b8-4a98-8e72-c86f1806d572` | `docs/TestDriverGeneralisationReview.md` |
|
| TD-WP-0003 T04/T05/T08 | Python claims, concept removal and not-ready assessment | `d80734d1-01b8-4a98-8e72-c86f1806d572` | `docs/TestDriverGeneralisationReview.md` |
|
||||||
| TD-WP-0003 T08 safety follow-up | Run-input manifests and incomplete-run handling | `afb38ade-893b-48a2-b1b3-c55e49cc40ee` | `docs/TestDriverGeneralisationReview.md` |
|
| TD-WP-0003 T08 safety follow-up | Run-input manifests and incomplete-run handling | `afb38ade-893b-48a2-b1b3-c55e49cc40ee` | `docs/TestDriverGeneralisationReview.md` |
|
||||||
| TD-WP-0003 T08 admission follow-up | Qualified crystallization, passing baselines and intent revisions | `88e51e10-cd32-44d2-a2d6-055675b5ce04` | `docs/TestDriverGeneralisationReview.md` |
|
| TD-WP-0003 T08 admission follow-up | Qualified crystallization, passing baselines and intent revisions | `88e51e10-cd32-44d2-a2d6-055675b5ce04` | `docs/TestDriverGeneralisationReview.md` |
|
||||||
|
| TD-WP-0003 T08 isolation/replay follow-up | Isolation acceptance gate and step-bound frozen replay | `e8fabf6e-3e5e-424e-9a60-152bf3dec641` | `docs/TestDriverGeneralisationReview.md` |
|
||||||
|
|
|
||||||
|
|
@ -179,6 +179,14 @@ def _has_complete_evidence(pack: Mapping[str, Any]) -> bool:
|
||||||
or not isinstance(o["data"], Mapping) or not o["data"]
|
or not isinstance(o["data"], Mapping) or not o["data"]
|
||||||
for o in records)):
|
for o in records)):
|
||||||
return False
|
return False
|
||||||
|
isolation = [o for o in observations if o["kind"] == "actor_isolation"]
|
||||||
|
isolation_steps = [o["step_id"] for o in isolation]
|
||||||
|
if (len(isolation_steps) != len(steps) + 1
|
||||||
|
or set(isolation_steps) != {None, *steps}
|
||||||
|
or any(o["stratum"] != "S3" or not isinstance(o["data"], Mapping)
|
||||||
|
or o["data"].get("violations") != []
|
||||||
|
for o in isolation)):
|
||||||
|
return False
|
||||||
if any(o["kind"] == "surface_violation" for o in observations):
|
if any(o["kind"] == "surface_violation" for o in observations):
|
||||||
return False
|
return False
|
||||||
revisions = pack["intent_revisions"]
|
revisions = pack["intent_revisions"]
|
||||||
|
|
|
||||||
|
|
@ -137,16 +137,28 @@ class CrystallizedDriver:
|
||||||
|
|
||||||
def __init__(self, trajectories: Sequence[Trajectory], session_factory) -> None:
|
def __init__(self, trajectories: Sequence[Trajectory], session_factory) -> None:
|
||||||
self._by_step = {t.step_id: t for t in trajectories}
|
self._by_step = {t.step_id: t for t in trajectories}
|
||||||
self._by_action = {t.action_name: t for t in trajectories}
|
if len(self._by_step) != len(trajectories):
|
||||||
|
raise ValueError("duplicate frozen step ids")
|
||||||
|
self._by_action: dict[str, list[Trajectory]] = {}
|
||||||
|
for trajectory in trajectories:
|
||||||
|
self._by_action.setdefault(trajectory.action_name, []).append(trajectory)
|
||||||
self._session_factory = session_factory
|
self._session_factory = session_factory
|
||||||
self.surface = None # set per action; a frozen path may span surfaces
|
self.surface = None # set per action; a frozen path may span surfaces
|
||||||
|
|
||||||
def realize(self, actor: Actor, action: SemanticAction) -> Realization:
|
def realize(self, actor: Actor, action: SemanticAction) -> Realization:
|
||||||
trajectory = self._by_action.get(action.name)
|
matches = self._by_action.get(action.name, [])
|
||||||
if trajectory is None:
|
if len(matches) != 1:
|
||||||
|
return Realization("crystallized", {"action": action.name},
|
||||||
|
raised="NotCrystallized: action needs an unambiguous step id")
|
||||||
|
return self.realize_step(actor, matches[0].step_id, action)
|
||||||
|
|
||||||
|
def realize_step(self, actor: Actor, step_id: str,
|
||||||
|
action: SemanticAction) -> Realization:
|
||||||
|
trajectory = self._by_step.get(step_id)
|
||||||
|
if trajectory is None or trajectory.action_name != action.name:
|
||||||
return Realization(
|
return Realization(
|
||||||
"crystallized", {"action": action.name},
|
"crystallized", {"action": action.name},
|
||||||
raised="NotCrystallized: no frozen path for this action",
|
raised="NotCrystallized: no matching frozen path for this step and action",
|
||||||
)
|
)
|
||||||
action.check_surface(trajectory.surface_id)
|
action.check_surface(trajectory.surface_id)
|
||||||
args = dict(action.args)
|
args = dict(action.args)
|
||||||
|
|
|
||||||
|
|
@ -29,6 +29,18 @@ class Driver(Protocol):
|
||||||
def realize(self, actor: Actor, action: SemanticAction) -> Realization: ...
|
def realize(self, actor: Actor, action: SemanticAction) -> Realization: ...
|
||||||
|
|
||||||
|
|
||||||
|
def realize_step(driver: Driver, actor: Actor, step_id: str,
|
||||||
|
action: SemanticAction) -> Realization:
|
||||||
|
"""Pass schedule identity to drivers that bind mechanics to a specific step.
|
||||||
|
|
||||||
|
Ordinary drivers retain their action-only interface.
|
||||||
|
"""
|
||||||
|
method = getattr(driver, "realize_step", None)
|
||||||
|
if method is not None:
|
||||||
|
return method(actor, step_id, action)
|
||||||
|
return driver.realize(actor, action)
|
||||||
|
|
||||||
|
|
||||||
class UnsupportedAction(Exception):
|
class UnsupportedAction(Exception):
|
||||||
"""The driver has no mechanical implementation for this semantic action."""
|
"""The driver has no mechanical implementation for this semantic action."""
|
||||||
|
|
||||||
|
|
@ -95,11 +107,16 @@ class CompositeDriver:
|
||||||
self.surface = drivers[default].surface
|
self.surface = drivers[default].surface
|
||||||
|
|
||||||
def realize(self, actor: Actor, action: SemanticAction) -> Realization:
|
def realize(self, actor: Actor, action: SemanticAction) -> Realization:
|
||||||
|
return self.realize_step(actor, None, action)
|
||||||
|
|
||||||
|
def realize_step(self, actor: Actor, step_id: str | None,
|
||||||
|
action: SemanticAction) -> Realization:
|
||||||
permitted = action.permitted_surfaces or {self._default}
|
permitted = action.permitted_surfaces or {self._default}
|
||||||
for surface_id in sorted(permitted):
|
for surface_id in sorted(permitted):
|
||||||
driver = self._drivers.get(surface_id)
|
driver = self._drivers.get(surface_id)
|
||||||
if driver is not None:
|
if driver is not None:
|
||||||
return driver.realize(actor, action)
|
return (realize_step(driver, actor, step_id, action) if step_id is not None
|
||||||
|
else driver.realize(actor, action))
|
||||||
raise UnsupportedAction(
|
raise UnsupportedAction(
|
||||||
f"no driver for any permitted surface of {action.name!r}: "
|
f"no driver for any permitted surface of {action.name!r}: "
|
||||||
f"{sorted(permitted)}"
|
f"{sorted(permitted)}"
|
||||||
|
|
|
||||||
|
|
@ -14,7 +14,7 @@ from datetime import datetime, timezone
|
||||||
from typing import Any
|
from typing import Any
|
||||||
|
|
||||||
from .actions import SurfaceNotPermitted
|
from .actions import SurfaceNotPermitted
|
||||||
from .drivers import Driver
|
from .drivers import Driver, realize_step
|
||||||
from .evidence import EvidencePack, Observation, Stratum
|
from .evidence import EvidencePack, Observation, Stratum
|
||||||
from .observers import StateObserver
|
from .observers import StateObserver
|
||||||
from .oracles import Judgment, Oracle, Verdict, overall
|
from .oracles import Judgment, Oracle, Verdict, overall
|
||||||
|
|
@ -149,12 +149,25 @@ class Runner:
|
||||||
for claim in scenario.use_case.claims:
|
for claim in scenario.use_case.claims:
|
||||||
claims_by_step.setdefault(claim.after_step, []).append(claim)
|
claims_by_step.setdefault(claim.after_step, []).append(claim)
|
||||||
|
|
||||||
|
def skip_remaining(index: int, reason: str) -> None:
|
||||||
|
for skipped in scenario.steps[index:]:
|
||||||
|
for assertion in (*scenario.use_case.invariants,
|
||||||
|
*claims_by_step.get(skipped.id, ())):
|
||||||
|
judgments.append(Judgment(
|
||||||
|
assertion.id, assertion.text, Verdict.INCONCLUSIVE,
|
||||||
|
skipped.id, {"reason": reason},
|
||||||
|
))
|
||||||
|
|
||||||
for step_index, step in enumerate(scenario.steps):
|
for step_index, step in enumerate(scenario.steps):
|
||||||
|
if isolation:
|
||||||
|
aborted = True
|
||||||
|
skip_remaining(step_index, "framework actor isolation violated")
|
||||||
|
break
|
||||||
actor = self._world.cast[step.actor_id]
|
actor = self._world.cast[step.actor_id]
|
||||||
|
|
||||||
# --- S1: how it was done -------------------------------------
|
# --- S1: how it was done -------------------------------------
|
||||||
try:
|
try:
|
||||||
realization = self._driver.realize(actor, step.action)
|
realization = realize_step(self._driver, actor, step.id, step.action)
|
||||||
except SurfaceNotPermitted as exc:
|
except SurfaceNotPermitted as exc:
|
||||||
# D-05: routing around a control is a finding, not a recovery.
|
# D-05: routing around a control is a finding, not a recovery.
|
||||||
self._record(
|
self._record(
|
||||||
|
|
@ -191,6 +204,17 @@ class Runner:
|
||||||
step.id,
|
step.id,
|
||||||
)
|
)
|
||||||
|
|
||||||
|
isolation = self._isolation_violations()
|
||||||
|
self._record(
|
||||||
|
pack, Stratum.JUDGMENT, self._observer.name, "actor_isolation",
|
||||||
|
{"violations": isolation, "actors": sorted(self._world.cast.actors)},
|
||||||
|
step.id,
|
||||||
|
)
|
||||||
|
if isolation:
|
||||||
|
aborted = True
|
||||||
|
skip_remaining(step_index, "framework actor isolation violated")
|
||||||
|
break
|
||||||
|
|
||||||
# --- S3: what is now true ------------------------------------
|
# --- S3: what is now true ------------------------------------
|
||||||
snapshot = self._observer.snapshot()
|
snapshot = self._observer.snapshot()
|
||||||
self._record(
|
self._record(
|
||||||
|
|
|
||||||
|
|
@ -103,12 +103,12 @@ def check_isolation_was_examined(pack: Mapping[str, Any]) -> list[str]:
|
||||||
private marker and the runner examines them on every scenario, so the absence
|
private marker and the runner examines them on every scenario, so the absence
|
||||||
of this observation is itself a failure.
|
of this observation is itself a failure.
|
||||||
"""
|
"""
|
||||||
for obs in _observations(pack):
|
records = [o for o in _observations(pack) if o["kind"] == "actor_isolation"]
|
||||||
if obs["kind"] != "actor_isolation":
|
if not records:
|
||||||
continue
|
|
||||||
violations = obs["data"].get("violations") or []
|
|
||||||
return [f"actor isolation violated: {v}" for v in violations]
|
|
||||||
return ["this run did not examine actor isolation at all"]
|
return ["this run did not examine actor isolation at all"]
|
||||||
|
return [f"actor isolation violated: {v}" for o in records
|
||||||
|
for v in o["data"].get("violations", [])]
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
# --- td://self/oracle-independence ---------------------------------------
|
# --- td://self/oracle-independence ---------------------------------------
|
||||||
|
|
|
||||||
110
tests/test_isolation_and_replay.py
Normal file
110
tests/test_isolation_and_replay.py
Normal file
|
|
@ -0,0 +1,110 @@
|
||||||
|
"""Framework isolation and frozen schedule identity are acceptance boundaries."""
|
||||||
|
from copy import deepcopy
|
||||||
|
from dataclasses import replace
|
||||||
|
import json
|
||||||
|
|
||||||
|
import pytest
|
||||||
|
|
||||||
|
from scenarios.alice_bob_carol import build
|
||||||
|
from testdriver import Runner, Verdict
|
||||||
|
from testdriver.actions import SemanticAction
|
||||||
|
from testdriver.classification import classify
|
||||||
|
from testdriver.crystallization import CrystallizedDriver, Trajectory, assess_stability
|
||||||
|
from testdriver.drivers import CompositeDriver
|
||||||
|
from testdriver.scenario import Step
|
||||||
|
|
||||||
|
|
||||||
|
@pytest.mark.parametrize('leak_at', [None, 0, 1, 2])
|
||||||
|
def test_isolation_breach_stops_run_and_cannot_be_accepted_or_frozen(leak_at):
|
||||||
|
world, driver, observer, asset, oracle = build()
|
||||||
|
calls = []
|
||||||
|
|
||||||
|
def leak():
|
||||||
|
world.cast['bob'].remember('overheard', world.cast['alice'].canary)
|
||||||
|
|
||||||
|
class LeakingDriver:
|
||||||
|
def realize(self, actor, action):
|
||||||
|
result = driver.realize(actor, action)
|
||||||
|
calls.append(action.name)
|
||||||
|
if len(calls) - 1 == leak_at:
|
||||||
|
leak()
|
||||||
|
return result
|
||||||
|
|
||||||
|
if leak_at is None:
|
||||||
|
leak()
|
||||||
|
result = Runner(world, LeakingDriver(), observer, oracle).run(asset)
|
||||||
|
assert result.verdict is Verdict.INCONCLUSIVE
|
||||||
|
assert len(calls) == (0 if leak_at is None else leak_at + 1)
|
||||||
|
assert any(j.verdict is Verdict.INCONCLUSIVE for j in result.judgments)
|
||||||
|
pack = json.loads(result.evidence.to_json())
|
||||||
|
assert any(o['data']['violations'] for o in pack['observations']
|
||||||
|
if o['kind'] == 'actor_isolation')
|
||||||
|
assert not classify(pack, pack).safe_to_accept
|
||||||
|
assert not assess_stability([pack, deepcopy(pack), deepcopy(pack)]).stable
|
||||||
|
|
||||||
|
|
||||||
|
@pytest.mark.parametrize('damage', ['violation', 'missing', 'stratum', 'duplicate', 'malformed'])
|
||||||
|
def test_passing_product_verdicts_cannot_hide_invalid_isolation_evidence(damage):
|
||||||
|
packs = []
|
||||||
|
for _ in range(3):
|
||||||
|
world, driver, observer, asset, oracle = build()
|
||||||
|
pack = json.loads(Runner(world, driver, observer, oracle).run(asset).evidence.to_json())
|
||||||
|
guard = [o for o in pack['observations'] if o['kind'] == 'actor_isolation'][-1]
|
||||||
|
if damage == 'violation':
|
||||||
|
guard['data']['violations'] = ['actor leaked']
|
||||||
|
elif damage == 'missing':
|
||||||
|
pack['observations'].remove(guard)
|
||||||
|
elif damage == 'stratum':
|
||||||
|
guard['stratum'] = 'S1'
|
||||||
|
elif damage == 'duplicate':
|
||||||
|
pack['observations'].append(deepcopy(guard))
|
||||||
|
else:
|
||||||
|
guard['data'].pop('violations')
|
||||||
|
assert all(v['verdict'] == 'PASS' for v in pack['verdicts'])
|
||||||
|
assert not classify(pack, pack).safe_to_accept
|
||||||
|
packs.append(pack)
|
||||||
|
assert not assess_stability(packs).stable
|
||||||
|
|
||||||
|
|
||||||
|
def trajectories():
|
||||||
|
return [Trajectory('a', 'grant_access', 'browser', '/resources/A/grant', ('subject_id',)),
|
||||||
|
Trajectory('b', 'grant_access', 'browser', '/resources/B/grant', ('subject_id',))]
|
||||||
|
|
||||||
|
|
||||||
|
@pytest.mark.parametrize('composite', [False, True])
|
||||||
|
def test_runner_replays_repeated_actions_by_step_and_can_reuse_driver(composite):
|
||||||
|
world, _, observer, asset, oracle = build()
|
||||||
|
calls = []
|
||||||
|
|
||||||
|
class Session:
|
||||||
|
def post_form(self, path, fields):
|
||||||
|
calls.append((path, fields))
|
||||||
|
return 200, ''
|
||||||
|
|
||||||
|
driver = CrystallizedDriver(trajectories(), lambda actor: Session())
|
||||||
|
if composite:
|
||||||
|
driver = CompositeDriver({'browser': driver}, 'browser')
|
||||||
|
asset.scenario = replace(asset.scenario, steps=tuple(
|
||||||
|
Step(step_id, 'alice', SemanticAction('grant_access', {'subject_id': subject},
|
||||||
|
frozenset({'browser'})))
|
||||||
|
for step_id, subject in [('a', 'bob'), ('b', 'carol')]
|
||||||
|
))
|
||||||
|
for _ in range(2):
|
||||||
|
Runner(world, driver, observer, oracle).run(asset)
|
||||||
|
assert calls == [('/resources/A/grant', {'subject_id': 'bob'}),
|
||||||
|
('/resources/B/grant', {'subject_id': 'carol'})] * 2
|
||||||
|
|
||||||
|
|
||||||
|
def test_ambiguous_unknown_and_mismatched_frozen_actions_do_not_send_requests():
|
||||||
|
world, _, _, _, _ = build()
|
||||||
|
|
||||||
|
def unexpected_session(actor):
|
||||||
|
pytest.fail('invalid frozen dispatch must not open a session')
|
||||||
|
|
||||||
|
driver = CrystallizedDriver(trajectories(), unexpected_session)
|
||||||
|
action = SemanticAction('grant_access', {}, frozenset({'browser'}))
|
||||||
|
assert driver.realize(world.cast['alice'], action).raised
|
||||||
|
assert driver.realize_step(world.cast['alice'], 'unknown', action).raised
|
||||||
|
assert driver.realize_step(world.cast['alice'], 'a', replace(action, name='revoke_access')).raised
|
||||||
|
with pytest.raises(ValueError, match='duplicate'):
|
||||||
|
CrystallizedDriver([trajectories()[0]] * 2, unexpected_session)
|
||||||
|
|
@ -80,5 +80,5 @@ def test_every_run_records_a_verdict_on_isolation():
|
||||||
examined = [
|
examined = [
|
||||||
obs for obs in result.evidence.observations if obs.kind == "actor_isolation"
|
obs for obs in result.evidence.observations if obs.kind == "actor_isolation"
|
||||||
]
|
]
|
||||||
assert len(examined) == 1
|
assert len(examined) == 4
|
||||||
assert examined[0].data["violations"] == []
|
assert examined[0].data["violations"] == []
|
||||||
|
|
|
||||||
|
|
@ -337,3 +337,19 @@ postcondition guards passed **32 boundary tests** (including four new cases).
|
||||||
The earlier classification/crystallization subset passed 69 tests. Process/path
|
The earlier classification/crystallization subset passed 69 tests. Process/path
|
||||||
stability and captured-value redaction are covered; `git diff --check` is clean.
|
stability and captured-value redaction are covered; `git diff --check` is clean.
|
||||||
No new task or workplan; T01/T06/T07 remain waiting and this workplan stays blocked.
|
No new task or workplan; T01/T06/T07 remain waiting and this workplan stays blocked.
|
||||||
|
|
||||||
|
|
||||||
|
**2026-09-28 isolation/replay follow-up — done.** Isolation breaches at entry
|
||||||
|
or after an action now abort further execution and leave unreached judgments
|
||||||
|
INCONCLUSIVE, preserving prior observed failures. Classification and
|
||||||
|
crystallization require complete, clean S3 isolation checks. Frozen replay binds
|
||||||
|
mechanics to scheduled step identity, including composite routing, and rejects
|
||||||
|
ambiguous action-only calls, mismatched steps and duplicate frozen step ids.
|
||||||
|
Ordinary drivers retain their action-only interface.
|
||||||
|
|
||||||
|
Validation: **343 tests passed** in the full suite; the focused subset passed
|
||||||
|
81 tests. New regressions cover leaks at each action boundary, invalid isolation
|
||||||
|
evidence despite passing product verdicts, repeated action names with distinct
|
||||||
|
targets, reusable frozen drivers and invalid dispatch. `git diff --check` is
|
||||||
|
clean. Decision: `e8fabf6e-3e5e-424e-9a60-152bf3dec641`. No new task or workplan;
|
||||||
|
T01/T06/T07 remain waiting and this workplan remains blocked.
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue