From 39260e7055bf6b934d4cc9b241643bc836fca135 Mon Sep 17 00:00:00 2001 From: vignesh07 Date: Mon, 26 Jan 2026 20:32:12 -0800 Subject: [PATCH 1/6] 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/) From b3003ed1aa234a8c73ed2bbfe59e4edbe730d1d2 Mon Sep 17 00:00:00 2001 From: vignesh07 Date: Mon, 26 Jan 2026 20:37:23 -0800 Subject: [PATCH 2/6] docs: add formal verification page to Mintlify navigation --- docs/docs.json | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/docs.json b/docs/docs.json index 01a338a18..ec1314a90 100644 --- a/docs/docs.json +++ b/docs/docs.json @@ -956,6 +956,7 @@ "gateway/doctor", "gateway/logging", "gateway/security", + "gateway/security/formal-verification", "gateway/sandbox-vs-tool-policy-vs-elevated", "gateway/sandboxing", "gateway/troubleshooting", From 4c2d8eedb0077eb0d787b5a499a46a23b020b8f3 Mon Sep 17 00:00:00 2001 From: Kenny Lee Date: Mon, 26 Jan 2026 16:33:56 -0800 Subject: [PATCH 3/6] fix(macos): auto-scroll to bottom when sending message while scrolled up When the user sends a message while reading older messages, scroll to bottom so they can see their sent message and the response. Fixes #2470 Co-Authored-By: Claude Opus 4.5 --- .../ClawdbotKit/Sources/ClawdbotChatUI/ChatView.swift | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/apps/shared/ClawdbotKit/Sources/ClawdbotChatUI/ChatView.swift b/apps/shared/ClawdbotKit/Sources/ClawdbotChatUI/ChatView.swift index 44399a3e6..bc8c3493e 100644 --- a/apps/shared/ClawdbotKit/Sources/ClawdbotChatUI/ChatView.swift +++ b/apps/shared/ClawdbotKit/Sources/ClawdbotChatUI/ChatView.swift @@ -132,6 +132,14 @@ public struct ClawdbotChatView: View { self.hasPerformedInitialScroll = false self.isPinnedToBottom = true } + .onChange(of: self.viewModel.isSending) { _, isSending in + // Scroll to bottom when user sends a message, even if scrolled up. + guard isSending, self.hasPerformedInitialScroll else { return } + self.isPinnedToBottom = true + withAnimation(.snappy(duration: 0.22)) { + self.scrollPosition = self.scrollerBottomID + } + } .onChange(of: self.viewModel.messages.count) { _, _ in guard self.hasPerformedInitialScroll, self.isPinnedToBottom else { return } withAnimation(.snappy(duration: 0.22)) { From 913530402dfa0fcf4a565eb91be73313166379c7 Mon Sep 17 00:00:00 2001 From: Gustavo Madeira Santana Date: Mon, 26 Jan 2026 23:41:19 -0500 Subject: [PATCH 4/6] fix: local updates for PR #2471 Co-authored-by: kennyklee --- .../Sources/ClawdbotChatUI/ChatView.swift | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/apps/shared/ClawdbotKit/Sources/ClawdbotChatUI/ChatView.swift b/apps/shared/ClawdbotKit/Sources/ClawdbotChatUI/ChatView.swift index bc8c3493e..99b32779f 100644 --- a/apps/shared/ClawdbotKit/Sources/ClawdbotChatUI/ChatView.swift +++ b/apps/shared/ClawdbotKit/Sources/ClawdbotChatUI/ChatView.swift @@ -13,6 +13,7 @@ public struct ClawdbotChatView: View { @State private var showSessions = false @State private var hasPerformedInitialScroll = false @State private var isPinnedToBottom = true + @State private var lastUserMessageID: UUID? private let showsSessionSwitcher: Bool private let style: Style private let markdownVariant: ChatMarkdownVariant @@ -141,7 +142,19 @@ public struct ClawdbotChatView: View { } } .onChange(of: self.viewModel.messages.count) { _, _ in - guard self.hasPerformedInitialScroll, self.isPinnedToBottom else { return } + guard self.hasPerformedInitialScroll else { return } + if let lastMessage = self.viewModel.messages.last, + lastMessage.role.lowercased() == "user", + lastMessage.id != self.lastUserMessageID { + self.lastUserMessageID = lastMessage.id + self.isPinnedToBottom = true + withAnimation(.snappy(duration: 0.22)) { + self.scrollPosition = self.scrollerBottomID + } + return + } + + guard self.isPinnedToBottom else { return } withAnimation(.snappy(duration: 0.22)) { self.scrollPosition = self.scrollerBottomID } From d2b5037203ea260fe687316c7959b5d1538c9005 Mon Sep 17 00:00:00 2001 From: Gustavo Madeira Santana Date: Mon, 26 Jan 2026 23:45:29 -0500 Subject: [PATCH 5/6] fix: auto-scroll to bottom on user send (#2471) (thanks @kennyklee) --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index a974f0f57..c4073193b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -60,6 +60,7 @@ Status: unreleased. - **BREAKING:** Gateway auth mode "none" is removed; gateway now requires token/password (Tailscale Serve identity still allowed). ### Fixes +- macOS: auto-scroll to bottom when sending a new message while scrolled up. (#2471) Thanks @kennyklee. - Gateway: suppress AbortError and transient network errors in unhandled rejections. (#2451) Thanks @Glucksberg. - TTS: keep /tts status replies on text-only commands and avoid duplicate block-stream audio. (#2451) Thanks @Glucksberg. - Security: pin npm overrides to keep tar@7.5.4 for install toolchains. From f72b881276648c756ee34d2ea8aa74d9bc87ecc0 Mon Sep 17 00:00:00 2001 From: Vignesh Date: Mon, 26 Jan 2026 20:50:11 -0800 Subject: [PATCH 6/6] docs: fix formal verification route (#2583) --- docs/docs.json | 2 +- docs/gateway/security.md | 2 +- docs/gateway/security/formal-verification.md | 107 ------------------- docs/security/formal-verification.md | 104 +++++++++++++++++- 4 files changed, 105 insertions(+), 110 deletions(-) delete mode 100644 docs/gateway/security/formal-verification.md diff --git a/docs/docs.json b/docs/docs.json index ec1314a90..f4f6258a9 100644 --- a/docs/docs.json +++ b/docs/docs.json @@ -956,7 +956,7 @@ "gateway/doctor", "gateway/logging", "gateway/security", - "gateway/security/formal-verification", + "security/formal-verification", "gateway/sandbox-vs-tool-policy-vs-elevated", "gateway/sandboxing", "gateway/troubleshooting", diff --git a/docs/gateway/security.md b/docs/gateway/security.md index db2e732c8..f83ea3eb6 100644 --- a/docs/gateway/security.md +++ b/docs/gateway/security.md @@ -7,7 +7,7 @@ read_when: ## Quick check: `clawdbot security audit` -See also: [Formal Verification (Security Models)](/gateway/security/formal-verification/) +See also: [Formal Verification (Security Models)](/security/formal-verification/) Run this regularly (especially after changing config or exposing network surfaces): diff --git a/docs/gateway/security/formal-verification.md b/docs/gateway/security/formal-verification.md deleted file mode 100644 index de4d080fe..000000000 --- a/docs/gateway/security/formal-verification.md +++ /dev/null @@ -1,107 +0,0 @@ ---- -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 8e8b98366..6028b8291 100644 --- a/docs/security/formal-verification.md +++ b/docs/security/formal-verification.md @@ -1,5 +1,107 @@ --- +title: Formal Verification (Security Models) +summary: Machine-checked security models for Clawdbot’s highest-risk paths. permalink: /security/formal-verification/ --- -This page moved to: [/gateway/security/formal-verification/](/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)