BYO-OS: optional per-component memory isolation — native MPU/PMP-program-on-switch TCB (+ synth#377 dependency)

[avrabe]

Context

In the dissolved (library-OS) BYO-OS mode, verified components + scheduler + app link into one native ELF in a single address space. Memory safety of the verified core is by construction (Verus/Kani: no OOB/over/underflow). But that is "no bugs in verified code," not containment of (a) the unverified seam-TCB or (b) a co-located untrusted/unverified component (e.g. a 3rd-party driver). synth does not provide inter-component isolation here:

• --native-pointer-abi (used by the pointer-passing modules / gust) deliberately uses real native pointers — no linmem sandbox.
• --safety-bounds {software,mpu} exists but is a no-op on the optimized codegen path today — blocked by synth#377.

So today's gust is safe only because it's a single verified failsafe task. The moment multiple mutually-distrusting components are dissolved together, isolation is an explicit, unbuilt design item.

Proposal (OPT-IN)

Make per-component memory isolation an option, layered on top of verification (which stays the primary line), enabled where the use-case/hardware warrants:

1. Native MPU/PMP-program-on-switch TCB (C-free): a thin Rust TCB that programs ARM MPU / RV32 PMP regions per task/partition and reprograms on context switch. gale already verifies the partition arithmetic + non-overlap (src/mem_domain.rs, src/mpu.rs, MpuRegion.lean); the Zephyr drop-in lets C do the register writes — the BYO-OS path needs this in the native TCB.
2. (Optional) software bounds as belt-and-suspenders — gated on synth#377 (so --safety-bounds software actually emits checks on the optimized path).

Default vs option

• Default: verification-only (smallest TCB, zero isolation overhead) — correct when all co-located components are verified.
• Option: +mpu per-switch partitions for containing the seam-TCB and/or unverified components — pay the MPU-reprogram cost only when you need the boundary.

Kill-criterion

"A dissolved component can read/write another partition's memory after a context switch with +mpu enabled" → isolation broken.

Tracks under gale#74 (BYO-OS). Depends on: synth#377 (for the software-bounds option).

[avrabe]

Design option: multi-memory ↔ MPU-region (the structural alternative to hand-carving)

Beyond "shared memory + MPU sub-regions carved by the TCB", there's a cleaner shape worth recording: keep each component in its own wasm memory and map each memory to one MPU/PMP region. Then the memory boundary is the protection boundary — the embedder programs one MPU region per memory on context switch, instead of hand-maintaining an address map over a shared blob.

Trade-off: multi-memory is structural isolation for free at the hosted level (kiln/wasmtime — no cross-memory pointers, runtime-enforced), but it does not survive dissolve on its own (native code has no bounds checks) and currently doesn't lower to a single-address-space MCU (synth#369 cross-memory loud-skip; meld#172). So this option is gated on synth's backend stance.

→ Posed as a design question to synth (synth#404): should synth lower multi-memory to one distinct native region per memory (MPU-protectable), or stay single-shared-memory and leave isolation to MPU-carving? gale#86's design forks on synth's answer:

• synth multi-memory→region ⇒ pursue multi-memory ↔ MPU-region (structural, preferred).
• synth single-shared-only ⇒ commit to shared + MPU-carve (the current opt-in plan).

Verification stays the primary line either way; this only shapes the containment layer for untrusted/unverified components.

[avrabe]

DECISION (meld#300): model 2 — multi-memory structural isolation — is committed

The fork above is resolved (meld maintainer decision, gale-consumer concurs):

• Committed isolation model: multi-memory → one MPU/PMP region per component memory (memory boundary = protection boundary). meld is ready (MemoryStrategy::MultiMemory, meld-core/tests/multi_memory.rs).
• Secondary (lean-now): --memory shared + single region — for the single-trust-domain image (gust failsafe / PR feat(kiln): lean grow-free library-OS dissolve (972B) via wit-bindgen no-grow branch #90 lean dissolve: one memory, no isolation needed). This is what ships today and is unaffected.
• Gate: synth#404 — carry memidx through the IR, place each memory at a distinct native base, lower cross-memory ops explicitly (synth#369), expose per-memory base/size so the TCB programs one region each.
• Budget: N ≤ ~8 components/image (ARMv7-M MPU / PMP region cap) — the per-image component budget; not a model differentiator.

gale#86 status: design decided, implementation gated on synth#404. Downstream gale work when it lands: multi-memory build → dissolve → TCB programs one MPU region per memory on context switch (verification primary, MPU containment for the untrusted). No hand-carved address maps.