From 286b3caf2feab9e73a7b8913d2493d144da4990e Mon Sep 17 00:00:00 2001 From: vignesh07 Date: Mon, 26 Jan 2026 19:54:21 -0800 Subject: [PATCH 1/3] docs(security): add formal verification page (draft) --- docs/security/formal-verification.md | 92 ++++++++++++++++++++++++++++ 1 file changed, 92 insertions(+) create mode 100644 docs/security/formal-verification.md diff --git a/docs/security/formal-verification.md b/docs/security/formal-verification.md new file mode 100644 index 000000000..6a12a2e78 --- /dev/null +++ b/docs/security/formal-verification.md @@ -0,0 +1,92 @@ +--- +title: Formal Verification (Security Models) +summary: Machine-checked security models for Clawdbot’s highest-risk paths. +status: draft +--- + +# Formal Verification (Security Models) + +This page tracks Clawdbot’s **formal security models** (TLA+/TLC today; more as needed). + +**Goal (north star):** provide a machine-checked argument that Clawdbot enforces its +intended security policy (authorization, session isolation, tool gating, and +misconfiguration safety), under explicit assumptions. + +**What this is (today):** an executable, attacker-driven **security regression suite**: +- Each claim has a runnable model-check. +- Most claims have a paired **negative model** that produces a counterexample trace for a realistic bug class. + +**What this is not (yet):** a proof that “Clawdbot is secure in all respects” or that the full TypeScript implementation is correct. + +## Where the models live + +Models are maintained in a separate repo: `vignesh07/clawdbot-formal-models`. + +## Reproducing results + +From the models repo: + +```bash +export PATH="/opt/homebrew/opt/openjdk@21/bin:$PATH" # or any Java 11+ +make +``` + +### Gateway exposure / open gateway misconfig + +**Claim:** binding beyond loopback without auth makes remote compromise reachable; token/password blocks unauth attackers. + +- Green runs: + - `make gateway-exposure-v2` + - `make gateway-exposure-v2-protected` +- Red (expected): + - `make gateway-exposure-v2-negative` + +See also: `docs/gateway-exposure-matrix.md` in the models repo. + +### Nodes.run pipeline (highest-risk capability) + +**Claim:** `nodes.run` requires (a) node command allowlist + declared commands and (b) live approval when configured; approvals are tokenized to prevent replay. + +- Green runs: + - `make nodes-pipeline` + - `make approvals-token` +- Red (expected): + - `make nodes-pipeline-negative` + - `make approvals-token-negative` + +### Pairing store (DM gating) + +**Claim:** pairing requests respect TTL and pending-request caps. + +- Green runs: + - `make pairing` + - `make pairing-cap` +- Red (expected): + - `make pairing-negative` + - `make pairing-cap-negative` + +### Ingress gating (mentions + control-command bypass) + +**Claim:** in group contexts requiring mention, an unauthorized “control command” cannot bypass mention gating. + +- Green: + - `make ingress-gating` +- Red (expected): + - `make ingress-gating-negative` + +### Routing/session-key isolation + +**Claim:** DMs from distinct peers do not collapse into the same session unless explicitly linked/configured. + +- Green: + - `make routing-isolation` +- Red (expected): + - `make routing-isolation-negative` + +## Roadmap + +Next models to deepen fidelity: +- Pairing store concurrency/locking/idempotency +- Provider-specific ingress preflight modeling +- Routing identity-links + dmScope variants + binding precedence +- Gateway auth conformance (proxy/tailscale specifics) From e03e2ba11aeb88c6a3b84b3cfa42a000ce99a2e9 Mon Sep 17 00:00:00 2001 From: vignesh07 Date: Mon, 26 Jan 2026 19:58:40 -0800 Subject: [PATCH 2/3] docs(security): clarify formal models caveats and reproduction --- docs/security/formal-verification.md | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/docs/security/formal-verification.md b/docs/security/formal-verification.md index 6a12a2e78..b88c17eba 100644 --- a/docs/security/formal-verification.md +++ b/docs/security/formal-verification.md @@ -13,8 +13,8 @@ intended security policy (authorization, session isolation, tool gating, and misconfiguration safety), under explicit assumptions. **What this is (today):** an executable, attacker-driven **security regression suite**: -- Each claim has a runnable model-check. -- Most claims have a paired **negative model** that produces a counterexample trace for a realistic bug class. +- Each claim has a runnable model-check over a finite state space. +- Many claims have a paired **negative model** that produces a counterexample trace for a realistic bug class. **What this is not (yet):** a proof that “Clawdbot is secure in all respects” or that the full TypeScript implementation is correct. @@ -22,8 +22,18 @@ misconfiguration safety), under explicit assumptions. Models are maintained in a separate repo: `vignesh07/clawdbot-formal-models`. +## Important caveats + +- These are **models**, not the full TypeScript implementation. Drift between model and code is possible. +- Results are bounded by the state space explored by TLC; “green” does not imply security beyond the modeled assumptions and bounds. +- Some claims rely on explicit environmental assumptions (e.g., correct deployment, correct configuration inputs). + ## Reproducing results +Today, results are reproduced by cloning the models repo locally and running TLC (see below). A future iteration could offer: +- CI-run models with public artifacts (counterexample traces, run logs) +- a hosted “run this model” workflow for small, bounded checks + From the models repo: ```bash @@ -31,9 +41,9 @@ export PATH="/opt/homebrew/opt/openjdk@21/bin:$PATH" # or any Java 11+ make ``` -### Gateway exposure / open gateway misconfig +### Gateway exposure and open gateway misconfiguration -**Claim:** binding beyond loopback without auth makes remote compromise reachable; token/password blocks unauth attackers. +**Claim:** binding beyond loopback without auth makes remote compromise reachable; token/password blocks unauth attackers (per the model assumptions). - Green runs: - `make gateway-exposure-v2` @@ -45,7 +55,7 @@ See also: `docs/gateway-exposure-matrix.md` in the models repo. ### Nodes.run pipeline (highest-risk capability) -**Claim:** `nodes.run` requires (a) node command allowlist + declared commands and (b) live approval when configured; approvals are tokenized to prevent replay. +**Claim:** `nodes.run` requires (a) node command allowlist plus declared commands and (b) live approval when configured; approvals are tokenized to prevent replay (in the model). - Green runs: - `make nodes-pipeline` From e487fe2fc411548a4c211b6713477546c45bda51 Mon Sep 17 00:00:00 2001 From: vignesh07 Date: Mon, 26 Jan 2026 20:16:33 -0800 Subject: [PATCH 3/3] docs(security): improve formal verification page reproducibility --- docs/security/formal-verification.md | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/docs/security/formal-verification.md b/docs/security/formal-verification.md index b88c17eba..e2704e7b3 100644 --- a/docs/security/formal-verification.md +++ b/docs/security/formal-verification.md @@ -20,7 +20,7 @@ misconfiguration safety), under explicit assumptions. ## Where the models live -Models are maintained in a separate repo: `vignesh07/clawdbot-formal-models`. +Models are maintained in a separate repo: . ## Important caveats @@ -34,16 +34,21 @@ Today, results are reproduced by cloning the models repo locally and running TLC - CI-run models with public artifacts (counterexample traces, run logs) - a hosted “run this model” workflow for small, bounded checks -From the models repo: +Getting started: ```bash -export PATH="/opt/homebrew/opt/openjdk@21/bin:$PATH" # or any Java 11+ +git clone https://github.com/vignesh07/clawdbot-formal-models +cd clawdbot-formal-models + +# Java 11+ required (TLC runs on the JVM). +# The repo vendors a pinned `tla2tools.jar` (TLA+ tools) and provides `bin/tlc` + Make targets. + make ``` ### Gateway exposure and open gateway misconfiguration -**Claim:** binding beyond loopback without auth makes remote compromise reachable; token/password blocks unauth attackers (per the model assumptions). +**Claim:** binding beyond loopback without auth can make remote compromise possible / increases exposure; token/password blocks unauth attackers (per the model assumptions). - Green runs: - `make gateway-exposure-v2`