From 286b3caf2feab9e73a7b8913d2493d144da4990e Mon Sep 17 00:00:00 2001 From: vignesh07 Date: Mon, 26 Jan 2026 19:54:21 -0800 Subject: [PATCH 1/5] 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/5] 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/5] 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` From 1b219cc5cb234cc5936b54068cacb6d7009daabb Mon Sep 17 00:00:00 2001 From: Peter Steinberger Date: Tue, 27 Jan 2026 04:17:27 +0000 Subject: [PATCH 4/5] fix(macos): gate project-local node_modules bins to DEBUG --- CHANGELOG.md | 1 + apps/macos/Sources/Clawdbot/CommandResolver.swift | 7 +++++++ 2 files changed, 8 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index abfd5fc34..a974f0f57 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,7 @@ Docs: https://docs.clawd.bot Status: unreleased. ### Changes +- macOS: limit project-local `node_modules/.bin` PATH preference to debug builds (reduce PATH hijacking risk). - Agents: summarize dropped messages during compaction safeguard pruning. (#2509) Thanks @jogi47. - Skills: add multi-image input support to Nano Banana Pro skill. (#1958) Thanks @tyler6204. - Agents: honor tools.exec.safeBins in exec allowlist checks. (#2281) diff --git a/apps/macos/Sources/Clawdbot/CommandResolver.swift b/apps/macos/Sources/Clawdbot/CommandResolver.swift index f83638b10..ba5f96d75 100644 --- a/apps/macos/Sources/Clawdbot/CommandResolver.swift +++ b/apps/macos/Sources/Clawdbot/CommandResolver.swift @@ -83,7 +83,10 @@ enum CommandResolver { "/usr/bin", "/bin", ] + #if DEBUG + // Dev-only convenience. Avoid project-local PATH hijacking in release builds. extras.insert(projectRoot.appendingPathComponent("node_modules/.bin").path, at: 0) + #endif let clawdbotPaths = self.clawdbotManagedPaths(home: home) if !clawdbotPaths.isEmpty { extras.insert(contentsOf: clawdbotPaths, at: 1) @@ -189,9 +192,13 @@ enum CommandResolver { } static func projectClawdbotExecutable(projectRoot: URL? = nil) -> String? { + #if DEBUG let root = projectRoot ?? self.projectRoot() let candidate = root.appendingPathComponent("node_modules/.bin").appendingPathComponent(self.helperName).path return FileManager().isExecutableFile(atPath: candidate) ? candidate : nil + #else + return nil + #endif } static func nodeCliPath() -> String? { From 39260e7055bf6b934d4cc9b241643bc836fca135 Mon Sep 17 00:00:00 2001 From: vignesh07 Date: Mon, 26 Jan 2026 20:32:12 -0800 Subject: [PATCH 5/5] docs(security): publish formal verification page under gateway/security --- docs/gateway/security.md | 2 + docs/gateway/security/formal-verification.md | 107 +++++++++++++++++++ docs/security/formal-verification.md | 106 +----------------- 3 files changed, 111 insertions(+), 104 deletions(-) create mode 100644 docs/gateway/security/formal-verification.md diff --git a/docs/gateway/security.md b/docs/gateway/security.md index ca532aae0..db2e732c8 100644 --- a/docs/gateway/security.md +++ b/docs/gateway/security.md @@ -7,6 +7,8 @@ read_when: ## Quick check: `clawdbot security audit` +See also: [Formal Verification (Security Models)](/gateway/security/formal-verification/) + Run this regularly (especially after changing config or exposing network surfaces): ```bash diff --git a/docs/gateway/security/formal-verification.md b/docs/gateway/security/formal-verification.md new file mode 100644 index 000000000..de4d080fe --- /dev/null +++ b/docs/gateway/security/formal-verification.md @@ -0,0 +1,107 @@ +--- +title: Formal Verification (Security Models) +summary: Machine-checked security models for Clawdbot’s highest-risk paths. +permalink: /gateway/security/formal-verification/ +--- + +# 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 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. + +## Where the models live + +Models are maintained in a separate repo: . + +## 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 + +Getting started: + +```bash +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 can make remote compromise possible / increases exposure; token/password blocks unauth attackers (per the model assumptions). + +- 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 plus declared commands and (b) live approval when configured; approvals are tokenized to prevent replay (in the model). + +- 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) diff --git a/docs/security/formal-verification.md b/docs/security/formal-verification.md index e2704e7b3..8e8b98366 100644 --- a/docs/security/formal-verification.md +++ b/docs/security/formal-verification.md @@ -1,107 +1,5 @@ --- -title: Formal Verification (Security Models) -summary: Machine-checked security models for Clawdbot’s highest-risk paths. -status: draft +permalink: /security/formal-verification/ --- -# 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 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. - -## Where the models live - -Models are maintained in a separate repo: . - -## 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 - -Getting started: - -```bash -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 can make remote compromise possible / increases exposure; token/password blocks unauth attackers (per the model assumptions). - -- 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 plus declared commands and (b) live approval when configured; approvals are tokenized to prevent replay (in the model). - -- 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) +This page moved to: [/gateway/security/formal-verification/](/gateway/security/formal-verification/)