Skip to content
PointSav Digital Systems

seL4 Unikernel Substrate for os-console

← All revisions

9ad6df5a · PointSav Digital Systems ·

Phase C A1d: topic-* batch complete — 4 merges into canonical articles (+ content backfill), 4 prefix-drop renames, 2 merge-checks resolved (capability-geometry, private-git-paid-customer-endpoint); research/ seeded (preprint-notice-convention + landing cleanup). Track A (documentation) complete.

View the full record as of this revision →

@@ -0,0 +1,205 @@
---
schema: foundry-doc-v1
content_type: topic
title: "seL4 Unikernel Substrate for os-console"
slug: sel4-unikernel-substrate
aliases:
  - topic-sel4-unikernel-substrate
short_description: "os-console is intended to run as a seL4 Microkit unikernel image in its final production form, compiling application code directly with a formally verified kernel to eliminate general-purpose OS attack surface."
category: substrate
type: reference
quality: complete
status: active
audience: public
bcsc_class: public-disclosure-safe
language_protocol: PROSE-TOPIC
last_edited: 2026-06-20
editor: pointsav-engineering
paired_with: sel4-unikernel-substrate.es.md
cites: []
---

# seL4 Unikernel Substrate for os-console

[[os-console-architecture|os-console]] is intended to run as a [[sel4-microkernel-substrate|seL4 Microkit]] unikernel image in its final
production form (planned Phase H2). This article explains what that means, what
already works, and what remains to be built.

---

## What Is a Unikernel

A unikernel is an application compiled directly with the operating system primitives
it requires, producing a single bootable binary. There is no general-purpose OS,
no shell, no package manager, no user account system, and no attack surface beyond
the application's own code and the minimal kernel it depends on.

The distinction from a conventional VM:

| Conventional VM | Unikernel |
|---|---|
| Guest OS (Linux/BSD) + application | Application + minimal kernel |
| General-purpose OS: shell, users, packages | Single-purpose: one application only |
| Shared kernel attack surface | No shared kernel; no ambient authority |
| ~500 MB to 2 GB typical footprint | 10–50 MB typical footprint |
| Boot time: 5–30 seconds | Boot time: < 1 second |
| Exploit: OS misconfig, privilege escalation | Exploit: only application-layer bugs |

A unikernel cannot be "rooted" in the conventional sense because there is no root to
escalate to. There is no shell to drop into. There is only the application and its
formally bounded capability set.

---

## seL4 Microkit

seL4 is a formally verified microkernel. The seL4 kernel has been verified using
machine-checked proofs (Isabelle/HOL) establishing correctness of the kernel's
capability model, memory management, and IPC mechanisms. These are not unit tests —
they are mathematical proofs over the kernel's entire implementation.

seL4 Microkit is seL4's minimal operating environment for embedded and unikernel
applications. It defines:

**Protection Domains (PDs):** The unit of isolation. Each PD has its own capability
namespace and cannot read or write another PD's memory. PDs are statically declared
at build time in a TOML system specification.

**Protected Procedure Call (PPC):** Synchronous IPC between PDs. A PD invokes a
PPC endpoint. The kernel switches execution context. The callee returns. The caller
resumes. No shared memory is involved unless explicitly mapped with a capability.

**Channels and Notifications:** Asynchronous communication between PDs via kernel-
mediated notification objects. A PD that has the channel capability can signal; a PD
that has the notification capability can receive.

---

## What Already Works

[[moonshot-toolkit-build-orchestrator|moonshot-toolkit]] v0.3.1 (PointSav's build orchestrator, 35 tests passing) already produces
bootable [[sel4-aarch64-qemu-substrate-target|seL4 AArch64]] images:

```toml
# examples/hello-world.toml — working today
[system]
kernel = "vendor-sel4-kernel/build/aarch64-qemu/kernel.elf"
elfloader = "vendor-sel4-tools/elfloader-tool"

[[pd]]
name = "hello-pd"
binary = "examples/hello.elf"
priority = 100
```

Running `cargo run -- build examples/hello-world.toml` produces an elfloader ELF.
QEMU boots it to: `Booting all finished, dropped to user space`.

vendor-sel4-kernel (v15.0.0-dev, BSD-2-Clause) is vendored in the monorepo and
built from source. vendor-sel4-tools (elfloader, 44 C/ASM sources) is vendored and
compiled by moonshot-toolkit.

The kernel boots. The infrastructure is in place.

---

## The 3-Protection-Domain Design for os-console

The intended seL4 system image for os-console contains three Protection Domains:

```
os-console seL4 system image
┌─────────────────────────────────────────┐
│ os-console PD        priority 100       │
│  Cartridges: F2 F3 F4 F6 F9 F11 F12   │
│  ratatui TUI; no network access direct │
│  Stack: 256 KiB; heap: 1 MiB           │
└──────────┬──────────────────┬───────────┘
           │ PPC (sync IPC)   │ PPC (sync IPC)
           ▼                  ▼
┌──────────────┐   ┌────────────────────┐
│ network-pd   │   │ serial-pd          │  priority 150/180
│ smoltcp      │   │ VirtIO serial      │
│ VirtIO-net   │   │ ratatui output     │
│ HTTP/1.1     │   │ keyboard input     │
└──────────────┘   └────────────────────┘
       ▲
       │ VirtIO-net (DMA capability)
       ▼
moonshot-hypervisor → host network → Totebox services
```

os-console PD makes an HTTP request by calling the network-pd via PPC. The network-pd
holds the VirtIO-net device capability. The os-console PD never directly holds a
network device capability. If the os-console PD is compromised, it cannot exfiltrate
data directly over the network — it can only call the network-pd via its defined
PPC interface.

---

## moonshot-sel4-vmm: The Sovereign PD Runtime

The seL4 Microkit requires a small Rust runtime inside each PD: an entry point,
a heap allocator, and system call wrappers for seL4's ABI. External projects provide
this (rust-sel4 from the seL4 Foundation). The intended approach is to author a
PointSav-maintained runtime in moonshot-sel4-vmm.

The seL4 ABI is small and formally verified — it does not change arbitrarily because
the proofs constrain it. Writing dedicated bindings (~300 lines of Rust) takes the same
time as integrating an external library but leaves the code under PointSav control.

moonshot-sel4-vmm is intended to provide:
- `_start()` → stack/heap initialization → `pd_main()`
- seL4 system call wrappers (`sel4_call`, `sel4_send`, `sel4_recv`)
- `microkit_msginfo_t` IPC type matching the Microkit ABI
- `notified(ch: u64)` and `protected(ch: u64, msginfo)` callbacks per the Microkit protocol
- `DebugPutChar` for development-time output

This crate is shared across all three OS-family binaries: os-console PDs, [[os-totebox|os-totebox]]
service PDs, and [[os-orchestration|os-orchestration]] app PDs all use the same runtime.

---

## The Sovereign Build Stack

The intended runtime dependency chain for os-console as a seL4 unikernel:

| Layer | Component | Status |
|---|---|---|
| Application | os-console cartridge code | Active |
| Build orchestrator | moonshot-toolkit v0.3.1 | Active |
| Host VMM | moonshot-hypervisor | Scaffold — to be filled |
| PD runtime | moonshot-sel4-vmm | Scaffold — Phase H1 fill-in |
| Capability substrate | system-core, system-ledger v1.0.0 | Active |
| Kernel | vendor-sel4-kernel v15.0.0-dev | Vendored BSD-2-Clause; built from source |
| Elfloader | vendor-sel4-tools | Vendored BSD-2-Clause; compiled in build |
| Network PD | smoltcp | MIT; vendorable; replaces reqwest |
| Dev boot | QEMU | Dev tool only; not in product image |

Nanos (commercial unikernel) and hermit-os (external mini-OS architecture) are not
used. The path to a working prototype is through moonshot-sel4-vmm (~300 lines), which
takes the same time as integrating an external library and leaves every layer under
PointSav control.

---

## Phase Roadmap

**Phase H0 (current):** Alpine Linux in QEMU — validates the service stack before
investing in the seL4 substrate. No seL4 code required.

**Phase H1 (planned, 4–6 weeks):** Fill in moonshot-sel4-vmm. Boot os-console as a
single seL4 PD. Render the TUI via VirtIO serial. Connect to a test Totebox service
via smoltcp network PD. VirtIO clipboard working (non-optional for SMB operators).

**Phase H2 (planned, 8–16 weeks):** Full 3-PD design. moonshot-hypervisor replaces
QEMU. os-console image built by moonshot-toolkit from `examples/os-console-sel4.toml`.
Boots in under 1 second. 100% sovereign stack; QEMU removed from product path.

**Phase H3 (intended, Leapfrog 2030):** F11 pairing becomes capability minting.
Machine-level seL4 capability tokens. system-core Capability types carried in the
PD's CNode. Revocation via system-ledger propagates to kernel level.

---

*Woodfine Capital Projects™, MCorp™, PointSav Digital Systems™, Totebox Orchestration™, Totebox Archive™, and Capability Geometry™ are trademarks of Woodfine Capital Projects Inc., used in Canada, the United States, Latin America, and Europe. All other trademarks are the property of their respective owners.*
Important Information

Important Information

Corporate structure. PointSav Digital Systems ("PointSav") is a trade name of Woodfine Capital Projects Inc. ("Woodfine"). PointSav does not itself offer, sell, or solicit any security. Any securities offering associated with Woodfine's real-property direct-hold solutions is made exclusively by Woodfine, and only by means of the applicable Private Placement Memorandum.

No investment advice. This wiki's content is provided for engineering, operational, research, and development purposes. Nothing on this wiki constitutes investment advice or a solicitation to invest in any Woodfine partnership or direct-hold solution.

Intellectual property. The PointSav name, trade name, wordmark, and marks, together with all current and future PointSav- and Totebox-branded products, services, and offerings — and the software, source code, documentation, design system, and all related materials — are proprietary to Woodfine and its affiliates, except for components identified as open source. No rights are granted except as expressly set out in a written license or agreement. See TRADEMARK.md in this repository for the full trademark notice.

Open source components. Portions of the platform are made available under permissive open-source licenses identified in the accompanying repository. Use of those components is governed by their respective license terms.

No warranty; informational use. Content on this wiki is provided for general informational purposes only and does not constitute a representation, warranty, or commitment with respect to product functionality, availability, pricing, or roadmap. Some articles describe planned or intended features, capabilities, and milestones — language such as "planned," "intended," "targeted," "may," and "expected" marks this forward-looking content, which is subject to change and does not constitute a commitment regarding future performance.

Confidentiality. Where an article describes an operational or deployment detail that is not intended for public disclosure, that article is not published on this wiki. Content here is general-purpose engineering documentation, not customer-specific configuration.

Jurisdiction. Woodfine Capital Projects Inc. is organized in British Columbia, Canada. References to the Sovereign Data Foundation on this wiki describe a planned or intended initiative only, not a current equity holder or active governance body.

Changes to this notice. PointSav may update this notice from time to time; the version posted on this page governs.

Not a filing system. This wiki is not a securities filing system, an electronic disclosure repository, or a substitute for SEDAR+ or any other regulatory filing system. Formal securities filings are made through the applicable regulatory filing system, not through this wiki.

Full disclaimer. This notice supplements, and does not replace, the full Disclaimers article. In the event of any conflict, the full Disclaimers article governs.

Read the full disclaimer →