Capability Threat Model

This is the one page that says what March’s capability system protects against, what it assumes, and what it does not do. Three older pages each describe a part of it, and before 2026-10-30 they disagreed with each other:

Where this page and one of those disagree, this page is the one checked against the code, and the other is a bug to fix. Every behaviour below was checked against the compiler on 2026-10-30. The capabilities claim is the short version of this page.

Who the attacker is

The system is built for one situation: you run code you did not write line by line, mostly your dependencies, and want to know and limit what it can touch.

Party Trusted? Why
You, writing the program and choosing main’s grant Yes You decide the policy.
The March compiler, runtime and standard library Yes They do the checking. A bug in them is a bug in the claim (see Assumptions).
Your dependencies (March source) No This is the main case. A dependency can be careless or hostile.
C code reached through extern No, and not analysed The compiler can’t see inside it. See IO.Foreign.
Whoever signs a hot deploy Partly The node checks the signature and a policy, but it trusts the patch’s own list of capabilities. See Hot deploys.
Someone with a shell on the machine No, and out of scope They can run the binary under a debugger or swap it.

What is checked, layer by layer

1. At compile time, always on

These checks run on every march --check and march --compile. There is no flag to skip the first three.

Every module declares what it touches (needs). If any function in a module reaches a capability the module does not declare in needs, the build fails with cap_needs. This holds for every route: a Cap(X) in a signature, a capability builtin called directly (file_write(...)), and a function from another module that needs it. It is an error, not a warning, and it fires even for a function nothing calls. (Calling a builtin directly was only a warning before 2026-08-06. Some older pages still said so; they were wrong after that date.)

The upper limit (the “ceiling”). The compiler checks every module’s emitted code, after inlining and specialisation, against that module’s own needs, and fails the build ([cap_ceiling]) if a module uses a capability it did not declare, including through a standard-library wrapper such as File.write. This covers dependencies that never opted into anything. It is on by default; --no-cap-strict turns off the emitted-code part (the needs check above still runs). march --compile runs the full check; march --check runs a subset of it that doesn’t over-report.

main’s grant bounds the whole program. main’s capability parameters are the program’s grant. A program that reaches anything outside the grant fails to build ([cap_grant_exceeded]), no matter what any module declares. A main with no capability parameter is granted nothing, so a program that performs IO without stating its grant does not compile (cap_grant). Cap(IO) grants everything. Code that is never reached from main costs nothing against the grant.

Capabilities can’t be forged or widened. A Cap(X) value can only be received (from main, or from a function that was given it) and narrowed to something smaller (cap_narrow). It can’t be built from JSON, a literal or any other data, and it can’t be widened. Proof capabilities (Session.Live, your own proof cap) can only be created by the module that declares them.

Per-role grants. A protocol role declared role Ledger needs IO.FileWrite gets its grant checked the same way main’s is: its code may reach only what the role names.

2. What is not checked per function

There are no per-function capability bounds in 1.0 today. Inside a module, every function shares that module’s needs. A Cap(X) parameter marks authority at a module boundary, but it does not limit what that function reaches.

A per-function check did exist from 2026-08-10 to 2026-08-13 (“R1 stage C”, a check called check_fn_grants). It was removed on 2026-08-13 because it forced every caller to pass capabilities it didn’t otherwise need (specs/progress/2026-08-13-remove-per-function-grant-ceiling.md). The provable-sandbox design page described it as shipped; that was true for those three days only.

A declared per-function bound with no effect on callers (fn fetch(url) needs IO.NetConnect.TLS do) is planned for 1.0, with module-level bounds as the fallback if it proves too noisy (road-to-1.0 plan, “Pillar 2 — per-function bounds”). The per-function data it needs already exists (lib/caps/cap_rows.ml); only the declaration and the check are missing.

3. Reading a binary or a dependency tree

Two tools report what code may do. They do not stop it.

  • forge audit compares your dependencies’ capabilities with a recorded baseline (forge.caps.lock) and exits 1 when one asks for more. forge add, forge deps and forge outdated run the same comparison. By default it reads needs declarations, which the compile-time checks above keep honest; --inferred reads what the code uses.
  • forge cap inspect <binary> reads the capability markers and runtime symbols left in a compiled binary, says which module is responsible for each, and with --strict re-checks the upper limit on a binary you didn’t build.

4. At run time, opt-in: the OS sandbox

Everything above is checked before the program runs and then erased. To make the operating system enforce the grant on the running process, which also covers C code and raw syscalls, you opt in:

  • march --compile --cap-sandbox: the binary installs a deny-by-default sandbox on itself before any of your code runs (Seatbelt on macOS, seccomp-bpf on Linux). It fails closed: if the sandbox can’t be installed, or the platform or CPU architecture isn’t supported, the program exits (status 70) instead of running unconfined. Decided 2026-10-30: it stays opt-in in 1.0, and keeps failing closed.
  • forge cap run [--allow-only X] ./binary: forge puts the sandbox on from outside before the program starts (Seatbelt on macOS, bubblewrap on Linux). With --allow-only you choose the policy, so a binary that under-reports its capabilities gains nothing.

Not every capability can be enforced by every OS mechanism. The ones that can’t are reported as advisory, never silently dropped. In short: IO.FileRead is advisory under --cap-sandbox on both platforms (enforced by forge cap run on Linux); IO.NetListen is advisory under forge cap run on Linux; IO.Clock, IO.Spawn, IO.Console, IO.Random and IO.Foreign are advisory everywhere. The full table, capability by capability, is on Capability Enforcement.

The sandbox works on tier-1 platforms only (darwin-arm64, linux-x86_64, linux-aarch64; see Supported Platforms).

5. Hot deploys

A hot deploy (forge deploy hot) replaces functions in a running program. It has two gates:

  • On your machine, a deploy that widens what a function or protocol role may reach stops unless you pass --grant-cap for the new capabilities.
  • On the node, each activated function arrives signed (ed25519) with its own list of capabilities and a BLAKE3 digest of that list. The node rejects a tampered list, and, if MARCH_DEPLOY_POLICY names a policy file, rejects a function or role whose capabilities fall outside it.

The node gate trusts the patch’s own list: anyone with the signing key can claim less than the code uses. With no MARCH_DEPLOY_POLICY set, every signed patch is admitted. A hot deploy is therefore outside the “the grant bounds the program” claim. Under --cap-sandbox the OS sandbox installed at startup still applies to patched code, because it can’t be loosened at run time.

Foreign code (IO.Foreign)

An extern block calls C, and the compiler’s knowledge stops there. The rules:

  • A module with an extern block should declare needs IO.Foreign. If it doesn’t, the compiler warns ([extern_needs_foreign]). This is still a warning, not an error.
  • A program that reaches an extern block can’t be built under any grant narrower than Cap(IO): a narrow grant over C code would be a lie, so the compiler refuses it.
  • forge audit and forge cap inspect report IO.Foreign; read it as “the rest of this list is no longer complete”.

So the compile-time claim covers March code only. For C code, the OS sandbox is the only enforcement.

Assumptions

The compile-time claim holds only if all of these are true:

  1. The compiler, runtime and standard library are correct. The checks are a whole-program static analysis, not a proof. No machine-checked proof covers them (the Lean model of the type system has no grant check).
  2. Every language form is visited by the capability walks. The checks follow a static reference graph. A new language form the walk forgets is a hole: five past bugs were exactly that. Nothing tests this mechanically yet (see Gates).
  3. You build with the default checks on. --no-cap-strict drops the emitted-code check.
  4. The binary you run is the one you built. Nothing stops someone from replacing it after the build. Release archives are checksummed but not yet signed.
  5. No C code, or C code you trust. See Foreign code.

What is not claimed

  • Per-function bounds. A module’s functions share its authority (see above).
  • What code does with a capability it holds. IO.NetConnect allows a telemetry ping and a data leak equally.
  • Output to the console. Anything a program may print, it may leak; no capability stops that.
  • C code, dlopen and raw syscalls, unless you run under the OS sandbox.
  • Hot-patched code beyond its signed, self-reported list (see Hot deploys).
  • Against whoever builds the binary. --cap-sandbox is chosen by the person compiling, so a hostile publisher simply leaves it out. For code you don’t trust, use forge cap run --allow-only.
  • Capabilities the OS can’t tell apart (the advisory rows above).

Known holes (open today)

  • Path scopes. needs IO.FileWrite("/var/lib/app") narrows the sandbox, but a few calls can bypass the compile-time scope check (specs/todos/2026-08-04-path-scope-followups.md).
  • The reload server under --cap-sandbox. A deploy’s own file writes happen under a withheld IO.FileWrite (specs/todos/2026-10-18-hcr-reload-writes-under-cap-sandbox.md).
  • Handles minted from a name. Vault.open(name) and Vault.whereis(name) turn any string into a handle whose element type the caller chooses (stdlib/vault.march). This is a type-safety gap rather than an authority gap, but it is the same pattern a capability must never follow.

Gates

What runs in CI today:

  • The capability unit tests in the run_compiler suite (test/test_cap_*.ml, including the ceiling, unforgeability and both sandbox tests), on Linux (test (ubuntu, compiler)) and macOS (test (macos-15, all)).
  • The capability rejects in the static-semantics corpus (specs/lang/types/reject/), run by the conformance job.
  • --cap-sandbox runs real compiled binaries and checks that withheld operations fail (test/test_cap_sandbox_runtime.ml).

Planned, not built:

  • A walk-completeness test: every syntax-tree and IR constructor is visited by every capability walk, checked mechanically instead of by review.
  • A must-reject corpus: one program per past capability bypass, run in CI.
  • The Lean model of the type system has no grant check, so it can’t catch a grant bug.