Skip to content
PointSav Digital Systems

Revision as of · aeec5ebf

Historical revision — this record as it stood on 3 July 2026, not the current version. View the current record →

PPN Three-Path seL4 Architecture

The PointSav Private Network node stack is designed around the seL4 microkernel. Three architecture options define the roadmap. They are sequential: Option B is the current development path; Option C gates on Option B shipping and remaining stable; Option A gates on Option C. All three are documented together so that decisions made in Option B do not foreclose the later options.

Option B — seL4 hypervisor with Linux guest

Current path.

seL4 runs as a Type 1 hypervisor at EL2 (AArch64) or with VT-x (x86-64). The CAmkES VMM runs as a seL4 protection domain and hosts one Linux (Debian 12) guest VM. All PPN services — WireGuard, fleet management, inference routing — run inside the Linux guest.

Hardware
└── seL4 microkernel (EL2 / VT-x)
    └── CAmkES VMM [seL4 PD]
        └── Linux (Debian 12) guest
            ├── WireGuard mesh interface
            ├── service-vm-fleet
            ├── service-vm-host
            └── os-network-admin

What seL4 provides: The kernel is formally verified. No guest VM can access the hypervisor layer, another guest's memory, or any seL4 kernel object without an explicit seL4 capability grant. On AArch64 EL2, the integrity proof (April 2025) extends this to a machine-checked guarantee.

What seL4 does not provide in Option B: The CAmkES VMM and Linux guest are not formally verified. A compromised Linux guest remains confined by seL4's capability topology, but services inside the guest are trusted relative to each other by Linux's normal process model.

Formal security coverage:

Architecture Formal claim Notes
AArch64 EL2 seL4 integrity proof (April 2025) Valid formal security claim at the hypervisor boundary
x86-64 Functional correctness only No formal integrity proof; development target only

Option C — seL4 protection domains own WireGuard

Status: planned/intended. Gate: Option B ships and is stable for six months or more.

Hybrid architecture. seL4 protection domains own WireGuard and the PPN network control plane. A Linux guest VM hosts non-critical workloads. The security boundary is the WireGuard protection domain — the Linux VM cannot modify peer tables without going through seL4 IPC.

seL4 microkernel (EL2 / VT-x)
├── PD: wireguard-control  [WireGuard peer table, CPace gating]
├── PD: ppn-gate           [seL4 IPC channel enforcement]
└── CAmkES VMM
    └── Linux guest (Doorman, fleet, telemetry, media)

By moving the WireGuard mesh interface to a seL4 protection domain, a fully compromised Linux VM cannot gain access to peer tables or the ability to add or remove nodes. Peer addition flows through seL4 IPC to the wireguard-control domain, which validates each request independently.

What changes from Option B: os-network-admin's WireGuard management moves from Linux to a seL4 PD; the Linux guest has no wg0 interface; peer addition requests flow Linux VM → seL4 IPC → wireguard-control PD → kernel state.

Option A — Pure seL4 protection domains, no virtual machines

Status: planned/intended. Gate: Option C ships and is stable.

No virtual machines. No VMM. Every PPN service is a seL4 protection domain. WireGuard is ported to a seL4 PD with no Linux socket layer. Fleet management and service routing are protection domains. This produces the smallest possible trusted computing base.

seL4 microkernel (EL2 — AArch64 only for formal claims)
├── PD: wireguard     [WireGuard crypto + peer table, seL4 IPC only]
├── PD: fleet-tracker [service-vm-fleet, no tokio, no std net]
├── PD: doorman       [inference routing, seL4 IPC-based]
└── PD: ppn-control   [os-network-admin, CPace ceremony]

Eliminating the Linux guest removes the largest unverified component from the stack. On AArch64 EL2 with the confidentiality proof in progress as of mid-2026, Option A targets all three CIA properties at the kernel layer — the deepest security posture of the three options.

Microkit 2.2.0 architecture targets

Microkit 2.2.0 — the seL4 Foundation's recommended framework for new seL4 projects — supports these hardware targets:

Target Architecture Hardware virtualisation Verification
aarch64 AArch64 No (EL2 only) Integrity proof (April 2025)
x86_64_generic x86-64 No (TCG software) Functional correctness
x86_64_generic_vtx x86-64 Yes (VT-x/AMD-V) Functional correctness

x86-64 support was added in Microkit 2.1.0. This architecture is a valid development and runtime target but does not carry the integrity or confidentiality proofs available on AArch64.

Summary

Option seL4 as Linux Trusted computing base Verification Status
B (current) Hypervisor Guest VM seL4 + VMM + Linux AArch64 integrity Active
C (planned) Hypervisor + WireGuard PD Guest VM (limited) seL4 + VMM + WireGuard PD + Linux AArch64 integrity Planned/intended
A (planned) OS (all components) None seL4 only AArch64 all CIA (in progress) Planned/intended

See also

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 →