Security
形式驗證（安全模型）
OpenClaw 的正式安全模型（目前為 TLA+/TLC）提供經機器檢查的論證，證明在明確陳述的假設下，特定最高風險路徑——授權、工作階段隔離、工具閘控與錯誤設定安全性——會執行其預期政策。
注意：部分較舊的連結可能會使用先前的專案名稱。
這是什麼
一套可執行、由攻擊者驅動的安全性迴歸測試套件：
- 每項聲明都有可在有限狀態空間中執行的模型檢查。
- 許多聲明都搭配負向模型，可針對實際的錯誤類別產生反例追蹤。
這並非證明 OpenClaw 在所有方面皆安全，也不會驗證完整的 TypeScript 實作。
模型的位置
模型維護於獨立的儲存庫：vignesh07/openclaw-formal-models。
注意事項
- 這些是模型，而非完整的 TypeScript 實作——模型與程式碼之間可能存在偏差。
- 結果受限於 TLC 探索的狀態空間。綠色結果不代表超出模型假設與界限後仍然安全。
- 部分聲明依賴明確的環境假設（例如正確部署與正確的設定輸入）。
重現結果
複製模型儲存庫並執行 TLC：
git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # 需要 Java 11+（TLC 在 JVM 上執行）。# 此儲存庫內含固定版本的 tla2tools.jar，並提供 bin/tlc 與 Make 目標。 make <target>目前尚未整合回此儲存庫的 CI；未來版本可加入由 CI 執行並提供公開成品（反例追蹤、執行記錄）的模型，或為小型有限範圍檢查提供託管的「執行此模型」工作流程。
聲明與目標
閘道暴露與開放閘道的錯誤設定
**聲明：**根據模型的假設，在沒有驗證的情況下繫結至回送介面以外的位址，可能導致遠端入侵並增加暴露範圍；權杖／密碼可阻擋未經驗證的攻擊者。
| 結果 | 目標 |
|---|---|
| 綠色 | make gateway-exposure-v2, make gateway-exposure-v2-protected |
| 紅色（預期） | make gateway-exposure-v2-negative |
另請參閱模型儲存庫中的 docs/gateway-exposure-matrix.md。
節點執行流水線（最高風險能力）
**聲明：**在模型中，exec host=node 需要 (a) 節點命令允許清單與宣告的命令，以及 (b) 設定後的即時核准；核准會權杖化以防止重播。
| 結果 | 目標 |
|---|---|
| 綠色 | 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 |
傳入閘控（提及與控制命令略過）
**聲明：**在需要提及的群組情境中，未經授權的控制命令無法略過提及閘控。
| 結果 | 目標 |
|---|---|
| 綠色 | make ingress-gating |
| 紅色（預期） | make ingress-gating-negative |
路由與工作階段金鑰隔離
**聲明：**除非明確連結或設定，來自不同對等端的私訊不會合併至同一個工作階段。
| 結果 | 目標 |
|---|---|
| 綠色 | make routing-isolation |
| 紅色（預期） | make routing-isolation-negative |
v1++ 模型：並行、重試與追蹤正確性
後續模型進一步強化對實際故障模式的擬真度：非不可分割更新、重試與訊息扇出。
配對儲存區的並行與冪等性
**聲明：**即使操作交錯執行，配對儲存區仍會強制執行 MaxPending 與冪等性——檢查後寫入必須是不可分割或已鎖定的操作，重新整理不得建立重複項目。具體而言：並行要求不得超過頻道的 MaxPending，且對相同 (channel, sender) 的重複要求／重新整理不得建立重複的有效待處理資料列。
| 結果 | 目標 |
|---|---|
| 綠色 | make pairing-race（不可分割／已鎖定的上限檢查）、make pairing-idempotency、make pairing-refresh、make pairing-refresh-race |
| 紅色（預期） | make pairing-race-negative（非不可分割的開始／提交上限競爭）、make pairing-idempotency-negative、make pairing-refresh-negative、make pairing-refresh-race-negative |
傳入追蹤關聯與冪等性
**聲明：**擷取程序會在扇出期間保留追蹤關聯性，並在提供者重試時維持冪等性。當一個外部事件轉換成多則內部訊息時，每個部分都會保留相同的追蹤／事件識別資訊；重試不會導致重複處理；若缺少提供者事件 ID，重複資料刪除會改用安全的金鑰（例如追蹤 ID），以避免捨棄不同的事件。
| 結果 | 目標 |
|---|---|
| 綠色 | 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 |
路由 dmScope 優先順序與 identityLinks
聲明：dmScope 的優先順序與身分連結會以確定性方式運作：預設的 main 範圍會在單一擁有者的私訊之間共用一個滾動工作階段（個人代理程式的預設值），而任何已設定的隔離範圍（per-peer、per-channel-peer、per-account-channel-peer）都會嚴格分隔私訊工作階段。頻道專屬的 dmScope 覆寫優先於全域預設值；identityLinks 僅會在明確連結的群組內合併工作階段，不會合併不相關對等端的工作階段。多使用者收件匣應選用隔離範圍（執行階段安全性稽核偵測到多使用者私訊流量時會建議這樣做）。
| 結果 | 目標 |
|---|---|
| 綠色 | make routing-precedence, make routing-identitylinks |
| 紅色（預期） | make routing-precedence-negative, make routing-identitylinks-negative |
