substrate/sel4-microkernel-substrate

The seL4 microkernel is the mathematically formally-verified L1 kernel on which all PointSav operating systems run — its security properties are proved by formal mathematical proof, not asserted by testing. [^1] PointSav adopts seL4 as raw material rather than building a custom kernel, and constructs its proprietary Rust layer above it. Memory isolation, zero buffer overflows, capability-based permissions, and deterministic execution are guaranteed structurally — the foundation for security claims that can be reasoned about formally and presented to regulators rather than merely asserted through penetration testing. This article covers the architectural rationale, the layered stack, the toolchain constraints, and the language discipline enforced above the kernel.

[edit]Why adopt rather than build

A reasonable alternative would be to write a custom kernel. PointSav explicitly rejects that path:

Option	Cost	Outcome
Build a custom kernel	Tens of millions of dollars; five or more years of formal-verification work	Catching up to a 2009 standard in the 2030s
Adopt seL4	Zero	Already proved; ready to build on

The principle is to use seL4 as a raw material — like structural steel — and build the proprietary value above it. PointSav's competitive technical work happens in the Rust layer above seL4, not in the kernel itself.

[edit]The layered stack

Layer	Component	Owner
L0 — Hardware	x86_64 Haswell+ CPU (see [[hardware-reference	hardware reference]])
L1 — Microkernel	seL4 [^2]	seL4 project (adopted upstream; minor patches)
L2 — Driver framework	sDDF (seL4 Device Driver Framework) with VirtIO	seL4 ecosystem
L3 — System packages	system-* Rust crates — drivers, networking, filesystem	PointSav
L4 — Services	service-* Rust crates — application logic	PointSav
L5 — Operating systems	os-* compositions	PointSav
L6 — Applications	app-* user surfaces	PointSav

The boundary between L2 (kernel-adjacent) and L3 (PointSav-owned) is the line PointSav draws around its proprietary value. Everything below is adopted commodity; everything above is owned.

When the target hardware does not support native seL4 boot, a Linux or BSD guest VM inside a seL4-based hypervisor provides equivalent structural isolation around the guest OS. The hypervisor layer supplies formally-verified containment even when the guest itself is a conventional operating system.

[edit]What seL4 provides

Property	What it means in practice
Mathematical isolation	If service-email crashes, service-people cannot feel it; the kernel guarantees the boundary
Deterministic execution	Real-time guarantees on instruction timing — important for synchronisation protocols
Capability-based security	Permissions are passed as cryptographic capability tokens, not entries in a central permission table
Zero buffer overflows in the kernel	The class of vulnerability that produces most OS CVEs is mathematically excluded from the kernel

The result is a substrate where security properties can be reasoned about formally rather than asserted by penetration testing. This changes what kinds of security claims can be defensibly presented to a regulator — and forms the continuous-proof compliance foundation.

[edit]The Microkit and toolchain constraints

seL4 is intentionally minimal: it provides capabilities and inter-process communication and very little else. To make it practically usable, PointSav relies on the seL4 Microkit, a framework that translates higher-level system descriptions (XML manifests, ELF binaries) into the low-level capability operations the kernel expects.

The Microkit has constraints. One is documented in detail in the engineering archive: the Microkit's x86_64 builder eagerly maps 1 GB Huge Pages for kernel code, and then fails to shatter those pages back into 4 KB sub-pages when subsequent small mappings collide. The pragmatic resolution — placing the IPC buffer at the very bottom of memory and the kernel just above it — is the kind of fine-grained discipline that working at this layer demands.

This is a Microkit tooling quality-of-life issue, not a kernel bug. seL4 is working as designed for a high-assurance system that prioritises deterministic memory layout over developer convenience.

[edit]Language discipline

The substrate enforces one language above the kernel: Rust.

Language	Status	Reasoning
Rust	Mandatory for all system-*, service-*, and os-* code	Memory safety without garbage collection; aligns with seL4's formal verification
C / C++	Banned at L3 and above	A single buffer overflow in C undoes the value of seL4's proofs
Python / JavaScript	Banned at L3 and above	Requires heavyweight runtimes; cannot run as a seL4 Protection Domain without violating isolation guarantees
WebAssembly	Permitted for guest user extensions only	A future user-plugin format; runs inside a Rust-hosted Wasm runtime, never as a core service

Allowing one non-Rust service into a Protection Domain would reintroduce runtime bloat and unpredictable execution that the microkernel substrate is designed to eliminate.

[edit]The end-state architecture

The long-term shape of the substrate is a Multi-Server Microkernel OS: every service — networking, filesystem, application logic — runs as an isolated unikernel passing messages through seL4 IPC. The kernel's only job is hardware routing and capability enforcement.

This is one of the most difficult patterns in computer science to engineer correctly. The substrate is now mature enough — through frameworks like Genode and Rust-based unikernel compilers — for an institutional vendor to build operating system surfaces on it.

[edit]See also

• machine-based-auth — capability-based authorization built above the seL4 capability model
• diode-standard — the unidirectional command flow protocol enforced above the kernel
• os-family-overview — the five OS surfaces that compose above this substrate
• hardware-reference — the CPU architectural requirements (Haswell+, fsgsbase, 1 GB Huge Pages)
• compliance-and-continuous-disclosure — how formal kernel verification supports continuous-proof compliance