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

このページは、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>

ゲートウェイの露出とオープンゲートウェイの誤設定

主張： 認証なしでループバックを超えてバインドすると、リモート侵害が可能になる/露出が増加する可能性があります。トークン/パスワードは未認証の攻撃者をブロックします（モデルの仮定に従って）。

  • グリーンラン：
    • 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 を超えることはできません。

  • 同じ（チャネル、送信者）に対する繰り返しのリクエスト/リフレッシュは、重複するライブペンディング行を作成すべきではありません。

  • グリーンラン：

    • 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）にフォールバックして、異なるイベントを削除しないようにします。

  • グリーン：

    • 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
← ドキュメントに戻る