OpenClaw 安全模型驗證：執行形式化驗證與安全性檢查

寫程式最怕的就是安全性漏洞，尤其是那些在複雜併發（Concurrency）情況下才會出現的邊緣案例。你可能寫了一堆測試，但總覺得心裡不踏實，擔心某個邏輯漏洞會讓攻擊者繞過你的 Gateway。

這就是為什麼我們引入了形式化驗證。這份文件記錄了 OpenClaw 的 形式化安全性模型（Formal Security Models）（目前使用 TLA+/TLC，未來會根據需要增加）。我們的終極目標是提供一個經由機器檢查的論據，證明 OpenClaw 在明確的假設下，確實執行了預期的安全性政策，包括授權、Session 隔離、Tool Gating 以及誤配置的安全性。

目前的現狀是，這是一個可執行的、由攻擊者驅動的 安全性回歸測試套件：

每個主張（Claim）都有一個在有限狀態空間內運行的模型檢查。
許多主張都配對了一個 負面模型（Negative Model），可以針對現實中的 Bug 類別產生反例追蹤（Counterexample Trace）。

不過要先說明，這並不是證明「OpenClaw 在所有方面都絕對安全」，也不是證明完整的 TypeScript 實作完全正確。

模型存放位置

模型維護在獨立的 Repo 中：vignesh07/openclaw-formal-models。

重要注意事項

這些是模型，而不是完整的 TypeScript 實作。模型與實際程式碼之間可能存在差異。
結果受限於 TLC 探索的狀態空間；「Green（通過）」並不代表在模型假設和邊界之外也是安全的。
某些主張依賴於明確的環境假設（例如正確的部署、正確的配置輸入）。

重現結果

目前你可以透過在本地複製模型 Repo 並執行 TLC 來重現結果。未來的版本可能會提供 CI 自動執行模型並發佈公開產物（如反例追蹤、執行日誌），或是提供一個託管的「執行此模型」工作流。

開始步驟：

git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-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 暴露與開放 Gateway 誤配置

主張： 在沒有 Auth 的情況下將綁定超出 Loopback 可能導致遠端入侵；根據模型假設，Token 或密碼可以阻擋未經授權的攻擊者。

Green runs:
- make gateway-exposure-v2
- make gateway-exposure-v2-protected
Red (expected):
- make gateway-exposure-v2-negative

另請參閱模型 Repo 中的 docs/gateway-exposure-matrix.md。

Node 執行管線（最高風險能力）

主張： exec host=node 需要 (a) Node 命令白名單及宣告的命令，以及 (b) 配置時的即時核准；核准過程經過 Token 化以防止重放攻擊（在模型中）。

Green runs:
- make nodes-pipeline
- make approvals-token
Red (expected):
- make nodes-pipeline-negative
- make approvals-token-negative

配對儲存（DM Gating）

主張： 配對請求遵循 TTL 和待處理請求上限（Pending-request caps）。

Green runs:
- make pairing
- make pairing-cap
Red (expected):
- make pairing-negative
- make pairing-cap-negative

Ingress Gating（提及 + 控制命令繞過）

主張： 在需要提及（Mention）的群組情境中，未經授權的「控制命令」無法繞過提及限制。

Green:
- make ingress-gating
Red (expected):
- make ingress-gating-negative

路由/Session 金鑰隔離

主張： 來自不同 Peer 的 DM 不會塌陷（Collapse）到同一個 Session 中，除非有明確的連結或配置。

Green:
- make routing-isolation
Red (expected):
- make routing-isolation-negative

v1++：額外的有界模型（併發、重試、追蹤正確性）

這些是後續模型，旨在加強對現實世界失敗模式（非原子更新、重試和訊息扇出）的擬真度。

配對儲存併發 / 冪等性

主張： 配對儲存即使在交錯執行（Interleavings）的情況下，也應執行 MaxPending 和冪等性（即「先檢查後寫入」必須是原子操作或加鎖；重新整理不應產生重複項）。

具體含義：

在併發請求下，你不能超過該頻道的 MaxPending 上限。
針對同一個 (channel, sender) 的重複請求或重新整理，不應產生重複的待處理資料列。
Green runs:
- make pairing-race（原子/加鎖的上限檢查）
- make pairing-idempotency
- make pairing-refresh
- make pairing-refresh-race
Red (expected):
- make pairing-race-negative（非原子的開始/提交上限競爭）
- make pairing-idempotency-negative
- make pairing-refresh-negative
- make pairing-refresh-race-negative

Ingress 追蹤關聯 / 冪等性

主張： Ingress 應在扇出（Fan-out）過程中保持追蹤關聯，並在 Provider 重試時保持冪等。

具體含義：

當一個外部事件變為多個內部訊息時，每個部分都保持相同的 Trace/Event ID。
重試不會導致重複處理。
如果缺少 Provider 事件 ID，去重機制會回退到安全金鑰（例如 Trace ID），以避免丟棄不同的事件。
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

路由 dmScope 優先級 + identityLinks

主張： 路由預設必須保持 DM Session 隔離，且僅在明確配置（頻道優先級 + 身份連結）時才合併 Session。

具體含義：

頻道特定的 dmScope 覆蓋必須優於全域預設值。
identityLinks 應僅在明確連結的群組內合併，而不應跨越無關的 Peer。
Green:
- make routing-precedence
- make routing-identitylinks
Red (expected):
- make routing-precedence-negative
- make routing-identitylinks-negative

想要了解更多關於如何配置你的安全性模型？請諮詢 AI Setup Assistant。

下一步

OpenClaw Expert

還是卡住了？

如果這篇文件沒有解決你的情境，直接問 OpenClaw Expert，拿到可執行步驟。