Revocation Store

Types and implementations

The RevocationStore trait

Four methods, two with defaults that set the node's failure posture:

pub trait RevocationStore: Send + Sync {
    fn is_revoked(&self, capability_id: &str) -> Result<bool, RevocationStoreError>;

    /// Revoke a capability. Returns `true` if it was newly revoked.
    fn revoke(&self, capability_id: &str) -> Result<bool, RevocationStoreError>;

    fn observe_revocation(
        &self,
        capability_id: &str,
    ) -> Result<RevocationObservation, RevocationStoreError> {
        Ok(RevocationObservation {
            revoked: self.is_revoked(capability_id)?,
            commit: None,
        })
    }

    /// Whether this store loses its revocation set on process restart. The
    /// default is the safe (loud) assumption so an unknown store is treated as
    /// ephemeral; durable and remote stores override to `false`.
    fn is_ephemeral(&self) -> bool {
        true
    }
}

Without an installed view or the opt-in, an implementor who leaves is_ephemeral at its default is refused dispatch, so a store of unknown durability never loses revocations silently. InMemoryRevocationStore keeps the default, so it reports ephemeral by construction (in_memory_revocation_store_is_ephemeral_by_default in chio-kernel/src/kernel/tests/revocation_durability.rs).

Durability gate scope

The gate is default-on and covers one node and one kernel at pre-dispatch: ensure_revocation_durability_ready, the three gate tests in kernel/tests/revocation_durability.rs, and call sites in evaluation/async_evaluation_core.rs and evaluation/nested_flow_evaluation.rs. It routes through build_receipt_persistence_failclosed_deny_response_with_metadata. It checks that durable revocation state exists, and an installed view satisfies it whether or not a snapshot has arrived; currency is the freshness check's job. As the fourth readiness check, it runs after a poisoned TCB lock or an unhealthy receipt writer has already refused with the same guard attribution.

Schema and write path

SqliteRevocationStore::open creates the parent directory; refuses a database provisioned with a joint serving owner, one whose application_id belongs to another product, or one whose stamped revision is newer than supported; initializes the schema; stamps revision 2 under the revocation key; and runs a foreign_key_check.

PRAGMA journal_mode = WAL;
PRAGMA synchronous = FULL;
PRAGMA busy_timeout = 5000;
PRAGMA foreign_keys = ON;

CREATE TABLE IF NOT EXISTS revoked_capabilities (
    capability_id TEXT PRIMARY KEY,
    revoked_at INTEGER NOT NULL,
    revocation_index INTEGER UNIQUE,
    admission_authority_commit_index INTEGER UNIQUE
);

CREATE INDEX IF NOT EXISTS idx_revoked_capabilities_revoked_at
    ON revoked_capabilities(revoked_at);

initialize_revocation_schema also creates the singleton counter table revocation_replication_meta, or, opened alongside a joint serving owner, admission_authority_meta plus an admission_authority_commits log and a migration table; the mode decides which index column a row gets. Every mutation takes the next value from the counter row through allocate_revocation_index. Reads run in a deferred transaction that is rolled back; writes take TransactionBehavior::Immediate and check the serving-owner fence first. A standalone --revocation-db store carries no owner, since open refuses any file that has one, so its fence check passes trivially.

revocation_index is a per-mutation counter and is the commit_index that observe_revocation returns; in joint mode the same allocation anchors the admission_authority_commits log, whose density verify_admission_authority_invariants checks. Cluster paging uses a different cursor: list_revocations_after orders by revoked_at ASC, capability_id ASC and pages on that tuple, and RevocationRecord carries no index field.

is_ephemeral is computed from the open path. rusqlite enables URI filenames, so :memory:, file::memory:, and any file:...?mode=memory URI open a database that loses every revocation on restart, and all three report ephemeral (in_memory_revocation_store_reports_ephemeral). open_alongside sets ephemeral: false for the store it shares with a provisioned serving owner.

Call sites, locking, and observation guarantees

check_revocation lives in kernel/validation.rs. Resource and prompt admissions route through evaluation/evaluation_entry.rs, which calls check_revocation once before delegation admission; plan-step evaluation and the governed active-response path each call it once, and none of the three takes the trace-emitting admission wrapper. with_revocation_store takes no kernel-level lock, so concurrency control belongs to the store. revoke_capability and the admission check take the runtime-trace transition lock, so RevocationCommitted and RevocationAdmission events are ordered, and both recover from a poisoned lock: poisoned_runtime_trace_lock_does_not_disable_revocation_or_admission.

observe_revocation is the stricter read. The SQLite store answers membership and reads the commit index in one transaction, attaching RevocationCommitMetadata only with a serving owner. The durable-admission coordinator refuses a supplemental quota claim whose observation carries no commit metadata (supplemental authorization requires atomic revocation observation) or whose guarantee level is neither SingleNodeAtomic nor HaLinearizable. InMemoryRevocationStore and RemoteRevocationStore inherit the trait default and return commit: None, so neither backs a supplemental quota claim.

View snapshot and feature gate

RevocationSnapshot deserializes with deny_unknown_fields. Unit tests cover equal-epoch replay, stale-epoch rewind, and eight concurrent writers installing epochs 1 to 8, after which the view reads 8 and an epoch-7 write still fails. The core leaves root_hash to the layer that produced the snapshot, which verifies its signature. chio-federation/src/revocation_gossip.rs owns the feed's wire envelope, push queue, and catch-up path. validate_delegation_admission runs the freshness check before its empty-chain early return, so the stale refusal covers calls with no delegation chain; empty_view_denies_as_stale in kernel/delegation.rs tests the helper's half.

The consultation call site is #[cfg(feature = "delegation")], and default = ["delegation"] in chio-kernel, so a stock build consults the view. A --no-default-features build drops the consultation and keeps only the per-row lookup. With no view installed, the helper returns Ok(()) and the per-row lookup is the whole check.

Proofs, models, and tests

Deny-if-leaf-or-ancestor-revoked is proved over a projection. The Kani harness revocation_snapshot_denies_presented_token_or_ancestor in chio-kernel-core/src/kani_harnesses.rs asserts revocation_snapshot_denies(a, b) == a || b over both booleans, and the Lean theorems revocationSnapshot_revoked_token_denies and revocationSnapshot_revoked_ancestor_denies in formal/lean4/Chio/Chio/Proofs/Protocol.lean discharge row P2. The projection takes two flags, not a store: P2 in formal/proof-manifest.toml lists audited_storage_assumption and sqlite_projection among its evidence kinds, and the manifest's excluded_surfaces treats the SQLite implementations as audited assumptions.

The view never rewinding is tested and modeled. The install_if_newer loop has concurrency tests in revocation_view.rs and crates/kernel/chio-kernel-core/tests/revocation_view_concurrency.rs; the symbol is a covered entry in the proof manifest, and its model is formal/tla/RevocationPropagation.tla, where Propagate absorbs a stale or duplicate epoch without moving the receiver. The harness verify_revocation_view_freshness checks the boolean deny predicate, separate from the loop and the wall-clock check. Status for every theorem is in the theorem inventory.

Lookup cost, record contents, and propagation

The per-row path issues one store call per subject, so a chain of depth n costs n + 1 lookups, each a SQLite transaction against a durable store. The view path loads one snapshot and runs a BTreeSet::contains per subject: no per-subject transactions, with membership work still growing with depth. Durability across restart holds for a filesystem-backed SQLite store or a remote one (sqlite_revocation_store_persists_across_reopen).

A row records membership and time. Revocation is permanent: rows in revoked_capabilities are never deleted, and a row holds no reason or revoker. Other nodes learn a revocation through the cluster layer, which reads list_revocations_after over the (revoked_at, capability_id) cursor: the control-plane cluster snapshot and delta handlers, and the denylist warm-up in chio-api-protect.