Formal Verification (Security Models)
OpenClaw の高リスク経路に対して、機械的に検証するセキュリティモデル。
このページは OpenClaw の形式セキュリティモデル（現在は TLA+/TLC；必要に応じて追加）を追跡します。
Tutorial.alert.info
目標（北極星）： OpenClaw が明示的な仮定の下で、意図した
セキュリティポリシー（認証、セッション分離、ツールゲート、
誤設定の安全性）を強制することを機械的にチェックできる引数を提供する。
これが何であるか（現在）：実行可能な、攻撃者駆動型のセキュリティ回帰スイート：
- 各主張は有限状態空間で実行可能なモデルチェックを持っています。
- 多くの主張は、現実的なエラークラスの反例トレースを生成できるペアの負のモデルを持っています。
これが何ではない： "OpenClaw がすべての面で安全である"または完全な TypeScript 実装が正しいことの証明。
モデルの場所
モデルは別のリポジトリで維持されています：''vignesh07/openclaw-formal-models''。
重要な注意事項
- これらはモデルであり、完全な TypeScript 実装ではありません。モデルとコード間のドリフトは可能です。
- 結果は TLC が探索した状態空間によって制限されます；"緑"はモデリングの仮定と境界を超えた安全性を意味しません。
- 一部の主張は明示的な環境仮定（正しいデプロイ、正しい構成入力など）に依存しています。
結果の再現
現在、モデルリポジトリをローカルにクローンして TLC を実行することで結果を再現します（下記参照）。今後の反復では提供される可能性があります：
- パブリックアーティファクト（反例トレース、実行ログ）を含む CI でモデルを実行
- 小規模な有界チェックのためのホストされた「このモデルを実行」ワークフロー
開始するには：
git clone https://github.com/vignesh07/openclaw-formal-models cd openclaw-formal-models make '<target>'
ゲートウェイの露出とオープンゲートウェイの誤設定
主張： 認証なしでループバックを超えてバインドすると、リモート侵害が可能になる/露出が増加します；トークン/パスワードは認証されていない攻撃者をブロックします（モデルの仮定に基づく）。
- 緑の実行：
- ''make gateway-exposure-v2''
- ''make gateway-exposure-v2-protected''
- Red (expected):
- ''make gateway-exposure-v2-negative''
参照：モデルリポジトリの ''docs/gateway-exposure-matrix.md''。
Nodes.run パイプライン（最もリスクの高い機能）
''主張：'' ''nodes.run'' には (a) ノードコマンド許可リストと宣言されたコマンド、および (b) 構成時のライブ承認が必要です；承認はリプレイを防ぐためにトークン化されます（モデル内）。
- 緑の実行：
- ''make nodes-pipeline''
- ''make approvals-token''
- Red (expected):
- ''make nodes-pipeline-negative''
- ''make approvals-token-negative''
ペアリングストア（DM ゲート）
主張： ペアリングリクエストは TTL と保留リクエストの上限を尊重します。
- 緑の実行：
- ''make pairing''
- ''make pairing-cap''
- Red (expected):
- ''make pairing-negative''
- ''make pairing-cap-negative''
イングレスゲート（メンション+制御コマンドのバイパス）
主張： メンションを必要とするグループ環境では、認可されていない「制御コマンド」はメンションゲートをバイパスできません。
- Green:
- ''make ingress-gating''
- Red (expected):
- ''make ingress-gating-negative''
ルーティング/セッションキーの分離
主張： 異なるピアからの DM は、明示的にリンク/構成されていない限り、同じセッションにマージされません。
- Green:
- ''make routing-isolation''
- Red (expected):
- ''make routing-isolation-negative''
v1++：追加の有界モデル（並行性、再試行、トレースの正確性）
これらは、現実世界の障害モード（非アトミック更新、再試行、メッセージファンアウト）の忠実度を強化するフォローオンモデルです。
ペアリングストアの並行性/べき等性
**Claim:** a pairing store should enforce `MaxPending` and idempotency even under interleavings (i.e., "check-then-write" must be atomic / locked; refresh shouldn't create duplicates).
これが意味するもの：
- Under concurrent requests, you can't exceed `MaxPending` for a channel.
- Repeated requests/refreshes for the same `(channel, sender)` should not create duplicate live pending rows.
- 緑の実行：
- ''make pairing-race''（アトミック/ロックされたキャップチェック）
- ''make pairing-idempotency''
- ''make pairing-refresh''
- ''make pairing-refresh-race''
- Red (expected):
- ''make pairing-race-negative'' （非アトミック開始/コミットキャップ競争）
- ''make pairing-idempotency-negative''
- ''make pairing-refresh-negative''
- ''make pairing-refresh-race-negative''
イングレストレースの相関/べき等性
主張： インジェストはファンアウト間でトレースの相関を保持し、プロバイダーの再試行下でべき等である必要があります。
これが意味するもの：
- 外部イベントが複数の内部メッセージになる場合、各部分は同じトレース/イベント ID を保持します。
- 再試行は二重処理を引き起こしません。
- プロバイダーイベント ID が欠落している場合、重複排除は異なるイベントを失わないように安全なキー（例：トレース ID）にフォールバックします。
- Green:
- ''make ingress-trace''
- ''make ingress-trace2''
- ''make ingress-idempotency''
- ''make ingress-dedupe-fallback''
- Red (expected):
- ''make ingress-trace-negative''
- ''make ingress-trace2-negative''
- ''make ingress-idempotency-negative''
- ''make ingress-dedupe-fallback-negative''
ルーティング dmScope 優先順位 + IdentityLinks
主張： デフォルトでは、ルーティングは DM セッションを分離したままにし、明示的に構成された場合にのみセッションを折りたたむ必要があります（チャネル優先順位 + ID リンク）。
これが意味するもの：
- チャネル固有の dmScope オーバーライドはグローバルデフォルトより優先する必要があります。
- IdentityLinks は明示的にリンクされたグループ内でのみ折りたたまれ、関連のないピア間では折りたたまれてはいけません。
- Green:
- ''make routing-precedence''
- ''make routing-identitylinks''
- Red (expected):
- ''make routing-precedence-negative''
- ''make routing-identitylinks-negative''