|
| 1 | +<!-- SPDX-FileCopyrightText: Sudo Apt Holdings LLC --> |
| 2 | +<!-- SPDX-License-Identifier: Apache-2.0 --> |
| 3 | +# 10: Assurance case |
| 4 | + |
| 5 | +An assurance case is a structured argument that a system's security claims hold, with the evidence |
| 6 | +for each claim named so that a reader can check it rather than take it on trust. This document is |
| 7 | +Trinity's. |
| 8 | + |
| 9 | +It is organised as claims, each with the argument for it and the evidence that supports it. Every |
| 10 | +piece of evidence is a path in this repository, a test that can be run, or a command that produces |
| 11 | +the stated output. Where a claim has a limit, the limit is stated with the claim rather than left |
| 12 | +for a reader to discover. |
| 13 | + |
| 14 | +**The top claim.** *An action with an effect outside the conversation cannot happen unless a |
| 15 | +decision was made to allow it, and what happened can be reconstructed afterwards from records that |
| 16 | +cannot be silently altered.* |
| 17 | + |
| 18 | +Everything below decomposes that claim. The scope is the software in this repository. It excludes |
| 19 | +the machine's own security, the model provider's conduct, and any external authority layer a |
| 20 | +deployment supplies, each of which is named as an assumption at the end. |
| 21 | + |
| 22 | +--- |
| 23 | + |
| 24 | +## C1. No effect happens without a decision |
| 25 | + |
| 26 | +**Argument.** Every tool call is decided before it runs. The decision is made by one component, |
| 27 | +recorded before the effect is attempted, and cannot be bypassed by the surface that requested it: |
| 28 | +approval surfaces carry no authority of their own, they only report a decision made elsewhere. |
| 29 | + |
| 30 | +**Evidence.** |
| 31 | +- `lib/trinity/permissions/gate.ex` is the single decision point; `lib/trinity/effects/runner.ex` |
| 32 | + asks it once per validated call and writes a decision receipt before anything runs. |
| 33 | +- A decision that cannot be receipted refuses the call, so an unrecorded effect is not a |
| 34 | + possibility the code allows. |
| 35 | +- `test/trinity/permissions/gate_test.exs`, `test/trinity/permissions/session_flow_test.exs`. |
| 36 | +- The tier of a call is code, not configuration supplied by a caller: a runtime-registered tool |
| 37 | + cannot claim a core tool's name or lower its own tier. |
| 38 | + |
| 39 | +**Limit.** The gate decides; it does not sandbox. A tool that is allowed to run does run, with the |
| 40 | +privileges of the operating-system user. Isolation of executable content is a separate mechanism |
| 41 | +(`Trinity.Sandbox`) and is not claimed here. |
| 42 | + |
| 43 | +## C2. Identity is separated from authority |
| 44 | + |
| 45 | +**Argument.** Establishing who is calling and deciding whether an effect may happen are different |
| 46 | +questions answered by different components. A credential never carries an entitlement. |
| 47 | + |
| 48 | +**Evidence.** |
| 49 | +- ADR-0008 records the decision and its consequences. |
| 50 | +- `Trinity.MCP.Auth` authenticates a caller and answers with a principal, never a permission; the |
| 51 | + permission gate still decides every call that principal makes. |
| 52 | +- A token's scopes are checked *before* the gate is consulted and never in place of it: a scoped |
| 53 | + token is permission to ask, not permission to act |
| 54 | + (`test/trinity/mcp/auth/resource_server_test.exs`). |
| 55 | +- An approval arriving from a chat channel is capped below what the local desktop may approve, and |
| 56 | + the cap is applied *after* the gate's own decision, never instead of it |
| 57 | + (`lib/trinity/gateways/cap.ex`, `test/trinity/gateways/approvals_test.exs`). |
| 58 | + |
| 59 | +**Limit.** Where a deployment supplies an external authority layer, this tree keeps no executor for |
| 60 | +the effects that layer governs; what that layer decides is outside this case. |
| 61 | + |
| 62 | +## C3. Content from outside the machine is never treated as instruction |
| 63 | + |
| 64 | +**Argument.** Anything Trinity reads from the world — a web page, a file, a tool result, another |
| 65 | +agent's response over the protocol — is marked at the boundary where it enters and stays marked. |
| 66 | +The model sees it as data. |
| 67 | + |
| 68 | +**Evidence.** |
| 69 | +- `lib/trinity/tools/untrusted.ex` marks content at the boundary with its origin and source. |
| 70 | +- The persona instructs that tool results and web pages are data and never instructions, and the |
| 71 | + provenance rules in `docs/07-security-model.md` state where the mark is applied. |
| 72 | +- Model output reaches the interface through one rendering path, so an injection cannot escape |
| 73 | + into markup by a second route. |
| 74 | + |
| 75 | +**Limit.** Marking is not proof against a model choosing to follow instructions it was told to |
| 76 | +ignore. The mitigation that does not depend on the model's judgement is C1: whatever the model is |
| 77 | +persuaded to attempt still meets the gate. |
| 78 | + |
| 79 | +## C4. Model output is never executed |
| 80 | + |
| 81 | +**Argument.** No path evaluates text a model produced. This is enforced by a tool over the whole |
| 82 | +tree rather than by review. |
| 83 | + |
| 84 | +**Evidence.** |
| 85 | +- `credo_checks/no_eval_on_model_output.ex`, a project-specific static analysis rule covering |
| 86 | + `Code.eval_string` and its family, run in the quality gate on every commit. |
| 87 | +- `test/no_eval_on_model_output_test.exs` holds the rule itself. |
| 88 | +- `docs/03-conventions.md`, engineering rules. |
| 89 | + |
| 90 | +## C5. The architecture is enforced rather than described |
| 91 | + |
| 92 | +**Argument.** The module layering in `docs/01-architecture.md` is compiled. A dependency that |
| 93 | +violates it is a compile error, so the document cannot drift from the code. |
| 94 | + |
| 95 | +**Evidence.** |
| 96 | +- `boundary` runs as a compiler and the gate compiles with warnings as errors, so a violation fails |
| 97 | + the build. |
| 98 | +- The authorization package is declared with no dependency on the rest of the tree, and the |
| 99 | + refusal of a planted violation is reproducible: add a call to `Trinity.Sessions` inside |
| 100 | + `lib/trinity/mcp/auth/` and `mix compile --warnings-as-errors` exits 1 naming it. |
| 101 | +- `test/trinity/mcp/auth/boundary_test.exs` holds the declaration and a source census beside it. |
| 102 | + |
| 103 | +## C6. What happened can be reconstructed |
| 104 | + |
| 105 | +**Argument.** Decisions and effects are written to an append-only hash chain, each entry signed, |
| 106 | +with periodic checkpoints, and a verifier that detects alteration. |
| 107 | + |
| 108 | +**Evidence.** |
| 109 | +- `lib/trinity/receipts/` — the chain writer, the signer (Ed25519), checkpoints, and |
| 110 | + `verifier.ex`. |
| 111 | +- `test/trinity/receipts/verifier_test.exs` and `standalone_verifier_test.exs`: the verifier |
| 112 | + detects a tampered entry, and it runs without the application so an auditor need not trust the |
| 113 | + program that wrote the records. |
| 114 | +- Receipts carry the caller's issuer, subject and scope where the call arrived over the protocol, |
| 115 | + and never the credential itself. |
| 116 | + |
| 117 | +**Limit, stated plainly.** A chain signed by a key held in a file proves the records were not |
| 118 | +altered after the fact. It does not prove custody of the key. Key custody is a separate concern |
| 119 | +and is not claimed here. |
| 120 | + |
| 121 | +## C7. Cryptography is standard, correctly sourced, and measured |
| 122 | + |
| 123 | +**Argument.** Only published, reviewed algorithms are used; none is implemented in this project; |
| 124 | +keys and nonces come from a cryptographically secure generator; and the claims about approved |
| 125 | +algorithms are measured on a dedicated build rather than asserted. |
| 126 | + |
| 127 | +**Evidence.** |
| 128 | +- Ed25519 (RFC 8032), SHA-256 (FIPS 180-4), AES-256-GCM (NIST SP 800-38D), and the JOSE algorithms |
| 129 | + ES256, EdDSA and RS256 (RFC 7518, RFC 8037). All performed by Erlang/OTP's `:crypto` (OpenSSL) |
| 130 | + and the JOSE library. |
| 131 | +- All keys, nonces and credentials from `:crypto.strong_rand_bytes/1`. A census test forbids the |
| 132 | + non-cryptographic generator in the gateway package |
| 133 | + (`test/trinity/gateways/identities_test.exs`), added after an audit found a pairing code drawn |
| 134 | + from `Enum.random/1`; the fix is in the history and is not hidden. |
| 135 | +- A continuous integration leg builds from source and runs the cryptographic properties inside a |
| 136 | + FIPS-mode container (`docs/fips-leg.md`, the `fips` job). |
| 137 | + |
| 138 | +## C8. The supply chain is controlled and the provenance of changes is established |
| 139 | + |
| 140 | +**Argument.** Dependencies are pinned and audited; every change carries an attested author; and no |
| 141 | +change reaches the main branch without the full gate. |
| 142 | + |
| 143 | +**Evidence.** |
| 144 | +- Versions pinned in `VERSIONS.md` and verified against the lock file by the gate; `hex.audit` and |
| 145 | + `deps.audit` run on every commit. |
| 146 | +- Every commit carries a Developer Certificate of Origin sign-off, enforced by a local hook and |
| 147 | + independently by CI, so a bypassed hook still fails the build. |
| 148 | +- The main branch is protected: changes merge only through a pull request with the gate green. |
| 149 | + |
| 150 | +**Gap, stated rather than omitted.** The project does not yet publish a signed Software Bill of |
| 151 | +Materials. It is planned work, and until it exists this claim is weaker than current federal |
| 152 | +guidance asks for. |
| 153 | + |
| 154 | +## C9. Memory safety by construction |
| 155 | + |
| 156 | +**Argument.** The classes of defect that dominate vulnerability data in memory-unsafe languages do |
| 157 | +not arise in this tree, because of the languages it is written in rather than because of diligence. |
| 158 | + |
| 159 | +**Evidence.** The application is Elixir on the BEAM; the desktop shell is Rust. Both are |
| 160 | +memory-safe. There is no C or C++ in the project's own code. |
| 161 | + |
| 162 | +**Limit.** Dependencies below the runtime — OpenSSL, the BEAM itself, the GTK stack the desktop |
| 163 | +shell links — are written in memory-unsafe languages. The claim is about this project's code. |
| 164 | + |
| 165 | +## C10. Secrets do not enter the repository or the records |
| 166 | + |
| 167 | +**Argument.** Credentials live in the environment or the operating system's keychain, never in the |
| 168 | +tree, and are kept out of the records the system writes. |
| 169 | + |
| 170 | +**Evidence.** |
| 171 | +- A secrets scan runs in the quality gate on every commit; `.env*` is excluded from version |
| 172 | + control. |
| 173 | +- No credential material reaches a receipt, a log line, or the model's context: the authorization |
| 174 | + layer answers with a principal and never the token, and tests scan the records and the session's |
| 175 | + messages for credential material and find none. |
| 176 | + |
| 177 | +--- |
| 178 | + |
| 179 | +## Assumptions |
| 180 | + |
| 181 | +An assurance case that does not name its assumptions is an advertisement. These are Trinity's, and |
| 182 | +each is outside the software's control. |
| 183 | + |
| 184 | +1. **The machine is trusted.** Trinity runs as the operator's user and protects them from what it |
| 185 | + reads, not from themselves or from an attacker who already controls the machine. |
| 186 | +2. **The BEAM is not an operating-system sandbox.** It isolates processes from each other; it does |
| 187 | + not confine what a permitted tool may do to the filesystem or the network. |
| 188 | +3. **Key custody is the operator's.** See the limit under C6. |
| 189 | +4. **The model provider is not trusted for safety.** Every claim above is arranged so that a model |
| 190 | + behaving badly is contained by the gate and the membrane rather than by its own compliance. |
| 191 | +5. **An external authority layer, where a deployment supplies one, is outside this case.** |
| 192 | + |
| 193 | +## What is not claimed |
| 194 | + |
| 195 | +`SECURITY.md` states the boundaries in the project's own words. In summary: no claim is made about |
| 196 | +resistance to an attacker with local privileges, about the sandboxing of executable content before |
| 197 | +the sandbox slice, or about any regulatory compliance not carrying a row in |
| 198 | +`docs/09-standards-register.md` with an evidence path and a status. |
| 199 | + |
| 200 | +## How to check this document |
| 201 | + |
| 202 | +Every claim above names files, tests or commands. `mix gate` runs the checks referenced throughout |
| 203 | +in one command. The standards register records which external requirements are claimed and which |
| 204 | +are not, and the risk register records what is known to be wrong and what would lift it. If a |
| 205 | +claim here cannot be checked by a reader from those artefacts, that is a defect in this document |
| 206 | +and worth reporting as one. |
0 commit comments