Seedcore logo

Rust · capability microkernel

Authority is a token
you have to hold.

Seedcore is a deterministic microkernel simulator in pure Rust. A tiny privileged core provides only four things, threads and a scheduler, address spaces, synchronous IPC, and unforgeable capabilities, and everything else, the filesystem and the console, runs as an ordinary unprivileged user space service. Press a button below to watch a client read a file entirely over IPC, then watch the core deny an access no one ever granted.

Open the playground View on GitHub
capability based isolation synchronous IPC user space services teaching accurate model
How to use this playground

This is a faithful reimplementation of the Seedcore engine, small enough to read. The three boxes below are tasks. The filesystem and console are ordinary user space services. The app is a client. Watch what each is allowed to do, and what the core denies.

  1. Send a file request. Press Send file request. The app sends a request to the filesystem service over its endpoint, handing it a one shot reply capability inside the message. The filesystem writes the file bytes into a region shared with the app, replies, and the app reads the bytes back. Watch the boxes light up, the shared memory fill, and the scheduler timeline grow.
  2. Try an unauthorized access. Press Try unauthorized access. The app names a capability slot it was never granted. There is no such capability, so the core denies it. The denial appears in red and the app box flashes red.
  3. Try a type confusion. Press Send on a memory capability. The app tries to send a message using a memory capability where an endpoint is required. The core refuses the wrong object kind.
  4. Read the state. Each box lists its capability tokens as slot: object [rights]. A capability transferred over IPC appears highlighted in the receiver. The shared region shows which tasks can see it.
  5. Reset to start over. Everything here is deterministic, so the same buttons always produce the same trace.

Guided tour. Start with Send file request and read the event log top to bottom. Notice the cap transfer line: that is the reply capability moving from the app into the filesystem. Then press Try unauthorized access and see that naming a slot is not the same as holding one. That single idea, that authority is a token you must hold and cannot forge, is the whole point of a capability microkernel.

The system

Three tasks, their capabilities, and their address spaces.

Scheduler timeline

Round robin dispatch order. Each chip is one dispatched thread step.

Event trace

Every effect the core records, in order.

    Every run is checked against a shadow model

    Five properties are asserted over randomized, seeded, bounded scenarios, plus unit tests per module. Every gate compares the kernel against an independent shadow model that decides what should happen without ever calling the kernel, so a pass is never vacuous.

    # five gates: capability enforcement, IPC exactly once, address space
# isolation and determinism, a bounded stress harness, and the
# capability derivation tree, each compared to the shadow model
cargo test

# raise the bounds. at a million ops the auth harness runs about
# two million shadow comparisons per pass, with zero disagreement
SEEDCORE_FUZZ_OPS=1000000 cargo test

    A syscall succeeds if and only if the caller holds a capability of the right kind with the right permission; fabricated, guessed, and revoked slots are always denied. Synchronous send and receive deliver every message exactly once, a transferred capability moves from sender to receiver and leaves the sender, and the same seed produces a byte identical trace. Minting never adds a right the parent lacked, and revoking a capability removes exactly its subtree, wherever the descendants travelled.

    How it differs

    Real microkernels boot on hardware. Seedcore keeps only the idea that makes them interesting to a security engineer, the capability spine, and makes it small enough to read and to fuzz.

    seL4

    A real, formally verified capability microkernel that runs on hardware. The gold standard for capability-based isolation, and a large, deep system to study end to end.

    Mach, MINIX

    Real microkernels. Mach pioneered the split of IPC and user space services; MINIX is a teaching microkernel that actually boots. Both carry the weight of real hardware and drivers.

    Seedcore

    Not bootable, and honest about it. It models the microkernel philosophy directly in pure Rust std: threads, address spaces, synchronous IPC, and unforgeable capabilities, with everything else as an unprivileged user space service. Deterministic from a seed, small enough to read in an afternoon, and every property checked against an independent shadow model.

    The parts that matter

    The capability spine, in six pieces.

    Each is a real part of the core in src, and each has a gate in tests that pins it against the shadow model.

    core Threads and scheduler

    A deterministic dispatcher runs each thread's small program of syscall-level Op steps. The core interprets them, accounts for cost, and records every effect in a trace.

    core Address spaces

    Memory is private unless a capability says otherwise. A shared region genuinely carries data between the tasks that hold it, while outsiders are denied.

    core Synchronous IPC

    A blocking send and receive rendezvous over endpoints. Every message is delivered exactly once, with correct blocking semantics in either arrival order.

    security Unforgeable capabilities

    A task holds no ambient authority. It cannot name a file, a page, or another task without a capability, and it cannot forge one. Fabricated, guessed, and revoked slots are always denied.

    security Delegation and revocation

    Minting a copy never adds a right the parent lacked. Revoking a capability removes exactly its derivation subtree, wherever the descendants live and however they travelled.

    proof The shadow-model gate

    Every gate compares the kernel against an independent shadow model that decides what should happen without ever calling the kernel, so a pass is never vacuous.

    Use it

    CLI

    seedcore demo stands up filesystem and console services and reads a file over IPC, run drives a seeded randomized run, and delegate shows delegation and transitive revocation.

    Library

    seedcore::prelude: a Kernel creates objects, mints capabilities with grant and mint, revokes a subtree with revoke_tree, spawns threads, and runs the loop into a RunReport.

    Gates

    Five shadow-checked properties over randomized, seeded, bounded scenarios: capability enforcement, IPC exactly once, isolation and determinism, a stress harness, and the derivation tree. Raise the bounds with SEEDCORE_FUZZ_OPS.

    Determinism

    The only inputs are the seed and the thread programs, so a run reproduces byte for byte. The same buttons in the playground always produce the same trace.

    # stand up fs + console services, read a file over IPC, then two denials
cargo run --bin seedcore -- demo

# a seeded, randomized run
cargo run --bin seedcore -- run --seed 42 --pairs 4 --burst 3

# capability delegation and transitive revocation
cargo run --bin seedcore -- delegate

cargo run --bin seedcore -- help