Chio/Docs
LOGIN · JOIN

Assurance Model

Assess Chio’s guarantees against the components you trust, the host’s isolation, and the assumptions behind proofs and signed records.

Concept chio@5f63e6e

On this page

A guarantee reaches exactly as far as the component that enforces it. Chio offers three kinds, each with its own reach: checks that run before dispatch, which govern the calls routed through the kernel; signatures, which bind a record to the key that signed it; and Lean proofs, which hold for a bounded model of the decision core. The host and the operator supply what lies outside those reaches: the isolation that routes calls through the kernel, custody of the keys, the clock, and the store.

Reading a Chio claim correctly means naming its boundary. A kernel refusal prevents a write only on the path the kernel governs. A valid receipt signature establishes what a key signed, not that the tool's effect happened. A proof about a decision establishes nothing about the I/O that follows it.

The boundary covers the calls routed through it

An agent presents a capability, the kernel checks authority and policy, and an allowed request reaches the tool. That boundary governs the calls that pass through it. A writable mount, an inherited credential, or a separate native tool gives the agent a second route to the same resource, and the kernel never sees a call on that route.

Routes from the agent to the resource, and whether every one crosses the kernelcut at Kwritable mounttnative toolinherited credentialrequestadmitteddispatchaKdRagentkerneladapterrepository/governed
mandatory(R)  ⟺  ∀ π∈Π(a,R): K∈π\text{mandatory}(R) \iff \forall\, \pi \in \Pi(a, R):\ \htmlClass{role-seal}{K} \in \pi
π0=(a,K,d,R)∋K\htmlClass{role-seal}{\pi_0 = (a, K, d, R) \ni K}
π1=(a,R)mount∌K\pi_1 = (a, R)_{\text{mount}} \not\ni K
π2=(a,t,R)∌K\pi_2 = (a, t, R) \not\ni K
π3=(a,R)cred∌K\pi_3 = (a, R)_{\text{cred}} \not\ni K
mandatory(R)=1\text{mandatory}(R) = \htmlClass{role-seal}{1}
every route to R crosses the kernelclick a dashed route to grant it
Routes from the agent to the resource, and whether every one crosses the kernelcut at Kwritable mounttnative toolinherited credentialaKdRagentkerneladapterrepository/governed
mandatory(R)  ⟺  ∀ π∈Π(a,R): K∈π\text{mandatory}(R) \iff \forall\, \pi \in \Pi(a, R):\ \htmlClass{role-seal}{K} \in \pi
π0=(a,K,d,R)∋K\htmlClass{role-seal}{\pi_0 = (a, K, d, R) \ni K}
π1=(a,R)mount∌K\pi_1 = (a, R)_{\text{mount}} \not\ni K
π2=(a,t,R)∌K\pi_2 = (a, t, R) \not\ni K
π3=(a,R)cred∌K\pi_3 = (a, R)_{\text{cred}} \not\ni K
mandatory(R)=1\text{mandatory}(R) = \htmlClass{role-seal}{1}
click a dashed route to grant it

Every route from the agent to the repository crosses the kernel, so admission is mandatory.

In Rust · lib.rs:25913 lines
/// Invoke a bridged tool. A dispatcher is required so the kernel cannot
/// sign successful receipts for simulated side effects.
pub fn invoke_tool(&self, tool_name: &str, arguments: Value) -> Result<Value, BridgeError> {
    // …
    if let Some(dispatcher) = &self.dispatcher {
        // … egress contract checks
        let response = dispatcher(&binding.method, &url, &arguments)?;
        // …
    } else {
        Err(BridgeError::Kernel(
            "OpenAPI bridge requires a dispatcher for live tool invocation".to_string(),
        ))
    }
An illustrative deployment. The host, not Chio, enforces the cut: it decides which processes run and which credentials, handles, and mounts they receive. An embedded library cannot isolate itself from a compromised host.Architecture

Deployment isolation closes those routes. The host decides which processes run, which credentials and handles they receive, and which adapters can reach protected resources. Every guarantee below assumes that isolation; the threat model describes the host profiles that provide it.

Name what each component is trusted for

Each trusted component has a defined responsibility and a corresponding failure boundary.

ComponentTrusted forIf it fails
The kernelChecking authority and policy, and signing the record of each decision. It is part of the trusted computing base.A compromised kernel can authorize calls or sign false records.
The capability authorityIssuing the intended permissions and protecting its signing keys.Wrongly issued or stolen authority is honored until it expires or is revoked.
AgentsNothing. They supply untrusted requests; a governed call needs a valid capability, and an agent’s identity alone grants no tool access.A misbehaving agent can ask for anything; it can do only what a grant covers.
Tool serversPerforming effects. An allowed request does not make its executor trustworthy.The effect is bounded by the tool’s own process, filesystem, and network isolation.
OperatorsKey custody, accepted issuer keys, clocks, and storage.These set what the deployment can guarantee at all.

A failed check stops the call before dispatch

Chio fails closed. A check that cannot establish its answer counts as a refusal, so an error never becomes permission: a revocation lookup that fails, an internal error in the guard pipeline, and a budget hold that goes unanswered each end the call before dispatch. Every check before dispatch returns one of three answers, and only one of them reaches the tool.

Three values, two outcomesChoose a check and its answer.
Three checks before dispatch and one after it; each returns established, refused, or unanswered, and only established continuesrrequest1established0refused⊥unanswereddispatch to the toolbefore: a refusal prevents the effectafter: a refusal withholds the result1capabilitynextdenydeny⊥guardsnextdenydenybudget holdnextdenydenyresult checkreturnwithholdwithholdrefused before dispatchthe tool never ran; one receipt records the denial
dispatch(r)  ⟺  ⋀k=13[ ck(r)=1 ],ck(r)∈{1, 0, ⊥}\mathrm{dispatch}(\htmlClass{role-call}{r}) \iff \bigwedge_{k=1}^{3} \big[\, c_k(\htmlClass{role-call}{r}) = 1 \,\big], \qquad c_k(\htmlClass{role-call}{r}) \in \{1,\, 0,\, \htmlClass{role-deny}{\bot}\}
Three checks before dispatch and one after it; each returns established, refused, or unanswered, and only established continuesrrequest10⊥dispatch to the tool1capability10⊥⊥guards10⊥budget hold10⊥result check10⊥refused before dispatchthe tool never ran; one receipt records the denial
dispatch(r)  ⟺  ⋀k=13[ ck(r)=1 ],ck(r)∈{1, 0, ⊥}\mathrm{dispatch}(\htmlClass{role-call}{r}) \iff \bigwedge_{k=1}^{3} \big[\, c_k(\htmlClass{role-call}{r}) = 1 \,\big], \qquad c_k(\htmlClass{role-call}{r}) \in \{1,\, 0,\, \htmlClass{role-deny}{\bot}\}

A guard error is a denial

An internal guard error counts as a denial. The pipeline stops at the first one, and nothing is dispatched.

The kernel's admission order for one call, with each check reduced to three answers. Approval, request matching, and the separate checks inside each stage are left out; a call that needs approval waits as pending until the approval path resolves it.

A request that needs human approval is neither admitted nor refused: it remains pending until the approval path resolves it. A check on the returned result runs after the tool has acted, so Chio withholds the result and the work the tool already performed is not undone.

After dispatch, a refusal can only act on what came back. Availability, crash recovery, and external effects depend on the runtime and the deployment as well as on the decision checks; what survives a crash follows them.

Authority stays as narrow as the grant

A capability identifies the servers, tools, operations, and constraints it permits. Its expiry bounds the time window. Configured budget and rate checks bound spending and activity. Delegation must preserve or narrow the parent’s scope, duration, and limits, so authority can only shrink as it is passed down.

A compromised agent can still request everything its grant covers. Choose the scope accordingly. Capabilities covers token validation and delegation, and Guards covers the request-level checks that narrow a grant further.

Plan for that case as an incident. After you revoke the agent’s capability, the kernel refuses it and every token delegated from it, and the receipts of its earlier calls record what it attempted. Detect, Contain, Recover follows an attempt from detection to containment. Contain a compromised agent gives the commands that withdraw a real host’s bearer credential, capability, and process admission.

A signature establishes what a key signed

A receipt records the request, the kernel’s decision, and the evidence available to it. A verifier holding the trusted kernel public key can check that the signed fields have not changed since they were signed. That check establishes what the key signed, and no more.

A valid signature establishesIt does not establish
The signed fields are unchanged since the key signed them.Who originated the request.
The decision and its evidence are the ones the kernel recorded.That the tool’s external effect happened, or happened as reported.
Which policy and capability the decision names.That a store retained every receipt, or that the record is the latest.

Completeness and freshness need more evidence and an explicit verifier policy: retained checkpoints, inclusion proofs, and a commitment held outside the producer. Receipts and Verifiable evidence follow those checks.

The kernel key is one of several. A deployment checks signatures on capability tokens, delegation links, approval tokens, receipts and checkpoints, peer directories, and model cards, and each verifier needs a basis for accepting the signing key.

Signing key treeChoose a chain.
verifier’s pins

Every chain of trust ends at a pin

A verifier accepts a signing key from its own configuration or from a signed artifact it already trusts. Six chains cover the keys a deployment signs with:

pinned
Listed in the verifier’s own configuration: trusted issuers, approvers, receipt signers, directory issuers, an expected identity.
signs
The key signs the artifact, and the signature verifies against that key alone.
named
An accepted artifact names the next key: a capability’s subject, a directory’s passport keys, an endorsed oracle key.
In Rust · validation.rs:266
pub(crate) fn trusted_issuer_keys(&self) -> Vec<chio_core::PublicKey> {
    let mut trusted = self.config.ca_public_keys.clone();
    for authority_pk in self.capability_authority.trusted_public_keys() {
        if !trusted.contains(&authority_pk) {
            trusted.push(authority_pk);
        }
    }
    let kernel_pk = self.config.keypair.public_key();
    if !trusted.contains(&kernel_pk) {
        trusted.push(kernel_pk);
    }
    trusted
}
The keys the pinned source signs with and checks. The agent’s proof-of-possession key, the delegator’s key, and the federation’s passport and oracle keys are trusted only because an accepted artifact names them. Workload identity and runtime attestation are bound by other evidence and are left out.

A verifier accepts a key through a local pin or a trusted parent binding. A pinned key is listed in the verifier’s own configuration: the trusted issuers a kernel accepts for capability tokens, the approvers a request names, the signer list a recipient keeps for receipts, the directory issuers a federated kernel accepts, and the identity a deployment expects on a model card. A key named by its parent is trusted only because something the verifier already accepts names it. A delegation link verifies against the key a stored parent capability names as its subject, a proof of possession against the token’s subject, and a revocation root against the oracle key an operator’s passport endorsed.

Each chain therefore ends at a pin, and whoever configures the verifier chooses its pins: the operator chooses the kernel’s trusted issuers, and a recipient chooses its own list of receipt signers. A key on a trust list is accepted whoever holds it; a key missing from one is refused, as a token from an unlisted issuer is refused with UntrustedIssuer.

Verify one record both ways to see the split. The fixer's refused test write from the Quickstart is a genuine record of a denial, signed by your kernel. Checked with your kernel's pinned key and without it, the signature verifies both times; only the pin decides whether the record is trusted:

verify-pin.tsverify_pin.pysrc/main.rs · in mainTerminal
import { readFileSync } from "node:fs";
import { parseReceiptJson, verifyReceiptWithTrustedSigners } from "@chio-protocol/sdk/invariants";
import { TrustFile } from "@chio-protocol/sdk/trust";

const trust = await TrustFile.load();
const receipt = parseReceiptJson(readFileSync("refused-write.json", "utf8"));

const fields = ["signature_valid", "signer_trusted", "ok", "authorized"] as const;
for (const [label, keys] of [["pinned", trust.keys("receipt-kernel")], ["unpinned", []]] as const) {
  const v = verifyReceiptWithTrustedSigners(receipt, [...keys]);
  console.log(label.padEnd(9), fields.map(f => `${f}=${v[f]}`).join(" "));
}
Output
pinned    signature_valid=true signer_trusted=true ok=true authorized=false
unpinned  signature_valid=true signer_trusted=false ok=false authorized=false

ok is true for the pinned check and authorized is false, because the record is trusted and it records a refusal. Without the pin the same bytes still carry a valid signature, and ok is false. chio trust pins lists every pin a verifier on this machine reads, with the card or file each came from, and chio trust roles lists the roles a pin can serve.

The formal proof ends inside the core

Lean proofs cover stated properties of bounded models and selected decision-core functions. They do not prove the full Rust runtime, the operating system, or arbitrary tool-server behavior. Concrete cryptography, serialization, clocks, storage, and transport carry separate assumptions, recorded in an audited registry, and a proof about a decision does not establish that its later I/O succeeded.

Where the formal proof applies, and the audited assumptions each property rests onscope of formal reasoningdeploymentOS, network, tool servers, operatorsRust runtimestores, adapters, transport, I/Odecision coreportable, no_stdproof modelsLean: bounded models andselected core functions1 allowed axiomproofspropertiesaudited assumptions, by classP1P2P3P4P5P6P7P8P9P10cryptography2serialization1platform3storage1transport3external services3external chains1observability1
Where the formal proof applies, and the audited assumptions each property rests onscope of formal reasoningdeploymentOS, network, tool serversRust runtimestores, adapters, I/Odecision coreportable, no_stdproof modelsLean modelspropertiesaudited assumptions, by classP1P2P3P4P5P6P7P8P9P10cryptographyserializationplatformstoragetransportexternal servicesexternal chainsobservability
claim(Pk)  ⇐  proof(Pk) ∧⋀a ∈ A(Pk)a∣A(P4)∣=7\begin{aligned} &\text{claim}(P_k) \;\Leftarrow\; \htmlClass{role-seal}{\text{proof}(P_k)} \,\wedge \bigwedge_{a \,\in\, A(P_k)} \htmlClass{cor-parent}{a} \\ &\lvert A(P_{4}) \rvert = 7 \end{aligned}
P4 · receipt integrity

The registry lists 7 audited assumptions for this property: ED25519, SHA256, CANONICAL-JSON, SQLITE-ATOMICITY, CHAIN-FINALITY, TRACE-OBSERVER, FINDING-STATUS-OPERATOR-COMPLETENESS.

In TOML · assumptions.toml:517 lines
required_assumption_ids = [
  "ASSUME-ED25519",
  "ASSUME-SHA256",
  "ASSUME-CANONICAL-JSON",
  "ASSUME-OS-CLOCK",
  "ASSUME-SQLITE-ATOMICITY",
  "ASSUME-TLS",
  "ASSUME-NETWORK-TRANSPORT",
  "ASSUME-GOSSIP-FAIRNESS-PARTITION-BOUND",
  "ASSUME-EXTERNAL-REGISTRIES",
  "ASSUME-SUBPROCESS-ISOLATION",
  "ASSUME-CHAIN-FINALITY",
  "ASSUME-TRACE-OBSERVER",
  "ASSUME-WASM-ENGINE",
  "ASSUME-FINDING-STATUS-OPERATOR-COMPLETENESS",
  "ASSUME-FINDING-SELLER-TOOL-SERVER",
]
The regions show containment, not size. Properties, classes, and edges come from the audited assumption registry; an edge means the registry lists an assumption of that class for the property. Each property also rests on its proof evidence, which Formal assurance lists by lane.Formal assurance

Read a property’s guarantee as a conjunction: its proof evidence and every audited assumption the registry lists for it. The registry lists none for capability attenuation or for delegation-chain semantic validity, and seven for receipt integrity, from Ed25519 and SHA-256 to SQLite atomicity and the external status operator. A reviewer can accept or reject each assumption on its own terms.

Read every audited assumption

The manifest permits these axioms inside the proofs: Chio.Json.hash_collision_resistant. The audited assumptions below describe the production dependencies outside them.

  • ASSUME-ED25519: Ed25519 verification and signing are assumed to satisfy standard unforgeability for trusted public keys.
  • ASSUME-SHA256: SHA-256 and Merkle hash collision resistance are assumed for concrete receipt and checkpoint evidence.
  • ASSUME-CANONICAL-JSON: The production canonicalizer is assumed to agree byte-for-byte with the mechanized UTF-8 renderer on Unicode scalar strings, normalized bounded integers, arbitrary finite arrays, and UTF-16-ordered objects. Float rendering and float-bearing compound receipt fields outside that domain remain assumed deterministic and byte-stable.
  • ASSUME-OS-CLOCK: The injected clock is assumed to report operator-accepted Unix time within the deployment tolerance.
  • ASSUME-SQLITE-ATOMICITY: SQLite transactions are assumed to provide atomic committed updates for revocation, budget, receipt, and registry state per single-row write. Cross-row crash recovery, ordering, and conservation are not assumed or discharged and remain outside the current formal claim boundary.
  • ASSUME-TLS: TLS endpoint authentication and channel confidentiality are assumed for configured remote control and hosted HTTP surfaces.
  • ASSUME-NETWORK-TRANSPORT: Network delivery is not assumed reliable, but authenticated messages received by Chio are assumed not to be silently rewritten below TLS or signature checks.
  • ASSUME-GOSSIP-FAIRNESS-PARTITION-BOUND: For a configured bilateral revocation peer set, correct connected peers are assumed to have recurring push or catch-up opportunities governed by weak fairness, local clocks remain within the declared skew bound, and declared partitions heal within the operator-declared partition bound. Loss, duplication, reordering, and invalid frames are modeled rather than assumed away. No finite delivery-step or raw-evaluation bound is assumed.
  • ASSUME-EXTERNAL-REGISTRIES: Hosted package, certification, DID, and registry services are assumed to return state they have durably accepted or else fail closed.
  • ASSUME-SUBPROCESS-ISOLATION: Tool-server subprocess isolation and OS process boundaries are assumed for effects outside the pure kernel decision core.
  • ASSUME-CHAIN-FINALITY: External chain and oracle finality are assumed only after the configured confirmation/finality policy accepts the evidence.
  • ASSUME-TRACE-OBSERVER: An installed synchronous runtime trace observer is assumed to receive exactly once before finalization every successful revocation commit, completed tool-call revocation admission, and receipt append. Kernel-assigned source sequences, checked revocation subject identities, exact revocation-source identities, and other callback fields are not rewritten before recording, and the recorder runs without calibration mutations. Delivery reordering is reconciled from source sequences; detectable omissions, duplicates, inconsistent kernel depth limits, ambiguous admission-to-receipt joins, unmatched revocation sources, and relevant revocations between admission and receipt append fail closed. This assumption does not assert that any observed kernel decision is safe.
  • ASSUME-WASM-ENGINE: Wasmtime is assumed to enforce its documented i32 return, trap, fuel-metering, memory-limiter, and in-process sandbox semantics for untrusted guest code.
  • ASSUME-FINDING-STATUS-OPERATOR-COMPLETENESS: The qualified cognition-market profile verifies authentic fresh status-feed state but assumes the external status operator inserts every required retraction into that feed.
  • ASSUME-FINDING-SELLER-TOOL-SERVER: The qualified cognition-market profile binds kernel-observed seller output bytes and receipts but assumes the seller tool server performs any claimed effect outside Chio's observation boundary.

Follow the evidence

Locate the componentsSystem map, call sequence, deployment choices, and proof boundary.Inspect the formal assumptionsRead the trusted computing base and the scope of each claim.Verify a receipt packageExport the Quickstart records and check them offline.Cross organizational boundariesConfigure issuer recognition and bilateral trust.

For the complete application boundary, read the Security threat model and select the host profile that enforces your intended paths.

PreviousReputation & PassportsNextFederation & Swarms