Substrates

Release 20260415-259056f has no published substrate contract. The installed CLI exposes build, logs, push, run, and sbom. Its run help describes QEMU partitions loaded from a topology file. It does not list run.yaml, an isolation field, backend identifiers, hypervisor support, or accelerator access.

Current source code is not evidence for an older installed release. Publish a backend only after a test runs against that release artifact and records:

• the accepted configuration and backend identifier;
• the workload format and CPU architectures;
• the required host kernel, VMM, tender, and hardware features;
• the observed process, namespace, VM, device, and DMA boundaries;
• startup, shutdown, crash, and resource-limit behaviour;
• rejection of unsupported runtime and backend combinations.

Isolation is not authentication or encryption. A process sandbox shares the host kernel. A virtual machine can provide a separate memory boundary. It does not authenticate the workload. It also does not encrypt storage or traffic. Accelerator passthrough requires evidence for IOMMU policy and DMA isolation. A backend name alone proves none of these properties.

The remaining text is an unreleased design record. It is not a contract for the installed CLI.

Unreleased design record

A substrate is the isolation mechanism that runs a service inside a SpaceOS partition. The runtime selects it from service metadata, the target profile’s declared backends, and the service-level isolation field in run.yaml.

Example

A run.yaml service can request a substrate with isolation:

schema: space.run
version: "1"
image: _build/spaceos

partitions:
  payload:
    memory: 256
    services:
      - name: eo-classifier
        isolation: runc
      - name: sdls-downlink
        isolation: hvt

--dry-run reports the backend each service resolved to, so a request the target cannot satisfy is visible before the boot:

$ space run _build/spaceos --runtime run.yaml --dry-run | sed -n '4,8p'
partitions:
  payload   256 MB  apids (none)
    services:
      eo-classifier    runc
      sdls-downlink    hvt

Substrate matrix

A service can name these backends in isolation:

Substrate	Isolation	Host requirement	Architectures	Workload
Solo5/KVM (hvt)	Hardware virtual machine	KVM	x86-64, arm64	MirageOS and Unikraft unikernels
runc (runc)	Linux namespaces, cgroups, and seccomp	Linux	x86-64, arm64	OCI containers
Solo5/spt (spt)	Seccomp process sandbox	Linux	x86-64, arm64	Solo5 unikernels
QEMU (qemu)	Emulated virtual machine	QEMU on x86-64	x86-64	Unikraft unikernels
Firecracker (firecracker)	Hardware micro-VM, reduced device surface	KVM	x86-64, arm64	MirageOS and Unikraft unikernels
Host process (host)	None	Development host	x86-64, arm64	Test fixtures

The substrate sets the strength of the isolation guarantee. The manifest format stays the same across backends. One build.yaml composition runs on any backend that meets the service’s requirements, and run.yaml picks the backend per service. Build validation checks the pairing: a service whose runtime and isolation disagree fails at build time.

Firecracker takes Linux micro-VM images in 1.1, which gives a container workload a hardware boundary without a unikernel port. Today that workload runs under runc.

Host hypervisors

Solo5 defines a host interface of about ten calls, so any hypervisor or separation kernel that implements it runs a MirageOS unikernel unmodified. Host hypervisors sit beneath the isolation backends, and you do not name them in isolation:

• Xen. Type-1 hypervisor, validated on arm64, in two shapes. SpaceOS unikernels run on it through the Solo5 host interface today. It becomes a target-profile substrate once the runner can prepare, launch, observe, stop, and release a Xen guest through the same signed admission path as every other backend.

  • Static, dom0less. Xen starts each domain itself at boot from the device tree. There is no dom0 and no toolstack, so nothing on the running system can create, destroy, or inspect a domain. The resource assignment is fixed when the image is built. A domain grants pages and opens event channels to itself, never to a control domain.
  • Dynamic. An ordinary guest under a dom0 running the xl toolstack, reaching network and block backends through the usual XenStore rendezvous.

  The static shape removes the Linux control domain and all runtime domain management from the trusted computing base.

• Muen. Separation kernel written in Ada/SPARK, with absence of runtime errors proven. x86-64 only.

• seL4. Microkernel whose functional correctness is verified in Isabelle/HOL. arm64 only.

No target profile selects Muen or seL4.

seL4’s proofs cover specific verified configurations. The Microkit framework, the virtual-machine monitor, and the device drivers used by SpaceOS sit outside that proof boundary, so the verification holds for the kernel alone.

Acceleration

Accelerator access (GPU, FPGA, AI engine) is a property of the target profile. A profile declares the device classes it grants. A privileged broker checks each request against the partition’s signed capability envelope. Direct passthrough needs both a dedicated device and an IOMMU; a target that lacks either one turns passthrough off and keeps the isolation boundary whole.