# ICA Gateway Security Property Catalog Machine-checked safety properties of the ICA Tool Gateway (the enforcement plane every governed agent action passes through). Each property is verified by the TLA+ model checker (TLC) over the **entire** finite input domain, not sampled by tests. Deliberately broken *red* twins, each a copy of a model with one guard removed, must be rejected by TLC: a spec that cannot fail proves nothing. The suite runs 15. Run it: `bash formal/run.sh` (needs Java + `tla2tools.jar`; CI runs it on every change to the gateway). Status below reflects the committed suite. | ID | Property | Module | Abstracts (real code) | Green | Red twin | | --- | --- | --- | --- | --- | --- | | P1 | **Deny by default**: an `allow` implies every positive precondition held | `ICAGatewayDecision` · `DenyByDefault` | `tool-gateway.js` `decide()` ordered guards | ✅ | the P2 to P5 twins break it too | | P2 | **Revoked agents have no authority**: `REVOKED`/`WASHED_OUT` ⇒ deny | `ICAGatewayDecision` · `RevokedNeverAllow` | `decide()` agentState guard | ✅ | `skip_revoked` caught | | P3 | **Tenant isolation**: cross-tenant request ⇒ deny | `ICAGatewayDecision` · `CrossTenantNeverAllow` | `decide()` requestTenant≠agentTenant | ✅ | `skip_tenant` caught | | P4 | **Fail-closed**: no signed scope contract ⇒ deny | `ICAGatewayDecision` · `FailClosedNoContract` | `decide()` "fail closed" branch | ✅ | `skip_contract` caught | | P5 | **No authority from untrusted content**: untrusted-only action never allowed | `ICAGatewayDecision` · `NoAuthorityFromUntrustedContent` | `tool-gateway.js` instruction/data separation | ✅ | `allow_untrusted` caught | | P6 | **Consequential actions need approval**: never a bare allow | `ICAGatewayDecision` · `ConsequentialNeedsApproval` | `decide()` require_approval branch | ✅ | `auto_consequential` caught | | P7 | **Total decision**: every request maps to exactly one of {allow, require_approval, deny} | `ICAGatewayDecision` · `Total` | `decide()` return contract | ✅ | holds by construction | | P8 | **Single-use capability**: no capability executes more than once, under any interleaving | `ICAGatewayNonce` · `SingleUse` | `capability-store.js` `redeemCapability` nonce burn | ✅ | `no_burn` caught | | P9 | **Invariant-preserving upgrade**: an upgrade never grants authority the baseline withheld and still satisfies every invariant | `ICAGatewayUpgrade` · `UpgradePreservesSafety` | the gate a hot policy/logic upgrade must pass | ✅ | `weaken_revoked`, `weaken_tenant` caught | **Coverage today:** P1 to P7 are checked over all 1,152 resolved-request combinations (agent state × tenant match × contract × allowlist × denylist × action class × untrusted-only × deps health × approval). P8 is checked over concurrent redemptions of a bounded nonce set. **Red twins:** `formal/run.sh` runs 15, and every one returns a concrete counterexample witness (the exact violating input, or the trace that reaches the violation). Eight cover the table above: one each for P2 to P6 and P8, and two for P9. Four cover M1 to M4 (below) and three the TrustScore kernel (`RelationshipTrust.tla`); `README.md` lists all fifteen. P1 and P7 have no red twin of their own. P1 is the conjunction of the decision guards, so the P2 to P5 twins each produce an allow that P1 forbids: point any of those four configs at `DenyByDefault` and TLC returns a counterexample. P7 holds by construction: every branch of `Decide` returns allow, require_approval or deny, so no removed guard can break it. ## Refinement to the running system (informal mapping) The TLA+ variables map to the production gateway as follows. Keep this in sync when `decide()` or `redeemCapability` changes. A change to those paths triggers the CI job that re-checks this catalog. ``` Abstract (TLA+) Concrete (engine/*) ------------------------------ ---------------------------------------------- Decide(req) tool-gateway.js decide() / evaluate() req.agentState ica_internal_systems.agent_state req.tenantMatch requestTenant === agentTenant req.hasContract a signed scope contract on record req.inAllowlist / req.denied the agent's intent allow/deny lists req.actionClass benign | consequential | dangerous req.untrustedOnly instruction/data separation verdict req.depsHealthy policy/evidence dependency health req.approved a target-bound human approval (D9) burned / SingleUse capability-store.js redeemCapability (nonce burn) stuttering steps logging, metrics, retries, DB round-trips ``` P9 demonstrates the invariant-preserving-upgrade gate: TLC accepts a tightening upgrade and rejects one that drops a guard (`ICAGatewayUpgrade.tla`). This is the model-checked foundation the "hot upgrade only if it preserves the invariants" story rests on. ## From the model to the running code (the conformance + refinement gate) A proof of a model is only worth as much as the model's fidelity to the code. Two mechanisms close that gap, both enforced in CI (`.github/workflows/formal.yml`) and reproducible locally: - **Conformance oracle** (`formal/gateway-verify.js`, `formal/gateway-domain.js`): runs the REAL `decide()` exported by `engine/tool-gateway.js` over the entire finite input domain (2,592 concrete requests) and checks every concrete output against the checks listed below, each mapped to the catalog property it covers. A single violation blocks the deploy. - **Refinement gate** (P9 against the running code): fingerprints the policy's full decision vector and compares a proposed change to the certified baseline (`formal/gateway-baseline.{json,vector}`). A change that only TIGHTENS (removes authority) passes; a change that LOOSENS (grants authority the baseline withheld) is refused unless a human acknowledges it for that exact fingerprint. Green/red proven in `formal/gateway-domain.test.js`: an allow-everything policy trips the oracle, and an invariant-clean loosening the oracle alone would miss is caught by the diff. - **Runtime attestation**: `engine/trust-center.js` recomputes the live fingerprint on the deployed code and surfaces `certified_policy` + a "Running gateway policy is the certified one" check on the Trust Center, so the live system asserts it is the proven one. ### What the conformance oracle checks The oracle names its checks itself, in `checkInvariants()` of `formal/gateway-domain.js`. Each one maps to the catalog as follows. | Oracle check | Holds on every output of `decide()` | Catalog property | | --- | --- | --- | | `P7_total` | the decision is `allow`, `require_approval` or `deny` | P7 | | `P2_revoked_never_allow` | a `REVOKED` or `WASHED_OUT` agent is denied | P2 | | `P3_cross_tenant_never_allow` | an agent whose recorded tenant differs from the request's is denied | P3 | | `P4_fail_closed_no_contract` | with no scope contract, every action class except `read` is denied | P4 | | `P5_denylist_wins` | an intent on the denied list is denied | P1, the denied-list guard | | `P6_dangerous_default_deny` | an `irreversible` or `unclassified` action is denied | P1, the dangerous-class guard | | `P1b_consequential_needs_approval` | a `consequential` or `controlled_write` action never gets `allow` | P6, the part inside `decide()` | | `P8_budget_exhausted_denies` | a run that has used up its call budget is denied | the budget guard, which the model does not include | | `P1_allow_implies_preconditions` | an `allow` comes only when every guard above passed | P1, without the allowlist and untrusted-content guards | `P5_denylist_wins`, `P6_dangerous_default_deny` and `P8_budget_exhausted_denies` are guards inside `decide()`, not catalog P5, P6 and P8. The allowlist decisions are part of the certified decision vector, so the refinement gate refuses any change that loosens one unless a person acknowledges that exact fingerprint. Catalog P5, the approval half of P6, and P8 are not properties of `decide()`: the untrusted-content verdict and the human approval are applied outside it, and the single-use burn is `redeemCapability` in `engine/capability-store.js`. [`ENVIRONMENT-ASSUMPTIONS.md`](./ENVIRONMENT-ASSUMPTIONS.md) (K2) records what those rest on. ## UCA Mission Contract authority (`UCAMissionAuthority.tla`, added 2026-09-24) Models the Universal Control Architecture mission rules that `engine/uca/mission-amendment.js` and `engine/uca/capability.js` implement. Checked by `formal/run.sh` over 3 capabilities and 2 people (21,248 distinct states, green): - **M1 NoUnapprovedAuthority:** mission scope never exceeds the initial grant plus what a distinct human approved. Automation may narrow; it never widens. - **M2 NoSelfApproval:** the requester of an expansion cannot approve it. - **M3 NoExecAfterRevoke:** a revoked mission executes nothing, whatever tokens exist. - **M4 NoExecOutOfScope:** execution is checked against the LIVE scope, so narrowing kills every token that carried a removed capability. Each property has a red config that injects the one bug it guards against (`uca-mission-red-{auto-expand,self-approve,no-revoke-check,stale-token}.cfg`); all four are caught. Scope is the model, bounded: it proves the rules, not that every caller wires them (the property tests in `tests/uca-*.test.js` and `proving/harness-13` cover the code). ## Not yet modelled (honest scope) Proven and enforced: the **decision kernel** (P1 to P7), the **single-use capability** (P8), the **upgrade-safety gate** (P9), the **conformance** of the running `decide()` to the oracle checks above, and the **refinement gate** on every change. The conformance/refinement layer is exhaustive over a bounded finite domain: model-checking strength, not yet a deductive (TLAPS) proof for the unbounded case. Not yet modelled: the authority-passport epoch lifecycle; break-glass containment propagation; budget accounting over time; and the WORM receipt seal. Those are the next layers. Everything claimed above is machine-checked and reproducible from `formal/run.sh` + `node formal/gateway-verify.js`; nothing here is aspirational. The environment every property above assumes (signing-key custody, the time-stamp authority's clock, the window before a receipt is anchored, the database, the deployed code) is listed in [`ENVIRONMENT-ASSUMPTIONS.md`](./ENVIRONMENT-ASSUMPTIONS.md), with what checks or bounds each assumption.