形式検証(セキュリティモデル)

このページは、OpenClawの形式的なセキュリティモデル(現在はTLA+/TLC、必要に応じて追加)を追跡します。

注意:一部の古いリンクは以前のプロジェクト名を参照している場合があります。

**目標(北極星):**OpenClawが意図したセキュリティポリシー(認可、セッション分離、ツールゲーティング、および誤設定の安全性)を強制することを、明示的な仮定の下で機械検証された引数を提供します。

これが現在のもの:実行可能な攻撃者駆動型セキュリティ回帰スイート:

  • 各クレームには有限状態空間上の実行可能なモデルチェックがあります。
  • 多くのクレームには、現実的なバグクラスの反例トレースを生成するネガティブモデルがペアになっています。

これがまだでないもの:「OpenClawはすべての点で安全である」という証明、または完全なTypeScript実装が正しいという証明。

モデルの場所

モデルは別のリポジトリで管理されています: vignesh07/openclaw-formal-models。

重要な注意事項

  • これらはモデルであり、完全なTypeScript実装ではありません。モデルとコードの間にずれがある可能性があります。
  • 結果はTLCによって探索された状態空間によって制限されます。「緑」は、モデル化された仮定と境界を超えたセキュリティを意味するものではありません。
  • 一部のクレームは明示的な環境仮定(正しい展開、正しい構成入力など)に依存しています。

結果の再現

現在、結果はモデルリポジトリをローカルにクローンしてTLCを実行することで再現されます(以下を参照)。将来の反復では以下を提供できる可能性があります:

  • 公開アーティファクト(反例トレース、実行ログ)を含むCI実行モデル
  • 小規模な境界付きチェック用のホストされた「このモデルを実行」ワークフロー

開始方法:

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

# Java 11+が必要(TLCはJVM上で実行されます)。
# リポジトリはピン留めされた`tla2tools.jar`(TLA+ツール)をベンダー化し、`bin/tlc` + Makeターゲットを提供します。

make <target>

Gatewayエクスポージャーとオープンgateway誤設定

クレーム: ループバックを超えた認証なしのバインディングは、リモート侵害を可能にする/エクスポージャーを増加させる可能性があります。トークン/パスワードは未認証の攻撃者をブロックします(モデルの仮定による)。

  • グリーン実行:
    • make gateway-exposure-v2
    • make gateway-exposure-v2-protected
  • レッド(予想):
    • make gateway-exposure-v2-negative

参照: モデルリポジトリのdocs/gateway-exposure-matrix.md。

Nodes.runパイプライン(最もリスクの高い機能)

クレーム: nodes.runは(a)ノードコマンド許可リストと宣言されたコマンド、および(b)構成された場合のライブ承認を必要とします。承認はリプレイを防ぐためにトークン化されます(モデル内)。

  • グリーン実行:
    • 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と冪等性を強制する必要があります(つまり、「check-then-write」はアトミック/ロックされている必要があります。リフレッシュは重複を作成してはいけません)。

意味:

  • 並行リクエストの下では、チャネルのMaxPendingを超えることはできません。

  • 同じ(channel, sender)に対する繰り返しリクエスト/リフレッシュは、重複するライブ保留行を作成してはいけません。

  • グリーン実行:

    • make pairing-race(アトミック/ロックされたcapチェック)
    • make pairing-idempotency
    • make pairing-refresh
    • make pairing-refresh-race

  • レッド(予想):

    • make pairing-race-negative(非アトミックbegin/commit capレース)
    • make pairing-idempotency-negative
    • make pairing-refresh-negative
    • make pairing-refresh-race-negative

イングレストレース相関/冪等性

クレーム: 取り込みは、ファンアウト全体でトレース相関を保持し、プロバイダ再試行の下で冪等である必要があります。

意味:

  • 1つの外部イベントが複数の内部メッセージになると、すべての部分が同じトレース/イベントIDを保持します。

  • 再試行は二重処理にはなりません。

  • プロバイダイベント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
← ドキュメントに戻る