feat(v0.5.0): CI-gate the MPU enforcement oracle, and make its control mechanical - #349
Merged
Conversation
…l mechanical
VER-OS-ISO-001 is `verified` and cites a qemu fault-injection oracle as evidence:
a cross-region write takes a REAL MemManage fault, CFSR=0x82 DACCVIOL+MMARVALID,
"handler-flag-gated, non-vacuous (granting the hole flips it to FAIL)".
Two things were true about that at once. The oracle is real and it works -- it runs
in about a second and I confirmed it before touching anything:
gust-iso-fault-probe OK: inside-write ok, outside-write denied @0x20008000
(CFSR=0x00000082 DACCVIOL+MMARVALID; MPU programmed via verified switch_to_partition)
And no workflow ran it. The artifact says so honestly ("evidence is local qemu, not
yet CI-gated"), which is the difference between this and gale#324 -- but it still
meant the only MPU ENFORCEMENT evidence gale held ran on somebody's laptop.
The non-vacuity claim was worse: "granting the hole flips it to FAIL" was performed
by a MANUAL EDIT. A control CI cannot run is not a control CI has. Wiring the probe
up without fixing that would have installed exactly the gate this sweep keeps
removing -- green, with nothing establishing it can distinguish.
So the control is now a cargo feature. `grant-hole` adds region 3 over exactly the
denied range -- region 3 is free, the verified core emits 3-7 disabled -- still
through switch_to_partition, never by hand. Measured both directions:
control OFF: OK ... denied @0x20008000 (CFSR=0x00000082) exit 0
control ON: FAIL: write to denied 0x20008000 fell through
-- MPU not enforcing exit 1
So the denial is PROVEN caused by the region table rather than by a bad address, a
stray handler, or an MPU that was never enabled.
The CI job runs the control FIRST and separately, as the other five jobs here do.
Worth separating while I am here: the neighbouring Renode gate (gust_iso.robot)
executes the region programmer's COMPUTATION and the seam order -- iso-region-ok,
iso-mpu-seam-ok, iso-nointerfere-ok -- on cortex-m3 over plain MappedMemory, and
asserts no fault anywhere. I checked: it contains no fault or exception assertion at
all. Computation and enforcement are different claims, and only one of them was
gated. Now both are.
This is REQ-OS-MPU-001's kill-criterion ("a crafted tenant writes outside its region
without a fault") executing on every PR. It does not discharge the requirement --
that needs synth RQ-62-MEMISOLATE for real per-tenant regions, and silicon -- but the
venue question I raised on synth#1145 is answered: gale can execute this criterion in
CI today.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
I wrote "See gale#348" guessing the PR number before opening it. The PR is #349; #348 is an unrelated issue filed minutes later (jess's MPU-primitive packaging gap). A code comment pointing at the wrong issue is a small defect that ages badly. Replaced with the stable artifact IDs it actually concerns — REQ-OS-MPU-001 for the kill-criterion and VER-OS-ISO-001 for the oracle this control makes non-vacuous. Those do not move when a PR number does. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
avrabe
added a commit
that referenced
this pull request
Sep 4, 2026
Both new jobs in kill-criteria.yml — the composed-graph env sweep (#346) and the MPU enforcement oracle (#349) — were running on every PR and gating nothing. Every other job in that workflow is a required context; these two were not, because I added them to the workflow and never to branch protection. That is the gale#294 defect class, reintroduced by me, in the workflow built to hold that line, on the day I closed #294 saying the invariant was now watched. The check-required-contexts gate did not catch it, and correctly so: it asserts that every REQUIRED context can report, not that every gate worth requiring IS required. Those are different properties and I had only built the first. Worth stating plainly because "we have a gate for that" was exactly the reasoning that let this through. Added to protection only after confirming both complete `success` on main (kill-criteria run, all six jobs green) — requiring a context not proven producible is the deadlock #340 was about, and doing it twice would be careless. Adding them to protection first made the committed list lag at 20 against 22, and the gate's own --protection direction reported it: NOT_LISTED a denied write really faults (REQ-OS-MPU-001 kill-criterion) NOT_LISTED no raw env import survives in the composed graph FAIL: 2 required context(s) may not be produced on a PR exit 1 Second time that direction has caught real drift rather than a planted one. This commit closes it: 22 contexts, list and protection matching exactly. Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
REQ-OS-MPU-001's kill-criterion — "a crafted tenant writes outside its regionwithout a fault" — now executes on every PR.
What I found
VER-OS-ISO-001isverifiedand cites a qemu fault-injection oracle: a cross-regionwrite takes a real MemManage fault,
CFSR=0x82 DACCVIOL+MMARVALID,"handler-flag-gated, non-vacuous (granting the hole flips it to FAIL)".
Two things were true at once.
The oracle is real and it works. I ran it before touching anything — about a
second:
And no workflow ran it. The artifact says so honestly — "evidence is local qemu,
not yet CI-gated" — which is the difference between this and #324. But it still meant
the only MPU enforcement evidence gale held ran on somebody's laptop.
The part that needed fixing first
"Granting the hole flips it to FAIL" was performed by a manual edit. A control
CI cannot run is not a control CI has. Wiring the probe up as-is would have installed
precisely the gate this sweep keeps removing: green, with nothing establishing it can
distinguish.
So the control is now a cargo feature.
grant-holeadds region 3 over exactly thedenied range — region 3 is free, since the verified core emits 3–7 disabled — still
through
switch_to_partition, never by hand:OK … denied @0x20008000 (CFSR=0x00000082)FAIL: write to denied 0x20008000 fell through — MPU not enforcingThe denial is now proven caused by the region table, rather than by a bad address, a
stray handler, or an MPU that was never enabled. The CI job runs the control first
and separately, as the other five jobs in this workflow do.
A distinction worth having in the open
The neighbouring Renode gate (
gust_iso.robot) executes the region programmer'scomputation and the seam order —
iso-region-ok,iso-mpu-seam-ok,iso-nointerfere-ok— oncortex-m3over plainMappedMemory. I checked it: itcontains no fault or exception assertion at all.
Computation and enforcement are different claims. Only one was gated. Now both are.
What this does and does not do
It does answer the venue question I raised on synth#1145: gale can execute this
kill-criterion in CI today, not only on a bench. That removes a dependency I had
flagged as "not mine to schedule".
It does not discharge
REQ-OS-MPU-001. That needs synthRQ-62-MEMISOLATEforreal per-tenant regions, and silicon. The fault-containment vs security-containment
boundary in
VER-OS-ISO-001is unchanged — the demo tenant runs privileged and thePPB is not MPU-checked.
rivet validate: PASS (333 warnings, unchanged baseline).Kill-criterion for this gate: the probe passes with
grant-holeenabled.🤖 Generated with Claude Code
https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo