Isolation backends

A service in space.yaml runs behind one isolation backend, named by its isolation field. The backend decides which kernel runs the workload and what the machine must provide to start it. The target profile decides which backends a machine offers.

Example

schema: space.project
version: "1"

run:
  partitions:
    payload:
      memory: 256
      services:
        - name: eo-classifier
          image: ghcr.io/parsimoni-labs/classifier:dev
          runtime: oci
          isolation: runc
        - name: sdls-downlink
          image: ghcr.io/parsimoni-labs/sdls-downlink:dev
          runtime: mirage
          isolation: hvt

space run --dry-run prints the backend each service resolved to, before anything boots:

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

Backends

Value	Workload runs as	Program the machine provides	Runtimes it accepts	Profiles that declare it
`runc`	An OCI container inside its tenant's machine	`runc`	`oci`, `host`	all five
`hvt`	A unikernel in its own KVM virtual machine, through a Solo5 tender	`solo5-hvt` and `/dev/kvm`	`mirage`, `unikraft`	`cm5`, `cm5-dev`
`spt`	A unikernel in a seccomp-confined process, through a Solo5 tender	`solo5-spt`	`mirage`, `unikraft`	none
`firecracker`	A virtual machine of its own under Firecracker	`firecracker` and `/dev/kvm`	`mirage`, `unikraft`, `oci`	none
`qemu`	A Unikraft ELF-loader image under the x86-64 system emulator, on any host architecture	`qemu-system-x86_64`	`mirage`, `unikraft`, `oci`	none
`host`	An uncontained process on the node's own kernel	nothing	`host`	none
`auto`	Whatever the build resolves: `runc` for an `oci` service, `host` for a `host` service		any

The list is Space_schema.Runtime.isolations, and isolation accepts exactly these values. The target profiles name which of them a machine offers.

A build refuses a service whose runtime its isolation cannot hold, naming both. The qemu launcher boots the service's image as the emulator's kernel and <image>.initrd beside it as the initial RAM disk, the pair a Unikraft ELF-loader build produces. A mirage or oci service passes the build's check under qemu and is launched the same way, so it starts only when its image is such a kernel and initrd pair. The qemu launcher attaches no block device, and it refuses a service that binds a volume. The runner refuses a host service unless it was started with --allow-host, which is for development machines only.

Tenant machines

A tenant is one project's partition. Each tenant's workloads run in a machine that belongs to that tenant alone: tenants never share a kernel. The container controls (a user namespace, seccomp, dropped capabilities, cgroups, and a read-only root) hold a tenant's own workloads apart from each other inside that machine.

A runc container reaches its tenant's machine in one of two ways:

The node is the tenant's machine. When the release a node boots names a single tenant, the runner runs inside that tenant's machine and starts the container there. It refuses a workload of any other tenant, naming both.
The runner raises the machine. Otherwise the runner boots one Firecracker virtual machine per tenant from the sandbox appliance under /usr/lib/space/sandbox, and starts each container inside it through the appliance's agent. This needs /dev/kvm, the firecracker binary, and the appliance, and the runner refuses the launch naming whichever is missing.

The hvt, firecracker, and qemu backends give each workload a virtual machine of its own. They still trust the node's kernel, the tender or virtual machine monitor, and the CPU's virtualization support.

Hypervisors under a target

The hypervisor under a virtual machine belongs to the target, and a service does not name it. Solo5 defines a host interface of about ten calls, so a unikernel built against it runs unmodified on any host that implements that interface. KVM on Linux is the hypervisor every profile that offers hvt uses. No profile uses Xen, Muen, or seL4 yet, and none of them is an isolation backend. Partition model dates when each arrives.

Xen is a type-1 hypervisor, one that runs directly on the hardware with no host operating system below it. It is validated on arm64, and SpaceOS unikernels run on it through the Solo5 host interface. It becomes a target-profile hypervisor once the runner prepares, launches, observes, stops, and releases a Xen guest through the same signed admission path as every other backend. In Xen, a domain is one virtual machine. A domain shares memory with another by granting it pages, and signals it through event channels, the virtual interrupts Xen delivers. Xen comes 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. The resource assignment is fixed when the image is built, and a domain grants pages and opens event channels to its peers, never to a control domain. This shape removes the Linux control domain and all runtime domain management from the trusted computing base.
- Dynamic. An ordinary guest under a dom0 running the xl toolstack, reaching network and block backends through XenStore, a key-value directory that dom0 serves and in which each domain finds its devices.
Muen is a separation kernel written in Ada and SPARK, whose proof shows the absence of runtime errors. It runs on x86-64 only.
seL4 is a microkernel whose functional correctness is verified in Isabelle/HOL. It runs on arm64 only. Its proofs cover specific verified configurations: the Microkit framework, the virtual machine monitor, and the device drivers SpaceOS uses sit outside that proof, so the verification holds for the kernel alone.

Accelerators

A backend gives a workload no device access. Access to a GPU or an FPGA is a signed grant checked by a broker, described in Partition model, and no shipped profile declares an accelerator.