lerux is a static Microkit system: protection domains, memory maps, and channels are fixed at image build time. Isolation is therefore a property of the composed SDF + typed IPC contracts, not of a dynamic process model.

This document is the Phase 60 threat model and trust map. It does not claim formal verification of lerux PDs (kernel seL4 is verified; userspace is not).

┌─────────────────────────────────────────────────────────────────┐
│  Platform (highest privilege for devices)                       │
│  serial-driver, virtio-*-driver, genet, emmc2, RTC/timer PDs    │
│  Maps: MMIO, IRQs, DMA rings                                    │
└────────────────────────────▲────────────────────────────────────┘
                             │ rings / device RPC (not app-facing)
┌────────────────────────────┴────────────────────────────────────┐
│  Trusted services                                               │
│  fatfs, serial virtualisers, network virtualisers, copier       │
│  Maps: shared queues; no app DMA share                          │
└────────────────────────────▲────────────────────────────────────┘
                             │ LionsOS queues (`fs_cmd_t`, rings)
┌────────────────────────────┴────────────────────────────────────┐
│  Untrusted / interactive apps                                   │
│  shell, sddf-agent, sddf-program, crash-demo                    │
│  Maps: **no** virtio/net/blk/display DMA; channels only         │
└─────────────────────────────────────────────────────────────────┘

Rule (ADR-003): untrusted apps never map NIC or block DMA. On the device-framework images they speak LionsOS queues. The remaining virtio boards keep the driver DMA off the app.

Rule (ADR-009): untrusted apps never map display MMIO. The live browser shell paints through the graphics client queues. The desk-browser spec names request-server and display-server again; those protection domains are not in this tree.

Channel numbers come from profile [[channel]] manifests; PPC callees outrank callers (qos.md, ADR-006).

Those boards are a phase record. Milestone 17 deleted display-server, request-server, browser-ui, web-content, and the postcard agent. The live browser image is qemu_virt_aarch64_browser_sddf: the shell owns smoltcp and lerux-tls, and paints through the graphics client queues. The desk-browser spec names the Ladybird-shaped set again.

The table below is the phase-72–80 trust map. Those protection domains are not in this tree.

The live residual is that the browser shell owns smoltcp. A later smoke should crash the shell's worker and still complete a filesystem round-trip from another protection domain.

just test-debug still nests crash-demo under debug-handler and logs the fault. Milestone 17 deleted qemu_virt_aarch64_isolation, so there is no follow-on filesystem round-trip after that crash.

Production images stay flat (no debug parent) per ADR-005. Isolation is a property of the protection-domain layout.

Declare with trust_class = "admin" (etc.) in support/profiles/*.toml. Host tooling:

lerux profile list              # shows [trust_class] column
lerux profile audit             # all profiles
lerux profile audit workstation # one profile: PD domains + high-risk edges

The shell holds many RPC ends by design (REPL admin console). High-risk edges flagged by profile audit:

• shell ↔ supervisor — reboot / status
• shell ↔ config-server — policy R/W (see secrets ACL)
• shell ↔ fs-server / net-server — full storage and network RPC
• shell ↔ edit / chat / backup — app launch

Shrink the surface by choosing a lower tier profile, not by runtime capability dropping (Microkit is static). Prefer dev-workstation or net-appliance when bulk apps or a full REPL are unnecessary.

config-server allows Get/List of secrets from shell (operator inspection) but Set/Delete on secret.* is supervisor-only. Non-supervisor writers receive ConfigResponse::Denied. Ordinary keys (hostname, net.*, log.*) remain writable from shell.

Still open: encryption at rest; path-level FS ACL for apps that speak FsRequest directly (any FS client can open /config/secrets/ if it has FS rights — prefer config IPC).

Host-side SHA-256 digests for loader.img (not asymmetric signing, not measured boot):

BOARD=rpi4b_4gb_workstation just image   # writes loader.img + loader.img.sha256
lerux verify-image --board rpi4b_4gb_workstation
lerux deploy --board rpi4b_4gb_workstation --dest /media/$USER/boot
# sha256sum -c build/rpi4b_4gb_workstation/loader.img.sha256   # host cross-check

Trust model: the sidecar is only as strong as the host that wrote it (CI or developer machine). It catches accidental corruption and casual SD-card swap of loader.img without the matching digest. It does not replace secure boot, signed releases, or a hardware root of trust.

Phase 67: optional ed25519 signatures next to the digest (loader.img.sig). Smoke key: support/keys/smoke.ed25519 (not a production secret).

lerux keygen --out support/keys/smoke.ed25519
lerux sign --board qemu_virt_aarch64
lerux verify-image --board qemu_virt_aarch64 --key support/keys/smoke.ed25519.pub --require-sig

Measured boot / TPM / in-guest verification remain out of scope.

MCS budgets and raising shell above bulk apps remain deferred (ADR-006). See qos.md.

1. Reduce shell channel set further — launch apps without giving shell every service end (may need non-PPC notify; see ADR-006)
2. Asymmetric image signing / measured boot — ed25519 is Phase 67; measured boot stays hardware-gated

lerux does not vendor seL4 / Microkit / rust-sel4 trees into git. Security and feature bumps are pin updates followed by rebuild and smoke. This section is the operational runbook.

Invariant: deps/versions.toml [rust].rust_sel4.tag and every sel4* git dep tag in root Cargo.toml must be the same string. lerux fetch clones seL4/Microkit from versions.toml; Cargo resolves rust-sel4 from Cargo.toml.

Document the CVE / advisory ID in the commit message and, if user-facing, a short note in docs/plan.md version table when seL4/Microkit major pins move.

Work on a branch. Prefer one logical bump per PR (e.g. “seL4 16.0.0 → 16.0.1” or “rust-sel4 v5.0.0 → v5.0.1”).

# seL4 and/or Microkit
$EDITOR deps/versions.toml

# rust-sel4: edit root Cargo.toml (all sel4* git tags) AND deps/versions.toml [rust].rust_sel4
# Then refresh the lockfile for git deps:
cargo update -p sel4
# (or cargo update for a broader refresh; review Cargo.lock diff)

# Drop stale checkouts when tags change (fetch re-clones/updates deps/workspace/)
rm -rf deps/workspace/seL4 deps/workspace/microkit   # only if tags moved
just fetch

# Rebuild SDK for boards you care about (CI builds a matrix; local minimum:)
MICROKIT_BOARDS=qemu_virt_aarch64,x86_64_generic,qemu_virt_riscv64,rpi4b_4gb just build-sdk
# Or prebuilt fallback when the pin matches a published SDK:
# just fetch-sdk

If only rust-sel4 moved (kernel/Microkit tags unchanged), SDK rebuild is usually not required; still run just check-pd so PD crates recompile against new bindings.

just check          # host fmt + clippy (lerux-cli, interface-types)
just check-pd       # cross-arch PD clippy (needs SDK)
just test-isolation # Phase 60 isolation smoke (fast security-relevant)
just test-workstation
# Prefer full matrix before merge when seL4/Microkit moved:
# just test-all

CI also runs check → sdk → check-pd + smoke matrix (ci.md).

lerux package build edit --board qemu_virt_aarch64_workstation
lerux package upgrade --all --board qemu_virt_aarch64_workstation
# review support/package-pins.toml; commit with the bump

• Commit pin files + Cargo.lock + any necessary PD/API fixups.
• Push and wait for green CI (smoke matrix is the acceptance bar for kernel/Microkit bumps).
• Rebuild and redeploy field images (just image / lerux deploy) for boards in use; old loader.img files are not hot-patched.
• Optional lab: RPi4 just test-hw after deploy (boards.md).

Copy into the PR or issue body:

## Security pin update

- **Advisory / CVE / issue:** …
- **Component:** seL4 | Microkit | rust-sel4 | host crate | package pin
- **Old pin → new pin:** …
- **Affects deployed images?** yes/no (if yes: boards …)
- **SDK rebuild required?** yes/no
- **Verification:**
  - [ ] `just check`
  - [ ] `just check-pd`
  - [ ] smoke: isolation / workstation / test-all (link CI)
  - [ ] package-pins updated (if applicable)
  - [ ] field images rebuilt / operators notified
- **Residual risk:** …

• Do not commit trees under deps/workspace/ or deps/microkit-sdk/ (gitignored).
• Do not bump seL4 without checking Microkit compatibility notes for that release.
• Do not leave versions.toml rust-sel4 tag different from Cargo.toml.
• Do not treat lerux package pins as a substitute for rebuilding from source in CI — they record artifact digests, they do not load arbitrary remote ELFs at runtime.

• Smoke matrix and caches: ci.md
• RPi4 deploy after image rebuild: boards.md
• Package pin CLI: packages.md

• ADR-003 — net trust map
• ADR-005 — fault parent (not production default)
• ADR-006 — priorities / PPC
• debug.md — test-debug and GDB
• plan-arch.md — Phase 60 checklist
• net-topology.md — NIC channel map
• ci.md — CI gates after pin bumps