93 lines
2.8 KiB
Markdown
93 lines
2.8 KiB
Markdown
---
|
||
title: Formal Verification (Security Models)
|
||
summary: Machine-checked security models for Clawdbot’s highest-risk paths.
|
||
status: draft
|
||
---
|
||
|
||
# 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.
|
||
- Most 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: `vignesh07/clawdbot-formal-models`.
|
||
|
||
## Reproducing results
|
||
|
||
From the models repo:
|
||
|
||
```bash
|
||
export PATH="/opt/homebrew/opt/openjdk@21/bin:$PATH" # or any Java 11+
|
||
make <target>
|
||
```
|
||
|
||
### Gateway exposure / open gateway misconfig
|
||
|
||
**Claim:** binding beyond loopback without auth makes remote compromise reachable; token/password blocks unauth attackers.
|
||
|
||
- 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 + declared commands and (b) live approval when configured; approvals are tokenized to prevent replay.
|
||
|
||
- 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)
|