admin/Moltbot
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

docs: update security + formal verification pages for Moltbot rename

Browse Source
This commit is contained in:
vignesh07
2026-01-27 15:12:26 -08:00
parent 0b1c8db0ca
commit 8198e826da
3 changed files with 38 additions and 144 deletions
Download Patch File Download Diff File Expand all files Collapse all files

107
docs/gateway/security/formal-verification.md
View File

@@ -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 <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)

61
docs/gateway/security/index.md
View File

@@ -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/<agentId>/sessions/*.jsonl`.
Clawdbot stores session transcripts on disk under `~/.clawdbot/agents/<agentId>/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 <npm-spec>`), treat it like running untrusted code:
- If you install plugins from npm (`clawdbot plugins install <npm-spec>`), treat it like running untrusted code:
- The install path is `~/.clawdbot/extensions/<pluginId>/` (or `$CLAWDBOT_STATE_DIR/extensions/<pluginId>/`).
- 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 <channel>
moltbot pairing approve <channel> <code>
clawdbot pairing list <channel>
clawdbot pairing approve <channel> <code>
```
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/<channel>-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/<agentId>/agent/auth-profiles.json`: API keys + OAuth tokens (imported from legacy `credentials/oauth.json`).
- `agents/<agentId>/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/<agentId>/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)

14
docs/security/formal-verification.md
View File

@@ -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.