Capability-based security

@@ -1,78 +1,169 @@
---
schema: foundry-doc-v1
title: "Capability-based security"
slug: capability-based-security
category: security
type: topic
content_type: topic
quality: complete
short_description: "Capability-based security is the access-control model PointSav uses at the hardware and OS layers, where each component must hold a verified cryptographic token."
status: active
audience: vendor-public
bcsc_class: forward-looking
last_edited: 2026-07-30
language_protocol: PROSE-TOPIC
last_edited: 2026-08-03
editor: pointsav-engineering
cites: []
references:
  - id: 1
    text: "Klein, G. et al. 'seL4: Formal Verification of an OS Kernel.' ACM SOSP, 2009."
    url: "https://dl.acm.org/doi/10.1145/1629575.1629596"
  - id: 2
    text: "Lampson, B. W. 'Protection.' ACM SIGOPS Operating Systems Review, 8(1):18–24, 1974."
    url: "https://dl.acm.org/doi/10.1145/775265.775268"
short_description: "Capability-based security grants each component an unforgeable, scoped token it must present to act, replacing ambient privilege. One software layer implements it today; kernel-level enforcement is planned."
paired_with: capability-based-security.es.md
---

**Correction — rehedged to planned/intended (2026-07-30):** this article originally
described a live, enforced capability system in unhedged present tense. No matching
code exists today: neither a single-archive check nor a subsequent broader
cross-archive sweep (grep for "capability manager"/`CapabilityManager` across every
`.rs` file in all ~25 Totebox archives) found any implementation; `moonshot-hypervisor`
— the crate that would house a hypervisor-mediation layer — is a 4-file scaffold with
an empty dependency list. This is consistent with the separately-confirmed finding that
seL4 itself is not yet running anywhere in the platform today. Per operator direction,
this describes real, intended design rather than a fabrication — the body below is
rewritten to present it as planned/intended architecture, not current state.

> Capability-based security is the access-control model PointSav is designed to use at the hardware and operating-system layers, where each software component will be required to hold a mathematically verified cryptographic token to communicate with any other component. This is a planned architecture, not yet implemented.

**Capability-based security** is the access-control model intended to replace traditional operating-system privilege hierarchies in the [[pointsav-overview|PointSav]] platform, once implemented. Where conventional operating systems (Windows, macOS, Linux) grant broad permissions through administrative accounts and assume components at the same privilege level can be trusted, the design calls for each isolated component to hold an explicit, mathematically verified [[crypto-attestation|cryptographic token]] — called a capability — before it can communicate with any other component. A capability would be unforgeable and uncopyable, granted by the kernel at process start and revoked when withdrawn. [^2] The intended effect is that the blast radius of any compromise is mathematically bounded to the components the compromised process held capabilities for. See also [[capability-ledger-substrate|the capability ledger substrate]] and [[pairing-as-permission|pairing as permission]].

## Overview

Standard operating systems are vulnerable to privilege escalation: a single compromised application can, in many architectures, reach the core memory of the host machine and gain access to other components on the network. The capability model is designed to eliminate this class of vulnerability at the architecture level rather than through policy controls.

The [[pointsav-overview|PointSav]] implementation is planned to build on a [[sel4-microkernel-substrate|microkernel foundation]]. In the intended design, the microkernel would handle only the most primitive routing of physical memory and CPU time, with every driver, network interface, and service process running in isolated memory and none holding general administrative rights. To communicate with another isolated component, a process would present a cryptographic capability token, which the kernel would validate before permitting or denying the operation. **As of this writing, no such implementation exists** — no capability-manager code, isolation-wrapper, or hypervisor-bridge crate was found anywhere in the monorepo, and seL4 itself is not yet running in any shipped component.

## Architecture (planned)

The intended capability layer would sit between the [[sel4-microkernel-substrate|seL4 microkernel]] and the Rust service processes that make up the PointSav [[three-ring-architecture|Ring 1 and Ring 2]] services, with Rust-based capability managers engineering the isolation wrappers and hypervisor bridges that mediate communication between components.

The design calls for a strict, one-way command flow between isolation domains: an isolated edge delivery process — for example, the [[mediakit-os|MediaKit OS]] — would be unable to issue commands back into the secure [[totebox-os|ToteboxOS]] vault, so a compromised edge process would be contained within its own memory sandbox with no capability grants reaching the broader system, enforced by the kernel rather than a policy document.

## Intended properties

- **Formal verification.** The [[sel4-microkernel-substrate|seL4 microkernel]] that would underlie the capability manager is formally verified in Isabelle/HOL [^1] as a kernel in its own right — meaning the isolation properties *of seL4 itself* are mathematically proven, independent of whether PointSav's own capability-manager layer has been built on top of it.
- **Least privilege by default.** Intended: components start with no capabilities; the system grants only the minimum set required for their declared function.
- **Blast-radius containment.** Intended: compromise of one component could not propagate to components it holds no capability grants for.
- **Auditability.** Intended: capability grants would be recorded, with the set of grants in force at any time inspectable.

## How it is intended to work

At deployment time, a PointSav capability manager would read a system policy file declaring which processes communicate with which others and what operations each is permitted. The [[sel4-microkernel-substrate|microkernel]] would enforce this policy at runtime. No such capability manager or policy-file mechanism exists today.

## Intended applications

Once built, the capability model is intended to apply across the full [[pointsav-overview|PointSav]] deployment stack:

- **[[totebox-os|ToteboxOS]]** — the primary secure vault OS; data at rest would be accessible only to processes holding the appropriate capability token.
- **[[mediakit-os|MediaKit OS]]** — the edge delivery environment; intended to hold no capability grants reaching ToteboxOS, so a compromised delivery node could not reach stored data.
- **[[service-fs-architecture|service-fs]]** — the [[worm-ledger-architecture|WORM ledger]]; append capability would be granted to [[three-ring-architecture|Ring 1]] ingest services only.
**Capability-based security** is an access-control model in which a component may perform an
operation only by presenting an unforgeable token that names both the operation and its scope.
There is no ambient privilege: holding a capability *is* the permission, and a component that
holds none can do nothing, regardless of which user account it runs under or which machine it
sits on. The model dates to Lampson's 1974 protection matrix and reached its best-known modern
expression in the seL4 microkernel, where every kernel object — memory frames, threads,
communication endpoints — is reachable only through an explicit capability held in a per-process
table.

The distinction from the access-control lists most systems use is structural rather than
cosmetic. Under an access-control list, the subject's *identity* is checked against a policy at
the moment of use, and a compromised process inherits everything that identity is permitted to
do. Under a capability model, the subject's *possession* is what matters, and a compromised
process can reach only the specific objects whose capabilities it was handed. Privilege is
therefore bounded at the moment of delegation rather than at the moment of use.

## What is enforced today

One capability mechanism is implemented, tested, and running in platform code: the request gate
in `service-content`. It is a software layer, not a hardware or kernel one, and its scope is
cross-instance authorisation rather than process isolation.

The gate reads an `X-Foundry-Capability` header, resolves the calling peer's registered public
key, verifies an Ed25519 signature over a base64url-encoded payload, checks the payload's nonce
against a replay cache, and confirms that the archive scope named in the capability permits the
request being made. Expired tokens, scope mismatches, replayed nonces, and unregistered peers are
each rejected with distinct status codes, and the outcomes are appended to an interface audit
log. Ten integration tests exercise the gate directly — covering the pass-through case, exact and
wildcard scope matching, scope mismatches, unregistered peers, expired tokens, and nonce replay —
each asserting the specific status code the gate returns.

Two properties of this gate matter for an accurate reading. First, the capability is *signed*,
not merely presented — a token cannot be minted by anyone but the holder of a registered private
key. Second, and more importantly, a request arriving with **no** capability header passes
through unchanged, by design, to preserve the existing locally-trusted call path. The gate is
therefore a real, tested instance of capability-based access control — an unforgeable signed
token stands in for identity — but it is additive and optional rather than a mandatory
chokepoint through which all traffic must pass.

A second, adjacent enforcement layer exists in `service-vm-tenant`, which extracts a bearer
token, applies per-tenant quota checks, and serialises virtual-machine creation behind a lock
explicitly documented as a guard against time-of-check/time-of-use races. This is conventional
token authorisation rather than a capability model proper — the token names a tenant, not an
object and an operation — but it is the other place in the platform where authority is checked
against a presented credential rather than assumed from context.

## The intended architecture

The design most of this platform's security writing describes is broader than the gate above: a
capability layer sitting on a [[sel4-microkernel-substrate|microkernel foundation]], with every
driver, network interface, and platform service running as an isolated component holding no
general administrative rights. To communicate with another component, a process would invoke a
capability, which the kernel — not an application-level middleware — validates before permitting
the operation.

Above the kernel, the design envisions a capability-management layer: at deployment time, a
policy declaration would state which components may communicate with which others and what
operations each is permitted, and the resulting capability grants would be distributed at system
start. The plan applies this model across the intended deployment stack — the secure archive
operating system holding data at rest, the edge delivery environment serving public content, and
the [[worm-ledger-architecture|append-only ledger]] whose write path would be reachable only by
components holding an explicit append grant.

None of this deployment-time policy layer exists in running code today. Verified by searching the
entire canonical source tree rather than any single component: there is no capability-manager, no
isolation wrapper, and no hypervisor-bridge component anywhere. The `moonshot-hypervisor` package
that would house a mediation layer is a four-file placeholder whose dependency list is empty and
whose only function returns a scaffold-verification string.

Genuine seL4 work does exist, but it is bare-metal experimentation rather than a platform runtime.
The seL4 kernel source is vendored into the platform's source tree, and a standalone development
workspace, `moonshot-sel4-vmm`, contains early protection-domain runtime code with a series of
test binaries exercising console output, inter-process communication, serial and UART handling,
and VirtIO networking under emulation. No shipped PointSav component runs on seL4 today; the
platform's live services, including the fleet, host, and tenant services of the private compute
network, are ordinary Rust processes built on `axum` and `tokio`, with no seL4 dependency in any
of their manifests. This work is described further in [[sel4-capability-topology]] and
[[sel4-microkernel-substrate]].

The seL4 project's own published material quantifies why this foundation is attractive as a
target. A well-designed microkernel is on the order of ten thousand lines of code, against
roughly twenty million in a mainstream monolithic kernel — a trusted computing base three orders
of magnitude smaller. The project's analysis of critical Linux kernel compromises found that a
microkernel design would have fully eliminated about 29 percent of them and mitigated a further 55
percent below critical severity. Those figures describe the seL4 architecture in general, as
published by the seL4 project, not any PointSav deployment; they are recorded here as the
rationale for the platform's choice of intended foundation, not as a claim about work already
done.

## Why the two layers are not interchangeable

It is tempting to treat the software capability gate as an early increment of the planned kernel
model. They defend different things, and one does not grow into the other.

### Different threat boundaries

The software gate assumes a correct operating system, a correct language runtime, and a correct
process boundary; it protects one service's data from another organisation's caller. Kernel
capability enforcement assumes far less — it is intended to hold even when a service is fully
compromised, because the kernel, not the service, is what refuses the unauthorised operation.

### Different failure modes

A defect in the software gate is a bypassed authorisation check on one service's HTTP surface. A
defect in a kernel capability distribution is a breached isolation boundary between every domain
on the machine. This asymmetry is why seL4's formal proofs are addressed at the kernel and not at
applications above it.

### Different verification stories

The software gate's assurance is integration tests. The planned model's assurance would rest on
seL4's own machine-checked proofs — established in the Isabelle/HOL proof assistant, showing that
its implementation matches its specification and that a correctly configured system enforces
confidentiality, integrity, and availability — plus the integrity and confidentiality results
published for specific architectures. Those are third-party results about the kernel itself, and
they hold whether or not this platform ever adopts it.

## What this is not

**This is not a description of a running, mandatory capability system.** With the single
exception of the tested request gate described above, capability-based access control on this
platform is intended architecture. Statements about hardware-rooted capabilities, per-service
protection domains, and policy-driven capability distribution describe what is planned, not what
is deployed.

**seL4 is not running anywhere in the platform today.** The only capability enforcement that
exists inside seL4 itself is a formally verified property of that kernel — real, but not yet
placed into production by this platform.

**The software capability gate is not a mandatory chokepoint.** A request with no capability
header is not rejected. Any characterisation of the platform as one where "every request carries
a capability" would be inaccurate today.

**Formal verification of seL4 is not formal verification of this platform.** The Isabelle/HOL
proofs are properties of the microkernel as an artefact in its own right. They say nothing about
the correctness of software built above it, and this platform has published no formal proof of
its own.

**Capabilities are not a substitute for the other controls described in this category.** Even
under the planned model, commit-time secret scanning, ledger immutability, and pairing-based
device authorisation each address a class of risk that object capabilities do not touch. Nor does
this article claim that capability hardware or exotic processors are required — the intended
design uses a software capability model enforced by a microkernel on commodity hardware.

## See also

- [[sel4-capability-topology]]
- [[sel4-microkernel-substrate]]
- [[worm-ledger-architecture]]
- [[3-layer-stack]]
- [[machine-based-auth]]
- [[compounding-substrate]]

- [[cryptographic-ledgers]]
- [[worm-ledger-architecture]]
- [[pre-commit-defense-in-depth]]