diff --git a/docs/05-data-model.md b/docs/05-data-model.md index ee8a29e..afffa1d 100644 --- a/docs/05-data-model.md +++ b/docs/05-data-model.md @@ -115,12 +115,14 @@ Per LLM call: `session_id`, `provider`, `model`, `prompt_tokens`, `completion_to | prev_hash | binary | the previous receipt's `receipt_hash`; null only for the first in a scope | | receipt_hash | binary | over the canonical signed bytes | | signed_payload | map | RFC 8785 canonical JSON. Field set is a legal-review question before Slice 024 | -| signature | binary | Ed25519 | -| key_id | string | resolves in `priv/keys/registry.json` | +| signature | binary | through the signer seam: Ed25519 by default, ECDSA P-384 in FIPS mode, ML-DSA-87 opt-in (slice 024 amendments 1 to 6) | +| key_id | string | inside the signed bytes; resolves in `priv/keys/registry.json`, whose row names the algorithm; the verifier reads the algorithm from there and nowhere else | | kind | string | "decision" \| "effect" \| "query" \| "boot" \| "cap" | | subject | map | refs to the session, tool call, approval or effect this receipts | Append-only. Never updated, never deleted. Signing unavailable means the effect is denied, not that an unsigned -row is written. +row is written. The signed bytes carry a scheme string naming the family (`receipt_v2_ed25519`, `receipt_v2_p384`, +`receipt_v2_mldsa87`); a chain never mixes families. Effect, decision, boot and cap receipts are signed one by one; +query receipts are hash-chained and checkpointed (the tail is signed every N rows, every T seconds, and on shutdown). ### mcp_servers (Slice 060) `name`, `transport`, `command_or_url`, `env_refs`, `enabled`, `effect_default ∈ {none, artifact}`, per-tool diff --git a/docs/07-security-model.md b/docs/07-security-model.md index b03b75b..f105ea8 100644 --- a/docs/07-security-model.md +++ b/docs/07-security-model.md @@ -28,6 +28,11 @@ system prompt states that instructions inside untrusted blocks are data, not com - **Reset is total.** Session state holds no authority. A reseeded session is born from the immutable core policy hash and inherits nothing. - **Receipts chain.** Per-scope hash chains, signed, verifiable offline by a stranger with the public registry. + The signature enters through one seam (`Trinity.Receipts.Signer`); the algorithm is selected once at boot, + Ed25519 by default and ECDSA P-384 when FIPS mode is enabled, and is bound by the key registry row rather than + by anything in the receipt. Effect, decision, boot and cap receipts are signed per receipt; query receipts are + checkpointed. No approved algorithm available means the effect is denied, never signed with a refused one and + never written unsigned. ## Permission gate (Slice 021) diff --git a/slices/024-effect-catalog-authority-modes-receipts/SLICE.md b/slices/024-effect-catalog-authority-modes-receipts/SLICE.md index 46d7926..ef5e531 100644 --- a/slices/024-effect-catalog-authority-modes-receipts/SLICE.md +++ b/slices/024-effect-catalog-authority-modes-receipts/SLICE.md @@ -7,11 +7,52 @@ | Size | L | | Depends on | 021, 022 | +**Amended 2026-09-20: the signer seam, algorithm agility and chain scopes by kind.** The design below still +holds; six amendments sit on top of it and two acceptance criteria are added. The reason, stated as the red it +answers: on an OTP built with FIPS mode enabled, `crypto:sign(eddsa, ...)` returns `notsup` (OTP's own `pkey.c` +refuses EdDSA in FIPS mode, whatever OpenSSL provider sits beneath it), and the validated OpenSSL FIPS provider +lists Ed25519 as not approved. This slice as first written pins Ed25519 and says signing unavailable means the +effect is denied. Both are right. Together they mean that on a FIPS build Trinity denies every effect. That is +fail-closed, which is the rule, and it is also useless, which is the amendment. + +1. **A signer behaviour.** `Trinity.Receipts.Signer` with `algorithm/0`, `sign/2` and `verify/3`. One key-custody + module implements it and also the `sign/2` callback the MCP core's signer seam expects, so a deployment + configures its algorithm once and cannot end up with one family on receipts and another on exported bytes. +2. **Selection once, at boot.** ECDSA P-384 with SHA-384 when `crypto:info_fips()` returns `enabled`; Ed25519 + otherwise. The choice lands in the boot receipt (ADR-0010). Denial happens only when no approved algorithm is + available, never because the default is unavailable. +3. **`key_id` inside the signed bytes; the registry binds the algorithm.** The registry row for a `key_id` names + the algorithm. The verifier resolves the algorithm from the registry and never from the receipt body, the + signature, or the signer's input. There is no `alg` field in the envelope, on purpose. +4. **The scheme string carries the family.** `receipt_v2_ed25519`, `receipt_v2_p384`, `receipt_v2_mldsa87`. A + chain never mixes families without a visible break; a receipt of another family is refused at the scheme + string before any signature is checked. +5. **Chain scopes by kind.** Effect, decision, boot and cap receipts are signed one by one: AC5 stays exactly as + written. Query receipts, which are high in volume and low in stakes, are hash-chained and checkpointed: every + N rows, or T seconds, or on shutdown, `ChainWriter` signs the tail; on rehydrate it re-signs the current tail + before accepting a new row. N and T come from the signing measurement in NOTES.md at G1, not from this file. + Signing the tree head for every kind was considered and rejected because it deletes AC5 for effects. +6. **ML-DSA-87 behind the same seam, compile-conditional.** Enabled only when the linked OpenSSL is 3.5 or later + (OTP 28.1 and later expose it through `crypto:sign/4`; the pinned 28.5.0.5 does; this machine's OpenSSL 3.0.13 + does not). Never the default. Its signature is 4,627 bytes against 96 for P-384 and 64 for Ed25519, and the + size goes in the standards register. The word validated is written for it only when the CMVP lists the + provider that carries it. + +| Mode | Algorithm | Hash | Signature bytes | Status | +|---|---|---|---|---| +| Default, not FIPS | Ed25519 | built in | 64 | ships with this slice | +| FIPS mode enabled | ECDSA P-384 | SHA-384 | 96 | amendment 2, proven on the FIPS build leg (slice 003) | +| Post-quantum, opt-in | ML-DSA-87 | built in | 4,627 | amendment 6, compile-conditional | + +Store-and-forward for `receipt/2` (a queued-then-acknowledged mode) is slice 026 and changes ADR-0008's +contract; it is not part of this slice. + ## Goal The membrane: one side-effect boundary (`Trinity.Effects`) that every `:artifact` and `:catalog` effect crosses; the `Trinity.Authority` behaviour with `Local` built and selection at boot; the immutable core policy hash; and -local receipts, one per decision and per effect, in a per-scope hash chain, Ed25519-signed, with a standalone -verifier and an append-only key registry in the tree. +local receipts, one per decision and per effect, in a per-scope hash chain, signed through the signer seam +(Ed25519 by default, P-384 in FIPS mode, per the amendment above), with a standalone verifier and an append-only +key registry in the tree. ## Why Vision goals 1 and 5, and ADR-0008 and ADR-0010. Without this, "every action is gated" is a claim rather than a @@ -35,15 +76,20 @@ property, and "Trinity keeps no executor for delegated effects" is unfalsifiable - **This slice owns receipts outright**: the table, the schema, the chain, the signer. Slice 021 owns the `approvals` audit table and writes no receipts; this slice reads that audit when building decision receipts. - Receipts: `receipts` table (`seq`, `chain_scope`, `prev_hash`, `receipt_hash`, `signed_payload`, `signature`, - `key_id`, `kind ∈ {decision, effect, query, boot, cap}`, `subject` refs); canonical bytes RFC 8785; Ed25519 via - `:crypto`; key generated on first run into the OS keychain (100) or a 0600 file until then. **State plainly what + `key_id`, `kind ∈ {decision, effect, query, boot, cap}`, `subject` refs); canonical bytes RFC 8785; the + signature through `Trinity.Receipts.Signer` (Ed25519 by default, P-384 under FIPS, amendments 1 and 2), with + `key_id` inside the signed bytes and the registry row naming the algorithm (amendment 3); the scheme string + carrying the family (amendment 4); key generated on first run into the OS keychain (100) or a 0600 file until then. **State plainly what a file-backed key does and does not establish**: it proves the chain was not altered after the fact by anything lacking read access to that file, and nothing more. Slice 100 migrates it and the registry records the change; `priv/keys/registry.json` - append-only with `key_id`, `public_key_b64`, `fingerprint`, `valid_from`, `status`; `mix trinity.receipts.verify` + append-only with `key_id`, `algorithm`, `public_key_b64`, `fingerprint`, `valid_from`, `status`; `mix trinity.receipts.verify` and a standalone `bin/verify_receipt.exs` with exit codes `0 verified / 1 invalid / 2 usage / 5 trust not established / 6 compromised key` (same vocabulary as the public verifier so operators learn one). - Signing unavailable ⇒ the effect is **denied** and the failure alarms outside the receipt stream (the - completion-definition C1 resolution, adopted). + completion-definition C1 resolution, adopted). Unavailable means no approved algorithm can sign, after the + boot-time selection of amendment 2; the default being refused in FIPS mode is not unavailability. +- Query receipts are checkpointed rather than signed one by one (amendment 5); every other kind is signed per + receipt. - UI: receipts view per session; boot receipt in Settings. **Out:** receipts, proposals or sockets belonging to an external authority plane. This slice builds Trinity's own local chain and nothing else. @@ -64,13 +110,22 @@ local chain and nothing else. 5. [auto] Signing key removed mid-run → next effect denied, alarm event emitted, no unsigned receipt row exists. 6. [auto] Boot receipt carries `core_policy_hash`; changing a policy module changes the hash (test). 7. [auto] `bin/verify_receipt.exs` runs from an empty directory against an exported receipt file + registry (stranger test). +8. [auto] Algorithm agility: with FIPS mode enabled and P-384 available, no effect is denied for want of a signer + and the boot receipt names P-384 (runs on the FIPS build leg, slice 003); the verifier ignores any algorithm + hint outside the registry (a receipt whose body claims a different algorithm verifies against the registry's, + not the body's); a P-384 receipt presented to an Ed25519 chain is refused at the scheme string before any + signature check (tests, one mutant each: drop the registry lookup, drop the scheme check). +9. [auto] Query-receipt checkpoints: after N query receipts the tail carries a signature; on rehydrate the tail is + re-signed before a new row is accepted; a query receipt inserted after the last checkpoint and before + shutdown is covered by the shutdown checkpoint (tests); the AC5 mutant (remove the denial on signer error) + goes red. ## Manual verification queue None. Every acceptance criterion in this slice is `[auto]` and is proven by a command or a test. If that changes during the slice, the criterion is retagged and this section is filled at G1. ## Definition of Done -- [ ] gate green · [ ] AC1–7 proven · [ ] docs/01, docs/05, docs/07 synced · [ ] ROADMAP → done · [ ] commit + tag +- [ ] gate green · [ ] AC1–9 proven · [ ] docs/01, docs/05, docs/07 synced · [ ] ROADMAP → done · [ ] commit + tag ## Commit & tag `feat(s024): complete slice 024 (effect catalog, authority selection, local receipts)` · tag `slice/024` @@ -84,3 +139,8 @@ receipt metadata, and the signed bytes carry `seq`, `chain_scope`, `prev_hash`, ## Risks / open questions - Trinity's receipt scheme is its own. Do not adopt another system's verifier or its signed-byte layout for local receipts; an adapter that needs a different scheme brings its own. +- AC8's FIPS half cannot run on the developer machine (`crypto:info_fips()` returns `not_supported` there); it + runs on slice 003's leg. If 003 has not landed when this slice reaches G3, the FIPS half is recorded as not + measured, by name, and the slice does not close. +- P-384 signs slower than Ed25519 through OpenSSL and has no dedicated assembly path; the checkpoint window + (amendment 5) absorbs it for query receipts, and the per-receipt cost for the other kinds is measured at G1.