形式验证（安全模型）

This page tracks OpenClaw's **formal security models** (TLA+/TLC today; more as needed).

目标（北極星）： OpenClaw 但明示的那仮定的下在、意図已执行

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.

模型是別的仓库在維持已被：''vignesh07/openclaw-formal-models''。

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

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

开始执行在是：

git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models

make '<target>'

**Claim:** binding beyond loopback without auth can make remote compromise possible / increases exposure; token/password blocks unauth attackers (per the model assumptions).

- 緑的运行：

- ''make gateway-exposure-v2''

- ''make gateway-exposure-v2-protected''

- 赤（予想）：

- ''make gateway-exposure-v2-negative''

参照：模型仓库的 ''docs/gateway-exposure-matrix.md''。

**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).

- 緑的运行：

- ''make nodes-pipeline''

- ''make approvals-token''

- 赤（予想）：

- ''make nodes-pipeline-negative''

- ''make approvals-token-negative''

主張： 配对请求是 TTL 和待定请求的上限尊重执行。

- 緑的运行：

- ''make pairing''

- ''make pairing-cap''

- 赤（予想）：

- ''make pairing-negative''

- ''make pairing-cap-negative''

**Claim:** in group contexts requiring mention, an unauthorized "control command" cannot bypass mention gating.

- 緑：

- ''make ingress-gating''

- 赤（予想）：

- ''make ingress-gating-negative''

**Claim:** DMs from distinct peers do not collapse into the same session unless explicitly linked/configured.

- 緑：

- ''make routing-isolation''

- 赤（予想）：

- ''make routing-isolation-negative''

These are follow-on models that tighten fidelity around real-world failure modes (non-atomic updates, retries, and message fan-out).

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

- 緑的运行：

- ''make pairing-race'' (atomic/locked cap check)

- ''make pairing-idempotency''

- ''make pairing-refresh''

- ''make pairing-refresh-race''

- 赤（予想）：

- ''make pairing-race-negative'' (non-atomic begin/commit cap race)

- ''make pairing-idempotency-negative''

- ''make pairing-refresh-negative''

- ''make pairing-refresh-race-negative''

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

- 緑：

- ''make ingress-trace''

- ''make ingress-trace2''

- ''make ingress-idempotency''

- ''make ingress-dedupe-fallback''

- 赤（予想）：

- ''make ingress-trace-negative''

- ''make ingress-trace2-negative''

- ''make ingress-idempotency-negative''

- ''make ingress-dedupe-fallback-negative''

**Claim:** routing must keep DM sessions isolated by default, and only collapse sessions when explicitly configured (channel precedence + identity links).

What it means:

- 渠道固有的 dmScope 覆盖是全局默认比優先执行必要有。

- identityLinks should collapse only within explicit linked groups, not across unrelated peers.

- 緑：

- ''make routing-precedence''

- ''make routing-identitylinks''

- 赤（予想）：

- ''make routing-precedence-negative''

- ''make routing-identitylinks-negative''