let5see/clawdbot
1
0
Fork 0
Code Issues Pull Requests Actions 4 Packages Projects Releases Wiki Activity

docs(security): clarify formal models caveats and reproduction

Browse Source
This commit is contained in:
vignesh07
2026-01-26 19:58:40 -08:00
parent 286b3caf2f
commit e03e2ba11a
1 changed files with 15 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -13,8 +13,8 @@ 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.
- 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 “Clawdbot is secure in all respects” or that the full TypeScript implementation is correct.
@@ -22,8 +22,18 @@ misconfiguration safety), under explicit assumptions.
Models are maintained in a separate repo: `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
From the models repo:
```bash
@@ -31,9 +41,9 @@ export PATH="/opt/homebrew/opt/openjdk@21/bin:$PATH" # or any Java 11+
make <target>
```
### Gateway exposure / open gateway misconfig
### Gateway exposure and open gateway misconfiguration
**Claim:** binding beyond loopback without auth makes remote compromise reachable; token/password blocks unauth attackers.
**Claim:** binding beyond loopback without auth makes remote compromise reachable; token/password blocks unauth attackers (per the model assumptions).
- Green runs:
- `make gateway-exposure-v2`
@@ -45,7 +55,7 @@ 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.
**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`