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

Trust Boundaries

This page gives reviewers one place to find the hostile-input boundaries, trusted inputs, and current isolation assumptions that matter for capOS security review.

Like the verification workflow, this inventory is written for contributors and reviewers working inside the capOS repository, which is currently private. The source paths and REVIEW.md references below cite where each boundary is implemented and reviewed in that repository, not pages on this site.

Current Boundaries

Evidence labels below are deliberate. A named gate is a bounded proof of the stated scenario, not production assurance. Review-only means that this refresh found the enforcing code and symbol but no focused executable gate for the complete claim.

Stage 6 and Carried-Forward Surfaces

BoundaryCurrent observable stateGroundingEvidence
SQE entry and one-hop promised answersprocess_ring_with_budget validates the shared SQ/CQ state and dispatches bounded work. process_call_sqe resolves one-hop dependencies through the kernel-owned, 64-entry ENDPOINT_PROMISED_ANSWERS table. Endpoint antecedents can remain pending until dispatch_return resolves them; the private CAP_ENTER_PROMISE_RETRY latch resumes a deferred drain. Unknown, failed, unresolved, out-of-range, and exhausted answers return typed failures. Teardown clears entries by thread or process.kernel/src/cap/ring.rs: process_ring_with_budget, process_call_sqe, ENDPOINT_PROMISED_ANSWERS, clear_endpoint_promised_answers_for_thread, clear_endpoint_promised_answers_for_pid, dispatch_returnmake run-promise-pipeline proves the bounded QEMU path, including kernel-served and endpoint antecedents and cross-drain lifecycle. cargo test-ring-loom covers the generic ring protocol, not the endpoint answer table.
Capability copy, move, release, and epoch revocationTransfer descriptors are copied from the caller under its AddressSpace lock. prepare_transfer_grants admits explicit copy/move modes and rolls back reserved move sources on failure. CapTable::commit_prepared_move_transfer removes a committed move source; CapTable::remove releases a table hold; CapTable::revoke_object_caps advances shared object epochs so stale holds fail lookup. Copy preserves the source hold and shares the epoch.kernel/src/cap/transfer.rs: load_transfer_descriptors, prepare_transfer_grants; capos-lib/src/cap_table.rs: CapTable::prepare_copy_transfer, CapTable::prepare_move_transfer, CapTable::commit_prepared_move_transfer, CapTable::remove, CapTable::revoke_object_capscargo test-lib covers table transactions and epoch behavior. make run-promise-pipeline exercises result-cap insertion. The full cross-process atomicity argument remains review-only across complete_endpoint_recv_with_transfer_source and dispatch_return in kernel/src/cap/ring.rs.
Owner ↔ locally minted service-object facetCAP_OP_MINT_SERVICE_FACET admits only an endpoint owner. It rejects unsupported SQE fields and invalid result buffers before mutation, installs a client-only ServiceObject facet without spawning, rejects unauthorized interface or receiver-cookie relabeling, inherits rather than widens transfer scope, and rolls back provisional cap insertion and epoch allocation on failure.kernel/src/cap/ring.rs: dispatch_mint_service_facet; capos-lib/src/cap_table.rs: resolve_service_object_facet, resolve_endpoint_facet_delegation, EndpointFacetGrantMode::ServiceObjectmake test-service-facet-mint proves the owner-only grant path and injected epoch-allocation rollback in bounded QEMU scenarios.
CapObject::call params bytes ↔ generated decodersRing dispatch copies bounded caller params before selecting a capability object, but decoding remains distributed across each CapObject implementation. Implementations must parse with the generated Cap’n Proto reader before using fields or mutating state; malformed messages and schema values fail the call.capos-lib/src/cap_table.rs: CapObject::call, CapObject::call_with_context; kernel/src/cap/process_control.rs: ProcessControlCap::handle_retarget_caps; kernel/src/cap/notification.rs: handle_waitcargo test-lib covers capability-table dispatch behavior. Complete implementation-by-implementation decoder coverage remains review-only.
Log producers ↔ shared kernel log and readersA granted LogSinkCap accepts bounded records, truncates component and message fields, replaces non-printable bytes before storage and UART forwarding, filters below the configured minimum severity, and appends to a bounded drop-oldest ring. A separately granted LogReaderCap returns capped cursor/filter snapshots. Neither cap creates an ambient namespace or transfer authority; producer identity fields remain unauthenticated and per-producer backpressure remains future.kernel/src/cap/log.rs: LogSinkCap, handle_write, copy_sanitized, LogRing, LogReaderCap, handle_read, set_min_levelmake run-monitoring-log-smoke is a bounded QEMU proof of thresholding, truncation, neutralization, overflow, cursor, and reader filtering.
Endpoint RECV/RETURN and caller-session disclosuredispatch_recv admits a queued call and installs only explicitly transferred caps. dispatch_return completes the matching call, inserts result caps transactionally, and rejects stale or dead callers. Calls carry EndpointCallerSession, derived by endpoint_caller_session_for_thread; services that require it fail closed when the caller session is absent or no longer live. The disclosed reference is service-scope-keyed metadata, not a caller-selected badge and not authority.kernel/src/cap/ring.rs: dispatch_recv, complete_endpoint_recv_with_transfer_source, dispatch_return, endpoint_caller_session_for_thread, caller_session_is_live_for_thread; capos-lib/src/cap_table.rs: derive_endpoint_session_referencemake run-session-context proves immutable process context and service-scoped caller metadata. IPC transfer/rollback details beyond its scenarios remain review-only.
Notification signal/wait/revokeNotificationCap owns a shared pending-count/revoked cell. handle_signal either commits one waiter or latches a signal; handle_wait consumes or parks under a fixed 16-waiter global ceiling; revoke_shared makes the object inert and releases waiters with revoked. poll_waiters is the single deferred completion path and does not remove a committed wake before delivery succeeds.kernel/src/cap/notification.rs: NotificationCap, handle_signal, handle_wait, revoke_shared, poll_waiters, MAX_NOTIFICATION_WAITERSmake run-notification-object is a bounded QEMU proof for pre-signal, timeout, no-lost-wake, revoke release, and no-wake-after-drop.
Live-upgrade ProcessControl.retargetCapsProcessControlCap::handle_retarget_caps resolves generation-bound ProcessHandles, rejects self/same/dead targets, and requires an audit sink. retarget_endpoint_caps prepares and commits a bounded all-or-nothing move of endpoint owner caps. graceful refuses while the old process has an in-flight call or parked RECV; force moves the caps and cancel_endpoint_state_for_object_pid completes calls already taken by the old server with CAP_ERR_SERVER_DIED while preserving callers’ cap IDs for retry.kernel/src/cap/process_control.rs: ProcessControlCap::handle_retarget_caps, retarget_endpoint_caps; kernel/src/cap/ring.rs: cancel_endpoint_state_for_object_pid; capos-rt/src/client.rs: ProcessControlClient::retarget_caps, TransportError::ServerDiedmake run-cap-retarget proves the quiesced graceful path; make run-cap-retarget-force proves the typed disconnect/retry path. Both are bounded QEMU proofs, not a general availability proof for production upgrades.
Read-only debug attachmentA DebugSessionCap is minted only by ProcessHandleCap::handle_create_debug_session for the handle’s generation-bound target. DebugSessionCap::handle_cap_table_snapshot returns bounded metadata descriptors and zero result caps; it never serializes a raw CapId, badge, memory, or register state. Detach, exit, or PID reuse makes later snapshots fail closed and audited.kernel/src/cap/process_spawner.rs: ProcessHandleCap::handle_create_debug_session; kernel/src/cap/debug_session.rs: DebugSessionCap, DebugSessionCap::handle_cap_table_snapshot, record_debug_auditmake run-debug-session proves attach, bounded redacted snapshot, zero invokable-cap transfer, detach, stale-target refusal, and audit output in QEMU.
Crash-record teardown and redactionFault/kill paths note an unplanned death. Process teardown first revokes/releases caps, then Process::emit_crash_record_for_unplanned_death consumes the note and calls record_crash. The record contains a sanitized process name, schema-supported kind, load-base-relative fault offset, opaque session context, and monotonic timestamp; it contains no absolute RIP, cap ID/table entry, kernel pointer, or dead-process memory. Phase 1 emits to the kernel audit stream; the schema CrashRecord supervisor delivery remains future. Planned exit, including the current userspace panic handler, emits no crash record.kernel/src/process.rs: Process::emit_crash_record_for_unplanned_death; kernel/src/cap/audit_log.rs: CrashAuditRecord, record_crash; schema/capos.capnp: CrashRecordmake run-crash-disconnect proves fault-record emission after capability teardown and rejects an absolute fault-address leak. Other kinds and the absence of every possible disclosure remain review-only.
Kernel versus userspace networkingThe Phase C network-stack process owns the current production socket/protocol path. The remaining kernel NetworkManagerCap, TcpListenAuthorityCap, and virtio socket implementation are legacy QEMU fixtures. KernelCapSource::NetworkManager and KernelCapSource::TcpListenAuthority are constructed only under feature = "qemu"; the non-qemu BootCapFactory::build arms return errors directing manifests to userspace-served caps.kernel/src/cap/mod.rs: BootCapFactory::build match arms for KernelCapSource::NetworkManager and KernelCapSource::TcpListenAuthority; kernel/src/cap/network.rs: NetworkManagerCap, TcpListenAuthorityCap; demos/cloud-prod-network-stack-smoltcp-tcp-socket-cap-ipc-smoke/src/bin/server.rs: mint_service_objectmake run-cloud-prod-network-stack-smoltcp-tcp-socket-cap-ipc is a bounded QEMU proof of the userspace-served socket-cap path. The compile-time non-qemu refusal is code-review evidence here; it is not a production network-isolation proof.

The following supporting boundaries were rechecked for drift while performing the Stage 6 refresh. Their enforcement model did not change: Ring 0/user pointer validation, manifest and ELF parsing, spawn input validation, authentication/session brokering, host-tool containment, generated-code ownership, and panic-surface classification.

Ring 0 to Ring 3

  • Trust rule: the kernel trusts no userspace register, pointer, SQE, CapSet, or result-buffer field.
  • Implemented: syscall arguments, user-buffer ranges, page permissions, opcodes, and capability-table lookups are validated before privileged use in kernel/src/arch/x86_64/syscall.rs, kernel/src/mem/paging.rs, kernel/src/mem/validate.rs, and kernel/src/cap/ring.rs.
  • Validation: Panic Surface Inventory and REVIEW.md at the repository root.

Capability Table to Kernel Object

  • Trust rule: a process acts only through a live table-local CapId with matching generation and interface.
  • Implemented: capos-lib/src/cap_table.rs CapTable::get_arc rejects wrong generations and revoked object epochs; dispatch enters objects through CapObject::call_with_context.
  • Validation: cargo test-lib; cross-process behavior is covered only by the focused QEMU gates named in the Stage 6 table.

Capability Ring Shared Memory

  • Trust rule: userspace owns SQ writes, but the kernel owns validation, dispatch, completion, and failure semantics.
  • Implemented: capos-config/src/ring.rs CapRingHeader and CapSqe define the wire surface. kernel/src/cap/ring.rs process_ring_with_budget validates and dispatches it, using AddressSpace::copy_from_user / copy_to_user.
  • Validation: cargo test-ring-loom for the extracted ring protocol; the Stage 6 table names the focused IPC gates.

Endpoint IPC and Transfer

  • Trust rule: IPC cannot create or destroy authority except through explicit copy, move, release, or spawn transactions. Delegating an imported client facet must preserve service-visible identity, and shared-service handlers should derive caller identity from live caller-session metadata.
  • Implemented: the Stage 6 table names the dispatch_recv, dispatch_return, transfer-transaction, and caller-session symbols. Legacy badge metadata remains a debug/test surface, not ordinary caller identity.
  • Validation: Authority Accounting is the design invariant; executable coverage is split across the gates named in the Stage 6 table.

Manifest and Boot Package

  • Trust rule: boot manifest bytes and embedded binaries are untrusted until parsed and validated. Only BootPackage holders can request chunked manifest bytes; ordinary services receive no default boot-package authority.
  • Implemented: tools/mkmanifest validates the embedded initConfig graph before serialization. Kernel bootstrap validates the kernel-owned manifest boundary before loading one init process; init BootPackage validation resolves service graph references before spawning children. kernel/src/cap/boot_package.rs, capos-lib/src/elf.rs, and load paths still enforce manifest-read, ELF, load-range, CapSet, and interface bounds.
  • Validation: cargo test-config, cargo test-mkmanifest, cargo test-lib, manifest and ELF fuzz targets, and make run.

Process Spawn Inputs

  • Trust rule: parent-supplied spawn params, ELF bytes, grants, legacy badges, and result-cap insertion must fail closed. Endpoint kernel grants must not share owner caps with the parent. Delegated client facets must not be relabeled into another service identity.
  • Implemented: ProcessSpawner validates ELF load, grants, frame exhaustion, parent cap-slot exhaustion, child-local endpoint creation, and parent-only client result facets. Delegated ClientEndpoint grants preserve source identity; explicit relabel encodings fail closed except for owner or trusted parent endpoint-result caps.
  • Validation: spawn QEMU smoke evidence and review-finding task records.

Console Authentication and Setup

  • Trust rule: console input, account selectors, password verifiers, setup tokens, and passkey challenge state are hostile or sensitive until a login/session component validates them.
  • Implemented: Console remains output-only. The first interactive boundary is session-scoped TerminalSession with bounded readLine, visible/hidden echo, structured cancellation, one move-only foreground holder, caller-session-checked output, and stale-input scrubbing on cancel or owner teardown. CredentialStore verifies one manifest-supplied Argon2id operator credential and one bounded volatile RAM-overlay password created by first-boot setup. capos-shell drives login and setup; there is no separate ConsoleLogin service.
  • Validation: Boot to Shell, boot-to-shell gates on the loopyard task board (access-controlled), make run-terminal, make run-login, and make run-login-setup.
  • Open/future: durable multi-account credential storage, multiple verifier records, rotate/disable state, broader anti-enumeration audit policy, and bounded single-use setup-token/challenge state.

Session Authority and Audit

  • Trust rule: authenticated sessions receive only broker-issued narrow caps. Audit output, service logs, terminal output, and failed-auth diagnostics must not disclose secrets or verifier material.
  • Implemented: SessionManager mints entropy-backed UserSession metadata for operator, explicitly seeded guest, and anonymous profiles. Endpoint caller-session references are HMAC-SHA256 values scoped by an entropy-backed boot key and non-reused endpoint service-scope id. AuthorityBroker validates session/profile matches before minting bundles. RestrictedLauncher returns shell-scoped launch paths instead of BootPackage or broad ProcessSpawner authority.
  • Validation: User Identity and Policy, Boot to Shell, make run-login, make run-login-setup, and future auth/session hostile input tests.
  • Open/future: audit records, stable service-audit identity across endpoint replacement, opaque record IDs, mutable session liveness cells, UserSession.logout, owner-shell/gateway close propagation, narrow renewal paths, broader policy evaluation, and web-terminal origin/RP-ID validation.

SSH Remote Shell Ingress

  • Trust rule: SSH network input, keys, usernames, channel requests, PTY state, environment requests, and disconnects are hostile until the gateway validates protocol state, authenticates the user, and receives a broker-issued shell bundle.
  • Implemented: current proofs cover schema stubs, one development-only host-key fixture, manifest-seeded AuthorizedKeyStore, public-key session minting, unsupported-feature policy, restricted shell launch, and bounded terminal-host wiring over host-local plain TCP. The proposal keeps SSH transport authority in SshGateway; the spawned shell receives only an SshTerminalFactory-produced TerminalSession plus the normal scoped session bundle through RestrictedShellLauncher. Fixture host-key signing, authorized-key mapping, public-key session minting, SSH policy rejection, and restricted launcher inputs fail closed for malformed or unsupported cases.
  • Validation: SSH Shell Gateway, Runtime, Networking, and Shell, make run-ssh-host-key, make run-ssh-authorized-key, make run-ssh-public-key-session, make run-ssh-public-key-auth, make run-ssh-feature-policy, and make run-restricted-shell-launcher (the plain-TCP run-ssh-gateway-terminal-host terminal-host proof is retired with the kernel socket owner).
  • Open/future: full SSH transport transcript and channel binding, password-auth verifier/backoff wiring, production host-key storage, broader account storage, and production remote-shell hardening.

Identity Metadata and Account Records

  • Trust rule: users, principals, accounts, sessions, roles, and profile names are policy metadata, not kernel subjects, ambient authority, or substitutes for held capabilities.
  • Implemented: sessions receive capabilities only after authentication and broker policy evaluation; a principal or account record does not run or call the kernel.
  • Validation: Local Users, Storage, and Policy and User Identity and Policy.
  • Open/future: durable local account-store behavior, profile persistence, rollback checks, and quota enforcement.

Host Tools and Filesystem

  • Trust rule: manifest/config input must not escape intended source directories or invoke unconstrained host commands.
  • Implemented: tools/mkmanifest validates references and path containment, rejects unpinned CUE compilers, and Makefile targets route CUE and Cap’n Proto through pinned tool paths.
  • Validation: Trusted Build Inputs, make generated-code-check, and make dependency-policy-check.

Generated Code and Schema

  • Trust rule: schema, generated bindings, and no_std patches are trusted build inputs.
  • Implemented: schema/capos.capnp, build scripts, tools/generated/capos_capnp.rs, and tools/check-generated-capnp.sh make generated-code drift review-visible.
  • Validation: Trusted Build Inputs and make generated-code-check.

Device DMA and MMIO

  • Trust rule: userspace drivers may receive typed DeviceMmio, DMAPool, DMABuffer, and Interrupt capabilities, but not raw physical addresses, unrestricted BAR mappings, or unowned interrupt routes.
  • Implemented: kernel/src/cap/device_mmio.rs DeviceMmioCap, kernel/src/cap/dma_pool.rs DmaPoolCap, and kernel/src/cap/interrupt.rs InterruptCap bind operations to generation-checked device-manager ownership. kernel/src/dma_backend.rs select_and_report keeps backend selection kernel-owned and fail closed: verified IOMMU remapping where usable, otherwise kernel-owned bounce buffers.
  • Validation: DMA Isolation plus make run-devicemmio-grant, make run-dmapool-grant, make run-interrupt-grant, and make run-hardware-audit. These are bounded QEMU/device-fixture proofs; hostile bus-master isolation on production hardware still requires backend-specific evidence.

Panic and Emergency Paths

  • Trust rule: hostile input should produce controlled errors, not panic, allocate unexpectedly, or expose stale state.
  • Implemented: ring dispatch is mostly controlled-error; remaining panic surfaces are classified by reachability and tracked as hardening work.
  • Validation: Panic Surface Inventory and REVIEW.md.

Security Invariants

  • All authority is represented by capability-table hold edges; no syscall or host tool path should bypass the capability graph.
  • Identity metadata is not authority. Principals identify audit and policy subjects, accounts store durable policy inputs, profiles select bundle and quota templates, and sessions receive caps only through explicit broker minting.
  • The interface is the permission: method authority is expressed by the typed Cap’n Proto interface or by a narrower wrapper capability, not by ambient process identity.
  • Kernel operations at hostile boundaries validate structure, bounds, ownership, generation, interface ID, and resource availability before mutating privileged state.
  • Failed transfer, spawn, manifest, and DMA setup paths must leave ledgers, cap tables, frame ownership, and in-flight call state unchanged or explicitly rolled back.
  • Trusted build inputs must be pinned or drift-review-visible before their output becomes part of the boot image or generated source baseline.
  • Authentication/session code must treat credential records, setup tokens, passkey challenges, session IDs, and audit logs as security boundaries, not ordinary console text.

Open Work

  • Unify fragmented resource ledgers into the authority-accounting model so reviewers can audit quotas without following parallel counters.
  • Harden open panic-surface entries that become more exposed as spawn, lifecycle, SMP, or userspace drivers expand hostile input reachability.
  • Keep DMA backend selection kernel-owned and fail closed. Do not infer production hostile-device isolation from the bounded QEMU grant and lifecycle proofs.
  • Do not expand production authentication or remote-shell surfaces without hostile-input tests for bounded terminal input, credential failure paths, challenge expiry/replay, audit redaction, and narrow shell cap bundles.