EL0 isolation (P-SEC-3 / ADR-013)

Isolation: “EL0 isolated” is Verified only as the accepted ADR-091 sentence (M6, 2026-09-28; quoted with its limits below). History (2026-09-26 audit + gap list: ADR-086; M1 identity inventory ratchet: ADR-087 ; M2 MMIO high alias: ADR-088 — only the _start stub page remains identity-mapped, the one documented exception per ADR-089; M4 taken-SError evidence class B1 pin + B2-P per ADR-090; M5 umbrella sentence drafted in ADR-091, accepted in writing by the sponsor 2026-09-28 (B3, M6); G1 EL0-reachability walk + G2 EL0 write fault closed: ADR-092; G4 syscall pointers need EL0 permission on every page, closed: ADR-094; ADR-091 revision 3 drops the direct-access-only carve-out, G3 optional only) (ADR-047 / ADR-055; sponsor closure ADR-060). A first mile, a user-TTBR0 read mile, an ASID TLB mile, a standing EL0 context, a TTBR1 private-page first cut, an EL1 high-VA fetch mile, an identity-tear first cut, an identity .text range tear, a live identity .text tear after a high-VA vtable rewrite, an identity .rodata tear, a PAN ID-field probe (pan: present on cortex-a76 / ADR-079) and PAN enable + EL1-vs-EL0 fault (pan: enabled / pan: el1-fault / ADR-080), a documented SVC ABI mile, a libctos CRT mile, a guest ELF PT_LOAD loader mile, a standing-task (normal mode) mile, a thin VFS + memfs mile, a virtio-blk + FAT16 mile, and an OS/app slot first cut exist. Those miles alone are not the product claim. A8 is documented rebuild recipes (what-can-run.md). A9 is two artifacts + FAT /hello (ADR-030); leftover cross-update / embed-off landed (ADR-032). Product “app hosting is done” is Verified under ADR-048 / ADR-052 (freestanding slots). Do not claim Linux userspace, POSIX or containers, and do not widen “EL0 isolated” past the ADR-091 sentence. Standing enter/leave as a guest sample: apps-today.md. CRT + loader + standing-as-normal: building-or-porting.md.

Direction: ADR-013. TTBR1 first cut: ADR-016. EL1 fetch mile: ADR-017. Identity-tear first cut: ADR-018. Identity .text range tear: ADR-019. Live .text tear: ADR-020. Identity .rodata tear: ADR-025. Identity .data tear: ADR-037. Identity heap tear: ADR-038. Leftover identity RAM tear: ADR-049. EL0 entry without VMALLE1: ADR-039. Lower-EL IRQ while standing: ADR-040. IRQ-unmasked default ERET: ADR-041. Isolation leftover wrap: ADR-042. Lower-EL FIQ + SError park: ADR-043. Taken SError QMP attempt: ADR-045. Isolation leftovers decisions: ADR-047. Taken SError hard-stop: ADR-053. Taken SError reopen (still blocked): ADR-081 / ADR-082. PAN enable lock: ADR-054. Umbrella checklist: ADR-055. Sponsor leftovers closure: ADR-060. App hosting claim criteria: ADR-048. PAN capability: ADR-026. SVC ABI: ADR-021 / syscall.md. CRT / libctos: ADR-022. Guest loader: ADR-023. Standing-as-normal: ADR-024. Thin VFS + memfs: ADR-027. Threat model: security.md. Code: src/el0.rs, src/syscall.rs, src/libctos.rs, src/loader.rs, src/vfs.rs, libctos/, src/asid.rs, src/ttbr1.rs, src/teardown.rs, src/pan.rs.

flowchart TD
  EL1["EL1 kernel<br/>TTBR · SVC · VFS"]
  EL0["Standing EL0 task<br/>freestanding image"]
  SVC["SVC ABI<br/>exit · uart · yield · fs_*"]
  EL0 -->|"asks"| SVC --> EL1
  EL1 -->|"ERET"| EL0

Standing EL0 + SVC is a Verified mile class. It is not a Linux process; the umbrella claim is only the ADR-091 sentence.

flowchart LR
  M["Verified miles<br/>standing · tears · IRQ/FIQ<br/>PAN ID-field · SError park"]
  L["Limits kept<br/>stock-TCG SError parks · never-yank _start<br/>one core · not side-channel"]
  U["Umbrella “EL0 isolated”<br/>Verified: ADR-091 sentence only<br/>ADR-055 checklist Met"]
  M -.-> U
  L -.-> U

Miles alone are not the umbrella. “EL0 isolated” means only the accepted ADR-091 sentence (M6), never wider.

What exists today

• Kernel runs at EL1 (SPSel = 0).
• One map-window page (paging::EL0_PAGE) can be UXN-clear / PXN for a trampoline or standing payload.
• ERET to EL0 switches to a user TTBR0 (L1_USER, ASID=1) that maps kernel text/rodata + the exception stack + the trampoline window (every 2 MiB those ranges occupy), and omits .data / .bss / heap. The lower-EL handler restores kernel TTBR0 from TPIDR_EL1 before touching kernel data. After identity .data/heap tear, that path is MSR TTBR0 + ISB only — no TLBI VMALLE1 (ADR-039; serial el0: no-vmalle1).
• Dual EL1 ASIDs (1 vs 2) with nG probe pages switch without TLBI VMALLE1 (src/asid.rs).
• A bounded standing user context on that TTBR0: SVC #1 stays at EL0 (el0: standing), user MOVZ runs, SVC #2 restores EL1 (el0: restored). is_active() is true only for that lifetime. That dual-SVC is the ADR-013 probe.
• A standing task (A4 / ADR-024) is the supported path for a loaded freestanding image: the A3 loader maps PT_LOAD, is_active() is true while it runs, yield / uart_write stay at EL0 (el0: task-active), exit restores (el0: task-exit / el0: task-restored). An unexpected lower-EL sync restores fail-closed (el0: restore-fail) instead of parking. That is the ctos process model (ADR-035) — not Linux fork / execve / wait.
• TTBR1 walks are enabled. One kernel-private high page (TTBR1_PRIV) is EL1-only; EL0 load faults. Identity RAM is aliased at va + TTBR1_BASE via cloned RAM tables; EL1 can fetch a real path there and VBAR_EL1 is the high alias. After a high-VA jump, rustc vtables are rewritten to high aliases (ident: reloc) and live identity .text after the boot stub is unmapped (ident: live), plus the dedicated 16 KiB range (ident: range / ident: ok). Identity .rodata is unmapped after a pointer rewrite (ident: rodata / ident: rodata-fault / ident: rodata-high). Identity .data/stacks are unmapped after SP relocate (ident: data). Identity heap is unmapped after high GlobalAlloc VAs (ident: heap). _start / QEMU -kernel stay at 0x4008_0000 (ident: start-stay, ADR-042). Leftover identity frames after the heap are unmapped (ident: ram / ident: ram-fault / ident: ram-high, ADR-049); high twins stay. Never yank _start while -kernel needs that address (ADR-047). PAN ID field is printed (pan: present on -cpu cortex-a76, ADR-079; historical a57 pan: absent); PAN enable + EL1-vs-EL0 fault is Verified (ADR-080).
• Lower-EL AArch64 sync handles SVC (ADR-013 probes #0/#1/#2 plus public ABI #16–#23), a kernel-data IABORT, a kernel-data DABORT, and the TTBR1 private-page DABORT, then returns to EL1t (or stays at EL0 on standing SVC #1 / SYS_YIELD / SYS_UART_WRITE / memfs SVCs). Lower-EL IRQ while standing handles the timer (or other) IRQ, then returns to EL0 (el0: irq, ADR-040); default standing/task ERET clears IRQ mask (el0: irq-default, ADR-041). Lower-EL FIQ while standing is taken when GICC FIQEn is armed (el0: fiq, ADR-043). ADR-045 wires an A-clear standing SError probe (el0: serror-arm / eret_to_el0_serror); QEMU 10 virt TCG (a57 and a76) has no working host inject (ADR-081 / ADR-082), so hello keeps el0: serror-park. Short non-standing trampoline probes stay IRQ-masked. Default standing SPSR still masks FIQ and SError except the dedicated probes.
• Public SVC ABI (syscall.md): exit / uart_write / yield plus memfs fs_* (19–23). A libctos CRT wraps those numbers; a hello payload is copied onto the standing EL0 page (A2) and also parsed as ELF64 PT_LOAD on the guest (A3). A4 runs that loaded image as a standing task until exit. A6 is in-RAM memfs. ABI + CRT + loader + standing-task + memfs miles. App hosting Planned.
• Syscall pointers (ADR-094, G4 closed). Every pointer the kernel copies from EL0 must be EL0-readable (AP[1]=1) on every page. Every pointer it copies to EL0 must be EL0-writable (AP[1]=1, AP[2]=0). Execute-only, kernel-only and unmapped pages return the syscall’s error value, and no byte moves. The loader maps app text+rodata (one R+X page) EL0 read-only + executable (map_el0_text: AP=11, UXN clear, PXN set), so apps can pass their own string literals. Kernel-built probe payloads keep execute-only code and put their data on an EL0-RW NX page. Smoke: el0: sys-ptr denied {kernel-stub,kernel-window,xo-text,write-ro,straddle}, a seven-syscall sweep, el0: sys-ptr ok, and a sysptr-leak-probe build that must print el0: sys-ptr leaked …. ADR-097 (proposed): app text is EL0 execute-only, so a pointer into it now fails the copy-from-EL0 check (xo: sys-read text denied).

Probed miles

Still Planned / decided leftovers (isolation) — ADR-047 / locks ADR-053–ADR-055 / sponsor closure ADR-060

Unprobed stays Unknown. Do not say “EL0 works,” “Linux app host,” or “the kernel moved.” Say “EL0 isolated” only as the accepted ADR-091 sentence (below). The freestanding ADR-048 product claim is Verified separately.

Taken SError research + QMP attempt + hard-stop + reopen (ADR-044 / ADR-045 / ADR-047 / ADR-053 / ADR-081)

Taken lower-EL SError on this smoke machine is deferred / non-goal (hard-stopped) (ADR-053 / ADR-081 / ADR-082 / ADR-047). Research (ADR-044) recommended QMP/nmi; ADR-045 wired the guest A-clear path and attempted QMP — QEMU 10 virt reports machine does not provide NMIs. Re-probed 2026-09-14 (a57) and 2026-09-19 (default a76 + GICv3/virtualization=on/max): same error. Unlock = ADR-081 B1/B2/B3; B1 research ADR-082 (no shippable pin 2026-09-19). el0: serror-park stays Verified; A-clear stays dormant prep. Do not claim taken SError Verified on stock QEMU. 2026-09-26 (sponsor D1, ADR-090): the umbrella’s taken-SError evidence class is the B1 pinned-QEMU CI job qemu-nmi-pin (unconditional, fail-closed bare el0: serror) plus the B2-P one-off Graviton3 KVM run (ADR-085 run 4). ADR-055 §B row 1 is Met on that class; stock TCG still parks.

Umbrella “EL0 isolated” accepted (ADR-091, M6)

Since M6 (2026-09-28) umbrella “EL0 isolated” is Verified, and only as the sentence the sponsor accepted in writing in ADR-091 (B3, 2026-09-28 16:41 CEST). Revision 4 (2026-10-02): the sponsor accepted ADR-091 rev 4 in writing (“I accept ADR-091 rev 4”); only the PAN clause and the code-bytes limit changed. Verbatim, revision 4:

“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. No multi-core / SMP race story (no SMP TLB-shootdown story; syscall pointer checks are a one-core check-then-copy, ADR-094).
• The TCG default smoke machine only. Not a real-hardware claim (the B2-P KVM runs are a reduced one-off profile, ADR-085 / ADR-095).
• Not a speculative-execution or side-channel claim. Not a certification.
• app text is EL0 execute-only; EL1 can still read it (no FEAT_EPAN). ADR-097 moves rodata to the app-hdr page and maps app text EL0 execute-only (still five slots); accepted as ADR-091 revision 4 on 2026-10-02. Because this CPU has no FEAT_EPAN, PAN does not stop EL1 from reading that page, which is why the revision-4 PAN clause says the execute-only app text page is not covered. History: before 2026-10-02 the limit read “EL0 can read its own code bytes” (app text+rodata EL0 read-only + executable, ADR-094). The PAN-held fix is ADR-098.
• Also outside it (ADR-091 non-scope): task-vs-task isolation beyond ASIDs, DMA / IOMMU / EL2, and taken SError on stock QEMU (still parks). Separate evidence (not part of the sentence): ADR-096 probes that an EL0 task on ASID 1 cannot read or write another EL0 task’s page on ASID 2 at the same VA (t2t: ok; one core, TCG, kernel-built tasks).

Correction (2026-09-29): until ADR-098 the “PAN is enabled” clause held at boot but not while the kernel handled EL0 exceptions or after EL0 trips (the boot probe ran before any EL0 trip). ADR-098 fixes it and checks it live; the sentence was unchanged and true again. Update 2026-10-02: revision 4 now says “including while the kernel handles exceptions from EL0” in the PAN clause itself.

Checklist: ADR-055 (§A and §B all Met). Sponsor closure: ADR-060. Do not round single miles into the umbrella, and do not widen the sentence.

Before M6 (kept for history): Umbrella isolation stays Planned / non-claim until checklist. Verified miles vs unmet requirements: ADR-055. Sponsor-facing closure table (locks + reopen gates only): ADR-060. Unmet blockers include taken SError (ADR-053 / ADR-081 / ADR-082), never-yank _start, and umbrella sponsor accept (PAN enable is Met separately via ADR-080). Do not round Verified miles into “EL0 isolated.”