Substrates

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:

partitions:
  payload:
    memory: 256
    services:
      - name: eo-classifier
        isolation: runc
      - name: sdls-downlink
        isolation: 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	Linux micro-VM images
Host process (host)	None	Development host	x86-64, arm64	Test fixtures

The substrate determines the strength of the isolation guarantee. The manifest format stays the same: one build.yaml composition runs on any backend that satisfies the service’s requirements, and run.yaml picks the backend per service.

Host hypervisors

Solo5 defines a host interface of about ten calls, so any hypervisor or separation kernel that implements it can run a MirageOS unikernel unmodified. Host hypervisors sit beneath isolation backends rather than being named in isolation:

• Xen. Type-1 hypervisor, validated on arm64, in two shapes:

  • 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, and the resource assignment is fixed when the image is built. A domain grants pages and opens event channels to itself rather than 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 [roadmap]. Separation kernel written in Ada/SPARK, with absence of runtime errors proven. x86-64 only. It runs SpaceOS but is not part of a validated configuration.

• seL4 [roadmap]. Microkernel whose functional correctness is verified in Isabelle/HOL. arm64 only, and a working prototype rather than a supported path.

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 claim does not extend to the whole running system.

Acceleration

Accelerator access (GPU, FPGA, AI engine) is a fact of the target profile, not of the substrate table: a profile declares the device classes it grants, a privileged broker mediates access against the partition’s signed capability envelope, and direct passthrough requires a dedicated device and an IOMMU. Targets without both requirements disable passthrough and preserve the isolation boundary.