形式驗證（安全模型）

本頁追蹤 OpenClaw 的形式安全模型（目前使用 TLA+/TLC；未來視需要擴充）。

注意：部分較舊的連結可能仍指向先前的專案名稱。

目標（北極星）： 提供機器可驗證的論證，證明 OpenClaw 在明確的假設條件下執行其預期的安全策略（授權、工作階段隔離、工具管控和誤設定安全）。

目前的狀態： 一套可執行的、攻擊者驅動的安全迴歸測試套件：

每個宣告都有一個可在有限狀態空間上執行的模型檢查。
許多宣告搭配一個反向模型，會為真實的錯誤類別產生反例追蹤。

這不是（尚未到那一步）： 證明「OpenClaw 在所有方面都是安全的」，或完整 TypeScript 實作是正確的。

模型存放位置

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

重要注意事項

這些是模型，不是完整的 TypeScript 實作。模型和程式碼之間可能存在偏移。
結果受 TLC 探索的狀態空間所限；「綠燈」不代表超出模型假設和邊界之外的安全性。
部分宣告依賴明確的環境假設（例如正確的部署、正確的設定輸入）。

重現結果

目前的做法是將模型 repo 克隆到本機並執行 TLC（見下方）。未來的版本可能提供：

CI 執行的模型，附帶公開產物（反例追蹤、執行日誌）
適用於小型有限檢查的「線上執行此模型」工作流程

開始使用：

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

# 需要 Java 11+（TLC 在 JVM 上執行）。
# Repo 中附帶固定版本的 `tla2tools.jar`（TLA+ 工具），並提供 `bin/tlc` + Make 目標。

make <target>

Gateway 暴露與開放式 Gateway 誤設定

宣告： 在沒有驗證的情況下將繫結範圍擴展到迴路位址之外，可能讓遠端入侵成為可能／增加暴露面；token/密碼可阻擋未授權的攻擊者（在模型假設下）。

綠燈執行：
- make gateway-exposure-v2
- make gateway-exposure-v2-protected
紅燈（預期）：
- make gateway-exposure-v2-negative

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

Nodes.run 管線（最高風險能力）

宣告： nodes.run 需要 (a) node 指令允許清單加上已宣告的指令，以及 (b) 設定時的即時核准；核准以 token 化方式防止重放（在模型中）。

綠燈執行：
- make nodes-pipeline
- make approvals-token
紅燈（預期）：
- make nodes-pipeline-negative
- make approvals-token-negative

配對儲存（DM 管控）

宣告： 配對請求遵守 TTL 和待處理請求上限。

綠燈執行：
- make pairing
- make pairing-cap
紅燈（預期）：
- make pairing-negative
- make pairing-cap-negative

進入管控（提及 + 控制指令繞過）

宣告： 在需要提及的群組上下文中，未授權的「控制指令」無法繞過提及管控。

綠燈：
- make ingress-gating
紅燈（預期）：
- make ingress-gating-negative

路由/工作階段鍵隔離

宣告： 來自不同對等方的 DM 不會折疊到同一個工作階段，除非明確連結/設定。

綠燈：
- 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（非原子 begin/commit 上限競爭）
- 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

宣告： 路由必須預設保持 DM 工作階段隔離，只有在明確設定時才折疊工作階段（頻道優先順序 + 身分連結）。

含義：

頻道專屬的 dmScope 覆寫必須優先於全域預設值。
identityLinks 只應在明確連結的群組內折疊，不應跨越不相關的對等方。
綠燈：
- make routing-precedence
- make routing-identitylinks
紅燈（預期）：
- make routing-precedence-negative
- make routing-identitylinks-negative