mirror of
https://github.com/moltbot/moltbot.git
synced 2026-04-29 09:41:08 +00:00
docs: canonicalize docs paths and align zh navigation (#11428)
* docs(navigation): canonicalize paths and align zh nav * chore(docs): remove stray .DS_Store * docs(scripts): add non-mint docs link audit * docs(nav): fix zh source paths and preserve legacy redirects (#11428) (thanks @sebslight) * chore(docs): satisfy lint for docs link audit script (#11428) (thanks @sebslight)
This commit is contained in:
@@ -289,7 +289,7 @@ process env is missing the key (same non-overriding rule):
|
||||
}
|
||||
```
|
||||
|
||||
See [/environment](/environment) for full precedence and sources.
|
||||
See [/environment](/help/environment) for full precedence and sources.
|
||||
|
||||
### `env.shellEnv` (optional)
|
||||
|
||||
@@ -788,7 +788,7 @@ levels in one gateway:
|
||||
- **Read-only** tools + workspace
|
||||
- **No filesystem access** (messaging/session tools only)
|
||||
|
||||
See [Multi-Agent Sandbox & Tools](/multi-agent-sandbox-tools) for precedence and
|
||||
See [Multi-Agent Sandbox & Tools](/tools/multi-agent-sandbox-tools) for precedence and
|
||||
additional examples.
|
||||
|
||||
Full access (no sandbox):
|
||||
@@ -2857,7 +2857,7 @@ Example:
|
||||
Controls plugin discovery, allow/deny, and per-plugin config. Plugins are loaded
|
||||
from `~/.openclaw/extensions`, `<workspace>/.openclaw/extensions`, plus any
|
||||
`plugins.load.paths` entries. **Config changes require a gateway restart.**
|
||||
See [/plugin](/plugin) for full usage.
|
||||
See [/plugin](/tools/plugin) for full usage.
|
||||
|
||||
Fields:
|
||||
|
||||
|
||||
@@ -200,7 +200,7 @@ Use `accountId` to target a specific account on multi-account channels like Tele
|
||||
- `session`: optional session key for heartbeat runs.
|
||||
- `main` (default): agent main session.
|
||||
- Explicit session key (copy from `openclaw sessions --json` or the [sessions CLI](/cli/sessions)).
|
||||
- Session key formats: see [Sessions](/concepts/session) and [Groups](/concepts/groups).
|
||||
- Session key formats: see [Sessions](/concepts/session) and [Groups](/channels/groups).
|
||||
- `target`:
|
||||
- `last` (default): deliver to the last used external channel.
|
||||
- explicit channel: `whatsapp` / `telegram` / `discord` / `googlechat` / `slack` / `msteams` / `signal` / `imessage`.
|
||||
|
||||
@@ -168,7 +168,7 @@ Debugging:
|
||||
|
||||
Each agent can override sandbox + tools:
|
||||
`agents.list[].sandbox` and `agents.list[].tools` (plus `agents.list[].tools.sandbox.tools` for sandbox tool policy).
|
||||
See [Multi-Agent Sandbox & Tools](/multi-agent-sandbox-tools) for precedence.
|
||||
See [Multi-Agent Sandbox & Tools](/tools/multi-agent-sandbox-tools) for precedence.
|
||||
|
||||
## Minimal enable example
|
||||
|
||||
@@ -189,5 +189,5 @@ See [Multi-Agent Sandbox & Tools](/multi-agent-sandbox-tools) for precedence.
|
||||
## Related docs
|
||||
|
||||
- [Sandbox Configuration](/gateway/configuration#agentsdefaults-sandbox)
|
||||
- [Multi-Agent Sandbox & Tools](/multi-agent-sandbox-tools)
|
||||
- [Multi-Agent Sandbox & Tools](/tools/multi-agent-sandbox-tools)
|
||||
- [Security](/gateway/security)
|
||||
|
||||
@@ -1,164 +0,0 @@
|
||||
---
|
||||
title: Formal Verification (Security Models)
|
||||
summary: Machine-checked security models for OpenClaw’s highest-risk paths.
|
||||
permalink: /security/formal-verification/
|
||||
---
|
||||
|
||||
# Formal Verification (Security Models)
|
||||
|
||||
This page tracks OpenClaw’s **formal security models** (TLA+/TLC today; more as needed).
|
||||
|
||||
> Note: some older links may refer to the previous project name.
|
||||
|
||||
**Goal (north star):** provide a machine-checked argument that OpenClaw 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 “OpenClaw 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](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`
|
||||
|
||||
## v1++: additional bounded models (concurrency, retries, trace correctness)
|
||||
|
||||
These are follow-on models that tighten fidelity around real-world failure modes (non-atomic updates, retries, and message fan-out).
|
||||
|
||||
### Pairing store concurrency / idempotency
|
||||
|
||||
**Claim:** a pairing store should enforce `MaxPending` and idempotency even under interleavings (i.e., “check-then-write” must be atomic / locked; refresh shouldn’t create duplicates).
|
||||
|
||||
What it means:
|
||||
|
||||
- Under concurrent requests, you can’t exceed `MaxPending` for a channel.
|
||||
- Repeated requests/refreshes for the same `(channel, sender)` should not create duplicate live pending rows.
|
||||
|
||||
- Green runs:
|
||||
- `make pairing-race` (atomic/locked cap check)
|
||||
- `make pairing-idempotency`
|
||||
- `make pairing-refresh`
|
||||
- `make pairing-refresh-race`
|
||||
- Red (expected):
|
||||
- `make pairing-race-negative` (non-atomic begin/commit cap race)
|
||||
- `make pairing-idempotency-negative`
|
||||
- `make pairing-refresh-negative`
|
||||
- `make pairing-refresh-race-negative`
|
||||
|
||||
### Ingress trace correlation / idempotency
|
||||
|
||||
**Claim:** ingestion should preserve trace correlation across fan-out and be idempotent under provider retries.
|
||||
|
||||
What it means:
|
||||
|
||||
- When one external event becomes multiple internal messages, every part keeps the same trace/event identity.
|
||||
- Retries do not result in double-processing.
|
||||
- If provider event IDs are missing, dedupe falls back to a safe key (e.g., trace ID) to avoid dropping distinct events.
|
||||
|
||||
- Green:
|
||||
- `make ingress-trace`
|
||||
- `make ingress-trace2`
|
||||
- `make ingress-idempotency`
|
||||
- `make ingress-dedupe-fallback`
|
||||
- Red (expected):
|
||||
- `make ingress-trace-negative`
|
||||
- `make ingress-trace2-negative`
|
||||
- `make ingress-idempotency-negative`
|
||||
- `make ingress-dedupe-fallback-negative`
|
||||
|
||||
### Routing dmScope precedence + identityLinks
|
||||
|
||||
**Claim:** routing must keep DM sessions isolated by default, and only collapse sessions when explicitly configured (channel precedence + identity links).
|
||||
|
||||
What it means:
|
||||
|
||||
- Channel-specific dmScope overrides must win over global defaults.
|
||||
- identityLinks should collapse only within explicit linked groups, not across unrelated peers.
|
||||
|
||||
- Green:
|
||||
- `make routing-precedence`
|
||||
- `make routing-identitylinks`
|
||||
- Red (expected):
|
||||
- `make routing-precedence-negative`
|
||||
- `make routing-identitylinks-negative`
|
||||
@@ -175,7 +175,7 @@ Plugins run **in-process** with the Gateway. Treat them as trusted code:
|
||||
- OpenClaw 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)
|
||||
Details: [Plugins](/tools/plugin)
|
||||
|
||||
## DM access model (pairing / allowlist / open / disabled)
|
||||
|
||||
@@ -193,7 +193,7 @@ openclaw pairing list <channel>
|
||||
openclaw pairing approve <channel> <code>
|
||||
```
|
||||
|
||||
Details + files on disk: [Pairing](/start/pairing)
|
||||
Details + files on disk: [Pairing](/channels/pairing)
|
||||
|
||||
## DM session isolation (multi-user mode)
|
||||
|
||||
@@ -229,7 +229,7 @@ OpenClaw has two separate “who can trigger me?” layers:
|
||||
- `channels.discord.guilds` / `channels.slack.channels`: per-surface allowlists + mention defaults.
|
||||
- **Security note:** treat `dmPolicy="open"` and `groupPolicy="open"` as last-resort settings. They should be barely used; prefer pairing + allowlists unless you fully trust every member of the room.
|
||||
|
||||
Details: [Configuration](/gateway/configuration) and [Groups](/concepts/groups)
|
||||
Details: [Configuration](/gateway/configuration) and [Groups](/channels/groups)
|
||||
|
||||
## Prompt injection (what it is, why it matters)
|
||||
|
||||
@@ -627,7 +627,7 @@ access those accounts and data. Treat browser profiles as **sensitive state**:
|
||||
|
||||
With multi-agent routing, each agent can have its own sandbox + tool policy:
|
||||
use this to give **full access**, **read-only**, or **no access** per agent.
|
||||
See [Multi-Agent Sandbox & Tools](/multi-agent-sandbox-tools) for full details
|
||||
See [Multi-Agent Sandbox & Tools](/tools/multi-agent-sandbox-tools) for full details
|
||||
and precedence rules.
|
||||
|
||||
Common use cases:
|
||||
|
||||
@@ -56,8 +56,8 @@ Common signatures:
|
||||
Related:
|
||||
|
||||
- [/channels/troubleshooting](/channels/troubleshooting)
|
||||
- [/start/pairing](/start/pairing)
|
||||
- [/concepts/groups](/concepts/groups)
|
||||
- [/channels/pairing](/channels/pairing)
|
||||
- [/channels/groups](/channels/groups)
|
||||
|
||||
## Dashboard control ui connectivity
|
||||
|
||||
|
||||
Reference in New Issue
Block a user