Diff: substrate/capability-ledger-substrate.es

From 3f1e0da to 3f1e0da

+0 / −0 lines
BeforeAfter
--- ---
schema: foundry-doc-v1 schema: foundry-doc-v1
title: "The capability ledger substrate" title: "The capability ledger substrate"
slug: capability-ledger-substrate slug: capability-ledger-substrate
category: substrate category: substrate
type: topic type: topic
quality: complete quality: complete
short_description: "The Capability Ledger Substrate is the mechanism by which every access-control decision in a platform deployment becomes a cryptographically auditable event anchored to a log the customer controls." short_description: "The Capability Ledger Substrate is the mechanism by which every access-control decision in a platform deployment becomes a cryptographically auditable event anchored to a log the customer controls."
status: active status: active
bcsc_class: no-disclosure-implication bcsc_class: no-disclosure-implication
last_edited: 2026-05-22 last_edited: 2026-05-22
editor: pointsav-engineering editor: pointsav-engineering
cites: [] cites: []
references: references:
- id: 1 - id: 1
text: "C2SP signed-note specification" text: "C2SP signed-note specification"
url: "https://github.com/C2SP/C2SP/blob/main/signed-note.md" url: "https://github.com/C2SP/C2SP/blob/main/signed-note.md"
- id: 2 - id: 2
text: "RFC 9162 — Certificate Transparency Version 2.0" text: "RFC 9162 — Certificate Transparency Version 2.0"
url: "https://datatracker.ietf.org/doc/html/rfc9162" url: "https://datatracker.ietf.org/doc/html/rfc9162"
paired_with: capability-ledger-substrate.es.md paired_with: capability-ledger-substrate.es.md
--- ---
> The Capability Ledger Substrate is the mechanism by which every access-control decision in a platform deployment becomes a cryptographically auditable event anchored to a log the customer controls. > The Capability Ledger Substrate is the mechanism by which every access-control decision in a platform deployment becomes a cryptographically auditable event anchored to a log the customer controls.
The Capability Ledger Substrate extends the [[sel4-microkernel-substrate|seL4 microkernel's]] native capability model — which is correct by formal proof — with a transparency layer that makes the audit record portable, customer-rooted, and verifiable by third parties without any trust relationship with the operator. The Capability Ledger Substrate extends the [[sel4-microkernel-substrate|seL4 microkernel's]] native capability model — which is correct by formal proof — with a transparency layer that makes the audit record portable, customer-rooted, and verifiable by third parties without any trust relationship with the operator.
## 1. What the Capability Ledger Substrate is ## 1. What the Capability Ledger Substrate is
An operating system kernel mediates access to hardware resources. When a An operating system kernel mediates access to hardware resources. When a
process wants to write to a memory region, open a file, or send a network process wants to write to a memory region, open a file, or send a network
packet, the kernel decides whether the process is permitted. This decision is packet, the kernel decides whether the process is permitted. This decision is
what "access control" means at the system layer. what "access control" means at the system layer.
The [[sel4-microkernel-substrate|seL4 microkernel]] makes access-control decisions using *capabilities* — The [[sel4-microkernel-substrate|seL4 microkernel]] makes access-control decisions using *capabilities* —
unforgeable tokens that encode exactly what resource a process holds and what unforgeable tokens that encode exactly what resource a process holds and what
operations it may perform on that resource. A process that does not hold a operations it may perform on that resource. A process that does not hold a
valid capability for a resource cannot access it; there is no override, no valid capability for a resource cannot access it; there is no override, no
ambient authority, no root user that bypasses the check. The seL4 capability ambient authority, no root user that bypasses the check. The seL4 capability
model has been formally verified: the kernel's C implementation is proven model has been formally verified: the kernel's C implementation is proven
correct against a mathematical specification. This is the foundation. correct against a mathematical specification. This is the foundation.
The Capability Ledger Substrate does not replace this foundation. It adds one The Capability Ledger Substrate does not replace this foundation. It adds one
new property: every capability invocation decision can be linked, via a Merkle new property: every capability invocation decision can be linked, via a Merkle
inclusion proof, to a checkpoint in a signed transparency log. The customer inclusion proof, to a checkpoint in a signed transparency log. The customer
holds the signing keys for that log. The customer can audit the full history. holds the signing keys for that log. The customer can audit the full history.
Third parties can verify individual entries against published checkpoints Third parties can verify individual entries against published checkpoints
without access to the full log. without access to the full log.
The result is a security substrate with two independently verifiable layers: The result is a security substrate with two independently verifiable layers:
the kernel layer (seL4 formal proof — the kernel cannot be misled into the kernel layer (seL4 formal proof — the kernel cannot be misled into
honoring a capability it should refuse) and the ledger layer ([[worm-ledger-design|Merkle audit trail]] — the history of capability state changes cannot be rewritten without honoring a capability it should refuse) and the ledger layer ([[worm-ledger-design|Merkle audit trail]] — the history of capability state changes cannot be rewritten without
the customer's apex keys). The combination is what the Capability Ledger the customer's apex keys). The combination is what the Capability Ledger
Substrate names as the leapfrog: neither layer alone provides both properties. Substrate names as the leapfrog: neither layer alone provides both properties.
## 2. The `Capability` type — fields, kernel binding, and the ledger anchor ## 2. The `Capability` type — fields, kernel binding, and the ledger anchor
In `system-core`, the `Capability` struct is the ledger-bound authorisation In `system-core`, the `Capability` struct is the ledger-bound authorisation
token: token:
```rust ```rust
pub struct Capability { pub struct Capability {
pub cap_type: CapabilityType, // Endpoint, Memory, Irq, Notification, CNode pub cap_type: CapabilityType, // Endpoint, Memory, Irq, Notification, CNode
pub rights: Vec<Right>, // Read, Write, Invoke, Grant, Revoke pub rights: Vec<Right>, // Read, Write, Invoke, Grant, Revoke
pub expiry_t: Option<u64>, // Unix seconds; None = no built-in expiry pub expiry_t: Option<u64>, // Unix seconds; None = no built-in expiry
pub witness_pubkey: Option<String>, // SSH public key for expiry extension pub witness_pubkey: Option<String>, // SSH public key for expiry extension
pub ledger_anchor: LedgerAnchor, // Points into the customer Merkle log pub ledger_anchor: LedgerAnchor, // Points into the customer Merkle log
} }
``` ```
The `cap_type` and `rights` fields map directly to seL4 CDT (Capability The `cap_type` and `rights` fields map directly to seL4 CDT (Capability
Derivation Tree) semantics: an `Endpoint` capability with `[Invoke]` rights Derivation Tree) semantics: an `Endpoint` capability with `[Invoke]` rights
is the seL4 object that lets one protection domain send a message to another. is the seL4 object that lets one protection domain send a message to another.
A `Memory` capability with `[Read, Write]` is an IPC-shared memory region. A `Memory` capability with `[Read, Write]` is an IPC-shared memory region.
These are the kernel's native vocabulary; the Capability Ledger Substrate These are the kernel's native vocabulary; the Capability Ledger Substrate
adopts them without modification. adopts them without modification.
The `ledger_anchor` field is the new binding. It identifies the C2SP The `ledger_anchor` field is the new binding. It identifies the C2SP
signed-note checkpoint in the customer transparency log at which this signed-note checkpoint in the customer transparency log at which this
capability was committed: capability was committed:
```rust ```rust
pub struct LedgerAnchor { pub struct LedgerAnchor {
pub origin: String, // e.g. "foundry.<module-id>.capability-ledger" pub origin: String, // e.g. "foundry.<module-id>.capability-ledger"
pub tree_size: u64, // Log size at commitment time pub tree_size: u64, // Log size at commitment time
pub root_hash: Hash256, // Merkle root at that size pub root_hash: Hash256, // Merkle root at that size
} }
``` ```
A capability that carries a `ledger_anchor` pointing to tree position 1,247 A capability that carries a `ledger_anchor` pointing to tree position 1,247
in a log with a known root can be verified: produce an inclusion proof that in a log with a known root can be verified: produce an inclusion proof that
the capability's SHA-256 hash is at leaf 1,247 in the tree, and verify that the capability's SHA-256 hash is at leaf 1,247 in the tree, and verify that
proof against the signed checkpoint at tree_size = 1,247. If the proof proof against the signed checkpoint at tree_size = 1,247. If the proof
verifies, the capability's existence in the log is established. If the log verifies, the capability's existence in the log is established. If the log
has a published checkpoint history, the anchor ties the capability to a has a published checkpoint history, the anchor ties the capability to a
specific point in that auditable history. specific point in that auditable history.
The `Capability::hash()` method computes the SHA-256 of the JSON-serialized The `Capability::hash()` method computes the SHA-256 of the JSON-serialized
struct. This is the value used as the leaf in the Merkle tree and as the key struct. This is the value used as the leaf in the Merkle tree and as the key
in the revocation set. Determinism is tested: the same struct always produces in the revocation set. Determinism is tested: the same struct always produces
the same hash; changing any field — including `expiry_t` or the anchor's the same hash; changing any field — including `expiry_t` or the anchor's
`tree_size` — produces a different hash. `tree_size` — produces a different hash.
## 3. Time-Bound Capabilities (Mechanism A) ## 3. Time-Bound Capabilities (Mechanism A)
A capability with a non-None `expiry_t` field may not be invoked after the A capability with a non-None `expiry_t` field may not be invoked after the
Unix timestamp `t` without an extension. This is Mechanism A, Time-Bound Unix timestamp `t` without an extension. This is Mechanism A, Time-Bound
Capabilities, per the substrate operational specification §5. Capabilities, per the substrate operational specification §5.
The extension mechanism requires two parties: the capability itself names a The extension mechanism requires two parties: the capability itself names a
`witness_pubkey` (an SSH ed25519 public key), and the holder of that key signs `witness_pubkey` (an SSH ed25519 public key), and the holder of that key signs
a `WitnessRecord`: a `WitnessRecord`:
```rust ```rust
pub struct WitnessRecord { pub struct WitnessRecord {
pub capability_hash: Hash256, // identifies which capability is extended pub capability_hash: Hash256, // identifies which capability is extended
pub new_expiry_t: u64, // must be greater than the previous expiry_t pub new_expiry_t: u64, // must be greater than the previous expiry_t
pub signature: Vec<u8>, // ssh-keygen -Y sign, namespace "capability-witness-v1" pub signature: Vec<u8>, // ssh-keygen -Y sign, namespace "capability-witness-v1"
} }
``` ```
The namespace tag `capability-witness-v1` prevents cross-namespace replay. The namespace tag `capability-witness-v1` prevents cross-namespace replay.
An ed25519 signature produced by `ssh-keygen -Y sign` over a commit message An ed25519 signature produced by `ssh-keygen -Y sign` over a commit message
or an apprenticeship verdict cannot be replayed as a capability witness or an apprenticeship verdict cannot be replayed as a capability witness
extension, because the namespace tags differ. The `system-ledger` extension, because the namespace tags differ. The `system-ledger`
`witness.rs` module verifies signatures by shelling out to `ssh-keygen -Y verify` `witness.rs` module verifies signatures by shelling out to `ssh-keygen -Y verify`
with the correct namespace. with the correct namespace.
The kernel decision flow for a time-bound capability is: The kernel decision flow for a time-bound capability is:
1. If `now < expiry_t`: honor the invocation (no witness needed) 1. If `now < expiry_t`: honor the invocation (no witness needed)
2. If `now >= expiry_t` and no witness is supplied: `Refuse(Expired)` 2. If `now >= expiry_t` and no witness is supplied: `Refuse(Expired)`
3. If `now >= expiry_t` and a witness is supplied: 3. If `now >= expiry_t` and a witness is supplied:
- Verify the witness signature against the capability's `witness_pubkey` - Verify the witness signature against the capability's `witness_pubkey`
- Verify a Merkle inclusion proof that the witness record's hash is in the current log - Verify a Merkle inclusion proof that the witness record's hash is in the current log
- If both pass: `ExtendThenAllow { new_expiry_t }` — honor the invocation and update the ledger - If both pass: `ExtendThenAllow { new_expiry_t }` — honor the invocation and update the ledger
- If either fails: `Refuse(WitnessSignatureInvalid)` or `Refuse(WitnessNotInLedger)` - If either fails: `Refuse(WitnessSignatureInvalid)` or `Refuse(WitnessNotInLedger)`
The inclusion-proof requirement on the witness record is the key property: a The inclusion-proof requirement on the witness record is the key property: a
witness extension cannot be honored until it has been committed to the witness extension cannot be honored until it has been committed to the
customer's transparency log and an apex-signed checkpoint covers it. The customer's transparency log and an apex-signed checkpoint covers it. The
customer's apex sign-off is a prerequisite for capability lifetime extension. customer's apex sign-off is a prerequisite for capability lifetime extension.
This cannot be forged without the customer's ed25519 apex keys. This cannot be forged without the customer's ed25519 apex keys.
## 4. The apex-ownership ceremony (N+3+ handover) ## 4. The apex-ownership ceremony (N+3+ handover)
The customer's apex keys are the root of trust for the entire capability The customer's apex keys are the root of trust for the entire capability
ledger. A transparency log is only as trustworthy as the process for ledger. A transparency log is only as trustworthy as the process for
establishing and rotating those keys. The Capability Ledger Substrate establishing and rotating those keys. The Capability Ledger Substrate
specifies a formal ownership-transfer ceremony that produces an auditable specifies a formal ownership-transfer ceremony that produces an auditable
handover record in the same log it secures. handover record in the same log it secures.
The ceremony proceeds at checkpoints N, N+1, N+2, N+3+: The ceremony proceeds at checkpoints N, N+1, N+2, N+3+:
| Height | Action | Required signatures | | Height | Action | Required signatures |
|---|---|---| |---|---|---|
| N | Final checkpoint under P-old authority | P-old only | | N | Final checkpoint under P-old authority | P-old only |
| N+1 | Revocation entry: P-old is revoked | P-old (signing its own revocation) | | N+1 | Revocation entry: P-old is revoked | P-old (signing its own revocation) |
| N+2 | Handover checkpoint — co-signed by both apexes | P-old AND P-new (both required) | | N+2 | Handover checkpoint — co-signed by both apexes | P-old AND P-new (both required) |
| N+3+ | Post-handover checkpoints | P-new only; P-old refused with `StaleApex` | | N+3+ | Post-handover checkpoints | P-new only; P-old refused with `StaleApex` |
The C2SP signed-note format directly supports multi-signature: the same The C2SP signed-note format directly supports multi-signature: the same
checkpoint body (origin + tree_size + root_hash) can carry multiple signature checkpoint body (origin + tree_size + root_hash) can carry multiple signature
lines, each from a different named key. The `SignedCheckpoint::verify_apex_handover` lines, each from a different named key. The `SignedCheckpoint::verify_apex_handover`
composed primitive checks both signatures on a handover checkpoint. composed primitive checks both signatures on a handover checkpoint.
The N+3+ invariant is: any capability invocation presenting a checkpoint The N+3+ invariant is: any capability invocation presenting a checkpoint
signed only by P-old at height N+3 or later is refused with signed only by P-old at height N+3 or later is refused with
`Refuse(StaleApex)`. The `ApexHistory` module in `system-ledger` tracks the `Refuse(StaleApex)`. The `ApexHistory` module in `system-ledger` tracks the
effective lifetime of each apex (`effective_from` and `effective_until` effective lifetime of each apex (`effective_from` and `effective_until`
heights) and enforces this invariant at consult time. heights) and enforces this invariant at consult time.
The ceremony has three properties that matter to a customer: The ceremony has three properties that matter to a customer:
1. **Atomicity**: the handover is a single, self-contained event in the log. 1. **Atomicity**: the handover is a single, self-contained event in the log.
There is no out-of-band state migration. The log records the full ceremony. There is no out-of-band state migration. The log records the full ceremony.
2. **Auditability**: any third party examining the log can identify the exact 2. **Auditability**: any third party examining the log can identify the exact
checkpoint where P-old's authority ended and P-new's authority began. checkpoint where P-old's authority ended and P-new's authority began.
3. **Finality**: once the N+2 handover checkpoint is published, P-old cannot 3. **Finality**: once the N+2 handover checkpoint is published, P-old cannot
produce a valid checkpoint for N+3+ that the kernel will accept. The key produce a valid checkpoint for N+3+ that the kernel will accept. The key
rotation is permanent absent a further ceremony. rotation is permanent absent a further ceremony.
An end-to-end test in `system-ledger` (`full_handover_ceremony_end_to_end`) An end-to-end test in `system-ledger` (`full_handover_ceremony_end_to_end`)
verifies all four stages: pre-handover P-old allows; revocation applies; verifies all four stages: pre-handover P-old allows; revocation applies;
handover with both signatures accepts; post-handover P-old-only is refused handover with both signatures accepts; post-handover P-old-only is refused
with `StaleApex`. with `StaleApex`.
## 5. The `LedgerConsumer` state machine — consult flow and Verdict types ## 5. The `LedgerConsumer` state machine — consult flow and Verdict types
The `LedgerConsumer` trait in `system-ledger` is the kernel-facing interface: The `LedgerConsumer` trait in `system-ledger` is the kernel-facing interface:
```rust ```rust
pub trait LedgerConsumer { pub trait LedgerConsumer {
fn consult_capability( fn consult_capability(
&self, cap: &Capability, current_root: &SignedCheckpoint, &self, cap: &Capability, current_root: &SignedCheckpoint,
now: u64, witness: Option<&WitnessRecord> now: u64, witness: Option<&WitnessRecord>
) -> Result<Verdict, ConsultError>; ) -> Result<Verdict, ConsultError>;
fn apply_revocation(&mut self, event: RevocationEvent) -> Result<(), LedgerError>; fn apply_revocation(&mut self, event: RevocationEvent) -> Result<(), LedgerError>;
fn apply_apex_handover(&mut self, ...) -> Result<(), LedgerError>; fn apply_apex_handover(&mut self, ...) -> Result<(), LedgerError>;
fn apply_witness_record(&mut self, record: WitnessRecord, proof: InclusionProof) fn apply_witness_record(&mut self, record: WitnessRecord, proof: InclusionProof)
-> Result<(), LedgerError>; -> Result<(), LedgerError>;
} }
``` ```
`consult_capability` is the read-side hot path. It returns one of three verdicts: `consult_capability` is the read-side hot path. It returns one of three verdicts:
| Verdict | Meaning | Kernel action | | Verdict | Meaning | Kernel action |
|---|---|---| |---|---|---|
| `Allow` | Capability is current and unexpired | Honor the invocation | | `Allow` | Capability is current and unexpired | Honor the invocation |
| `Refuse(reason)` | Capability invalid; reason provided | Deny the invocation | | `Refuse(reason)` | Capability invalid; reason provided | Deny the invocation |
| `ExtendThenAllow { new_expiry_t }` | Witness extension accepted | Extend + honor | | `ExtendThenAllow { new_expiry_t }` | Witness extension accepted | Extend + honor |
The consultation decision flow: The consultation decision flow:
1. **Apex validity check**: is the current_root signed by the recognized apex? If the checkpoint is not apex-signed, all bets are off — `Refuse(ApexInvalid)`. 1. **Apex validity check**: is the current_root signed by the recognized apex? If the checkpoint is not apex-signed, all bets are off — `Refuse(ApexInvalid)`.
2. **Post-handover invariant check**: if an apex handover has occurred, is this checkpoint from a refused (stale) apex? If so, `Refuse(StaleApex)`. 2. **Post-handover invariant check**: if an apex handover has occurred, is this checkpoint from a refused (stale) apex? If so, `Refuse(StaleApex)`.
3. **Revocation check**: is the capability's hash in the revocation set? If so, `Refuse(Revoked)`. 3. **Revocation check**: is the capability's hash in the revocation set? If so, `Refuse(Revoked)`.
4. **Expiry check**: is `now < expiry_t` (or is `expiry_t` None)? If so, `Allow`. 4. **Expiry check**: is `now < expiry_t` (or is `expiry_t` None)? If so, `Allow`.
5. **Witness path**: if expired, attempt the witness extension flow (§3 above). 5. **Witness path**: if expired, attempt the witness extension flow (§3 above).
The three write-side methods (`apply_revocation`, `apply_apex_handover`, The three write-side methods (`apply_revocation`, `apply_apex_handover`,
`apply_witness_record`) update ledger state that subsequent consultations `apply_witness_record`) update ledger state that subsequent consultations
read. They are separated from the read-side precisely because the kernel's read. They are separated from the read-side precisely because the kernel's
read/write access patterns differ: `consult_capability` is called on every read/write access patterns differ: `consult_capability` is called on every
invocation; the write methods are called much less frequently (revocation invocation; the write methods are called much less frequently (revocation
events and apex handovers are rare; witness extensions happen at capability events and apex handovers are rare; witness extensions happen at capability
expiry boundaries, which may be hours or days apart). expiry boundaries, which may be hours or days apart).
## 6. Cache discipline — why the 358,000× speedup is architecturally critical ## 6. Cache discipline — why the 358,000× speedup is architecturally critical
The `consult_capability` decision flow requires verifying that the current The `consult_capability` decision flow requires verifying that the current
checkpoint is apex-signed. An ed25519 signature verification takes checkpoint is apex-signed. An ed25519 signature verification takes
approximately 4 milliseconds on the Intel Xeon 2.20 GHz hardware where approximately 4 milliseconds on the Intel Xeon 2.20 GHz hardware where
the substrate is developed. Any workload calling `consult_capability` hundreds the substrate is developed. Any workload calling `consult_capability` hundreds
of times per second would spend most of its time doing signature verification of times per second would spend most of its time doing signature verification
— an unacceptable overhead for kernel-mediated access control. — an unacceptable overhead for kernel-mediated access control.
The `CheckpointCache` in `system-ledger` resolves this. It holds the most The `CheckpointCache` in `system-ledger` resolves this. It holds the most
recent N (default 64) verified checkpoints, keyed by tree_size. A cache hit recent N (default 64) verified checkpoints, keyed by tree_size. A cache hit
— looking up a checkpoint the ledger has already verified — costs 11.2 — looking up a checkpoint the ledger has already verified — costs 11.2
nanoseconds. The cache stores the verified `SignedCheckpoint` objects; a nanoseconds. The cache stores the verified `SignedCheckpoint` objects; a
lookup confirms the checkpoint is present and returns it without re-running lookup confirms the checkpoint is present and returns it without re-running
ed25519. ed25519.
| Operation | Time | Ratio | | Operation | Time | Ratio |
|---|---|---| |---|---|---|
| Cache hit (most-recent lookup) | 11.2 ns | 1× (baseline) | | Cache hit (most-recent lookup) | 11.2 ns | 1× (baseline) |
| Cache miss (full 64-entry scan) | 362 ns | ~32× | | Cache miss (full 64-entry scan) | 362 ns | ~32× |
| `verify_signer` (ed25519, 1 apex) | 4.01 ms | ~358,000× | | `verify_signer` (ed25519, 1 apex) | 4.01 ms | ~358,000× |
| `consult_capability` (full path, cache miss) | 3.74 ms | ~334,000× | | `consult_capability` (full path, cache miss) | 3.74 ms | ~334,000× |
In steady-state operation, the kernel publishes checkpoints infrequently In steady-state operation, the kernel publishes checkpoints infrequently
(each checkpoint commits a batch of capability state changes). Between (each checkpoint commits a batch of capability state changes). Between
checkpoint publications, every capability invocation hits the cache. The checkpoint publications, every capability invocation hits the cache. The
cache hit rate approaches 100% for any sustained workload. The ed25519 cache hit rate approaches 100% for any sustained workload. The ed25519
verifier runs only when a new checkpoint is published — which happens on the verifier runs only when a new checkpoint is published — which happens on the
write path, not the read path. write path, not the read path.
The 64-entry bound covers: the apex-handover window (during which P-old and The 64-entry bound covers: the apex-handover window (during which P-old and
P-new checkpoints coexist at heights N+1 and N+2), the overlap period when P-new checkpoints coexist at heights N+1 and N+2), the overlap period when
multiple system components hold references to slightly different recent multiple system components hold references to slightly different recent
checkpoints, and reasonable checkpoint publishing rates without exceeding checkpoints, and reasonable checkpoint publishing rates without exceeding
kernel working-set constraints. The bound is a configuration choice, not a kernel working-set constraints. The bound is a configuration choice, not a
protocol requirement. protocol requirement.
The architectural lesson is that the cache and the Merkle inclusion proofs The architectural lesson is that the cache and the Merkle inclusion proofs
are not alternatives — they answer different questions on different access are not alternatives — they answer different questions on different access
paths. The cache makes the read path fast. The inclusion proofs make the paths. The cache makes the read path fast. The inclusion proofs make the
write path trustworthy. Both are required for a production substrate. write path trustworthy. Both are required for a production substrate.
## 7. Revocation and post-handover invariants ## 7. Revocation and post-handover invariants
**Revocation** is the mechanism for permanently revoking a capability's **Revocation** is the mechanism for permanently revoking a capability's
authority. A `RevocationEvent` carries the capability's SHA-256 hash and authority. A `RevocationEvent` carries the capability's SHA-256 hash and
a revocation record. After `apply_revocation` is called, `consult_capability` a revocation record. After `apply_revocation` is called, `consult_capability`
returns `Refuse(Revoked)` for that capability hash regardless of expiry or returns `Refuse(Revoked)` for that capability hash regardless of expiry or
witness state. The revocation set is a `HashSet<Hash256>` in the in-memory witness state. The revocation set is a `HashSet<Hash256>` in the in-memory
implementation — O(1) membership check. implementation — O(1) membership check.
Revocation events are themselves log entries, anchored to the same Revocation events are themselves log entries, anchored to the same
customer-signed transparency log as capability commitments. An auditor customer-signed transparency log as capability commitments. An auditor
examining the log sees the full sequence: capability committed at height N₁, examining the log sees the full sequence: capability committed at height N₁,
revoked at height N₂, and no subsequent witness extension is valid after N₂ revoked at height N₂, and no subsequent witness extension is valid after N₂
because any such extension would need to reference a checkpoint at N₂ or because any such extension would need to reference a checkpoint at N₂ or
later, where the revocation entry is visible. later, where the revocation entry is visible.
The **post-handover invariant** is a different property: it governs which The **post-handover invariant** is a different property: it governs which
apex signing key is authoritative on a given checkpoint, independent of apex signing key is authoritative on a given checkpoint, independent of
individual capability revocation. Once the apex handover ceremony completes individual capability revocation. Once the apex handover ceremony completes
at height N+2, any invocation presenting a checkpoint signed only by P-old at height N+2, any invocation presenting a checkpoint signed only by P-old
at height N+3 or later is refused. This prevents P-old from re-asserting at height N+3 or later is refused. This prevents P-old from re-asserting
authority after transferring it — the log records the transfer, and the authority after transferring it — the log records the transfer, and the
kernel enforces the cutoff height. kernel enforces the cutoff height.
The two properties operate at different levels of the substrate: The two properties operate at different levels of the substrate:
- Revocation is per-capability (a specific token is invalid) - Revocation is per-capability (a specific token is invalid)
- Post-handover is per-epoch (the old apex key is invalid for an entire - Post-handover is per-epoch (the old apex key is invalid for an entire
period of time) period of time)
Both are enforced by the `InMemoryLedger` in `system-ledger`. Both are tested Both are enforced by the `InMemoryLedger` in `system-ledger`. Both are tested
in the `full_handover_ceremony_end_to_end` integration test. in the `full_handover_ceremony_end_to_end` integration test.
## 8. Relationship to the WORM ledger ## 8. Relationship to the WORM ledger
The [[worm-ledger-architecture|WORM]] (Write-Once Read-Many) ledger substrate is the foundational The [[worm-ledger-architecture|WORM]] (Write-Once Read-Many) ledger substrate is the foundational
record-storage layer of the Foundry architecture. It implements a C2SP record-storage layer of the Foundry architecture. It implements a C2SP
tlog-tiles compatible transparency log: append-only, content-addressed, tlog-tiles compatible transparency log: append-only, content-addressed,
cryptographically signed by an apex. Service-level consumers interact with it at the application cryptographically signed by an apex. Service-level consumers interact with it at the application
tier. tier.
The Capability Ledger Substrate is the substrate-tier consumer of the same The Capability Ledger Substrate is the substrate-tier consumer of the same
log format. The data-primitive types (`Capability`, `WitnessRecord`, log format. The data-primitive types (`Capability`, `WitnessRecord`,
`LedgerAnchor`, `SignedCheckpoint`, `InclusionProof`, `ConsistencyProof`) `LedgerAnchor`, `SignedCheckpoint`, `InclusionProof`, `ConsistencyProof`)
defined in `system-core` are the L0 schema layer. The state machine in defined in `system-core` are the L0 schema layer. The state machine in
`system-ledger` is the L1+L2 consumer. `system-ledger` is the L1+L2 consumer.
The parallel with `service-fs` is structural and deliberate: The parallel with `service-fs` is structural and deliberate:
- `service-fs` is the application-tier WORM consumer: Ring 1, userspace, - `service-fs` is the application-tier WORM consumer: Ring 1, userspace,
network-accessible, human-scale record throughput network-accessible, human-scale record throughput
- `system-ledger` is the substrate-tier WORM consumer: kernel-adjacent, - `system-ledger` is the substrate-tier WORM consumer: kernel-adjacent,
single-threaded, microsecond-scale read latency required single-threaded, microsecond-scale read latency required
Both use the same C2SP signed-note format for checkpoints. Both verify Both use the same C2SP signed-note format for checkpoints. Both verify
apex ed25519 signatures. Both accept capability-state changes (revocations, apex ed25519 signatures. Both accept capability-state changes (revocations,
witness records) that need Merkle inclusion proofs to be trusted. The witness records) that need Merkle inclusion proofs to be trusted. The
difference is the access pattern and the consequence of failure: in difference is the access pattern and the consequence of failure: in
`service-fs`, a slow verification delays a file operation; in `service-fs`, a slow verification delays a file operation; in
`system-ledger`, a slow verification delays a kernel-mediated capability `system-ledger`, a slow verification delays a kernel-mediated capability
invocation, which is a system-level performance constraint. invocation, which is a system-level performance constraint.
This layer separation — same cryptographic primitives, different deployment This layer separation — same cryptographic primitives, different deployment
tiers, different performance envelopes — is the architectural pattern the tiers, different performance envelopes — is the architectural pattern the
Capability Ledger Substrate formalizes. A future system that replaces Capability Ledger Substrate formalizes. A future system that replaces
`service-fs` or adds a second WORM consumer does not need to reimplement the `service-fs` or adds a second WORM consumer does not need to reimplement the
proof mechanics; it shares `system-core` and composes the same primitives at proof mechanics; it shares `system-core` and composes the same primitives at
its own tier. its own tier.
## 9. Cross-references ## 9. Cross-references
- **The Capability Ledger Substrate** — the constitutional anchor for - **The Capability Ledger Substrate** — the constitutional anchor for
customer-rooted Merkle-log binding in platform deployments. Every customer-rooted Merkle-log binding in platform deployments. Every
capability authorization is anchored to a customer-held transparency log. capability authorization is anchored to a customer-held transparency log.
- **The Two-Bottoms Sovereign Substrate** — the [[system-substrate-doctrine|Two-Bottoms composition]] - **The Two-Bottoms Sovereign Substrate** — the [[system-substrate-doctrine|Two-Bottoms composition]]
(seL4 native-bottom + NetBSD compat-bottom) shares the same capability (seL4 native-bottom + NetBSD compat-bottom) shares the same capability
ledger substrate. The audit trail travels with the capability regardless ledger substrate. The audit trail travels with the capability regardless
of which bottom it runs on. of which bottom it runs on.
- **Substrate operational specification** - **Substrate operational specification**
The 12-section specification covering: §3.1 (Capability type schema), §4 The 12-section specification covering: §3.1 (Capability type schema), §4
(N+3+ apex handover ceremony), §5.1 (WitnessRecord schema and Mechanism A), (N+3+ apex handover ceremony), §5.1 (WitnessRecord schema and Mechanism A),
§6.1 (reproducible-verification artefact format), §8 (scoresheet). §6.1 (reproducible-verification artefact format), §8 (scoresheet).
- **[[worm-ledger-design|WORM ledger design]]** - **[[worm-ledger-design|WORM ledger design]]**
The foundational record-storage layer. §3 D1 (C2SP tlog-tiles wire format), The foundational record-storage layer. §3 D1 (C2SP tlog-tiles wire format),
§3 D3 (SHA-256 baseline). The Capability Ledger is a substrate-tier §3 D3 (SHA-256 baseline). The Capability Ledger is a substrate-tier
consumer of the same design. consumer of the same design.
- **[[merkle-proofs-as-substrate-primitive]]** - **[[merkle-proofs-as-substrate-primitive]]**
Companion technical article covering RFC 9162 inclusion and consistency Companion technical article covering RFC 9162 inclusion and consistency
proofs, the `InclusionProof` and `ConsistencyProof` structs, verification proofs, the `InclusionProof` and `ConsistencyProof` structs, verification
algorithms, and performance benchmarks. Read alongside this article for the algorithms, and performance benchmarks. Read alongside this article for the
cryptographic grounding. cryptographic grounding.
- **Implementation state (Phase 1A)** - **Implementation state (Phase 1A)**
- `system-core` v0.2.0: `Capability`, `WitnessRecord`, `LedgerAnchor`, - `system-core` v0.2.0: `Capability`, `WitnessRecord`, `LedgerAnchor`,
`Checkpoint`, `NoteSignature`, `SignedCheckpoint`, `InclusionProof`, `Checkpoint`, `NoteSignature`, `SignedCheckpoint`, `InclusionProof`,
`ConsistencyProof`. 51 tests. `ConsistencyProof`. 51 tests.
- `system-ledger` v0.2.1: `LedgerConsumer` trait, `InMemoryLedger`, - `system-ledger` v0.2.1: `LedgerConsumer` trait, `InMemoryLedger`,
`CheckpointCache`, `RevocationSet`, `ApexHistory`, `CheckpointCache`, `RevocationSet`, `ApexHistory`,
`verify_witness_signature`. 44 tests + 10 criterion benchmarks. `verify_witness_signature`. 44 tests + 10 criterion benchmarks.