注: 一部の古いリンクでは、以前のプロジェクト名が使用されている場合があります。
これは何か
実行可能で、攻撃者の行動を基にしたセキュリティ回帰スイートです。- 各主張には、有限状態空間で実行可能なモデル検査があります。
- 多くの主張には、現実的なバグの種類について反例トレースを生成する、対応するネガティブモデルがあります。
モデルの場所
モデルは別のリポジトリで管理されています: vignesh07/openclaw-formal-models。現在、そのリポジトリにはアクセスできません（本稿執筆時点では、GitHub が「Repository not found」を返します）。引き続きアクセスできない場合は、モデルが削除されたと判断する前に、OpenClaw のメンテナーチャンネルで現在の場所を確認してください。
注意事項
- これらはモデルであり、TypeScript 実装全体ではありません。そのため、モデルとコードの間に乖離が生じる可能性があります。
- 結果は、TLC が探索する状態空間によって制限されます。グリーンであっても、モデル化された前提と範囲を超えた安全性を意味するものではありません。
- 一部の主張は、明示的な環境上の前提（たとえば、正しいデプロイと正しい設定入力）に依存します。
結果の再現
モデルのリポジトリをクローンし、TLC を実行します。主張とターゲット
Gateway の公開とオープン Gateway の設定ミス
主張: 認証なしでループバック以外にバインドすると、リモートからの侵害が可能になり、公開範囲が拡大する可能性があります。モデルの前提では、トークンまたはパスワードによって未認証の攻撃者を阻止できます。
モデルのリポジトリにある
docs/gateway-exposure-matrix.md も参照してください。
Node 実行パイプライン（最もリスクの高い機能）
主張: モデルでは、exec host=node には、(a) Node コマンドの許可リストと宣言済みコマンド、および (b) 設定されている場合のリアルタイム承認が必要です。承認は再利用を防ぐためにトークン化されます。
ペアリングストア（DM ゲーティング）
主張: ペアリング要求には TTL と保留中要求数の上限が適用されます。受信ゲーティング（メンションと制御コマンドによる回避）
主張: メンションを必要とするグループコンテキストでは、認可されていない制御コマンドがメンションゲーティングを回避することはできません。ルーティングとセッションキーの分離
主張: 明示的にリンクまたは設定されていない限り、異なる相手からの DM が同じセッションに統合されることはありません。v1++ モデル: 並行処理、再試行、トレースの正確性
非アトミックな更新、再試行、メッセージのファンアウトなど、現実の障害モードに対する忠実度を高める追加モデルです。ペアリングストアの並行処理と冪等性
主張: ペアリングストアは、処理が交錯する場合でもMaxPending と冪等性を適用します。確認後の書き込みはアトミックまたはロック済みでなければならず、更新によって重複が作成されてはなりません。具体的には、同時リクエストがチャンネルの MaxPending を超えることはなく、同じ (channel, sender) に対するリクエストや更新を繰り返しても、有効な保留行が重複して作成されることはありません。
受信トレースの相関と冪等性
主張: 取り込み処理は、ファンアウト全体でトレースの相関を維持し、プロバイダーによる再試行に対して冪等です。1 つの外部イベントが複数の内部メッセージになる場合、各部分は同じトレースおよびイベントの識別情報を維持します。再試行によって二重処理されることはありません。プロバイダーのイベント ID がない場合、重複排除は安全なキー（たとえばトレース ID）にフォールバックし、異なるイベントが破棄されるのを防ぎます。ルーティングの dmScope 優先順位と identityLinks
主張:dmScope の優先順位と ID リンクは決定論的に動作します。デフォルトの main スコープでは、1 人の所有者の DM 全体で単一のローリングセッションが共有されます（個人用エージェントのデフォルト）。一方、分離するよう設定されたスコープ（per-peer、per-channel-peer、per-account-channel-peer）では、DM セッションが厳密に分離されます。チャンネル固有の dmScope オーバーライドはグローバルデフォルトより優先されます。identityLinks は、明示的にリンクされたグループ内でのみセッションを統合し、無関係な相手との間では統合しません。複数ユーザー向けの受信トレイでは、分離スコープを明示的に有効にすることが想定されています（複数ユーザーの DM トラフィックを検出すると、ランタイムのセキュリティ監査がこれを推奨します）。