形式検証（セキュリティモデル）

このページでは 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 の公開と Open 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 と冪等性を強制すべき（つまり「チェックしてから書き込む」は原子的/ロック付きでなければならない。リフレッシュは重複を作成すべきではない）。

具体的には:

  • 並行リクエスト下で、チャネルの 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

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

主張: インジェストはファンアウト全体でトレース相関を維持し、プロバイダーリトライ下で冪等であるべき。

具体的には:

  • 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 セッションを分離し、明示的に設定された場合のみセッションを統合すべき（チャネル優先順位 + identity links）。

具体的には:

  • チャネル固有の dmScope オーバーライドがグローバルデフォルトより優先。

  • identityLinks は明示的にリンクされたグループ内でのみ統合し、無関係なピア間では統合しない。

  • グリーン:

    • make routing-precedence
    • make routing-identitylinks

  • レッド（想定通り）:

    • make routing-precedence-negative
    • make routing-identitylinks-negative
arrow_back
前へ
Tailscale
次へ
README
arrow_forward