diff --git a/docs/gateway/security/formal-verification.md b/docs/gateway/security/formal-verification.md deleted file mode 100644 index 3d41aed06..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 Moltbot’s highest-risk paths. -permalink: /gateway/security/formal-verification/ ---- - -# Formal Verification (Security Models) - -This page tracks Moltbot’s **formal security models** (TLA+/TLC today; more as needed). - -**Goal (north star):** provide a machine-checked argument that Moltbot 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 “Moltbot 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/moltbot-formal-models](https://github.com/vignesh07/moltbot-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/moltbot-formal-models -cd moltbot-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/gateway/security/index.md b/docs/gateway/security/index.md index e3c85af7f..87a44f8e6 100644 --- a/docs/gateway/security/index.md +++ b/docs/gateway/security/index.md @@ -5,7 +5,7 @@ read_when: --- # Security 🔒 -## Quick check: `moltbot security audit` +## Quick check: `moltbot security audit` (formerly `clawdbot security audit`) See also: [Formal Verification (Security Models)](/security/formal-verification/) @@ -15,6 +15,8 @@ Run this regularly (especially after changing config or exposing network surface moltbot security audit moltbot security audit --deep moltbot security audit --fix + +# (On older installs, the command is `clawdbot ...`.) ``` It flags common footguns (Gateway auth exposure, browser control exposure, elevated allowlists, filesystem permissions). @@ -26,7 +28,7 @@ It flags common footguns (Gateway auth exposure, browser control exposure, eleva Running an AI agent with shell access on your machine is... *spicy*. Here’s how to not get pwned. -Moltbot is both a product and an experiment: you’re wiring frontier-model behavior into real messaging surfaces and real tools. **There is no “perfectly secure” setup.** The goal is to be deliberate about: +Clawdbot is both a product and an experiment: you’re wiring frontier-model behavior into real messaging surfaces and real tools. **There is no “perfectly secure” setup.** The goal is to be deliberate about: - who can talk to your bot - where the bot is allowed to act - what the bot can touch @@ -43,7 +45,7 @@ Start with the smallest access that still works, then widen it as you gain confi - **Plugins** (extensions exist without an explicit allowlist). - **Model hygiene** (warn when configured models look legacy; not a hard block). -If you run `--deep`, Moltbot also attempts a best-effort live Gateway probe. +If you run `--deep`, Clawdbot also attempts a best-effort live Gateway probe. ## Credential storage map @@ -79,7 +81,7 @@ For break-glass scenarios only, `gateway.controlUi.dangerouslyDisableDeviceAuth` disables device identity checks entirely. This is a severe security downgrade; keep it off unless you are actively debugging and can revert quickly. -`moltbot security audit` warns when this setting is enabled. +`clawdbot security audit` warns when this setting is enabled. ## Reverse Proxy Configuration @@ -100,7 +102,7 @@ When `trustedProxies` is configured, the Gateway will use `X-Forwarded-For` head ## Local session logs live on disk -Moltbot stores session transcripts on disk under `~/.clawdbot/agents//sessions/*.jsonl`. +Clawdbot stores session transcripts on disk under `~/.clawdbot/agents//sessions/*.jsonl`. This is required for session continuity and (optionally) session memory indexing, but it also means **any process/user with filesystem access can read those logs**. Treat disk access as the trust boundary and lock down permissions on `~/.clawdbot` (see the audit section below). If you need @@ -116,7 +118,7 @@ If a macOS node is paired, the Gateway can invoke `system.run` on that node. Thi ## Dynamic skills (watcher / remote nodes) -Moltbot can refresh the skills list mid-session: +Clawdbot can refresh the skills list mid-session: - **Skills watcher**: changes to `SKILL.md` can update the skills snapshot on the next agent turn. - **Remote nodes**: connecting a macOS node can make macOS-only skills eligible (based on bin probing). @@ -139,7 +141,7 @@ People who message you can: Most failures here are not fancy exploits — they’re “someone messaged the bot and the bot did what they asked.” -Moltbot’s stance: +Clawdbot’s stance: - **Identity first:** decide who can talk to the bot (DM pairing / allowlists / explicit “open”). - **Scope next:** decide where the bot is allowed to act (group allowlists + mention gating, tools, sandboxing, device permissions). - **Model last:** assume the model can be manipulated; design so manipulation has limited blast radius. @@ -162,9 +164,9 @@ Plugins run **in-process** with the Gateway. Treat them as trusted code: - Prefer explicit `plugins.allow` allowlists. - Review plugin config before enabling. - Restart the Gateway after plugin changes. -- If you install plugins from npm (`moltbot plugins install `), treat it like running untrusted code: +- If you install plugins from npm (`clawdbot plugins install `), treat it like running untrusted code: - The install path is `~/.clawdbot/extensions//` (or `$CLAWDBOT_STATE_DIR/extensions//`). - - Moltbot uses `npm pack` and then runs `npm install --omit=dev` in that directory (npm lifecycle scripts can execute code during install). + - Clawdbot uses `npm pack` and then runs `npm install --omit=dev` in that directory (npm lifecycle scripts can execute code during install). - Prefer pinned, exact versions (`@scope/pkg@1.2.3`), and inspect the unpacked code on disk before enabling. Details: [Plugins](/plugin) @@ -181,15 +183,15 @@ All current DM-capable channels support a DM policy (`dmPolicy` or `*.dm.policy` Approve via CLI: ```bash -moltbot pairing list -moltbot pairing approve +clawdbot pairing list +clawdbot pairing approve ``` Details + files on disk: [Pairing](/start/pairing) ## DM session isolation (multi-user mode) -By default, Moltbot routes **all DMs into the main session** so your assistant has continuity across devices and channels. If **multiple people** can DM the bot (open DMs or a multi-person allowlist), consider isolating DM sessions: +By default, Clawdbot routes **all DMs into the main session** so your assistant has continuity across devices and channels. If **multiple people** can DM the bot (open DMs or a multi-person allowlist), consider isolating DM sessions: ```json5 { @@ -201,7 +203,7 @@ This prevents cross-user context leakage while keeping group chats isolated. If ## Allowlists (DM + groups) — terminology -Moltbot has two separate “who can trigger me?” layers: +Clawdbot has two separate “who can trigger me?” layers: - **DM allowlist** (`allowFrom` / `channels.discord.dm.allowFrom` / `channels.slack.dm.allowFrom`): who is allowed to talk to the bot in direct messages. - When `dmPolicy="pairing"`, approvals are written to `~/.clawdbot/credentials/-allowFrom.json` (merged with config allowlists). @@ -285,7 +287,7 @@ Assume “compromised” means: someone got into a room that can trigger the bot - Check Gateway logs and recent sessions/transcripts for unexpected tool calls. - Review `extensions/` and remove anything you don’t fully trust. 4. **Re-run audit** - - `moltbot security audit --deep` and confirm the report is clean. + - `clawdbot security audit --deep` and confirm the report is clean. ## Lessons Learned (The Hard Way) @@ -308,10 +310,10 @@ This is social engineering 101. Create distrust, encourage snooping. ### 0) File permissions Keep config + state private on the gateway host: -- `~/.clawdbot/moltbot.json`: `600` (user read/write only) +- `~/.clawdbot/clawdbot.json`: `600` (user read/write only) - `~/.clawdbot`: `700` (user only) -`moltbot doctor` can warn and offer to tighten these permissions. +`clawdbot doctor` can warn and offer to tighten these permissions. ### 0.4) Network exposure (bind + port + firewall) @@ -330,7 +332,7 @@ Rules of thumb: ### 0.4.1) mDNS/Bonjour discovery (information disclosure) -The Gateway broadcasts its presence via mDNS (`_moltbot-gw._tcp` on port 5353) for local device discovery. In full mode, this includes TXT records that may expose operational details: +The Gateway broadcasts its presence via mDNS (`_clawdbot-gw._tcp` on port 5353) for local device discovery. In full mode, this includes TXT records that may expose operational details: - `cliPath`: full filesystem path to the CLI binary (reveals username and install location) - `sshPort`: advertises SSH availability on the host @@ -389,7 +391,7 @@ Set a token so **all** WS clients must authenticate: } ``` -Doctor can generate one for you: `moltbot doctor --generate-gateway-token`. +Doctor can generate one for you: `clawdbot doctor --generate-gateway-token`. Note: `gateway.remote.token` is **only** for remote CLI calls; it does not protect local WS access. @@ -413,9 +415,9 @@ Rotation checklist (token/password): ### 0.6) Tailscale Serve identity headers -When `gateway.auth.allowTailscale` is `true` (default for Serve), Moltbot +When `gateway.auth.allowTailscale` is `true` (default for Serve), Clawdbot accepts Tailscale Serve identity headers (`tailscale-user-login`) as -authentication. Moltbot verifies the identity by resolving the +authentication. Clawdbot verifies the identity by resolving the `x-forwarded-for` address through the local Tailscale daemon (`tailscale whois`) and matching it to the header. This only triggers for requests that hit loopback and include `x-forwarded-for`, `x-forwarded-proto`, and `x-forwarded-host` as @@ -427,7 +429,7 @@ you terminate TLS or proxy in front of the gateway, disable Trusted proxies: - If you terminate TLS in front of the Gateway, set `gateway.trustedProxies` to your proxy IPs. -- Moltbot will trust `x-forwarded-for` (or `x-real-ip`) from those IPs to determine the client IP for local pairing checks and HTTP auth/local checks. +- Clawdbot will trust `x-forwarded-for` (or `x-real-ip`) from those IPs to determine the client IP for local pairing checks and HTTP auth/local checks. - Ensure your proxy **overwrites** `x-forwarded-for` and blocks direct access to the Gateway port. See [Tailscale](/gateway/tailscale) and [Web overview](/web). @@ -450,7 +452,7 @@ Avoid: Assume anything under `~/.clawdbot/` (or `$CLAWDBOT_STATE_DIR/`) may contain secrets or private data: -- `moltbot.json`: config may include tokens (gateway, remote gateway), provider settings, and allowlists. +- `clawdbot.json`: config may include tokens (gateway, remote gateway), provider settings, and allowlists. - `credentials/**`: channel credentials (example: WhatsApp creds), pairing allowlists, legacy OAuth imports. - `agents//agent/auth-profiles.json`: API keys + OAuth tokens (imported from legacy `credentials/oauth.json`). - `agents//sessions/**`: session transcripts (`*.jsonl`) + routing metadata (`sessions.json`) that can contain private messages and tool output. @@ -471,7 +473,7 @@ Logs and transcripts can leak sensitive info even when access controls are corre Recommendations: - Keep tool summary redaction on (`logging.redactSensitive: "tools"`; default). - Add custom patterns for your environment via `logging.redactPatterns` (tokens, hostnames, internal URLs). -- When sharing diagnostics, prefer `moltbot status --all` (pasteable, secrets redacted) over raw logs. +- When sharing diagnostics, prefer `clawdbot status --all` (pasteable, secrets redacted) over raw logs. - Prune old session transcripts and log files if you don’t need long retention. Details: [Logging](/gateway/logging) @@ -572,9 +574,6 @@ If that browser profile already contains logged-in sessions, the model can access those accounts and data. Treat browser profiles as **sensitive state**: - Prefer a dedicated profile for the agent (the default `clawd` profile). - Avoid pointing the agent at your personal daily-driver profile. -- `act:evaluate` and `wait --fn` run arbitrary JavaScript in the page context. - Prompt injection can steer the model into calling them. If you do not need - them, set `browser.evaluateEnabled=false` (see [Configuration](/gateway/configuration#browser-clawd-managed-browser)). - Keep host browser control disabled for sandboxed agents unless you trust them. - Treat browser downloads as untrusted input; prefer an isolated downloads directory. - Disable browser sync/password managers in the agent profile if possible (reduces blast radius). @@ -678,7 +677,7 @@ If your AI does something bad: ### Contain -1. **Stop it:** stop the macOS app (if it supervises the Gateway) or terminate your `moltbot gateway` process. +1. **Stop it:** stop the macOS app (if it supervises the Gateway) or terminate your `clawdbot gateway` process. 2. **Close exposure:** set `gateway.bind: "loopback"` (or disable Tailscale Funnel/Serve) until you understand what happened. 3. **Freeze access:** switch risky DMs/groups to `dmPolicy: "disabled"` / require mentions, and remove `"*"` allow-all entries if you had them. @@ -690,13 +689,13 @@ If your AI does something bad: ### Audit -1. Check Gateway logs: `/tmp/moltbot/moltbot-YYYY-MM-DD.log` (or `logging.file`). +1. Check Gateway logs: `/tmp/clawdbot/clawdbot-YYYY-MM-DD.log` (or `logging.file`). 2. Review the relevant transcript(s): `~/.clawdbot/agents//sessions/*.jsonl`. 3. Review recent config changes (anything that could have widened access: `gateway.bind`, `gateway.auth`, dm/group policies, `tools.elevated`, plugin changes). ### Collect for a report -- Timestamp, gateway host OS + Moltbot version +- Timestamp, gateway host OS + Clawdbot version - The session transcript(s) + a short log tail (after redacting) - What the attacker sent + what the agent did - Whether the Gateway was exposed beyond loopback (LAN/Tailscale Funnel/Serve) @@ -748,9 +747,9 @@ Mario asking for find ~ ## Reporting Security Issues -Found a vulnerability in Moltbot? Please report responsibly: +Found a vulnerability in Clawdbot? Please report responsibly: -1. Email: security@molt.bot +1. Email: security@clawd.bot 2. Don't post publicly until fixed 3. We'll credit you (unless you prefer anonymity) diff --git a/docs/security/formal-verification.md b/docs/security/formal-verification.md index 437fc11a6..08431dc5d 100644 --- a/docs/security/formal-verification.md +++ b/docs/security/formal-verification.md @@ -1,6 +1,6 @@ --- title: Formal Verification (Security Models) -summary: Machine-checked security models for Moltbot’s highest-risk paths. +summary: Machine-checked security models for Moltbot’s highest-risk paths (formerly Clawdbot). permalink: /security/formal-verification/ --- @@ -8,7 +8,9 @@ permalink: /security/formal-verification/ This page tracks Moltbot’s **formal security models** (TLA+/TLC today; more as needed). -**Goal (north star):** provide a machine-checked argument that Moltbot enforces its +> Moltbot was formerly named Clawdbot; some older references and commands may still use `clawdbot`. + +**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. @@ -16,11 +18,11 @@ misconfiguration safety), under explicit assumptions. - 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 “Moltbot is secure in all respects” or that the full TypeScript implementation is correct. +**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/moltbot-formal-models](https://github.com/vignesh07/moltbot-formal-models). +Models are maintained in a separate repo: [vignesh07/clawdbot-formal-models](https://github.com/vignesh07/clawdbot-formal-models). ## Important caveats @@ -37,8 +39,8 @@ Today, results are reproduced by cloning the models repo locally and running TLC Getting started: ```bash -git clone https://github.com/vignesh07/moltbot-formal-models -cd moltbot-formal-models +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.