English简体中文繁體中文日本語EspañolPortuguês (BR)한국어DeutschFrançaisالعربيةItalianoTiếng ViệtNederlandsTürkçeУкраїнськаBahasa IndonesiaPolskiفارسیไทย

Security

形式化驗證（安全模型）

本頁追蹤 OpenClaw 的 正式安全模型（目前為 TLA+/TLC；日後視需要增加）。

注意：部分較舊連結可能會提及先前的專案名稱。

目標（北極星）： 提供一個經機器檢查的論證，證明 OpenClaw 在明確假設下會執行其 預期的安全政策（授權、工作階段隔離、工具控管，以及 錯誤設定安全性）。

目前這是什麼： 一套可執行、由攻擊者驅動的 安全迴歸套件：

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

目前這還不是什麼： 這不是「OpenClaw 在所有方面都是安全的」的證明，也不是完整 TypeScript 實作正確性的證明。

模型存放位置

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

重要注意事項

  • 這些是 模型，不是完整的 TypeScript 實作。模型與程式碼之間可能會出現偏移。
  • 結果受限於 TLC 探索的狀態空間；「綠燈」並不表示在已建模假設與邊界之外也具備安全性。
  • 部分主張依賴明確的環境假設（例如正確的部署、正確的設定輸入）。

重現結果

目前，結果可透過在本機 clone 模型 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 targets。

make <target>

Gateway 暴露與開放 Gateway 錯誤設定

主張： 在沒有 auth 的情況下綁定超出 loopback 的範圍，可能讓遠端攻陷成為可能 / 增加暴露面；token/password 會阻擋未經 auth 的攻擊者（依模型假設）。

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

另見模型 repo 中的 docs/gateway-exposure-matrix.md。

Node exec 管線（最高風險能力）

主張： exec host=node 需要 (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++：額外的有界模型（並行、重試、追蹤正確性）

這些是後續模型，用於提高對真實世界失敗模式（非原子更新、重試，以及訊息 fan-out）的擬真度。

配對儲存區並行 / 冪等性

主張： 配對儲存區即使在交錯執行下也應強制執行 MaxPending 與冪等性（也就是說，「check-then-write」必須是原子性的 / 已鎖定；refresh 不應建立重複項）。

含義：

  • 在並行請求下，不能超過某個 channel 的 MaxPending。

  • 對同一個 (channel, sender) 的重複請求 / refresh 不應建立重複的即時 pending 列。

  • 綠燈執行：

    • 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

輸入追蹤關聯 / 冪等性

主張： 擷取應在 fan-out 間保留追蹤關聯，並在 provider 重試下保持冪等。

含義：

  • 當一個外部事件變成多個內部訊息時，每個部分都保留相同的 trace/event identity。

  • 重試不會導致重複處理。

  • 如果 provider event ID 缺失，去重會退回到安全金鑰（例如 trace 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

主張： 路由必須預設保持 DM 工作階段隔離，且只有在明確設定時才折疊工作階段（channel 優先順序 + identity links）。

含義：

  • Channel-specific dmScope 覆寫必須優先於全域預設。

  • identityLinks 應只在明確連結的群組內折疊，而不是跨無關對等端。

  • 綠燈：

    • make routing-precedence
    • make routing-identitylinks

  • 紅燈（預期）：

    • make routing-precedence-negative
    • make routing-identitylinks-negative

相關