Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Current Status

capOS boots on x86_64 QEMU and on a real Google Compute Engine instance. It starts a standalone init from a Cap’n Proto boot manifest and runs a native shell plus a resident service over typed capabilities. No capOS endpoint is publicly exposed, and no path in the tree carries production authority.

A Validation: line names the gates that prove the claims above it. Those gates run locally: a candidate’s full gate set has to pass before it can integrate, and agents and the operator run focused gates on demand. What no gate establishes is currency. Nothing re-runs the whole set on a schedule, and each run’s output lives in its task worktree and is deleted with it, so a Validation: line means “this passed when the work was accepted”, not “this passes today”. Re-run the gate before relying on a claim.

Default Boot

make run builds the ISO from the default init-owned system.cue and boots it in QEMU. On that boot:

  • The kernel validates the kernel-owned boot boundary and boot-launches the standalone init process only. The service graph, login, session, and broker flow all live in userspace.
  • init starts exactly two services from the manifest graph: the resident chat-server endpoint service and the foreground capos-shell.
  • The shell mints its own anonymous UserSession on boot. login prompts for username> then hidden password>, validates the selected bootstrap account through CredentialStore and SessionManager, and upgrades the session in place to a broker-issued operator bundle. setup can create a volatile local operator credential and then follows the same upgrade path.
  • The adventure, paperclips, and chat-client demos are manifest binaries, not started services. The MOTD carries the exact run/spawn lines an operator uses to launch them after login.
  • make run forwards 127.0.0.1:2327 to guest port 2327 and 127.0.0.1:8080 to guest port 8080. Neither the remote-session CapSet gateway nor the Web UI is a default service, so those forwards reach nothing on a stock boot. Both binaries stay in the manifest so an operator overlay can rewire them onto the Phase C userspace network stack.

Validation: make test-default-boot, which also asserts that the two retired-listener services are never spawned.

Session expiry

Default password-authenticated local operator sessions have a bounded absolute expiry derived from the configured profile lifetime – 15 minutes by default – in addition to logout, terminal/connection/process-tree close, or administrator revocation. SessionLifetimeConfig::UNBOUNDED_MS (u64::MAX) is the reserved explicit opt-in for a non-expiring profile. Absolute expiry uses saturating addition, so a sufficiently large finite configured lifetime also reaches u64::MAX and behaves as non-expiring; such a value is not a safe way to express bounded policy.

Local password login is username-aware on the ordinary foreground shell path. Durable multi-account credential storage remains future work: the seeded accounts are manifest-sourced.

Implemented

Boot and kernel baseline

  • Limine boots the x86_64 kernel in QEMU. The kernel initializes dual UART output, GDT, IDT, LAPIC, syscall MSRs, memory management, page tables, heap allocation, and the global capability registry. The legacy PIC/PIT path remains as a fallback when LAPIC timer setup or PIT-based calibration is unavailable.
  • The kernel creates its own page tables with per-section permissions and keeps the higher-half direct map for physical memory access. SMEP/SMAP are enabled when the QEMU CPU advertises support.
  • User page-table map, unmap, and protect operations route through a TLB shootdown helper keyed by address-space CPU residency. Remote targets get pending full-TLB flush generations plus vector-49 IPIs, and the sender waits for observed target completion after ring dispatch releases address-space, cap-table, and scratch locks. Deferred queue slots are reserved before page-table mutation, and drains flush the current CPU before waiting.
  • AP cpu=1 can own scheduler and user execution under -smp 2. APs register their PerCpu records, program LAPIC timers from the BSP calibration, update AP TSS.RSP0 during context switches, and enter the scheduler from the AP idle loop. One scheduler owner is kept: while AP cpu=1 is online with a programmed timer, the BSP stays in kernel idle so the process-wide capability ring is not executed concurrently.
  • Independent CPU-bound worker processes scale across two vCPUs. make test-smp-process-scale builds its own ISO, runs repeated -smp 1, -smp 2, and best-effort 4-vCPU cases, stores raw serial logs under target/smp-process-scale/<timestamp>/, and enforces a 1.6x median speedup threshold when KVM-backed evidence is available. Measured 1-to-4 scaling is weaker than 1-to-2, so only the 1-to-2 gate is claimed.

Validation: cargo build --features qemu, make run-smoke, make test-smp-process-scale.

Process and userspace runtime

  • Processes have isolated address spaces, one or more internal Thread records with per-thread kernel stacks and saved CPU context, CapSet bootstrap pages, capability rings, and local capability tables.
  • ELF loading supports static no_std userspace binaries and TLS setup. targets/x86_64-unknown-capos.json defines the capOS userspace target for booted init, demos, shell, and capos-rt builds; the kernel default target remains x86_64-unknown-none.
  • capos-rt owns the userspace entry path, allocator initialization, ring-client access, typed clients, result-cap parsing, and owned-handle release. It is the only source owner for the userspace _start, panic, global allocator, raw syscall, and capos_rt_main handoff surfaces; a source check guards that split.
  • ProcessRingReactor gives process-scoped multithreaded calls one runtime-ring CQ drainer. Generation-checked user_data slots route completions to callers, while each caller blocks on ParkSpace through its own thread ring and never consumes the runtime CQ. A same-process ring kick makes a cap_enter-blocked drainer retry newly published SQ work.
  • In-process threading is implemented through ThreadSpawner/ThreadHandle caps and ThreadControl.exitThread: create, join, detach, self-join rejection, exit-code observation, and last-thread process exit. Private ParkSpace wait/wake carries timeout, wake, and reserved-waiter completion semantics. SharedParkSpace park-words remain future work.
  • The schema-bound host analyzer for bootstrap capability expectations, package emission of deterministic ServiceRevision analyzer inputs, and the launcher-visible startup-failure path are implemented. The artifacts remain host-only diagnostics and do not enter boot or launch authorization.

Validation: tools/check-userspace-runtime-surface.sh, make capos-rt-check, make init-capos-build, make demos-capos-build, make shell-capos-build, make capos-rt-capos-build, make run-smoke, make run-spawn, make test-runtime-ring-reactor.

Capability ring and IPC

  • The shared ring ABI carries CALL, RETURN, RECV, RELEASE, NOP, CANCEL, compact ParkSpace PARK/UNPARK, and owner-only service-facet minting without a spawn. Unauthorized or failed minting installs nothing. FINISH stays reserved for the future system capnp transport. The wire contract defines each opcode’s fields.
  • cap_enter processes submissions and can block until completions arrive or a timeout expires. Endpoints route ring-native IPC between processes, and direct IPC handoff lets a blocked receiver run before unrelated round-robin work once a matching CALL arrives.
  • One-hop promise pipelining is implemented over kernel-served and endpoint antecedents: a dependent call dispatches against a capability returned by another vat with no userspace round trip. Chains deeper than one hop remain out of scope until the ABI grows a distinct answer-allocation field.
  • Transport errors and application exceptions surface through CQEs and typed runtime client errors. Ordinary capability implementation errors, revoked ordinary/endpoint use, live endpoint target errors after endpoint identification, and endpoint RETURN application failures use serialized CapException payloads when a caller result buffer can safely receive one. No-payload application failures report CAP_ERR_APPLICATION_EXCEPTION_TRUNCATED; malformed transport metadata and unsafe result-buffer paths remain transport errors.
  • debug_tap builds export metadata-only ringtap: records for observed SQEs and posted CQEs on the QEMU/debug UART. The format is fixed, bounded, and deliberately records payload_len = 0 until a separate payload-capture authority lands. tools/ringtap-viewer/ parses those logs into SQE/CQE summaries.

Validation: cargo test-ring-loom, make run-smoke, make run-spawn, make run-smoke CARGO_FLAGS='--features debug_tap', make test-ringtap-failing-call, make run-promise-pipeline, make test-service-facet-mint.

Kernel capabilities

The implemented capabilities cover console and terminal output, boot package and manual, frame and memory objects, virtual memory, endpoints, timers and wall clock, entropy, threads and park spaces, process spawning and control, pipes, notifications, sessions and credentials, audit and log surfaces, block devices and filesystems, stores and namespaces, and device authority. Per-cap methods, grant sources, fail-closed rules, and proof targets are in Repository Map.

Per-process controls bound endpoint queues and scratch; ResourceLedger reserves cap slots, virtual pages, and frame grants before mutation, releasing on rollback or teardown. Exhaustion leaves calls usable and reports spawn OOM as overload. This is containment, not fairness; Resource Governance separates enforced from policy limits.

AuditLog reports ceilings, usage, and refusals but has no per-producer charge, protected lane, persistence, or retained records.

Validation: make run-smoke, make test-memoryobject-shared, make run-spawn, make test-shell, make test-terminal, cargo test-lib, make test-untrusted-exhaustion.

Capability transfer and release

  • IPC CALL and RETURN support sideband transfer descriptors. Copy and move transfer are implemented, and move transfer reserves the sender slot until destination insertion and commit.
  • Transfer result caps carry interface ids to userspace.
  • CAP_OP_RELEASE removes local capability-table slots. Runtime owned-handle drop queues one local release, and Runtime::flush_releases() forces queued releases when code cannot wait for the next ring-client acquisition or drop.

Validation: cargo test-lib, make run-smoke.

Manifest tooling and focused proofs

tools/mkmanifest turns a CUE manifest into a Cap’n Proto boot manifest. The build uses repo-pinned Cap’n Proto and CUE tool paths through the Makefile; direct mkmanifest invocation also rejects missing, unpinned, or version-mismatched CUE compilers. mkmanifest cue-to-capnp extends the same pinned-tool policy to general CUE-authored data messages.

Every focused proof boots its own manifest under manifests/ rather than the default graph, so a proof grants exactly the caps it needs and nothing else. Demo logic stays out of shell builtins and reaches its service only through explicit StdIO plus endpoint grants, and the accelerated Paperclips proof first verifies that normal server authority rejects fast-forward and a forged proof_accelerator: @timer grant. demos/service-common/ holds the shared caller-session endpoint loop and chat actor helpers those services reuse.

Validation: cargo test-mkmanifest, make generated-code-check, make run-smoke, make run-spawn, make test-shell, make test-chat, make test-adventure, make test-paperclips.

System manual

Boot-packaged Manual provides read-only shell, Web UI, and API access. It has 14 section-1 pages, three in section 7; generated section 2 covers every interface. Sections 3/5/8 are empty. One build ID grounds the corpus, not ISO contents.

Validation: make test-system-manual-smoke.

Storage and persistence

Storage is capability-scoped: a cap reaches one device, one mount, or one directory, and no method widens it. Attenuation is structural rather than a rights flag, so a read-only export cannot be upgraded at runtime.

  • Block devices. BlockDevice (readBlocks/writeBlocks/info/flush) is scoped to a single device index. The production build resolves it to the userspace-brokered NVMe arm; the qemu build routes bounded sector I/O to the kernel-owned virtio-blk driver as a named fixture, not production storage. Gates: make test-virtio-blk, make test-multi-virtio-blk.
  • Transactional record store. The CAPOSRS1 WAL provides atomic multi-record commit frames over an abstract block seam, checksum-chained bounded-prefix recovery with ordered tail invalidation, fail-stop remount after indeterminate I/O, fail-closed geometry validation, secondary-key lookup, and a compaction-capable A/B superblock format. In-system proofs cover reboot durability and bounded forced-poweroff torn-write recovery across three boots of one disk image (make test-record-store, make test-record-store-compaction).
  • Filesystems and key-value store. Read-only CAPOSRO1, FAT32 read, and writable CAPOSWF1 serve Directory/File capabilities; the CAPOSST1 disk store serves a Store (put/get/has/delete) whose durability commit point is the superblock rewrite. All back onto virtio-blk or a brokered NVMe window, all fail closed on a malformed image, and their mount parsers are fuzzed. Gates include make test-storage-fs and make test-storage-persist.
  • Host directory passthrough (development fixture). virtio-9p serves structurally separate read-only and opt-in writable Directory/File capabilities over a bounded 9P2000.L subset, including host-verified multi-chunk writes, a single spawn-granted writer whose writable results are non-transferable, and WASI payload hot reload. This is development infrastructure, not a production storage path; hostile-server reclaim, Tfsync crash durability, and host rename TOCTOU remain open residuals. Gates: make test-virtio-9p-fs, make test-virtio-9p-write, make test-wasi-9p-reload.
  • Task coordinator persistence. The Endpoint-serving coordinator restores and writes through canonical current/temp/backup files when granted a writable state Directory, and stays in-memory otherwise. Its bounded 9p path fails closed on malformed or ambiguous state and preserves fencing generations, and the Phase C network process serves the HTTP/JSON task API while only its coordinator child holds the writable state cap. That 9p path is explicitly weaker than the fenced CAPOSRS1 WAL over BlockDevice and is not production storage durability. Gates: make test-task-coordinator-9p, make test-task-coordinator-api-9p, make test-task-coordinator-persist.
  • Installable system. Persistent data-region mount, config-overlay compose/merge fallback, generation and rollback machinery, installable disk packaging, target-disk install, first-boot provision, and update/rollback are landed for a bounded local/QEMU contract. Namespace remains RAM-only, and no secure boot, image signing, or production release authority is claimed. Gates: make test-installable-install, make test-installable-provision, make test-installable-update.

Boot sources

The kernel boots from more than the default ISO path:

  • ISO under BIOS, the default (make run).
  • UEFI, booted through OVMF (make test-uefi).
  • A GPT disk image with an ESP, under both UEFI and BIOS (make test-disk, make test-disk-bios). The same image builder produces the GCE-importable tarball.
  • A digest-verified ISO binary registry. Under the boot_iso feature the kernel builds a validated (name, lba, size) registry from the ISO 9660 directory through its own ATAPI driver and loads binaries from the ISO rather than from embedded manifest blobs, verifying each against the manifest’s recorded SHA-256 before use. make test-boot-iso proves the load path, make test-boot-iso-read the on-demand read, and make test-boot-iso-failclosed that a digest mismatch refuses the binary.

Design: Boot Flow.

Validation: make test-uefi, make test-disk, make test-disk-bios, make test-boot-iso, make test-boot-iso-read, make test-boot-iso-failclosed.

Host-side SDKs

The language support below covers what runs inside capOS. The SDKs are the other axis: what talks to a running instance from another machine.

Two packages, both named capos, are published and speak deliberately different transports. The Python SDK (capos-python/, a pyo3 binding over tools/remote-session-client) reaches the remote-session CapSet gateway on guest port 2327 and is capability forwarding, bounded by session login, broker profiles, and the session’s CapSet. The JavaScript SDK (capos-js/, pure TypeScript with no runtime dependencies) reaches the web bridge HTTP API on guest port 8080 and is a data bridge that carries DTOs and never an invokable capability. Both published surfaces cover login, session metadata, MOTD, and CapSet listing; build-identity calls exist in the source tree ahead of a release.

Design: Host-Side SDKs, Capability Model.

Validation: make capos-sdk-check, make sdk-publish-dry-run.

Programming language support

Native Rust

Native capOS Rust is the only implemented booted Rust language path: #![no_std], alloc, capos-rt, static ELF binaries, and the targets/x86_64-unknown-capos.json custom target. Rust std is not supported.

Native C and POSIX

C boots through the libcapos C-substrate (make test-c-hello exercises Console + Timer + EntropySource + a 4 KiB anonymous VM round trip) and through the POSIX adapter. Both bypass WASI – they are static ELF binaries linked against libcapos.a and, for POSIX, libcapos_posix.a. The implemented POSIX surface is covered by focused make test-posix-* targets plus make run-posix-file, and spans:

  • pipes, fork-for-exec, direct posix_spawn, minimal file actions, read, and waitpid over ProcessSpawner/Pipe;
  • Console-backed stdio, where read(0, ...) stays closed without a stdin grant;
  • open, write, lseek, read, opendir, readdir, and closedir over a granted root Directory;
  • a focused printf/string/numeric/ctype subset;
  • Timer-backed time, nanosleep, and sleep plus documented fail-closed signal-delivery stubs.

posix_spawn() accepts argv/envp for source compatibility but does not deliver them until LaunchParameters/environment support lands. Broader C/libcapos surface and full POSIX adapter scope remain future design. The POSIX DNS resolver smoke is retired with the kernel socket owner and must be rebuilt on the userspace network stack before it counts as validation.

WASI

Sandboxed wasm32-wasi is the booted WASI-hosted language path. The wasm-host userspace binary (capos-wasm/, over vendored wasmi) hosts modules whose wasi_snapshot_preview1 imports are backed by typed capOS capabilities:

  • Console, Timer, and BootPackage; a per-instance argv text grant; a bounded environment text grant through initConfig.init.wasiEnv; and an optional EntropySource cap looked up under the well-known CapSet name random.
  • Filesystem: the manifest-granted root Directory is installed as a preopened fd. Payloads write and read back through path_open/fd_write/fd_close/ re-open/fd_read, and the preopen sandbox refuses absolute paths and parent-escape .. segments.
  • Clocks: clock_time_get(CLOCKID_REALTIME) reads UTC through a manifest-granted kernel WallClock cap. WallClock is a manifest-selectable boot-base UTC source with a historical fixed-base fallback; both sources remain untrusted, so timestamps are not cross-reboot comparable or security-grade validity evidence.
  • poll_oneoff services CLOCKID_MONOTONIC and CLOCKID_REALTIME clock subscriptions. Fd-readiness subscriptions still fail closed ERRNO_NOTSUP.

Every granted capability has a matching ungranted refusal gate: without the grant the corresponding import returns ERRNO_NOSYS or ERRNO_NOTSUP without entering the kernel. Storage and socket imports (path_open, fd_read, sock_send, sock_recv) keep their fail-closed gate.

Other languages

C++, Go, Python, JavaScript/TypeScript, and full POSIX shell/utilities are not implemented as supported capOS runtime paths. Lua has a Phase 0 in-tree capability-aware Lua-subset interpreter under demos/lua-smoke/ (make test-lua-smoke); it validates the long-term capability-userdata host API design but is not a PUC Lua dialect-compatible runner.

Partially Implemented

Focused init-owned spawn and measurement boots

The focused init-owned spawn path is make run-spawn. There the kernel boot-launches init with Console, BootPackage, and ProcessSpawner. Parent endpoint facets used for later service-sourced imports are returned by ProcessSpawner during child spawn, not granted at boot. init performs metadata-only manifest validation, resolves kernel and service cap sources, spawns children through ProcessSpawner, records exports, waits for children, and reports failures through Console output.

Measurement startup follows the same boundary. make test-measure uses manifests/system-measure.cue, where the kernel boots standalone init with Console, BootPackage, and ProcessSpawner, and init spawns ring-nop and thread-lifecycle with their measurement-only caps. Kernel bootstrap loads only initConfig.init and validates only the kernel-owned manifest boundary; mkmanifest and init own initConfig.services graph validation.

Recorded dispatch, schema-parsing, round-trip, throughput, and receiver- selection measurements live in Benchmarks and the tracked evidence bundles under docs/benchmark-data/. They are nested-QEMU/KVM observations, not hardware or production-performance claims.

Scheduling

The scheduler is weighted fair queuing over generation-checked ThreadRef per-CPU run queues, with per-CPU current and handoff slots, bounded stealing, eligibility-resolved wake placement, and per-thread runtime and virtual-runtime charging. Weight is a relative share among runnable work, and a migration preserves the thread’s accumulated fair-share position rather than resetting it. The runtime, virtual-runtime, and last-start ledger is unconditional because WFQ and budget charging depend on it; context-switch, migration, and placement counters remain measure-only diagnostics.

Landed on top of that baseline:

  • SchedulingContext: bind, revoke with generation identity, budget enforcement, endpoint donation and return, depletion notification, and a session-logout hook that makes a stale context fail closed.
  • CpuIsolationLease: pool grants and leases with timeout-based auto-revoke driven by a recorded leaseLifetimeNs.
  • Bounded SQPOLL ring mode with periodic-tick service and bounded producer-wake, plus the clockevent/deadline substrate underneath it.
  • Per-thread saturation inputs – preemption, voluntary-block, and runnable-but-not-running time – exported through SchedulingPolicyCap.snapshot and consumed by the AutoNoHz heuristic.

Tickless idle is not on for runnable contention: automatic nohz activation still waits on a proof that SQPOLL and poller progress do not depend on periodic scheduler ticks, and on the remaining network-polling, IRQ-affinity, and housekeeping dependencies. Priority and policy scheduling are deliberately deferred until the authority and IPC semantics settle. The recorded 1-to-4 thread-scale figure was manually accepted; the harness-enforced gates remain the 1-to-2 work and total speedups.

Design: Scheduling.

Validation: make test-thread-fairness, make test-thread-fairness-interactive, make test-thread-fairness-weight-change, make test-thread-fairness-sleeper-floor, make run-scheduling-context, make test-scheduler-cpu-isolation-lease, make test-scheduler-cpu-isolation-pool-grant, make test-scheduler-generic-sqpoll-nohz, make test-scheduler-autonohz-policy-service, make test-thread-scale.

TLS and key custody

capOS terminates TLS 1.3 itself. capos-tls/ is a workspace crate carrying the handshake core, X.509 verification and trust, DER, certificate store, ACME, renewal, self-signed issuance, and a TlsServerSigner seam that keeps the handshake away from private key bytes.

  • Server termination: remote-session-web-ui serves the Web UI over a TLS endpoint it terminates. Termination is a boot-manifest decision – a tls_terminated_endpoint marker makes the network stack forward the marker and grant an EntropySource – and the service refuses to boot on either marker without the other, or on a request for termination in a build that links no TLS stack. The proof drives a host OpenSSL client over hostfwd through a full handshake, pins the served leaf against the fingerprint the guest logged, fetches a Web UI response, and confirms plaintext HTTP is refused on the same port. The TLS stack is a default-off tls-endpoint feature, so the plain-HTTP path links none of it.
  • Client handshake: a userspace process completes a TLS 1.3 client handshake over the Phase C TcpSocket cap.
  • Alert path, ALPN, and close behaviour are landed, including the RFC 8446 §6 alert path and the epoch and deferred-accept lifecycle around a connection that never completed a handshake.
  • Key custody: PrivateKey/PublicKey RAM signing, handle-based KeyVault generation, open, list and destroy, and a development-only KeySource bootstrap for local proofs.
  • ACME account and order flow with certificate-store rotation and renewal.

The bounds are real. Key custody is RAM-only and both chains are development-signed; there is no public CA, DNS, or production key custody. The validity clock is the untrusted sampled-base WallClock, so certificate validity is not security-grade evidence. And this is all local and QEMU: a capOS-terminated public endpoint is a separate on-hold step.

Design: Certificates and TLS.

Validation: make capos-tls-test, make run-cloud-tls-webui-terminated, make test-cloud-tls-client-handshake, make test-cloud-tls-webui-deferred-accept, make test-cloud-tls-webui-epoch-drain-latch, make test-crypto-keyvault-custody, make test-crypto-symmetric-key, make test-crypto-keysource-bootstrap, make webui-login-peer-logic-test.

Remote-session CapSet gateway

The gateway is not started by the default manifest; it runs under its own focused manifests and proofs. Its connection table, per-slot aggregate charge, per-principal login table, deadline thresholds, selection-cycle work, and close-drain behavior are enforced ledger contracts with a bounded, secret-free readback.

The readback is read-side evidence. It measures rather than bounds head-of-line blocking: there is no independent reaper, no protected progress for unrelated slots, no synchronous-work budget, and no calibrated attacker/defender CPU ratio. One unauthenticated peer can still force credential hashing and serial multi-second waits that delay other slots and their timeout recovery.

Each bound, its derivation, its effective value, its overload and recovery behavior, and its open descriptor gaps are in the CapSet gateway connection descriptor inventory.

The host client has a loopback Web bridge and Tauri check/dev wrapper. Browsers get view models, not capabilities; neither tool is packaged or has a current guest gate.

Validation: make remote-session-tauri-policy-smoke.

SSH shell gateway

The authority prerequisites and the fixture authentication path that precede an encrypted SSH transport are implemented, each with a bounded QEMU smoke:

  • Host-key fixture signing (make test-ssh-host-key): a development-only non-production SshHostKey cap returns public metadata, signs bounded fixture exchange hashes, fails wrong-algorithm requests closed, and does not leak the private seed.
  • Authorized-key lookup (make test-ssh-authorized-key): a manifest-seeded AuthorizedKeyStore accepts configured ssh-ed25519 keys mapped to seed-account principals and denies unknown, disabled, and unsupported-algorithm keys.
  • Public-key session minting (make test-ssh-public-key-session, make test-ssh-public-key-auth): SessionManager.sshPublicKey verifies a bounded signature over fixture authentication bytes before minting a publicKey UserSession, and logs stable audit reason codes for each denial path. UserSession.auditContext fails closed after logout.
  • Unsupported feature policy (make test-ssh-feature-policy): the capos-config::ssh_policy surface classifies password auth, exec, SFTP, direct-tcpip, agent/X11 forwarding, env import, and extra session or shell channels into stable audit reason codes.
  • Restricted shell launcher (make test-restricted-shell-launcher): a manifest-declared RestrictedShellLauncher launches only capos-shell, injects supplied terminal/session caps plus child-local stdio, rejects session/profile mismatch and dangerous pass-through grants, and strips hidden process-supervision result caps.

Encrypted SSH packet transport, OpenSSH-compatible key exchange and channel handling, full userauth transcript validation, channel binding, TerminalSessionFromByteStream wiring, a terminal host over the userspace network stack, and a production OpenSSH harness remain open. The bounded terminal-host proof is retired: it sat on the removed qemu-only kernel socket owner, and any replacement must target the userspace network stack. The landed proofs use development/fixture key material; they are not a production SSH service and are not safe for non-loopback deployment.

Hardware and device authority

IOMMU and DMA backend

Backend selection is a runtime, fail-closed kernel decision: direct IOMMU remapping only when a probe verifies usable hardware, otherwise kernel-owned bounce buffers.

IOMMU reporting is currently policy-only. Malformed DMAR/IVRS structures fail closed. DMAR DRHD include-all or single-hop PCI endpoint device-scope metadata can mark retained DMA-capable PCI functions as IOMMU-attached; bridge and multi-hop scopes stay diagnostic-only until PCI topology traversal exists, and include-all fallback fails closed when retained coverage metadata is capped. Direct DMA remains blocked with zero trusted domains, remapping tables are not programmed, exported device addresses would be IOVA-only, host physical addresses are not user-visible, and every retained DMA-capable prototype function requires bounce buffering.

Bounded DMA, MMIO, and interrupt grants

Bounded manifest grants exist for DMAPool, DeviceMmio, and Interrupt. Reachable today: DeviceMmio read-only userspace mapping over boot-preseeded BAR pages plus brokered read32 and claimed-register write32; Interrupt info and admission-only wait/acknowledge/mask/unmask; and DMAPool allocation of eight fixed manager-attached bounce-buffer DMABuffer caps with typed free, single-page map/unmap, and manager-accounted descriptor submit/complete. A shared pure capos-lib::device_authority validator makes the range, alignment, protection, and handle-identity decisions before the kernel maps or touches anything, so writable, executable, unknown-protection, zero-size, unaligned, overflowing, and out-of-BAR requests are denied first.

Blocked: allocations beyond the eight fixed slots, real DMA side effects, writable userspace BAR mappings, arbitrary MMIO writes and doorbells, unbrokered register access, blocking IRQ wait, hardware acknowledgement, IRQ ownership, hardware mask/unmask, MSI/MSI-X programming, and general IRQ delivery. One narrower runtime-visible exception exists for make run-ddf-provider-consumer, where the selected TX queue publishes into the kernel-owned virtio-net ring after the same authority, bounce-scrub, and notify-policy gates.

Per-method invariants – authority, handle identity, physical range, buffer lifecycle, fixed-slot budget, descriptor effects, ledger and zero-live evidence, and stale/cross-reset behavior – are in DMA Isolation.

PCI, audit, and diagnostics

  • The hardware bring-up path has bounded ACPI RSDP/RSDT/XSDT, MADT, MCFG, DMAR, and IVRS diagnostics plus reusable PCI config-space access through legacy I/O ports and Q35 PCIe ECAM. The x86 path programs masked MADT-backed I/O APIC routes for legacy IRQs while honoring source overrides.
  • PCI memory-BAR subregions are validated and mapped through a shared kernel helper before in-kernel drivers use device MMIO, and PCI capability walking reports non-programming MSI/MSI-X metadata. make run-pci-nvme applies the same metadata-only path to a QEMU NVMe controller, with controller init, admin/I/O queues, doorbells, and direct DMA not started or blocked.
  • make test-diagnostics boots a feature-gated COM1 early-boot diagnostics prompt before capability, scheduler, timer, manifest, or userspace startup, with bounded commands for status, CPU, memory, ACPI, PCI, IRQ, timers, devices, logs, reboot placeholder, and halt.
  • HardwareAuditLog.snapshot decodes lifecycle records through the kernel’s in-memory ring, including cursor requests outside the default latest 16-record tail, below-oldest clamping, and past-end empty cursor metadata on the overflowed ring. That kernel ring is itself volatile and unsigned: it is a staging buffer, not the durable record.
  • A userspace audit-log service drains that staging ring onto the capability-native Store, giving a recoverable segment ring with explicit retention, drop-oldest overflow that records gap and eviction markers, segment-scan crash recovery, manifest-scoped reader admission, and hash-chained tamper-evidence with per-segment HMAC seals. Audit records therefore do survive reboot. The seals use a development-only RAM-local key source; external verifier key custody, production key rotation and revocation enforcement, and authority-broker runtime reader admission are future work, so this is tamper-evidence for a local operator rather than evidence a third party can verify.

Each driver has a provenance map recording its cited spec, implemented wire-format subset, and capOS authority mapping.

Validation: make test-ddf-audit-service-persist-reboot, make test-ddf-audit-service-keyed-signature, make test-ddf-audit-reader-smoke, make test-ddf-audit-reader-runtime-admission, make test-diagnostics, make test-iommu-acpi, make run-net, make test-hardware-grant-cycle, make test-hardware-audit, make run-ddf-provider-consumer.

Networking

Networking is userspace-first. The kernel no longer depends on smoltcp, and the qemu-only kernel TCP/UDP socket entry points fail closed; new protocol logic belongs in the userspace stack.

Kernel-side virtio-net fixture

make run-net remains a lower-layer QEMU fixture, not a socket path. It covers modern virtio PCI transport discovery for the common, notify, ISR, and device-specific MMIO regions, feature negotiation (VIRTIO_F_VERSION_1, MAC when safe, and VIRTIO_NET_F_MRG_RXBUF), RX/TX split-virtqueue initialization, a TX descriptor completion proof, Ethernet ARP resolution from 10.0.2.15 to 10.0.2.2, and an ICMP echo round trip validated against the QEMU user-mode gateway with checksum and identifier/sequence checks.

Its DMA pages pass through a bounded kernel-owned device_dma pool ledger that accounts live bytes, page counts, page-rounded MMIO mapping bytes, interrupt holds, ring depths, and descriptor submission/completion while exposing no userspace DMA/MMIO/interrupt handles. Scratch-ledger proofs cover the budget/OOM refusal matrix, zero-live teardown evidence, and stale DMA page handles without touching the live virtio-net ledger.

QEMU exposes a transitional 1af4:1000 function with modern vendor capabilities; capOS accepts that shape only through the modern capability layout and lets the in-kernel owner claim and unmask only its own MSI-X routes. The wire-format subset and register provenance are in virtio-net.

Userspace network stack

The Phase C userspace smoltcp network-stack process owns the production socket path. Landed local/QEMU evidence: a userspace stack service grants an application client a TcpListenAuthority and serves TcpListener/TcpSocket caps for a hostfwd TCP round trip; DHCP/IPv4 lease, default-route, and ARP configuration; bounded ICMPv4 Echo Reply diagnostics; and the Web UI L4 serving path with distinct public, local-health, and provider-health listener capabilities. Production transport randomization requires a per-boot EntropySource grant – a boot without it refuses to publish with a typed, secret-free reason and binds no listener.

IPv6 is landed on the same stack: link-local addressing and Neighbor Discovery, Router Advertisement with SLAAC, GCE-style DHCPv6 address configuration including bounded DNS-server and domain-search option inputs, ICMPv6 Echo Reply, and IPv6 TCP listen and connect, each with a local proof and the last also over a real NIC datapath. The DHCPv6 path also has a bounded synthetic-clock lifecycle proof covering Renew, Rebind, and address/resolver withdrawal at expiry; its contract is recorded in the DHCP Plan. A separate system resolver proof models bounded, replacement-based admission of option-23 upstreams and option-24 search domains, exposes both through the typed status surface with provenance distinct from DHCPv4 option 6, and preserves static precedence and the prior configuration on refusal. The focused system-cloud-prod-ipv6-dhcpv6-gce-config manifest connects the DHCPv6 client proof to the resolver proof service through a shared demo-local endpoint codec; it proves scoped authority and atomic replacement in local QEMU, not a deployed production resolver handoff. The contract and evidence are documented in the System Resolver Plan. The address ABI is explicitly family-tagged so an all-zero IPv4 configuration can never be misread as an IPv6 state: the legacy accessor accepts IPv4 and fails closed on IPv6 with a malformedAddress class, and capos-rt surfaces the family and an IPv6-support flag on NetworkConfig.

Operator tools expose read-only status and bounded IPv4/IPv6 ping. A granted PacketTrace is header-only with capacity, filter, and expiry limits. The old kernel-socket client proof is retired.

The shared socket-object table, its fixed service-object and transport-buffer byte readbacks, the ingress ledger, and the lane capacities are bounded and observable; their configured and effective values are in Resource Governance. All of it is local/QEMU evidence; what has been proven on a real cloud instance is below.

Validation: make test-cloud-prod-ipv6-dhcpv6-gce-config, make test-network-dhcpv6-lease-lifecycle, make test-network-system-dnsresolver, make test-network-status-tool, make test-network-ping-tool, make test-network-ping6-tool, and make test-network-packet-trace.

Cloud instances

capOS boots on a real Google Compute Engine instance. make capos-cloudboot-image builds a GCE-compatible disk image and make cloudboot-test imports it, launches a temporary instance with no public IP and no service account, captures serial output plus a structured provider.json evidence record, and deletes every resource it created. The harness exits non-zero when teardown fails or evidence capture is incomplete, so a resource-leaking run cannot be reported as a success.

The demonstrated operator access path is the serial-console shell, which emits its own cloudboot-evidence: access-path serial-console-shell marker over COM1 rather than the harness inferring it from the kernel boot landmark. Remote shell access on a cloud instance is not productized; SSH and WebShell remain future tracks.

Bars proven on live instances, each on a temporary private instance that was then torn down:

  • Imported-image serial boot through the capos kernel starting landmark to manifest load, init start, and shell spawn, on e2-small.
  • Legacy virtio-net raw-frame bind against the live GCE NIC, booting the production non-qemu cloud kernel from the legacy datapath manifest: candidate select over the PIO BAR, real device MAC read, feature negotiation, full 4096-entry vring materialization, a broadcast DHCP DISCOVER transmit, and a device-to-host RX DMA. QEMU caps queue size at 1024, so the vring materialization has no local equivalent.
  • gVNIC bring-up on the modern GCE NIC: the gVNIC PCI function (1ae0:0042) recorded with BAR and MSI-X metadata, BAR0 mapped through DeviceMmio, manager-owned DMA pages for the admin queue and descriptor buffer, and one GQI/QPL TX/RX queue pair brought up far enough to send one DHCP DISCOVER raw Ethernet frame and receive one inbound IPv4 frame before teardown. A separate hardware-only proof records typed Nic.transmit, Nic.receive, Nic.macAddress, and Nic.linkStatus over that queue path with inline frame transfer and no host-physical or IOVA export. There is no reusable gVNIC provider service, no host conformance suite, and no gVNIC device model in QEMU, so this path has no local smoke that can execute the device.
  • NVMe Persistent Disk brokered READ through the provider authority path on c3-standard-4: one READ, not a reusable storage provider, filesystem integration, virtio-scsi path, Local SSD path, direct-DMA claim, or device-autonomous MSI-X claim.
  • ICMP echo answered over the live NIC to a same-VPC probe.
  • Private self-hosted Web UI serving: a same-VPC probe byte-verified the served bundle over the live legacy NIC in the no-public-IP posture.

Each bar is one recorded billable run against a single sandbox project, not a gate that anything reruns, and no instance carries a public endpoint, an unattended lifecycle, or production authority. Register-level detail and each driver’s implemented wire-format subset live in the per-device provenance maps: gVNIC, GCP Persistent Disk, virtio-net, and NVMe.

The no-spend parts of the provider harness do run as ordinary local gates. Preflight, evidence-grammar validation for the private and public Web UI proofs, ingress planning, teardown, and the provider-command allowlist each put stub gcloud/gsutil binaries first on PATH and assert they were never invoked.

Two GCE follow-ups are held rather than open. Public ingress with TLS needs the public-readiness chain and then fresh explicit authorization for exposure; private or generic GCE authorization does not cover it. The private IPv6 reachability proof is blocked on IAM: the sandbox credential can neither create nor list the dual-stack subnet and IPv6 firewall rule it needs, so it fails closed before reaching a billable resource.

AWS and Azure have device-protocol logic but no instance has ever been launched. ENA and MANA are pure host-testable encode/decode logic with host conformance suites vetted against the published specifications and the Linux reference drivers, with no QEMU proof by deliberate exception; the AWS and Azure storage work is a cloud-shape classification delta on the shared NVMe path, proven in QEMU. Live proofs on both are held pending provider access and explicit approval for a billable run.

Validation: make cloudboot-test and make cloudboot-gcp-storage-nvme-io-read-test are billable and need sandbox credentials. make cloudboot-gce-private-webui-preflight-check, make cloudboot-public-webui-preflight-check, make cloudboot-gce-private-webui-evidence-fixture-check, make cloudboot-public-webui-proof-evidence-fixture-check, make cloudboot-public-webui-ingress-plan-check, make cloudboot-public-webui-teardown-fixture-check, and make cloudboot-public-webui-provider-command-allowlist-check spend nothing.

Security and verification

The tree carries Miri, proptest, fuzz, Loom, Kani, generated-code, dependency policy, trusted-build-input, panic-surface, and DMA-isolation work.

  • make kani-lib is a bounded Kani gate over capos-lib bitmap, cap-table stale-handle, transfer preflight, transfer rollback, and frame-grant accounting invariants. The heavier prepare-copy to provisional-destination seam proof needs more memory than a workstation run and passed once under make kani-lib-full on a high-memory builder. Coverage is not complete for every trust boundary.
  • make kani-ring runs in default and measure configurations. Its seven harnesses check full-field SQE validation panic-freedom, accepted and one-field-invalid cases from an independent SQE oracle, fail-closed transfer-descriptor arithmetic, bounded SQ/CQ pending-or-recovery classification across counter wrap, an abstract concurrent-protocol state machine with non-vacuous witnesses, and the production RingSqConsumerState duplicate-owner and stale-generation rejection.
  • That is bounded model checking of the pure ring core at fixed 16-entry SQ / 32-entry CQ capacities. Weak-memory interleavings and scheduler/teardown races remain Loom-only, and the Kani gate does not prove the volatile ring page or the kernel dispatcher.
  • Two protocol families are additionally modelled outside Rust: the DMA ownership handoff and the scheduler lease, LAPIC one-shot, and nohz transitions each have TLA+ and Alloy models, with Loom models for the DMA deferred-completion and nohz paths. These check the abstract protocol, not the implementation that runs.

Exact model bounds and exclusions are in the security and verification backlog.

Repository and Tooling State

Run-target naming

make run and make run-display are the only operator run entrypoints. Every focused proof and every alternate manifest, firmware, device, or measurement QEMU variant uses a test-* target. Seventeen further run-* targets remain Gate C naming debt: they are live gates that have not yet been renamed, and tools/check_doc_make_targets.py reports each citation of them as a warning. The same check fails when any target’s non-exempt citation count exceeds its pinned docs/workflow/run-target-citation-budget.toml ceiling or an unlisted debt target gains a citation; reductions remain refreshable. New command-bearing documentation follows the workflow citation-authoring rule. Their migration inventory and retained carve-out records which are expected to move and which stay.

Task-coordinator interchange

tools/capos-task-coordinator-snapshot.py provides a deterministic offline plan-loopyard step with classified create, resource, dependency, and status entries, plus a local verify-plan companion that validates completeness and determinism, reconstructs the plan’s post-application target state, and proves that state is an idempotent planning fixed point. Neither command performs authenticated ingestion or mutation; the operator-authorized PostgreSQL importer that would close that gap is not built.

Not Implemented

Absent as supported capOS behavior today: service restart policy, capability-scoped system monitoring beyond the Phase 1 log surface, notification-driven service composition, promise chains deeper than one hop, service-facing SharedBuffer APIs over the MemoryObject substrate, session quotas, durable multi-account credential storage, broader account policy, production SSH or WebShell ingress, public ingress and TLS exposure, any AWS or Azure instance boot, broader storage variants, high-throughput or multiqueue NIC work, direct-remapping DMA, aarch64, and persistence beyond the landed installable data-region and generation paths.