VPNプロトコル仕様が証明することと証明しないこと

プロトコル文書は実装間の契約であり、注意深く読めば、適合する二者が何を交換するのか、設計者がどの性質を意図したのかが分かる。しかし、接続先のサーバーでどのバイナリが動いているのか、そのサーバーがどう設定されたのか、その後アカウント記録がどうなるのかは分からない。これらは三種類の異なる証拠であり、仕様をその三つすべてとして扱うことが、プロトコル名ができない仕事を始めてしまう道である。三つを分けておくことがこの演習の全体である。

文書は論証の出発点であり、結論ではない。

文書が実際に規定するもの

WireGuard については、プロトコルの記述が Noise IK ハンドシェイク、固定されたプリミティブの集合、メッセージのレイアウト、そしてその後パケットを運ぶトランスポートのフレーミングを定義する。IKEv2 については、比較できる成果物は RFC 7296 であり、交換、ペイロード、提案の交渉を規定する。どちらの場合も範囲は正確であり、メッセージ、状態機械、そしてセキュリティ目標が成り立つ前提である。

任意モードは読解を難しくする。あるハンドシェイクで成り立つ性質が、別の認証の取り決めやフォールバック設定を使う配備には当てはまらないことがある。

保証が止まる場所

形式分析はモデルに関する問いに答える。WireGuard の検証作業は Tamarin 証明器の中の記号的モデルを用いており、その前提の下で設計が特定の攻撃に耐えることを示せるが、出荷されたユーザー空間実装にメモリ安全性の不具合がないことは示さない。モデルと機械の間のこの隙間こそ、実際の事故が住む場所である。証明を実装の証明書として読むのはカテゴリー錯誤である。

前方秘匿性も同じ境界を示す。この性質は鍵がプロトコルの意図どおりに破棄されることに依存しており、それはメッセージ形式ではなく実装とその環境の性質である。消去を規定する設計でも、メモリをディスクに退避するプラットフォームではそれを強制できない。

層状の依存関係は、TLS ベースのトンネルの背後の TLS ライブラリ、ユーザー空間トンネルが使うカーネルインターフェース、乱数生成器がすべてプロトコルの文面の外にあるため、隙間をさらに広げる。

バイトをビルドの中まで追う

バージョンを特定し、実際にトラフィックを処理しているものと比較することで、文書から成果物へ移る。プロトコル名を掲げる製品は、仕様が決して記述しないプロビジョニング、テレメトリ、管理のコンポーネントを追加していることがある。

openvpn --version | head -3
wg --version
dpkg -l | grep -E 'openvpn|wireguard|libssl'
ss -lunp | grep -E '1194|51820'
sha256sum ./wireguard-tools_1.0.20210914_amd64.deb

再現可能なビルドと公開されたチェックサムによって、ソースツリーと配布されたバイナリを結び付けられる。その結び付きがなければ、公開されたソースは検査が可能だということしか証明せず、実行中のファイルがそれと一致するかは分からない。

設定も同じ段階に属する。暗号スイート、許可されたピア、ルーティング設定は配備上の選択であり、適合するビルドでもいい加減に設定すれば弱いトンネルができる。

運用慣行は別に保つ

アカウント記録、支払いデータ、サポートへの提出は、どのプロトコル文書も制約しない事業者の判断である。監査報告は宣言された範囲で特定の構成要素を扱い、プライバシーポリシーは意図と慣行を述べるが、どちらも他方を代替せず、どちらも暗号学的な主張ではない。

正確な結論は累積的であり、仕様は設計を説明し、ビルドと設定はトンネルを説明し、事業者の文書化された慣行はトンネルが決して見ないすべてを説明する。そのどれを検証したのかを述べれば、主張は真のままでいられる。