Aether's isolation story is capabilities + tenants, not POSIX users. This is the invariant we would defend in a design review — and the places v0.1 is still incomplete.
A task holds a CapTable of 32 slots. A CPtr is an index into that
table. Slot 7 in tenant A's table is unrelated to slot 7 in tenant B's
table. There is no global “handle namespace” to guess.
Each Capability stores:
kind— Memory, Endpoint, AccelQueue, Notification, SpectralCut, FlowQuota, Activity, Partition, OperatorKernelrights— subset of READ/WRITE/GRANT/MAP/SUBMIT/WAIT/EXECUTE/BIND/UNIFIED (UNIFIEDis never inMEM_FULL)object— kernel object idgeneration— bumped at mint; withtenantthis is the derivation nodetenant— must match the table owner at lookupparent— derivation edge (set on derive / GRANT-copy)
- No cross-tenant mint.
CapTable::mintrejects a cap whose tenant field is not the table owner. - Monotonic derive. Rights may only shrink.
WouldEscalateotherwise. - GRANT required to transfer. No silent aliasing of a cap to another table without GRANT.
- Kind + rights checked on use.
require(cptr, AccelQueue, SUBMIT)fails for a Memory cap or a read-only queue cap. - Isolation demo. Tenant B does not
holds(Memory, A's arena)and cannotrequireA'sCPtr(the slot is empty in B's table). - Cut bind.
SpectralCutrequiresBIND. Tenant B does not hold A's cut. Cross-cut placements areCutError::CrossCut. - Hodge class.
FlowQuotabadge is a class mask. Harmonic +TREE_OFFLOADis refused even if the tenant is authorized (deadlock). AnOperatorKernelcap binds one topology to one class; Tree+Harmonic / Tree+Curl refuse at bind, and inject of a different class isClassMismatch.SparsifiedCollectivemay drop below-threshold harmonic before enqueue; it does not bypass Harmonic+TREE refuse. - Activity + partition. A virt accel is an
Activitycap, not an ioctl. Jobs bind aPartitionProfile(spatial slice, credits, blast radius). Isolation is spatial (slices/columns) first, temporal second—QoS and blast radius are invariants. - Typed spaces. A Memory cap does not imply a unified VAS.
CapRights::UNIFIEDmust be granted explicitly.TypedWindowis a Soft-SMMU pin stub (Exploration E); foreign-tenant windows areCrossCut. Not a CXL.mem decoder. - Revoke descendants.
deriveand GRANT-copy record a parent edge.revoke(parent)empties that lineage in the same table;revoke_in(parent, others)empties grant-children in the named tables too. Unrelated caps stay.
This is a research-prototype capability machine (Helios / M3 / Barrelfish / Twizzler-shaped names, seL4-inspired CPtrs). It does not claim seL4-level proofs. Formal caps are not a calendar item.
Host tests in core/src/caps.rs, core/src/caps_props.rs,
core/src/demo.rs, and core/src/blast.rs lock the statements below.
The blast-radius diligence clip serial-prints [blast] after CrossCut
and wrong-SID refuse. The SID-at-submit clip serial-prints [sid] after
two-tenant SET_SID, refuse-until-armed, and per-tenant SID budget
(core/src/sid.rs). Host1x is inspiration only — not a Tegra driver
and not hardware-grade isolation. The software SID budget (4 Bound CDs
per tenant) plus the inject_wrong_sid / SubmitSid host tests are
the isolation we can unit-test today; they are not a silicon SID
allocator or a Host1x fault-injection campaign.
SoftCmdFirewall (drivers/src/firewall.rs) copies the Soft-CP
command image into a kernel-owned arena before opcode / reloc /
SID / addr-cap validate, then enqueues the copy. That is Host1x's
copy-then-validate lesson: a client that mutates the buffer in the
validate window cannot sneak a rewritten stream. It is integrity
of the command stream only — not confidential GPU, not HBM
encryption, not GPU-CC HMAC (optional later), and not NVIDIA SEC2.
Serial: [firewall].
SoftChipletSync (core/src/chipsync.rs) is a software fence-domain
model (scoped timelines + SoftCCT last-writer elision). It is not
a coherence protocol, not UCIe, not a Vulkan / ROCm product, and not
hardware-grade isolation across chiplets.
SoftGreenCtx (core/src/greenctx.rs) is a software SM/WQ partition
on Soft-CP. CUDA Green Contexts / DetShare are inspiration only. It
is not HW MIG, not a BAR firewall, and not silicon SM isolation.
Host tests measure memcpy-like interference; they are not FLOPs.
SoftSFI (core/src/softsfi.rs) is a toy Soft-CP bytecode sandbox
(GPU-AToLL-shaped SFI). Every modeled load/store/dma/atomic_add
proves base+bound in the SID-allowed range. atomic_add is a
sequential toy RMW, not a coherent hardware atomic. It is not an
NVVM pipeline and not “safe multi-tenant kernels.” Tensor copies
are not in the modeled ISA. Heap/alloc is a named opcode
that is refused (SfiError::Unmodeled) — not a bump allocator.
Skip-verify fault injection still traps on the SID window and does
not cross-read. Software only. Sell clip: [softsfi] heap=refused.
PASID / SVA (core/src/sva.rs, IommuMap::bind_mm / map_va /
unmap_va) binds a process mm to a Soft-SMMU SSID so Soft-CP DMA
uses that process VA. Host unmap invalidates the SSID ATC. Skipping
invalidate is a stale translate. Linux SVA / PASID inspiration. It
is not ARM SVA, not PCIe PASID/PRI, not CUDA UVA, and
not zero-copy SVA without invalidate. No new syscall.
OperatorInject (core/src/opinject.rs) is a Soft-CP resident worker
plus a versioned function table (memcpy / saxpy, hot-add scale).
GPUOS / Mirage MPK are inspiration only. It is not NVRTC, CUDA, a
vendor compiler, or a full LLM compiler. SID-at-submit and
SoftCmdFirewall copy-then-validate still gate every call. Serial:
[opinject].
The host sell-path make red-team (examples/red-team) prints one
line per named attack ([redteam] attack=… result=refused) by calling
those same clips. It does not add isolation. Closer: not confidential
GPU, not HW MIG, Soft SMMU is software.
Aether stores a parent pointer (CdtNode = table owner + mint
generation). The tests in core/src/caps_props.rs are property /
exhaustive cases on that pointer. They are not a proof, not a
syscall, and not a reason to schedule a formal cap kernel.
| Id | Statement |
|---|---|
| P-Revoke | mint → derive (optional GRANT-copy) → revoke_in(root, named tables) empties descendants in those tables |
| P-Unrelated | a cap outside that lineage stays live |
| P-Named | GRANT-copy across tables is collected only if the dest table is passed to revoke_in; revoke alone leaves the foreign child live |
| P-Unforge | mint rejects a foreign tenant; a CPtr is a slot in one table |
| P-Monotone | derive / GRANT may only shrink rights; GRANT is required |
revoke_in walks tables the caller names. A GRANT-child in a table
that was not passed survives — that is P-Named, not a missing global
walk. No SYS_REVOKE. Syscall numbers 0–8 stay frozen.
These are marked so a security review does not assume them:
| Gap | Risk | Roadmap |
|---|---|---|
| Init is kernel-mode | A buggy demo can touch any PA | Ring-3 / U-mode / EL0 + user page tables — landed on x86, RISC-V, and aarch64: /init is user; send/recv/map/accel require() the CPtr. Kernel run_boot_demo is still a trusted self-check. |
| Send path in the kernel demo does not re-walk the sender CPtr on every fabric.send | A kernel-internal caller could pass a raw EndpointId | SYS_SEND is the user send path and always requires WRITE |
| No hardware SMMU | A real device DMA can ignore Soft SMMU | Soft SMMU walks STE→CD→S1/S2, hardens SSID/CD, aborts until Bound, ATS-invalidates a software ATC, allocates non-identity IOVA, refuses maps/binds without Memory+MAP, and (Soft-CP / IreeShapedCp) refuses DMA until SET_SID is armed for that submit; TypedWindow is a software pin stub; hardware SMMU still needs partner silicon |
| Revoke is not a user syscall | Ring-3 cannot name revoke; kernel World still has one shared CapTable (PR #10) |
Internal CapTable::revoke / revoke_in; per-task tables still open |
revoke is not a global CNode walk |
A GRANT-child in a table the caller did not pass to revoke_in survives |
Explicit named-table walk; not a seL4 MDB |
| Identity islands on kernel CR3 | Bulk 4 GiB identity is unmapped. Remaining supervisor islands: low 2 MiB (SIPI / mailbox / trampoline), virtio-blk window, APIC MMIO. SoftNPU is Soft SMMU + HH. User CR3 has no identity (KPTI subset). USER_MMAP_BASE is user-only, not an identity island |
Meltdown-complete trampoline unmap; POSIX MM |
| COW is one 4 KiB page | /init + /probe share one RO template until a write fault; SYS_CLONE shares the broken page |
fork-shaped aspace clone |
SYS_MMAP is a 64 KiB anon window |
First-fit 4 KiB USER pages at 0x02C0_0000 (after virtio-blk); no file / no MAP_SHARED / no munmap |
POSIX mmap / file-backed / MAP_SHARED |
| SoftSFI tensor / heap | A kernel that used those ops would bypass the toy sandbox | Named refuse: SfiError::Unmodeled (SoftOp::Tensor, SoftOp::Heap). atomic_add is SID-proved (in-range accept, cross-tenant Oob) but is a sequential toy RMW, not full SFI. Heap is refused, not a modeled bump allocator. Not a GPU-AToLL port. Hardware SMMU / real SFI still need partner silicon |
| No crypto / measured boot | Out of scope for v0.1 | — |
The intended story:
- Tenant A's weights live in an arena minted to A.
- The NPU queue receives a derived Memory cap (READ, maybe not GRANT).
- Tenant B never receives a cap to that object. Knowing the physical address (if it leaked) is not enough once a hardware IOMMU is present. v0.1 has Soft SMMU (software STE→CD→S1/S2 walk + ATS invalidate). That is policy complete and software-mechanism present; a real device can still ignore it. Hardware SMMU needs partner silicon.
Ring-3 is live; each user task has its own PML4 with USER only on its
2 MiB ELF window (the other user window is unmapped). SYS_CLONE
threads share that PML4 — they are not a second isolation domain.
CR4.SMEP/SMAP are on. The map API refuses a pin without a Memory cap, allocates a
non-identity IOVA per stream, and refuses wrong-stream / cross-tenant
unmap. Treat isolation as “the cap tables + Soft SMMU + task-local
USER leaves do the right thing” — which is the part we can unit-test
and boot-test today — not “the hardware cannot cheat.” The kernel
is linked at 0xffffffff80400000 and may run at a 16/32 MiB slide
after PIE .rela.dyn apply; the unused HH alias is unmapped. The
trampoline identity 4 GiB is torn down on the kernel CR3 except
SIPI / mailbox / trampoline / virtio-blk / APIC islands. SoftNPU
DMA is Soft SMMU + HH (KernelDma).
User CR3 maps only the
ELF window plus a 4 KiB supervisor trampoline — a forged low kernel
pointer is not present there. That is a KPTI subset, not
Meltdown-complete (trampoline pages remain mapped). PCID tags
KPTI mov cr3 when CPUID advertises it so the switch is not a
full TLB flush; stock qemu64 often falls back to a full flush.
PCID is not a speculation barrier. A documented COW subset
maps one shared 4 KiB USER page (0x0280_0000) read-only in
/init and /probe; a write fault copies the frame on that
aspace only. That is not fork and not POSIX mmap. RISC-V /
aarch64 do not map it. SoftNPU DMA still uses kernel CR3.
Scheduler timing, DRAM bank contention, and NPU occupancy are classic side channels. v0.1 does not mitigate them. A production AI-chip OS would need cache coloring / bank partitioning and probably a deterministic wave scheduler for high-assurance tenants.