75 lines
3.2 KiB
Markdown
75 lines
3.2 KiB
Markdown
|
---
|
||
|
|
id: F-0002
|
||
|
|
type: framework-finding
|
||
|
|
class: FRAMEWORK_LIMITATION
|
||
|
|
status: resolved
|
||
|
|
discovered: "2026-08-22"
|
||
|
|
resolved: "2026-08-22"
|
||
|
|
discovered_by: TD-WP-0002-T05
|
||
|
|
workplan: TD-WP-0002
|
||
|
|
task: TD-WP-0002-T05
|
||
|
|
---
|
||
|
|
|
||
|
|
# F-0002 — Two seeded defects were invisible to the reference scenario
|
||
|
|
|
||
|
|
## Observation
|
||
|
|
|
||
|
|
On first running the reference scenario against the twenty labelled mutations,
|
||
|
|
**six of six DEFECT mutations should have failed; only four did.**
|
||
|
|
|
||
|
|
| Mutation | Defect | Verdict before | Why it escaped |
|
||
|
|
|---|---|---|---|
|
||
|
|
| M16 | A READ grant confers WRITE | `PASS` | No claim mentioned writing. The scenario never attempted one. |
|
||
|
|
| M18 | Revocation is not audited | `PASS` | `i-audit-append-only` checks *ordering*, not *completeness*. A trail missing an entry is still ordered. |
|
||
|
|
|
||
|
|
Both passed cleanly. Nothing was flaky, nothing was ambiguous, and no oracle
|
||
|
|
reported `INCONCLUSIVE` — the framework simply had nothing to say, confidently.
|
||
|
|
|
||
|
|
## Why it matters
|
||
|
|
|
||
|
|
This is the failure mode most likely to be mistaken for success. A green run
|
||
|
|
against a lab carrying a seeded privilege escalation looks exactly like a green
|
||
|
|
run against a correct system. Had the catalogue been the six mutations the
|
||
|
|
milestones document originally sketched, this would not have surfaced at all —
|
||
|
|
which is the concrete argument for the larger catalogue, now made from evidence
|
||
|
|
rather than from assertion.
|
||
|
|
|
||
|
|
It also sharpens what a verification asset is: **a use case protects exactly what
|
||
|
|
it asserts, and not one thing more.** Coverage is a property of the claim set, not
|
||
|
|
of the framework. No amount of adaptation, crystallization or energy scoring
|
||
|
|
compensates for an assertion nobody wrote.
|
||
|
|
|
||
|
|
## Resolution
|
||
|
|
|
||
|
|
Path 1 — the implementation changes to match the concept.
|
||
|
|
|
||
|
|
Two claims were added to the reference use case, both `Provenance.HUMAN` and both
|
||
|
|
derivable from `INTENT.md` rather than from watching the lab:
|
||
|
|
|
||
|
|
- `c-bob-cannot-write` — "A READ grant does not let Bob write R".
|
||
|
|
`INTENT.md` § Security by Use-Case Mutation already derives this exact question
|
||
|
|
from the reference use case: *"Can Bob write when only read permission was
|
||
|
|
granted?"* It was always part of what sharing means; it had simply never been
|
||
|
|
written down as an assertion.
|
||
|
|
- `c-revoke-audited` — "Revocation is recorded in the audit trail". Enforcement
|
||
|
|
being correct is not sufficient: an access change nobody can later evidence is
|
||
|
|
a compliance failure even when the access itself is right.
|
||
|
|
|
||
|
|
Supporting changes: the lab gained a write path and the observation channel a
|
||
|
|
non-destructive `probe_write`.
|
||
|
|
|
||
|
|
Both defects are now detected. DEFECT detection is 6/6, and
|
||
|
|
`test_every_defect_is_detected` fails the suite if that ever regresses.
|
||
|
|
|
||
|
|
## Note on provenance
|
||
|
|
|
||
|
|
These claims were added *after* observing that mutations escaped, which is
|
||
|
|
uncomfortably close to fitting assertions to the lab. They are admissible because
|
||
|
|
both were already stated as intent in `INTENT.md` before any lab existed — the
|
||
|
|
finding revealed a transcription gap, not a new requirement. Had the intended
|
||
|
|
behaviour not already been on record, the correct resolution would have been to
|
||
|
|
escalate to a human, not to write the claim.
|
||
|
|
|
||
|
|
That distinction is exactly what `Provenance` exists to make checkable, and this
|
||
|
|
finding is the first case where it did real work.
|