Layer 03 · Substrate

One capability,
local to global

An seL4 capability and a NULLIUS capability are the same abstraction at two points on a distance parameter n. The substrate is that gradation made real.

A full deployment boots real Rust protection domains on the seL4 microkernel with an on-device STARK. NULLIUS reproduces the capability model and its n=1 local collapse in running code; the seL4 boot and on-device prover are represented. See Verify.
The distance parameter

n = 1 collapses to strong-local

A local install is a first-class deployment with the strongest properties — immediate revocation, synchronous commit, consistent checkpoint — because at n=1 the distributed bounds collapse to local ones. The moment a program reaches the network it flows into distributed mode with no seam: same handle, same attenuate / delegate / invoke, the bounds just relax along n.

n = 1 · local
Strongest bounds

Synchronous commit, immediate revocation, one consistent checkpoint.

n = few · cluster
Relaxed bounds

Quorum commit; revocation at finality; checkpoints coordinate.

n → many · federation
Same handle

Asynchronous handoff, custody receipts, eventual finality after GST.

The topology

The five-PD boot ladder

On seL4 the stack comes up as a small set of protection domains, with ~10kLOC of verified C as the only privileged code. Everything else — including the executor — is unprivileged and capability-confined.

seL4 microkernel        (verified C — the ONLY privileged code)
   ├── PD: root-task     (hands out initial capabilities)
   ├── PD: null-exec     (the executor — the one that runs turns)
   ├── PD: prover        (STARK prove/verify, on device)
   ├── PD: net           (strand-blocks, signatures, gossip)
   └── PD: substrate     (holds apps, gives them caps, checkpoints)

The executor is unprivileged. It has exactly the capabilities the root-task delegated and no ambient authority — the same discipline the surface above it lives under.

Durable state

pg-nullius — your node is your Postgres

Reads are free SQL; writes are verified turns. The commit log projects into queryable tables — cells, receipts, caps — and a row's policy calls null_admits(token,'read',id), the same decision the kernel makes, from the same capability token. Attenuation, offline delegation, time-boxing, revocation: the discipline row-level-security structurally cannot express, presented once per session.

Climb the protocol ladder →