Merge branch 'main' into claude/simplify-remediation-steps-AA2ao

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)

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? {

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

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: <https://github.com/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
+
+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 <target>
+```
+
+### 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)

docs/security/formal-verification.md

@@ -0,0 +1,5 @@
+---
+permalink: /security/formal-verification/
+---
+
+This page moved to: [/gateway/security/formal-verification/](/gateway/security/formal-verification/)