技術概要：Tofu による自動化されたチャネル障害分析

問題定義

分散プロトコルは現代のインターネットサービスの基盤を形成しているが、その通信チャネルは本質的に不完全である。メッセージは輻輳により失われたり、敵対者によって再生されたり、マルチパスルーティングにより順序が入れ替えられたりする。これらのチャネルレベルの障害は、微妙なバグ、サービス拒否（DoS）の脆弱性、および安全性違反の主要な原因である。

これらの障害を分析する既存のアプローチは、決定的な二律背反に苦しんでいる：

1. 実用的なテストツール：Scapy、Linux netem、PacketDrill などのツールは、手動での障害注入とファズテストを可能にする。しかし、これらは完全性の保証を欠いており、バグが見つからなかったからといって、その欠如が証明されるわけではない。
2. 形式的検証：既存の形式的手法（Tamarin、ProVerif、Spin、TLA+ など）は、しばしば攻撃者の能力の手動定義を必要とするか、チャネルレベルの障害よりも暗号的な性質に焦点を当てている。自動化された攻撃合成のためのフレームワークが存在するものもあるが、それらは特定のメッセージタイプを対象としたり、チャネル障害の場当たり的なモデリングを必要としたりしており、任意の線形時間論理（LTL）仕様に対する体系的で汎用性のあるアプローチが欠けている。

任意の分散プロトコル仕様におけるチャネル障害（破棄、再生、順序入れ替え）の健全かつ完全な自動化された分析を提供する手法に関する文献のギャップが存在する。

手法

著者らは、故障した通信チャネルを悪用して LTL プロトコル仕様に違反する攻撃トレースを自動的に合成するための厳密な手法を提案する。これは、以下のコアコンポーネントを実装するTofuというツールによって実現される：

1. 形式的基盤

この手法は、線形時間論理（LTL）とブーヒオートマトンの等価性に依存している。

• プロセス：分散プロトコルは、バッファ付きチャネルを介して相互作用する通信プロセス（ラベル付き遷移システム）としてモデル化される。
• 攻撃合成：問題は、プロトコル $P$ と攻撃者 $A$ の合成が性質 $\phi$ に違反する（すなわち、$(P \parallel A) \not\models \phi$）ような「攻撃者プロセス」$A$ を見つけることとして定式化される。
• 複雑性：この問題はブーヒオートマトンの言語包含問題に還元され、PSPACEに位置づけられる。

2. チャネル障害ガジェット

Tofu は、ユーザー指定の障害制限 $\ell$ を持つ被害チャネル $c$ 上で 3 つの異なる攻撃者能力をモデル化する特定の「ガジェット（プロセス）」を合成する：

• ドロップガジェット（$D_\ell$）：チャネルから最大 $\ell$ 個のメッセージを静かに消費する。メッセージを破棄するか、通過させるか、終了するかを決定するために非決定的な選択を使用し、受信者を飢えさせることで生存性を trivial に違反しないようにする。
• 再生ガジェット（$R_\ell$）：非破壊的読み取りを介してメッセージを観察し、それらをローカルバッファに格納し、非決定的に再生する。バッファからメッセージを削除するか削除せずに再生することをサポートし、メッセージを破棄することもできる。
• 順序入れ替えガジェット（$O_\ell$）：破壊的読み取りを介してメッセージを傍受し、バッファに格納し、異なる順序で再生する。正しい傍受セマンティクスを確保するため、このガジェットは合成システム内で最高優先度が割り当てられる。

これらのガジェットは汎用性を持つように設計されている。つまり、特定のメッセージタイプに依存せず、任意のプロトコルモデルと合成可能である。

3. 実装（Tofu ツール）

Tofu は、Promela言語を使用してSpin モデルチェッカーの上に実装されている。

• ワークフロー：ユーザーはプロトコルの Promela モデルを提供し、被害チャネルを選択し、攻撃者モデル（ドロップ、再生、順序入れ替え）を選択し、LTL 性質を指定する。
• 注入：Tofu はモデルを解析し、チャネルを特定し、対応するガジェットコードを合成してモデルに注入する。
• 検証：修正されたモデルは Spin に渡される。Spin は網羅的な状態空間探索を実行する。攻撃が存在する場合、それは反例トレースを返す。そうでない場合、攻撃の欠如を証明する。

主要な貢献

本論文は以下の貢献を提示する：

1. 汎用ガジェット：分散プロトコルの任意の通信チャネルに適用可能な、ドロップ、再生、順序入れ替えガジェットの形式的定義と構築。
2. Tofu ツール：上記の 3 つの攻撃者モデルをサポートする分散通信プロトコルに対する攻撃を合成する汎用ツール。Tofu は健全（偽陽性なし）かつ完全（障害制限内で攻撃が存在すれば、必ず発見される）である。
3. TCP に関するケーススタディ：その有用性を示すために、伝送制御プロトコル（TCP）の形式的モデルへの Tofu の適用。

結果：TCP ケーススタディ

著者らは、接続確立と切断に焦点を当てた TCP の Promela モデルを構築し、チャネル障害の影響を分離するために、実装レベルの耐性機能（再送信タイムアウト、シーケンス番号など）を意図的に省略した。彼らは、ドロップ、再生、順序入れ替え攻撃の下で、6 つの LTL 性質（安全性と生存性を含む）を検証した。

発見事項：

• ドロップおよび再生攻撃：Tofu は、6 つの性質のうち 5 つを違反する攻撃を正常に発見した。
  • 例：FIN メッセージを破棄すると、一方のエンドポイントがタイムアウトして閉じ、他方が Established 状態のまま残る（「半開き接続の不存在」という安全性性質の違反）。
  • 例：古くなった SYN を再生すると、受信者が誤ったハンドシェイク状態に強制された。
  • 生存性：攻撃者は重要な制御メッセージを消費または洪水させることで進行を妨げ、受容サイクルを作成した。
• 順序入れ替え攻撃：順序入れ替え攻撃者はいかなる性質も違反できなかった。TCP 状態機械は単に順序が入れ替わったパケットをスキップし、誤った状態ではなく、タイムアウトと閉鎖につながった。
• 結論：この分析は機械的に、再送信やシーケンスチェックなどの耐性メカニズムなしでは、ベースレベルの TCP 状態機械がチャネル障害に対処するには不十分であることを確認した。

意義と主張

本論文は、チャネル障害に関する推論に対する体系的かつ自動化されたサポートを提供することで、形式的検証の分野における特定のギャップを埋めると主張している。

• 完全性：テストツールとは異なり、Tofu は完全性の保証を提供する。ツールがバグを発見せずに終了した場合、指定された障害制限に対してそのようなバグの欠如が証明される。
• 自動化：攻撃者能力の場当たり的な手動モデリングの必要性を排除し、ユーザーは単にチャネルと障害タイプを選択するだけで済む。
• 健全性：このツールは LTL とブーヒオートマトンの間の厳密な等価性に依存しており、発見されたあらゆる反例が真の攻撃トレースであることを保証する。

著者らは、Tofu を既存の実装レベルのテストツールを補完するものとして位置づけている。Scapy などのツールは実務において攻撃を確認するために不可欠であるが、Tofu は形式的モデルにおける網羅性の理論的保証を提供する。コードとモデルはオープンソースとして公開されている。