ADR-100)

This is a written threat model for a QEMU virt learning kernel. It is not a certification, not an audit, and not a “secure OS” / “hardened” claim. File presence is not W^X. Image W^X is a separate ledger row that needs a QEMU probe.

Version: v1.76 (2026-10-19). Slice/update of v1.75. Docs only, no code change. Folds the ADR-099 risk and impact table (KVM re-check of the reduced b2-serror profile via GitHub OIDC on a Graviton metal Spot instance) into this threat model as section “KVM re-check via GitHub OIDC (ADR-099)”. Source: ADR-099 on main after PR #157 (merged 2026-10-14), so the table includes the #157 changes (run-scoped sweeper, TEARDOWN-SLOW, ABORTED-after-aws-call, snapshot resource kept out). No posture change for the kernel. Not “secure.” ADR-091 rev 4 sentence unchanged.

Prior v1.75 (2026-10-13). Slice/update of v1.74. ADR-100 (milestone item 5, the SMP race story) writes down the multi-core threat: an inventory of global mutable kernel state (262 statics: 25 static mut, 10 spin-mutex-wrapped, 208 atomics, 19 immutable) and the races each would have on a second core. The riskiest are local-only TLB invalidation (no …IS TLBI anywhere), page-table static mut storage guarded only by a convention lock, fixed ASIDs, global EL0-context / expected-fault flags, and per-core PAN/SPAN/VBAR setup. No posture change: the default kernel is one core and the ADR-091 rev 4 sentence (“-cpu cortex-a76, TCG, one core”) is unchanged. S1 adds an opt-in smp2-probe build that powers one secondary on via PSCI CPU_ON (MMU off, prints its MPIDR, parks; no EL0, no page tables, no shared kernel state beyond one flag word). Any multi-core claim needs a new written sponsor accept. Not “secure.”

Prior v1.74 (2026-10-02). Slice/update of v1.73. Docs only, no code change. The sponsor accepted ADR-091 revision 4 in writing (“I accept ADR-091 rev 4”, 2026-10-02; written in the DSO chat, recorded in the DSO vault, relayed by DSO). ADR-097 (PR #150) is Accepted and merged as 8344797; ADR-098 (PR #151) is on main as 3c47c0c. ADR-091 now carries revision 4: only the PAN clause (“including while the kernel handles exceptions from EL0, and EL1 faults on EL0-readable memory (the execute-only app text page is not covered: this CPU has no FEAT_EPAN)”) and the limit (“app text is EL0 execute-only; EL1 can still read it (no FEAT_EPAN)”, was “EL0 can read its own code bytes”) changed; every other clause is as accepted at revision 3. Threat-model effect: none on the mechanism; the written claim now matches it (no FEAT_EPAN, so EL1 can still read the execute-only app text page; PAN is held during EL0 exception handling). See below. Not “secure.”

Prior v1.73 (2026-09-29). Slice/update of v1.72 (ADR-098 PAN correction, PR #151), which builds on v1.71 (#149 ADR-096). ADR-097 (proposed at the time; merge required sponsor rev 4 written accept; accepted 2026-10-02, see v1.74): EL0 app text is execute-only. Every app’s .rodata moved onto the ELF-header page (app-hdr slot, EL0 RO + NX); .text alone on app-text is mapped EL1 RO / EL0 none / UXN=0. Still five slots. An EL0 load of its own text takes a permission fault, a syscall given a text pointer is refused, rodata still reads and prints, and the inventory still counts the UXN=0 page. Two findings: (1) the CPU has no FEAT_EPAN (ID_AA64MMFR1_EL1.PAN=2), so with PAN set an EL1 load of the XO text page does not fault; the ADR-091 clause “PAN is enabled and EL1 faults on EL0 memory” is therefore not literally true for that page, which is why merge waits for a sponsor rev 4 accept (ADR-091 is not edited). (2) The pre-existing PAN gap found here (PAN clear during EL0 exception handling and after EL0 trips) is split out and fixed by ADR-098 (v1.72); this branch merges it. Leak builds for both are caught.

Prior v1.72 (2026-09-29). Slice/update of v1.70 (#148 M6); v1.71 is ADR-096 (PR #149), numbered before this slice and merged after it. ADR-098 (correction): PAN was not held while the kernel handled EL0 exceptions (SCTLR_EL1.SPAN was 1) or after EL0 trips (return_from_el0 resumed with SPSR.PAN clear). The ADR-080 boot probe ran before any EL0 trip and missed it, so from the ADR-080 enable (and from the M6 accept) until this fix the ADR-091 clause “PAN is enabled” held at boot but not while handling EL0 exceptions. Fixed (SPAN=0 after enable; SPSR.PAN on return) with fail-closed live checks (pan: live-syscall pstate-pan=1 sctlr-span=0, pan: after-el0 …, pan: ok held …) and a negative build that undoes the fix (boot probe still passes; live checks report pan: lost …). Every clause of the ADR-091 sentence is literally true again; the sentence is unchanged.

Prior v1.71 (2026-09-28). Slice/update of v1.70 (#148 M6). ADR-096: a fail-closed task-to-task probe. An EL0 task on the user root (ASID 1) cannot read or write another EL0 task’s private page on the ASID-B root (ASID 2) at the same VA, right after that task ran (no TLBI of the VA in between). A’s root has no leaf for B’s frame. With its own page at that VA, each task sees and changes only its own frame. A leak build that maps B’s frame into A’s root is caught. Evidence next to the ADR-091 sentence, not part of it: the accepted sentence and its non-scope (task-vs-task) are unchanged. Limits: one core; QEMU TCG flushes its software TLB on an ASID change, so this is not a hardware stale-TLB test; two kernel-built tasks, not two loaded apps.

Prior v1.70 (2026-09-28). Slice/update of v1.69 (#147 ADR-095). M6: the sponsor accepted the ADR-091 revision-3 sentence and scope in writing (B3, 2026-09-28 16:41 CEST). ADR-091 is Accepted. Umbrella “EL0 isolated” is Verified, only as that sentence (below), with its limits: one core, the TCG default smoke machine; not a speculative-execution or side-channel claim, not a real-hardware claim, not a certification; EL0 can read its own code bytes; no multi-core race story. Docs only: no code change; the M6 PR CI run is the re-probe. (Revision 4, 2026-10-02: the limit and the PAN clause were reworded, see v1.74.)

Prior v1.69 (2026-09-28). Slice/update of v1.68 (#146 ADR-094). ADR-095 (G3): the ADR-085 B2-P procedure was re-run on main 8107578 on an AWS Graviton3 c7g.metal under KVM and passed (el0: serror / b2: taken, fail-closed smoke, attempt 1). The B2-P leg of the ADR-090 evidence class now also holds on the post-M1/M2 boot path. No posture change: reduced b2-serror profile, one-off, not CI. Umbrella still Planned / non-claim; ADR-091 is still Draft (B3 not Met).

Prior v1.68 (2026-09-27). Slice/update of v1.67 (#144 ADR-092). ADR-094 closes G4. Syscall user pointers now need EL0 read (copy from EL0) or write (copy to EL0) permission on every page. App text+rodata is mapped EL0 read-only + executable. Probes: refused kernel-stub / kernel-window reads, refused xo-text / RO writes, a straddle, a seven-syscall sweep, and a sysptr-leak-probe build that must fail. G1 allowlist unchanged. Umbrella still Planned / non-claim; ADR-091 revision 3 is still Draft (B3 not Met); G3 is optional.

Prior v1.67 (2026-09-26). Slice/update of v1.66 (#143 ADR-091). ADR-092 (sponsor option (b)): a fail-closed EL0-reachability walk over kernel / user / ASID-B TTBR0 and TTBR1, plus an EL0 store permission-fault probe, close ADR-091 gaps G1/G2. New gap G4: syscall copy helpers skip the EL0 permission check. Umbrella still Planned / non-claim.

Prior v1.66 (2026-09-26). Slice/update of v1.65 (#142 ADR-090). ADR-091 (M5, D4) is a draft umbrella sentence and scope, pending the sponsor’s written accept. No posture change. The umbrella stays Planned / non-claim.

Prior v1.65 (2026-09-26). Slice/update of v1.64 (#141 ADR-089). ADR-090 (M4, sponsor D1): the umbrella’s taken-SError evidence class is the B1 pinned-QEMU CI job (now unconditional) plus the B2-P one-off KVM run. Stock TCG still parks. Not the umbrella: the sponsor accept (B3) is still absent.

Prior v1.64 (2026-09-26). Slice/update of v1.63 (#140 ADR-088). ADR-089 (M3, sponsor D2): the _start stub page is the one documented identity exception, the checklist identity row is reworded accordingly and Met on this session’s evidence. Docs only. Still not “EL0 isolated.”

Prior v1.63 (2026-09-26). Slice/update of v1.62 (#139 ADR-087). ADR-088 (M2, sponsor D3): GIC / PL011 / virtio-mmio are reached only through three EL1-only, XN TTBR1 Device blocks (6 MiB); the identity 1 GiB MMIO block is cleared from kernel and ASID-B TTBR0. The fail-closed inventory now allows only the _start stub page (ident: inv k=1 u=1 a=1 leaks=0). Still not “EL0 isolated.”

Prior v1.62 (2026-09-26). Slice/update of v1.61 (#138 ADR-086). ADR-087 (M1): the RAM-side identity leftovers (low RAM below the image, the RO+X image padding tail, the pre-heap frame) are unmapped from kernel and user TTBR0. A committed fail-closed walk over kernel / user / ASID-B TTBR0 allows only the MMIO 1 GiB Device block and the _start stub page, and a planted identity page is caught (in-boot + inv-leak-probe kernel). The EL1-executable identity surface while EL0 runs shrinks from ≈ 1 MiB + 1 page to the single stub page. Still not “EL0 isolated.”

Prior v1.61 (2026-09-26). Slice/update of v1.60 (#137 ADR-085). ADR-086: sponsor unlocked the umbrella item. The ADR-055/060 checklist audit found every §A mile and PAN enable Verified this session (CI-gated by qemu-smoke.sh). §B is not Met: taken SError is Verified only on opt-in paths (B1 pin, B2-P one-off), while the accepted smoke machine parks. A scratch TTBR0 walker shows five identity ranges left in kernel TTBR0 (MMIO 1 GiB Device block, low RAM below the image, _start stub page, image padding tail RO+X, __kernel_end page) and two in user TTBR0 (stub + tail, EL1-only). No umbrella accept exists. Still not “EL0 isolated.”

Prior v1.60 (2026-09-26). Slice/update of v1.59 (#136 ADR-084). ADR-085: sponsor B2-P. On an AWS Graviton3 c7g.metal (eu-north-1, Spot), QEMU -accel kvm with patch 0002 set serror_pending via KVM_SET_VCPU_EVENTS, and the opt-in b2-serror profile took the lower-EL SError while standing at EL0 (el0: serror / b2: taken; fail-closed smoke PASS). That makes B2 Verified (opt-in, one-off paid run, not CI). Real hardware also exposed a latent TCR_EL1.TG1 reserved-encoding bug that TCG masked; it is fixed (TG1=4K). Stock distro QEMU still parks. B1 pin unchanged. Still not “EL0 isolated”, not “runs on real hardware” beyond the b2 profile, not “secure.”

Prior v1.59 (2026-09-25): Slice/update of v1.58 (#130 ADR-083). ADR-084: sponsor B2 spike (different runner/accelerator) on free GitHub-hosted runners is blocked — no arm64 KVM/HVF/WHPX; stock TCG still machine does not provide NMIs. B2 stays Planned / blocked on a sponsor decision. B1 opt-in pin (ADR-083) unchanged. Stock distro QEMU still parks. Still not “EL0 isolated” / BSD sockets / Linux/containers. Not a v2 model and not “secure.”

Prior v1.58 (2026-09-19): Slice/update of v1.57 (#129 ADR-082). ADR-083 ships opt-in pinned QEMU v10.0.0 + TYPE_NMI→async SError; CTOS_QEMU + CTOS_REQUIRE_TAKEN_SERROR=1 Verifies taken el0: serror. Stock distro QEMU still parks. Default CI/Docker stay on distro QEMU. Keep PAN enable + N1–N5 + samples. Still not “EL0 isolated” / BSD sockets / Linux/containers. Not a v2 model and not “secure.”

Scope

In: the ctos guest as built for qemu-system-aarch64 -machine virt (EL1, identity map + TTBR1 private page + TTBR1 RAM alias for EL1 fetch, PL011, GICv2, CNTP, first-fit heap, cooperative EL1 tasks, a deliberate EL0 first mile and a bounded standing context). The git repo (no secrets).

Out: Raspberry Pi or other boards, a second ISA, multi-tenant hosting, secure / measured boot, physical side channels, a hostile hypervisor. Networking: N1 ARP + N2 ICMP ping + N3 minimal UDP + N3.x EL0 UDP DNS SVC + N4 EL0 net SVCs + N5 thin TCP + N5.x EL0 TCP echo SVC (ADR-066 / ADR-067 / ADR-070 / ADR-071 / ADR-068 / ADR-074 / ADR-076); not a BSD sockets / TCP product stack.

QEMU and the host are the TCB we do not defend against. If the emulator or the CI runner is hostile, the guest cannot recover.

Assets

Asset	Why it matters	Where it lives
Kernel integrity	Text, `VBAR_EL1` table, page tables. Corruption ends the learning probe.	EL1 identity map (`0x4008_0000`…`__kernel_end`) plus TTBR1 RAM alias / high VBAR (ADR-017)
Secrets-none	Credentials in git would be a host/CI incident, not a guest exploit.	Repo policy (NFR-10). The guest stores no keys.
Availability of the virt guest	Smoke / `cargo test` must still print markers and exit. A silent lockup hides bugs.	UART, GIC, timer, fail-closed `scripts/qemu-smoke.sh`
Heap + cooperative stacks	Writable RAM used by `Box`/`Vec` and M9 workers. Execute-from-here is the W^X question.	Frame pool after `__kernel_end` (ADR-012)
Linker stacks (SP_EL0 / SP_EL1 / fatal)	Thread, first-level exception, and nested-fatal stacks. Live pages are RW+NX with `.data` (ADR-015).	Linker holes after `.bss` (ADR-005)
Guard pages (when mapped invalid)	4 KiB unmapped holes below each linker stack. Downward overflow should become a translation fault, not a silent smash of the previous image bytes.	`__stack_guard` / `__exc_stack_guard` / `__fatal_stack_guard` (ADR-014)
EL0 trampoline + bait + standing context	One UXN-clear map-window page and a kernel `.data` bait. Proves enter/return, “cannot execute kernel data,” “cannot read kernel `.data`,” and a bounded standing dual-SVC. Not POSIX, not isolation.	`paging::EL0_PAGE` + `KERNEL_DATA_BAIT` + `L1_USER` (ADR-013)
TTBR1 private page	One EL1-only high page. Proves EL0 cannot load it. Not a relocated kernel.	`paging::TTBR1_PRIV` (ADR-016)
TTBR1 RAM alias / high VBAR	EL1 can fetch `.text` at `identity + TTBR1_BASE`. `VBAR_EL1` is that alias. Identity `-kernel` stub stays.	`L1_HIGH[1]` → cloned `L2_HIGH_RAM` (ADR-017, ADR-018)
Identity-tear page	One dedicated identity text page unmapped from TTBR0. High twin stays. Not a relocated kernel.	`__ident_tear_*` (ADR-018)
Identity text range	Dedicated 16 KiB identity text range unmapped. High twins stay. Not a relocated kernel.	`__ident_tear_*` 16 KiB (ADR-019)
Live identity `.text`	rustc vtables rewritten to high aliases; live identity `.text` after `_start` unmapped. High twins stay. Not a relocated kernel.	`[0x4008_1000, __text_end)` (ADR-020)
Identity `.rodata`	Identity `.rodata` unmapped after a pointer rewrite. High twin stays. Not a relocated kernel.	`[__rodata_start, __ident_tear_start)` (ADR-025)
Identity `.data` / stacks	Identity `.data`/`.bss`/linker stacks unmapped after SP relocate + pointer rewrite. High twin stays. Not a relocated kernel.	`[__data_start, __kernel_end)` (ADR-037)
Identity heap	Identity heap unmapped after high `GlobalAlloc` VAs. High twin stays. Remaining frames after the heap stay identity-mapped. Not a relocated kernel.	64 KiB first-fit pool (ADR-038)
PAN capability + enable	`ID_AA64MMFR1_EL1.PAN` printed; PSTATE.PAN enabled on cortex-a76; EL1-vs-EL0 fault. Historical a57 enable non-goal (ADR-047).	`src/pan.rs` (ADR-026 / ADR-079 / ADR-080)
Remaining isolation gaps	Shared boot-stub text stays by decision (`ident: start-stay`; never yank `_start`). PAN enable Verified on cortex-a76 (ADR-080). Leftover identity RAM torn (`ident: ram`, ADR-049). Taken lower-EL SError hard-stopped* on stock QEMU after ADR-081 re-probe (`el0: serror-park`; A-clear dormant prep; ADR-053 / ADR-081 / ADR-082); Verified only under the B1 opt-in pin (ADR-083); B2 free-runner spike blocked (ADR-084).	User TTBR0 + ASID + TTBR1 + torn live `.text` / `.rodata` / `.data`/stacks / heap / leftover frame RAM + EL0 entry without `VMALLE1` + lower-EL IRQ while standing + default IRQ-unmasked ERET + lower-EL FIQ while standing + SError park honesty + A-clear dormant prep + start-stay honesty + PAN enable + SVC ABI; umbrella “EL0 isolated” Verified only as the accepted ADR-091 sentence (M6; checklist ADR-055 all Met); sponsor closure table ADR-060
SVC ABI (exit / uart_write / yield)	Documented numbers 16–18. `uart_write` rejects a kernel `.data` pointer and a TTBR1 / non-canonical alias. Not Linux. Not app hosting.	`src/syscall.rs` (ADR-021)
`libctos` CRT	Wrappers + `_start` CRT. Hello payload copied onto the standing EL0 page. Must not issue SVC #0–#2.	`libctos/` + `src/libctos.rs` (ADR-022)
Guest ELF PT_LOAD loader	Guest parses embedded ELF64 `ET_EXEC`, maps `PT_LOAD` into the user map-window, `ERET`s to `e_entry`. Rejects `PT_INTERP` and W+X. Not a Linux ABI.	`src/loader.rs` (ADR-023)
Standing EL0 as normal mode	Loaded image stands until `SYS_EXIT`. `is_active()` is a task flag. Unexpected lower-EL sync restores fail-closed. Not a process table.	`src/el0.rs` (ADR-024)
Thin VFS + memfs	Named heap buffers. Create / open / read / write / close. User path/I/O pointers must be user-mapped and kernel-mapped. Not POSIX.	`src/vfs.rs` (ADR-027)
virtio-net (N1 ARP + N2 ICMP + N3 UDP + N5 thin TCP + N3.x/N4/N5.x EL0 SVC)	Guest programs a virtio-mmio net DMA master for ARP, ICMP echo, one UDP datagram, then one thin TCP active-open + payload vs QEMU SLIRP/`guestfwd`. EL0 uses tiny SVCs only (kernel owns NIC), including quiet TCP echo. Not a BSD sockets / TCP product.	`src/virtio.rs` + `src/syscall.rs` (ADR-066, ADR-067, ADR-070, ADR-071, ADR-068, ADR-074, ADR-076)
virtio-blk + FAT16	Guest programs a virtio-mmio DMA master. Image is host-built FAT16. Guest may write/create small root files (ADR-050), grow a file across a cluster boundary (ADR-064), list root names (ADR-056), delete a root file (ADR-057), create a root directory (ADR-073), and create one nested subdirectory + empty-rmdir (ADR-077). Same VFS `open`/`write`/`readdir`/`unlink`/`mkdir`/`rmdir` behind prefix mounts (ADR-058). Not a trusted disk.	`src/virtio.rs` + `src/fat.rs` + `src/vfs.rs` (ADR-028, ADR-050, ADR-056, ADR-057, ADR-058, ADR-064, ADR-073, ADR-077)
OS/app slots	Host kernel ELF + published app ELF. Guest reads FAT `/hello` and maps `PT_LOAD`. A2–A4 use the same file (no embed). Cross-update is a host two-boot probe. Not a trusted disk.	`src/slot.rs` (ADR-030, ADR-032)
Console / sensors	PL011 is how we see whether a probe ran.	Device MMIO `0x0900_0000`

Adversaries

Adversary	In scope?	Notes
Buggy kernel code (wrong store, bad `unsafe`, execute-from-heap, stack smash)	Yes	Primary adversary today. Mitigate with PXN on heap/frames, unmapped linker-stack guards, minimize `unsafe` (NFR-01), fail-closed smoke.
Malicious EL0 (standing or trampoline task executing kernel data or escalating via a bad map)	Named; standing context is bounded	First mile + user-TTBR0 read mile + ASID TLB mile + standing dual-SVC + standing task until `exit` + TTBR1 private page + EL1 high-VA fetch + a documented SVC ABI exist. Since M6 the umbrella “EL0 isolated” is Verified only as the accepted ADR-091 sentence (one core, TCG default smoke machine; not speculative-execution / side-channel, not real hardware, not a certification). The boot-stub identity page stays by decision (`ident: start-stay`, ADR-089); stock-QEMU taken SError still parks (`el0: serror-park`). Product freestanding hosting Verified under ADR-048/052; not Linux/POSIX/containers (ADR-048 / ADR-052).
Compromised device tree	Mostly out	M7 does not walk FDT. DTB sits at RAM base below the image. A hostile DTB is a QEMU/host problem until a walker exists; then it becomes an input-validation ADR.
DMA / virtio devices	Named; bounded	A7 programs virtio-mmio blk (one queue, poll `used.idx`, identity-PA DMA). N1–N3/N5 program virtio-mmio net (RX+TX queues, same poll/DMA pattern) for ARP, ICMP echo, one UDP datagram, then thin TCP (ADR-066 / ADR-067 / ADR-070 / ADR-074). QEMU is still TCB. A malicious virtio device is out (hostile hypervisor). No BSD sockets / TCP product.
Hostile QEMU or CI host	Out	Hypervisor / runner is trusted. Repo-secret leak is a host control (`.gitignore`, review), not a guest mitigation.
Network attacker	Named; bounded (link only)	N1–N3/N5 attach QEMU user netdev (+ N5 `guestfwd` echo) + guest virtio-net for ARP + ICMP + one UDP datagram + thin TCP (ADR-066 / ADR-067 / ADR-070 / ADR-074). No BSD sockets / TCP product. QEMU SLIRP/`guestfwd` is still TCB. Hostile on-wire peers beyond this probe are out of product scope.

Trust boundaries

[ host / QEMU / CI ]  --trusted config--  [ virt guest ]
                                              |
                                         EL1 kernel  ← TCB today
                                              |
                                         EL0 first mile + standing  ← entered / stood / left
                                              |                       (not a POSIX user)
                                         EL0 isolation    ← Verified only as the ADR-091 sentence (M6)

EL1 now. Page tables distinguish execute (RO+X text vs RW+NX data/stacks/heap vs Device XN), write (AP[2] on text), and presence (guard holes).
EL0 first mile + user TTBR0 + ASID TLB + standing + standing-as-normal + TTBR1 first cut + EL1 high-VA fetch + identity-tear first cut + identity .text range tear + live .text tear + identity .rodata tear + EL0 entry without VMALLE1 + lower-EL IRQ while standing + IRQ-unmasked default ERET + lower-EL FIQ while standing + SError park honesty + PAN ID-field + SVC ABI + libctos CRT + guest PT_LOAD loader; umbrella “EL0 isolated” = the ADR-091 sentence only (M6). Lower-EL AArch64 sync is taken (SVC / IABORT / DABORT). Lower-EL IRQ while standing is taken and returns to EL0 (el0: irq); default standing/task ERET clears I (el0: irq-default); lower-EL FIQ while standing is taken when FIQEn is armed (el0: fiq); SError park honesty (el0: serror-park); ADR-045 A-clear + QMP attempt (inject failed). Short non-standing trampoline probes stay IRQ-masked. Dual ASID without TLBI VMALLE1 is a probed mile (asid: ok). Standing/EL0 trampoline also switches without TLBI VMALLE1 after identity .data/heap tear (el0: no-vmalle1). Standing dual-SVC flips is_active(). A standing task runs a loaded image until exit (el0: task-ok); unexpected sync restores fail-closed (el0: restore-fail). TTBR1 private page is EL1-only (ttbr1: ok). EL1 can fetch a real path from the high RAM alias (ttbr1: el1 exec); VBAR_EL1 is that alias (ttbr1: vbar). A 16 KiB dedicated identity text range is unmapped (ident: range); live identity .text after _start is unmapped after a vtable rewrite (ident: reloc / ident: live); identity .rodata is unmapped (ident: rodata); identity .data/stacks are unmapped (ident: data); identity heap is unmapped (ident: heap); _start stays (ident: start-stay); leftover identity RAM after the heap is torn (ident: ram). ID_AA64MMFR1_EL1.PAN is 0 on -cpu cortex-a57 (pan: absent). A documented SVC ABI (svc: ok) is an ABI mile. A linked libctos hello (libctos: ok) is a CRT mile. A guest PT_LOAD (loader: ok) is a loader mile. Standing-as-normal (el0: task-ok) is a mile; product freestanding hosting is Verified separately under ADR-048/052. Umbrella “EL0 isolated” is Verified only as the accepted ADR-091 sentence (M6; PAN enabled on default cortex-a76 per ADR-080; taken SError on the ADR-090 evidence class while stock QEMU still parks; never yank _start; leftover RAM torn via ADR-049). A caught load of .data or of TTBR1_PRIV is that mile, not the umbrella by itself.
Repo vs guest. “No secrets in repo” is a host boundary. It does not harden the UART.

PAN enable + EL1-vs-EL0 fault (v1.55)

ADR-080 / #125 mile 2: on default -cpu cortex-a76, MSR PAN + EL1 load of an EL0-accessible page faults (pan: enabled / pan: el1-fault; SPSR.PAN at the fault). Syscall uaccess clears PAN around copies. Umbrella “EL0 isolated” stays non-claim (ADR-055). Taken SError still hard-stopped (ADR-053).

Taken SError reopen re-probe (v1.56)

ADR-081 / #125 mile 3: dated agent-box re-probe on default -cpu cortex-a76 plus GICv3 / virtualization=on / secure=on / max — QMP inject-nmi / HMP nmi still machine does not provide NMIs. FEAT_NMI ≠ SError. KVM absent on this smoke host. Unlock = sponsor B1/B2/B3. Park Verified; A-clear dormant prep. Still not taken Verified / “EL0 isolated.”

Taken SError B2-P on real arm64 + KVM (v1.60)

ADR-085 (2026-09-26): a paid one-off run on AWS c7g.metal (Graviton3, CPU: All CPU(s) started at EL2, /dev/kvm=present). The SError source is KVM’s virtual SError (HCR_EL2.VSE), which the host requests through KVM_SET_VCPU_EVENTS{serror_pending=1} (QEMU v10.0.0 + 0001 + 0002, inject-nmi on the el0: serror-arm cue). The guest runs natively. Run 4 console: el0: standing / el0: serror / el0: restored / b2: taken / b2-kvm-smoke: PASS ... accel=kvm. Threat-model relevance: the lower-EL SError vector, standing-EL0 A-clear window and restore path now have evidence on real Neoverse-V1 hardware, not only TCG. Real hardware also found TCR_EL1.TG1=0b00 (reserved), which broke every TTBR1 high-VA walk on Graviton3; it is fixed to 4K. Limits: opt-in profile only (no GIC/timer/virtio/FAT under KVM), no CI gate, no host-side ioctl trace. Umbrella “EL0 isolated” still a non-claim.

Taken SError B2 free-runner spike (v1.59)

ADR-084 (2026-09-25): sponsor chose ADR-081 B2 — a genuinely different runner/accelerator, not the B1 pin. Free GitHub-hosted runners were probed (runs 36193423604 / 36193613972): arm64 Linux kvm [1]: HYP mode not available / /dev/kvm absent; macOS arm64 HVF HV_UNSUPPORTED; Windows arm64 no VT / WHPX disabled; x86 /dev/kvm cannot run an AArch64 guest. Stock TCG on those runners still machine does not provide NMIs. The honest B2 source would be a KVM virtual SError (serror_pending) injected by a small VMM on real arm64 hardware — Planned / blocked on a sponsor choice (self-hosted arm64 KVM runner, paid bare metal, or wait). No new Verified. Threat surface unchanged; still not “EL0 isolated.”

Residual identity surface + umbrella audit (v1.61)

ADR-086 (2026-09-26). Threat-model relevance of the residual identity map: EL0 cannot touch any of it (every leaf is EL1-only, el0=false). The EL1-side exposure is: (1) an identity RO+X padding tail (≈ 1 MiB, no image content) and the stub page stay executable at EL1 through TTBR0, including while EL0 runs (user TTBR0 keeps both), which widens the EL1 gadget/ret2 surface through low VAs; (2) the MMIO block and two small RW RAM ranges stay reachable at EL1 through identity VAs, so a stray EL1 pointer into low VAs still hits memory instead of faulting. Mitigation plan: M1 ratchet + RAM-side tears, M2 MMIO high alias, M3 stub policy (sponsor D2). Taken SError evidence class is a sponsor decision (D1). Umbrella stays non-claim.

Identity inventory ratchet (v1.62)

ADR-087 (2026-09-26). Residual identity after M1: I1 MMIO block (EL1 RW, XN, Device; kernel + ASID-B only) and I3 _start stub page (EL1 RO+X; kernel + user + ASID-B). The ratchet turns “what we tore” into “what is still mapped”, so a regression that re-maps any identity page fails CI. Found while building it: the ADR-020/025 .rodata pointer rewrite silently relocated the allowlist constants themselves (compare physically). M2 removes I1; I3 stays as the one documented exception (sponsor D2).

MMIO high alias (v1.63)

ADR-088 (2026-09-26). Threat-model effect: a stray EL1 pointer into low VAs < 0x4000_0000 now faults instead of touching a device, and the device surface reachable at EL1 shrinks from a 1 GiB identity hole to three 2 MiB TTBR1 blocks. Residual identity: the _start stub page (EL1 RO+X) in kernel / user / ASID-B TTBR0, the documented exception (sponsor D2). B2-P KVM evidence predates this boot-path change.

`_start` stub identity exception (v1.64)

ADR-089 (2026-09-26). The residual identity page is EL1 RO+X (never EL0-accessible) in kernel / user / ASID-B TTBR0; it holds _start and the identity copy of the vectors. Any additional identity leaf fails CI. A possible later narrowing (drop it from user TTBR0 only) is noted, not decided.

Taken-SError evidence class (v1.65)

ADR-090 (2026-09-26). Threat-model effect: the lower-EL SError vector path (standing EL0, PSTATE.A clear) is exercised on every push/PR by a patched-QEMU TCG job; it is no longer opt-in. What this evidence does not show: RAS/hardware error semantics, SError on stock QEMU, or a CI-gated real-hardware run (B2-P was one paid run on a reduced profile at 159b178).

Umbrella accept draft: scope and non-scope (v1.66)

ADR-091 (2026-09-26, Draft). If accepted, the umbrella would cover only the architectural EL0→kernel page-table / exception-level boundary on the default QEMU TCG machine (one core). It explicitly excludes speculative execution / side channels (no KPTI: TTBR1 stays mapped EL1-only while EL0 runs), real hardware, multi-core, task-vs-task isolation beyond the ASID mile, DMA/IOMMU and EL2. Gaps recorded for the sponsor: no exhaustive EL0-permission walk (G1), no EL0 write probe (G2).

EL0 reachability + EL0 write fault (v1.67)

ADR-092 (2026-09-27). Threat-model effect: the EL0 attack surface is now enumerated rather than assumed. While an app stands, the only EL0-reachable pages are its header, text and stack slots (3 pages per shared window root); at rest there are none; nothing in TTBR1 is EL0-reachable. Any new EL0 leaf outside five allowlisted slots, or backed by kernel frames, fails CI. EL0 stores to kernel data fault. Open (G4): the kernel’s syscall copy path trusts “mapped in user TTBR0” instead of “EL0 may access”, a confused-deputy route to EL1-only pages mapped in user TTBR0 (the _start stub page; transient EL1-only window pages).

Syscall pointers need EL0 permission (v1.68)

ADR-094 (2026-09-27). Threat-model effect: the confused-deputy route recorded as G4 in v1.67 is closed on the default smoke machine. user_range_ok_max now checks the user leaf’s AP bits on every page in the range: AP[1] for a copy from EL0, AP[1] with !AP[2] for a copy to EL0. So no syscall can make the kernel read a page EL0 cannot read, or write a page EL0 cannot write. That covers the _start stub, kernel-only window pages, EL0 execute-only text and EL0-RO pages. CI gates every pointer-taking syscall (17, 19, 20, 21, 22, 24, 27), and a build without the check must fail. App text is now EL0-readable, the normal model for a shared text+rodata page, and still not writable. Residual: a check-then-copy software rule on one core. No AT S1E0R/W or LDTR/STTR copy, and no SMP TOCTOU story.

Taken SError B2-P re-run on current main (v1.69)

ADR-095 (2026-09-28). Threat-model effect: none on the posture; it removes a staleness caveat on the evidence. ADR-090’s B2-P leg was taken at 159b178, before the RAM-side identity tears (ADR-087), the TTBR1 MMIO alias and identity MMIO tear (ADR-088), ADR-092 and ADR-094. On main 8107578 the b2-serror profile booted natively on Graviton3 under KVM through ident: mmio-high, ident: low/tail/kend, ident: mmio, PAN enable and EL1 fault (Graviton3 reports pan: id=2), and took the KVM virtual SError (KVM_SET_VCPU_EVENTS{serror_pending=1} → HCR_EL2.VSE) at the lower-EL SError vector while standing at EL0. Residual: reduced profile (no GIC / timer / virtio / FAT, no inventory / reach / write / sys-ptr probes under KVM); one-off paid run, not CI; no host ioctl trace; not a real-hardware claim for the default image.

Umbrella “EL0 isolated” accepted (v1.70)

ADR-091 (2026-09-28, Accepted, M6). The sponsor accepted the revision-3 sentence and scope in writing (B3, 2026-09-28 16:41 CEST; sponsor wrote it in the DSO agent chat, DSO relayed it to ctos). Threat-model effect: the umbrella row moves from Planned / non-claim to Verified, and only as the sentence below. Revision 4 (2026-10-02, v1.74): the sponsor accepted ADR-091 rev 4 in writing (“I accept ADR-091 rev 4”); the sentence below is revision 4. Revision 3 differed only in its PAN clause (“PAN is enabled and EL1 faults on EL0 memory”) and in the limit “EL0 can read its own code bytes”:

“On the ctos default smoke machine (QEMU virt, -cpu cortex-a76, TCG, one core), EL0 is isolated from the kernel at the architectural page-table / exception-level boundary: each EL0 task runs on its own TTBR0 with its own ASID; EL0 faults when it reads, writes or executes kernel memory; in every translation table (kernel, user and ASID-B TTBR0, and TTBR1) the only EL0-reachable pages are five allowlisted user slots backed by non-kernel frames, checked fail-closed while a user app runs and at rest; PAN is enabled, including while the kernel handles exceptions from EL0, and EL1 faults on EL0-readable memory (the execute-only app text page is not covered: this CPU has no FEAT_EPAN); lower-EL IRQ and FIQ are taken while EL0 stands; taken lower-EL SError is evidenced by the ADR-090 evidence class; the only identity (VA = PA) mapping left in any TTBR0 is the documented EL1-only _start stub page (ADR-089); and a system call copies from or to an EL0 pointer only if EL0 itself may read (for a copy from EL0) or write (for a copy to EL0) every page in the range. It is not a speculative-execution or side-channel claim, not a real-hardware claim, and not a certification.”

Limits that stay with it: one core; the TCG default smoke machine; not speculative-execution / side-channel; not real hardware; not a certification; app text is EL0 execute-only; EL1 can still read it (no FEAT_EPAN) (ADR-097); no multi-core race story. The ADR-091 non-scope list stands (no task-vs-task isolation beyond ASIDs, no DMA / IOMMU / EL2, stock-QEMU taken SError still parks). No code change: the M6 PR CI run on main plus this change is the one-session re-probe. Older version notes and sections in this file that say “not ‘EL0 isolated’” record the posture at their version.

Task-to-task EL0 isolation probe (v1.71)

ADR-096 (2026-09-28). Threat-model effect: the “malicious EL0 task reads or corrupts another EL0 task” case now has a probe on the page-table/ASID mechanism, not only the EL1-side asid: ok mile. Task B (ASID-B root, ASID 2) stores a sentinel at 0x80007000; task A (user root, ASID 1) then loads and stores the same VA and takes a lower-EL translation fault (FAR = the VA) without seeing B’s value; B’s frame is unchanged; a walk of A’s root finds no leaf for B’s frame. With A’s own frame at the VA, each task reads and writes only its own frame. Markers t2t: … / t2t: ok, fail-closed in scripts/qemu-smoke.sh, plus a t2t-leak-probe build that must be caught. Not part of the ADR-091 sentence (task-vs-task stays in its non-scope; a revision 4 needs the sponsor in writing). Limits: one core; TCG flushes its own TLB on an ASID change, so no hardware stale-TLB claim; kernel-built tasks, not two loaded apps under a scheduler; not side-channel.

PAN held during EL0 exception handling (v1.72, correction)

ADR-098 (2026-09-29). Threat-model effect: PAN is the net for kernel bugs that dereference a user pointer outside the copy helpers. That net was down at the start of every EL0 exception handler and after EL0 trips (until the next copy helper restored PAN), i.e. exactly while the kernel serves EL0. The boot probe (pan: el1-fault) could not see it. Now SCTLR_EL1.SPAN=0 and return_from_el0 sets SPSR.PAN; the smoke checks PAN live inside the loaded app’s SYS_YIELD handler (MRS PAN, calibrated) and after the app exits (an EL1 load of an EL0-readable page faults with SPSR.PAN set). A pan-keep-leak-probe build that undoes the fix is caught. Limits: one core, TCG; one exception type and one post-trip point sampled.

EL0 execute-only app text (v1.73; accepted 2026-10-02)

ADR-097 (2026-09-28; accepted 2026-10-02 as ADR-091 revision 4, “I accept ADR-091 rev 4”; merged as 8344797; at v1.73 it was proposed and merge required that accept). Threat-model effect: a compromised or buggy EL0 app can no longer read its own code bytes (e.g. to harvest gadgets or leak code through a syscall): EL0 loads of 0x80002000 take a lower-EL permission fault (xo: el0-read-text fault … dfsc=perm-l3 got=0x0) and uart_write of a text pointer is refused (xo: sys-read text denied … checks=1). Rodata lives on the app-hdr page (EL0 RO + NX). Still five EL0-reachable slots; the fail-closed walk counts UXN=0 pages as reachable (reach=uxn) and catches an unallowlisted XO plant. What gets weaker in the wording, not in the mechanism: without FEAT_EPAN, PAN does not stop EL1 from reading the XO page (xo: el1-pan text … fault=no … epan=no), so “EL1 faults on EL0 memory” no longer covered every EL0 page; revision 4 words this exactly (“EL1 faults on EL0-readable memory (the execute-only app text page is not covered: this CPU has no FEAT_EPAN)”). PAN fix split out: PAN being clear during EL0 exception handling and after EL0 trips is fixed by ADR-098 (v1.72, merged into this branch); the xo live line echoes its reading (xo: pan live-syscall pstate-pan=1 sctlr-span=0). Leak builds xo-leak-probe / pan-keep-leak-probe are caught. Limits: one core, TCG, not real hardware; live check on hello-libctos only (other apps by build/loader checks).

KVM re-check via GitHub OIDC (ADR-099)

Folded from ADR-099 §7 (risk and impact evaluation, as on main after PR #157) in v1.76. ADR-099 stays the source of truth for the trust and permission policies, preconditions P1–P15 and the workflow; if the two disagree, ADR-099 wins and this section must be re-synced.

Asset and boundary. A GitHub Actions job (.github/workflows/kvm-recheck.yml, manual dispatch only, from main, behind the kvm-pilot environment) assumes one AWS role through GitHub OIDC (no stored keys) and starts one Graviton metal Spot instance that runs the reduced b2-serror profile under KVM, then terminates it. New trust boundary: GitHub’s OIDC token → the AWS role. New assets: the role, the cloud account’s spend, and the public CI log.

Status (2026-10-13 pilot, relayed by DSO; see the honesty ledger). One supervised run: smoke PASS under accel=kvm; the run verdict was red only from a false LEAK (teardown wait too short for metal), fixed by PR #157. Not a recurring check, not a required check.

Impact is “what an attacker or a mistake could cost”. Residual is after the listed mitigations, assuming ADR-099 P1–P15 are met.

#	Threat	Likelihood × impact (before)	Mitigations	Residual risk
1	Another repo, branch, fork or pull request assumes the role	Low × High	Exact `aud` and `sub` (no wildcard); environment with required reviewers and main-only branch policy; fork PRs get a different `sub` and no id-token for secrets	Low. Depends on the exact `sub` being right (P14) and the environment existing first (P5).
2	A PR edits the workflow to abuse the role	Medium × High	Dispatch runs only the default-branch file; guard refuses any ref but `main`; environment gate; `enforce_admins` is on	Low–Medium. `main` requires no approving review (observed), so the control is the sponsor merging by convention. DSO may ask the sponsor to require one review on `main` or a code-owner rule for `.github/workflows/`.
3	Role is over-permissioned (miner, wrong instance type, other region)	Medium × High	Conditions on instance type, Spot market, IMDSv2, tags and region; pinned image/subnets/SG; 1 h session; no IAM, no PassRole; Spot quota; budget alarm	Low. IAM conditions are untested until the pilot (P13).
4	Tag spoofing (a resource tagged `project=ctos` to dodge the sweeper, or the terminate scope abused)	Low × Low	Tags only at creation (`CreateAction`); terminate only matches tags the role itself applied; the sweeper counts the tag broadly	Low. A person with other credentials could still tag things; out of scope for this role.
5	Privilege escalation through the instance	Low × High	No instance profile, no `iam:PassRole`, explicit Deny on `iam:*`; IMDSv2 required, hop limit 1; no credentials on the box	Low.
6	Secret in user-data	Low × Medium	User-data holds only a commit, a nonce and a timer; no keys, tokens or URLs with secrets	Very low.
7	Identifier leakage in public logs (instance ID, account ID, host name, IP)	Medium × Low–Medium	Account-ID masking; instance IDs masked at creation; only `^CTOSB2:` lines and error codes are printed; no raw console or stderr; identifier guard on repo text	Low. Confirm on the pilot (P15).
8	Leaked running instance (cost, exposure)	Medium × Low	Pre-flight refusal; in-instance `shutdown -h +45` and terminate-on-shutdown; always-run terminate with fresh credentials, by tag; wait for terminated; sweeper gives LEAK; budget alarm	Low. Worst case about $0.40/h until noticed if the runner and the user-data both fail.
9	Console text is forged or replayed	Low × Medium	Per-run nonce and commit in the result line; anchored PASS line; KVM and arch markers; terminate-by-tag so one run’s console is read once	Low. The code under test can print its own PASS (inherent; the commit is recorded and the tested commit must be on `main`).
10	Silent green on a skip or timeout	Medium × High (trust)	Only PASS exits 0; SKIPPED, INCONCLUSIVE, REFUSED, LEAK, TEARDOWN-SLOW, ABORTED-after-aws-call, NOT-RUN are red; guard fails (not skips) on an unset variable	Low.
11	Spot capacity or interruption	High × Low	Multi-AZ retry; honest SKIPPED / INCONCLUSIVE; no on-demand fallback	Accepted: the check is sometimes unavailable.
12	Third-party action supply chain (`configure-aws-credentials`, `checkout`)	Low × High	Pin by full commit SHA before enabling (P12); `permissions: {}` at top level; the job only gets `id-token: write` and `contents: read`	Low–Medium until pinned.
13	Supply chain on the instance (apt, the rustup install script, git clone, QEMU source)	Medium × Low	QEMU is built from the pinned v10.0.0 source plus the repo’s patches; the repo is cloned at a commit already on `main`; the instance holds no credentials, has no ingress, IMDSv2 hop limit 1, and lives under an hour	Low. Open egress remains (needed for apt/rustup/git).
14	Repo rename or transfer (subject reuse by a new owner)	Low × High	The immutable subject (owner and repo IDs) is what the trust policy pins	Low once P14 is confirmed.
15	Cost runaway	Low × Low	Cost-cap guard; MaxPrice; lifetime; concurrency 1; budget alarm	Low; about $0.33 worst case per run [estimate].
16	CloudTrail off, so no audit trail	Unknown × High	Condition (a) is a hard precondition before the role is created or used	P1 met 2026-10-13 (multi-region trail, DSO-verified).
17	Unprotected environment auto-created by the workflow’s first reference	Medium × High	P5: create the environment with protections first; order matters	Low if the order is followed.
18	Unknown account facts (Spot service-linked role, quota, EBS default key)	Medium × Low	P8; pilot; any new permission goes to the sponsor, not added silently	Low.
19	Credential rule 4 is only relaxed for this role	Low × Medium	One role, one repository, one environment, no stored key, 1 h tokens; the exception record is referenced in the enabling PR (P10)	Low. Any second role or a schedule needs its own approval.

Not claimed here: the default image, real-hardware boot of the default image, or anything beyond the reduced b2-serror profile on one KVM host per run.

Non-goals

Not a certified secure OS (no Common Criteria, no PSA, no “hardened”).
Not side-channel complete (no cache/timing/Spectre story; QEMU TCG is the wrong lab).
Not a product “the kernel is W^X” sentence. The identity image on this virt guest is RO+X / RW+NX with WXN (ADR-015). Future mappings are not automatically covered. Guard pages remain holes.
Not ASAN / canaries / heap-stack guards. Coop worker stacks have no unmapped holes. Overflow there is still image-adjacent PXN RAM.
Not secure boot, PAN enable on historical cortex-a57 (non-goal on that CPU, ADR-047; enable Verified on cortex-a76 / ADR-080), or a fully torn-down identity map (ADR-020/025/037/038/049 unmap live .text / .rodata / .data+stacks / heap / leftover frame RAM; _start stays at 0x4008_0000 by decision).
Not multi-core. Every isolation claim is one core (ADR-091 rev 4). The ADR-100 smp2-probe secondary bring-up is a smoke, not SMP support.

Mitigations mapped to probes

Mitigation	Probe	Ledger
Secondary CPU powered on, parked, never runs kernel state or EL0 (ADR-100 S1, opt-in)	`smp2-probe` under `-smp 2`: `smp: secondary up mpidr=0x0000000080000001` + `smp: ok cpu1 … parked`; `-smp 1` negative must print `smp: cpu1 missed`; default run must show no `smp:` line	Verified locally 2026-10-13 + this PR’s non-required CI job. Not SMP support.
Threat-model v1.23 written	Read this file	Verified (file + review). Still no “secure OS”.
Device MMIO XN (L1 block 0)	`pxn_for(0x0900_0000) == Some(true)`	Covered by the W^X tests when they run.
Heap + coop stacks PXN	Serial `wx: ok`; `#[test_case]` flags + execute-from-heap IABORT	Verified: 2026-09-10 cloud `qemu-smoke` (honesty ledger).
Kernel text still executable	`is_executable(0x4008_0000)`	Same W^X probe.
Execute-from-writable heap forbidden	Armed permission IABORT → `wx: nx heap` then `wx: ok`	Fail-closed in `scripts/qemu-smoke.sh`.
Linker-stack guard holes	Serial `guard: fault` / `guard: ok`; store to `__stack_guard`	Verified: 2026-09-10 cloud `qemu-smoke` (honesty ledger).
Minimize `unsafe`	Review (NFR-01). Count is not a proof.	Policy.
Fail-closed smoke	`scripts/qemu-smoke.sh` greps + `force-fail` exit ≠ 0	NFR-04 / NFR-05.
No secrets in repo	Policy + `.gitignore` (including `.obsidian/`)	Host control.
IRQ least privilege	IRQ path does not allocate or `yield_now`	Convention. Ratchet if it fails twice.
EL0 entered and returned	Serial `el0: svc` / `el0: ok`; `#[test_case]`	Verified first mile — not isolation.
EL0 cannot execute kernel data	Serial `el0: nx kernel`; lower-EL IABORT	Verified first mile.
EL0 cannot read kernel `.data`	Serial `el0: no kernel read`; user TTBR0 omits `.data`	Verified read mile. One mile; alone it is not the ADR-091 umbrella claim.
ASID isolation (no `VMALLE1`)	Serial `asid: dual` / `asid: conflict` / `asid: ok`	Specific mile. One mile; alone it is not the ADR-091 umbrella claim.
Task-to-task EL0 isolation (ADR-096)	Serial `t2t: walk b-frame …` / `t2t: a-read fault …` / `t2t: a-write fault …` / `t2t: same-va …` / `t2t: ok …`; `t2t-leak-probe` build caught; `#[test_case]` `el0_task_cannot_read_or_write_other_task`	Verified (one core, TCG, kernel-built tasks). Not part of the ADR-091 sentence.
EL0 execute-only app text (ADR-097, accepted 2026-10-02)	Serial `xo: live …` / `xo: layout loader …` / `xo: el0-exec ok …` / `xo: el0-read-text fault …` / `xo: sys-read text denied …` / `xo: el1-pan …` / `xo: pan live-syscall pstate-pan=1 sctlr-span=0` / `xo: ok …`; `xo-leak-probe` + `pan-keep-leak-probe` build caught; `#[test_case]` `el0_app_text_is_execute_only`	Verified (one core, TCG); merged as `8344797` after the sponsor accepted ADR-091 rev 4 (2026-10-02).
EL0 entry without `VMALLE1`	Serial `el0: no-vmalle1`; `src/exception.rs` has no `tlbi vmalle1`	Trampoline cut (ADR-039). Not isolation.
Lower-EL IRQ while standing	Serial `el0: irq`	Taken IRQ from EL0 returns to standing (ADR-040). Not isolation.
IRQ-unmasked default ERET	Serial `el0: irq-default`	Default standing/task `ERET` clears I (ADR-041). Short probes stay masked. Not isolation.
Lower-EL FIQ while standing	Serial `el0: fiq`	Taken FIQ from EL0 returns to standing (ADR-043). Not isolation.
SError park honesty	Serial `el0: serror-park`	No working SError inject on virt TCG (ADR-043 / ADR-045 / ADR-081). Taken path deferred/non-goal (ADR-047).
Taken SError QMP attempt	Serial `el0: serror-arm` + QMP log	Guest A-clear path (ADR-045); `inject-nmi` fails on QEMU 10 virt+a76 (ADR-081).
Identity `_start` stay	Serial `ident: start-stay`	Honesty (ADR-042 / ADR-047). Not isolation.
Leftover identity RAM tear	Serial `ident: ram` / `ident: ram-fault` / `ident: ram-high`	Optional mile (ADR-049). High twin stays. Not isolation.
Standing EL0 context	Serial `el0: standing` / `el0: restored`; `is_active()` flips	Specific mile. Not POSIX. Not isolation.
Standing EL0 as normal mode	Serial `el0: task-enter` / `el0: task-active` / `el0: task-exit` / `el0: task-restored` / `el0: restore-fail` / `el0: task-ok`	Loaded image until `exit`. Fail-closed restore. Not isolation.
TTBR1 private page	Serial `ttbr1: el1` / `ttbr1: no el0` / `ttbr1: ok`	First cut (ADR-016).
EL1 fetch from TTBR1 high VA	Serial `ttbr1: el1 exec` / `ttbr1: vbar`	Exec mile (ADR-017).
Identity-tear first cut	Serial `ident: split` / `ident: fault` / `ident: high` / `ident: no el0` / `ident: ok`	First cut (ADR-018). Yank `_start` decided never; leftover RAM torn (ADR-049).
Identity text range tear	Serial `ident: jump` / `ident: range` / `ident: text`	Range cut (ADR-019).
High-VA vtable rewrite + live `.text` tear	Serial `ident: reloc` / `ident: live`	Live `.text` cut (ADR-020).
Identity `.rodata` tear	Serial `ident: rodata` / `ident: rodata-fault` / `ident: rodata-high`	`.rodata` cut (ADR-025).
Identity `.data` / stack tear	Serial `ident: data` / `ident: data-fault` / `ident: data-high`	`.data`/stacks cut (ADR-037).
Identity heap tear	Serial `ident: heap-reloc` / `ident: heap` / `ident: heap-fault` / `ident: heap-high`	Heap cut (ADR-038).
PAN ID field	Serial `pan: id=` / `pan: present`	Capability probe (ADR-026 / ADR-079).
PAN enable + EL1-vs-EL0 fault	Serial `pan: enabled` / `pan: el1-fault`	ADR-080. One mile; alone it is not the ADR-091 umbrella claim.
PAN held during EL0 exceptions + after EL0 trips (ADR-098)	Serial `pan: live-syscall pstate-pan=1 sctlr-span=0` / `pan: after-el0 trips=… mrs-pan=1 el1-load … fault=yes spsr-pan=1` / `pan: ok held boot,live-syscall,after-el0`; `pan-keep-leak-probe` build caught; `#[test_case]` `pan_span_cleared_after_enable`	Verified (one core, TCG). Correction of the ADR-091 PAN clause’s evidence; sentence unchanged.
SVC ABI (`exit` / `uart_write` / `yield`)	Serial `svc: ok`; user buffer + kernel-`.data` / TTBR1-alias reject	ABI mile (ADR-021). Not app hosting.
`libctos` CRT	Serial `libctos: hi` / `libctos: ok` / `libctos: linked`	CRT mile (ADR-022). Not app hosting.
Guest ELF PT_LOAD loader	Serial `loader: mapped` / `loader: ok`	Loader mile (ADR-023). Not a Linux ABI. Not app hosting.
Thin VFS + memfs	Serial `fs: create` / `fs: write` / `fs: read` / `fs: el0` / `fs: ok`	memfs mile (ADR-027). Not POSIX. Not app hosting.
virtio-net ARP (N1) + ICMP ping (N2) + UDP (N3) + thin TCP (N5)	Serial `net: virtio` / `net: mac` / `net: tx` / `net: rx` / `net: ok` + `net: icmp-tx` / `net: icmp-rx` / `net: ping-ok` + `net: udp-tx` / `net: udp-rx` / `net: udp-ok` + `net: tcp-syn` / `net: tcp-est` / `net: tcp-tx` / `net: tcp-rx` / `net: tcp-ok`	ADR-066 / ADR-067 / ADR-070 / ADR-074. ARP + ICMP + one UDP + thin TCP vs QEMU SLIRP/`guestfwd` only. Not BSD sockets / TCP product. Host `-netdev` alone is not the probe.
EL0 net SVC sample (N4)	Serial `libctos: net-hi` / `libctos: net-mac` / `libctos: net-ok` / `netdemo: ok`	ADR-068. SVCs only; kernel owns NIC. Not sockets.
EL0 UDP DNS SVC sample (N3.x)	Serial `libctos: udp-hi` / `libctos: udp-ok` / `udpdemo: ok`	ADR-071. `net_udp_dns` only; DNS is probe bait. Not sockets.
virtio-blk + FAT16	Serial `blk: ok` / `fat: ok` / `fat: write` / `fat: create` / `fat: grow` / `fat: mkdir` / `fat: nested` / `fat: rmdir` / `fat: readdir` / `fat: entries` / `fat: delete`; VFS `/probe`	block + FAT mile (ADR-028) + write depth (ADR-050) + multi-cluster grow (ADR-064) + mkdir (ADR-073) + nested+rmdir (ADR-077) + readdir (ADR-056) + delete (ADR-057). Host `-drive` alone is not the probe. Not POSIX `getdents`/`unlink`/`mkdir`/`rmdir`/write API.
OS/app slot first cut	Serial `slot: fat` / `slot: mapped` / `slot: ok`	Slot mile (ADR-030). A2–A4 load FAT (no embed).
A9 cross-update	Host smoke: same app `sha256` on this OS and `ba6541c`	Leftover (ADR-032). Not “apps update independently.”
RO+NX text/data	Serial `ro: ok`; execute-from-`.data` + write-to-RO-text	Verified: 2026-09-11 cloud `qemu-smoke` (honesty ledger).

Claim gate

A PR may say “threat-model v1.22 exists” after a file read. It may say “heap NX” / “identity image is W^X on this virt guest” only when the honesty ledger has a matching Verified QEMU probe. It may say “linker-stack guard faults” only with a matching translation-abort probe. It may say “EL0 entered and returned,” “EL0 cannot execute kernel data,” “EL0 cannot read kernel .data,” “standing EL0 context,” “ASID isolation,” “TTBR1 private page,” “EL1 fetched from a TTBR1 high VA,” “one identity text page was unmapped,” “a 16 KiB dedicated identity text range was unmapped,” “rustc vtables were rewritten to high aliases,” “live identity .text after the boot stub was unmapped,” “identity .rodata was unmapped,” “identity .data/stacks were unmapped,” “ID_AA64MMFR1_EL1.PAN is 0 on -cpu cortex-a57,” “EL0 issued the documented SVC ABI,” “a program linked against libctos issued that ABI,” “the guest mapped PT_LOAD and ERETed to e_entry,” or “a loaded image stood at EL0 until exit with fail-closed restore,” or “the guest created, wrote, and read a named in-RAM file,” or “the guest programmed virtio-blk and read a known FAT16 file through the thin VFS,” or “the guest wrote FAT16 bytes through the thin VFS,” or “the guest listed FAT16 root directory entries through the thin VFS,” or “the guest loaded a separate app ELF from FAT /hello into user TTBR0,” or “the same published app ELF loaded on this OS and on ba6541c,” or “identity heap was unmapped,” or “standing/EL0 trampoline switches without TLBI VMALLE1,” or “taken lower-EL IRQ while standing returned to EL0,” or “default standing/task ERET enters with IRQ unmasked,” or “_start stays mapped while live image ranges are torn” only for the mile that actually passed.

It may not say “secure OS,” “hardened,” “EL0 works,” “the kernel moved,” “immutable OS,” Linux app host, POSIX host, or container host. It may say the freestanding product app-hosting claim is Verified under ADR-048 when the ledger product row is Verified (ADR-052). It may say “EL0 isolated” only as the accepted ADR-091 sentence, quoted verbatim or pointed to, with its limits (M6). Scoped RO is immutability.md. Unprobed stays Unknown. https://ctos.artof.link HTTPS is Verified (2026-09-11 after #30; see the honesty ledger).

Taken SError research + QMP attempt (v1.25)

Research (ADR-044); implementation attempt (ADR-045): guest A-clear standing path + host QMP inject-nmi. On QEMU 10 virt+-cpu cortex-a57, QMP returns machine does not provide NMIs (no ARM_CPU_SERROR via nmi; FEAT_NMI needs a different CPU/GIC). Park marker remains Verified.

Isolation leftovers decisions + app-hosting claim gate (v1.26)

ADR-047: taken SError = deferred/non-goal on this smoke machine (A-clear dormant prep); PAN enable = non-goal on default cortex-a57; never yank _start; leftover identity RAM torn via ADR-049 (ident: ram*); umbrella “EL0 isolated” stays Planned/non-claim. ADR-048 (at v1.26): A1–A9 first cuts ≠ product “app hosting done”; claim stayed Planned until criteria Met + sponsor accept.

Product app-hosting claim Verified (v1.29)

ADR-048 criteria 1–5 Met; sponsor accept ADR-052. Product freestanding “apps run independently / hosting done” is Verified. Still not Linux userspace, POSIX, glibc/musl, guest OCI/Docker/k8s, “EL0 isolated,” PAN enable, taken SError Verified, immutable-OS marketing, or OTA

Isolation-gap locks (v1.30)

ADR-053: taken lower-EL SError hard-stopped on QEMU 10 virt+cortex-a57 (dated 2026-09-14 re-probe: inject-nmi / HMP nmi → machine does not provide NMIs); park Verified; A-clear dormant prep. ADR-054: PAN enable locked non-goal on default cortex-a57; explicit reopen gate (sponsor CPU + FEAT_PAN + enable+fault ADR). ADR-055: umbrella “EL0 isolated” non-claim until checklist — Verified miles listed; unmet blockers include PAN enable, taken SError, never-yank _start. Still not Guest Linux / containers / immutable-OS marketing..

FAT16 readdir (v1.31)

ADR-056: guest lists FAT16 root dirents as thin-VFS paths (fat: readdir / fat: entries). Not POSIX getdents / opendir. Keep write / /hello / slot: ok. Still not Linux/containers/“EL0 isolated.”

FAT16 delete (v1.32)

ADR-057: guest deletes a FAT16 root file via thin-VFS unlink (fat: delete). Not POSIX unlink / remove. Keep write / readdir / /hello / slot: ok. Still not Linux/containers/“EL0 isolated.”

VFS prefix mounts (v1.33)

ADR-058: guest routes path prefixes through a thin VFS mount table (vfs: mount / vfs: mounts). Not POSIX mount(2) / Linux vfsmount. Keep memfs / FAT write / readdir / delete / /hello / slot: ok. Still not Linux/containers/“EL0 isolated.”

Freestanding sample catalog (v1.34)

Two freestanding EL0 samples on FAT: /hello (hello-libctos, UART+yield) and /fsdemo (fs-libctos, libctos VFS create/open/read/write/close on /memdemo). Catalog docs list both. Not POSIX. Not getdents. Not a reopen of product app hosting.

ADR-060: single sponsor-facing table for taken SError / PAN enable / umbrella “EL0 isolated” / never-yank _start — locks + reopen gates only. Cites ADR-047 / ADR-053 / ADR-054 / ADR-055 / #98. Does not invent Verified. Does not reopen Guest Linux / containers / immutable-OS marketing.

Freestanding FAT-via-VFS sample (v1.36)

Three freestanding EL0 samples on FAT: /hello, /fsdemo (memfs /memdemo), and /fatdemo (fat-libctos, open/read FAT /probe via thin VFS / → FAT16). Catalog docs list all three (ADR-061). Not POSIX. Not getdents. Not a reopen of product app hosting.

FAT16 multi-cluster grow (v1.39)

ADR-064: guest grows a FAT16 root file across a cluster boundary (fat: grow); EL0 fat-libctos chunked SVC write/read-back (libctos: fat-grow). Not POSIX write API. Not exFAT. Keep write / readdir / delete / /hello / slot: ok. Still not Linux/containers/“EL0 isolated.” Track N untouched.

FAT vs memfs read CNTPCT (v1.40)

ADR-065: same-boot CNTPCT pair around FAT /probe read vs memfs /mrprobe read (perf: fat-read / perf: memfs-read / perf: fs-read-delta). Measure-first lab ticks only — not a latency SLA, percent, or product KPI. Keep ADR-051 write pair / fat: ok / Track N untouched. Still not “secure.”

Freestanding cooperative-yield sample (v1.37)

ADR-062: fourth freestanding EL0 sample yield-libctos on FAT /yldemo. Several cooperative yield_now() rounds (libctos: yld-hi / libctos: beat / libctos: yld-ok). Not preemption. Not multi-task EL0. Not a process table. Does not reopen ADR-048/052.

Track N network foundation scope (v1.38)

ADR-063: new Track N (network), separate from A/B. N0 = docs scope. Non-goals locked: TCP/UDP/sockets/DHCP/DNS product, Wi‑Fi, virtio-pci-only foundation, Linux net stack, “has networking” marketing, EL0 net ABI before deeper net miles.

Track N virtio-net first frame (v1.41)

ADR-066: N1 discovers virtio-net, programs RX+TX, TX ARP for 10.0.2.2, RX SLIRP reply (net: virtio / net: mac / net: tx / net: rx / net: ok). Host -netdev user,id=net0 -device virtio-net-device,netdev=net0. I/O surface: virtio-blk and virtio-net are programmed DMA masters. Still not TCP/UDP/sockets/DHCP/DNS/Wi‑Fi/“has networking.”

Track N virtio-net ICMP ping (v1.42)

ADR-067: after N1 ARP, guest TX ICMP echo request to 10.0.2.2 and RX echo reply (net: icmp-tx / net: icmp-rx / net: ping-ok). QEMU args unchanged. Kernel-path only. Still not TCP/UDP/sockets/DHCP/DNS/Wi‑Fi/“has networking.”

Track N EL0 net SVC sample (v1.43)

ADR-068: SYS_NET_MAC (24) + SYS_NET_PING (25); freestanding net-libctos on FAT /netdemo (libctos: net-hi / libctos: net-mac / libctos: net-ok / netdemo: ok). Kernel still owns virtio-net. Still not TCP product / sockets / DHCP/DNS product / Wi‑Fi / “has networking.”

Net-ping CNTPCT (v1.44)

ADR-069: CNTPCT around EL0 net_ping quiet ARP+ICMP (perf: net-ping ticks=<n>). Measure-first lab ticks only — not a latency SLA, percent, or product KPI. Smoke greps the marker prefix (tick values vary). Keep N1/N2/N4 / FAT / slot. Still not TCP/UDP/sockets/“has networking.” Still not “secure.”

Track N UDP transport (v1.45)

ADR-070: after N2 ICMP, guest TX one UDP DNS query to SLIRP 10.0.2.3:53 and RX a matching DNS response (net: udp-tx / net: udp-rx / net: udp-ok). QEMU args unchanged. Kernel-path only this mile. DNS is probe bait, not a guest DNS product. Still not BSD sockets / TCP product / DHCP/DNS product / Wi‑Fi / “has networking / sockets OS.” Still not “secure.”

Track N EL0 UDP DNS SVC (v1.46)

ADR-071: SYS_NET_UDP_DNS (26); freestanding udp-libctos on FAT /udpdemo (libctos: udp-hi / libctos: udp-ok / udpdemo: ok). Quiet kernel-path ARP + UDP DNS to SLIRP 10.0.2.3:53 (same bait as ADR-070). Kernel still owns virtio-net. Still not BSD sockets / TCP product / DHCP/DNS product / Wi‑Fi / “has networking.” Still not “secure.”

UDP DNS path CNTPCT (v1.47)

ADR-072: CNTPCT around EL0 net_udp_dns quiet ARP+UDP DNS (perf: udp-dns ticks=<n>). Measure-first lab ticks only — not a latency SLA, percent, or product KPI. Smoke greps the marker prefix (tick values vary). Keep N1/N2/N3/N3.x/N4 / ADR-069 / FAT / slot. Still not TCP/sockets/DNS product/“has networking.” Still not “secure.”

FAT16 mkdir (v1.48)

ADR-073: guest creates a FAT16 root directory through the thin VFS (fat: mkdir); dirent + empty cluster with . / ... Not POSIX mkdir. Not a directory tree. Not exFAT. No new SVC this mile (EL0 follow-up). Keep write / readdir / delete / grow / /hello / slot: ok / Track N markers. Still not Linux/containers/“EL0 isolated.” Track N / TCP untouched.

Thin TCP N5 (v1.49)

ADR-074: after N3 UDP, guest active-opens TCP to QEMU guestfwd 10.0.2.4:7, sends one payload ctos-tcp\n, requires matching echo (net: tcp-syn / net: tcp-est / net: tcp-tx / net: tcp-rx / net: tcp-ok). QEMU -netdev gains guestfwd=tcp:10.0.2.4:7-cmd:…/tcp-echo-stdio.sh. Kernel-path N5. One connection; no listen/accept. ADR-076 adds EL0 net_tcp_echo (28) + FAT /tcpdemo quiet re-run of the same probe. Still not BSD sockets / TCP product / TLS/HTTP / DHCP/DNS product / Wi‑Fi / “has networking / sockets OS.” Still not “secure.”

FAT16 nested mkdir + empty rmdir (v1.52)

ADR-077: guest creates one nested FAT16 subdirectory (/fdir/nest) and removes an empty directory through the thin VFS (fat: nested / fat: rmdir). Path grammar: flat /name or one /parent/child; deeper → BadPath. Not POSIX mkdir/rmdir. Not arbitrary-depth trees. Not recursive rm. No new SVC this mile. Keep fat: mkdir / write / readdir / delete / grow / /hello / slot: ok / Track N markers. Still not Linux/containers/“EL0 isolated.” TCP CNTPCT untouched.

Thin TCP echo CNTPCT (v1.53)

ADR-078: CNTPCT around the quiet EL0 net_tcp_echo path (perf: tcp-echo ticks=<n>). Measure-first lab probe on QEMU TCG — not a latency SLA, not SPEC, not “has networking.” Chosen surface is EL0 SVC (same as ADR-069/072); kernel N5 net: tcp-ok stays transport proof only. Keep N1–N5 / N5.x / ADR-069/072 / FAT nested+rmdir / samples. Still not BSD sockets / listen-accept / TLS/HTTP. Still not “secure.”

PAN CPU reopen foundation (v1.54)

ADR-079 / #125: sponsor unlock + default smoke CPU -cpu cortex-a76 + Verified ID-field pan: present (ADR-054 gate items 1–2). Historical cortex-a57 pan: absent retained. Enable+fault is ADR-080 (v1.55). Does not unlock taken SError — confirmed blocked in ADR-081. Umbrella “EL0 isolated” stays non-claim. Never yank _start. Still not “secure.”

Keyboard shortcuts

ctos (ctsOS)