# モジュラー検証 ## 定義 モジュラー検証(modular verification)とは、システムを構成するモジュール境界に沿って検証すべき性質を分割し、各性質を単一のモジュールの範囲だけで特定・実施・検証することで、全体を一括で検証するより計算量的に扱いやすくする検証戦略である。*The Real Internet Architecture* 第6章は、これをネットワークサービス検証の文脈で提案する。ネットワーク検証は既に活発な研究領域だが、現状はbase Internetの低レベルな性質にほぼ限定され、分散システムやユーザーが実際に必要とする性質の検証には手が届いていない。本章は、合成的ネットワークアーキテクチャ(compositional network architecture)がもたらす**合成の構造が明示的であること**こそが、この隔たりを埋める鍵だと主張する。ネットワークとセッションの合成(ブリッジング・レイヤリング・サブダクション)が暗黙的・場当たり的ではなく明示的な演算子として定義されていれば、その境界に沿って性質を分割でき、検証がモジュラーになる。(Source: [[@2024__PrincetonUP__The Real Internet Architecture - Chapter 6 Ideas for a Better Internet]] ch.6 §6.3) ## 3つの検証パターン 第6章は3つの思考実験(グローバル私設マルチキャスト、セキュアな企業ネットワーク、フローアフィニティオーバーレイ)を通じて、モジュラー検証が依拠する3つのパターンを識別する。 - **intra-network パターン**: ある性質が単一のネットワーク内で特定され、同じネットワーク内で実施・検証される。最も強力な形のモジュール性で、他ネットワークの設計目標(例: base Internetのグローバル到達可能性)を考慮せずに検証できる。 - **standard-layering パターン**: 性質がオーバーレイネットワークのリンク上で特定され、そのリンクを実装するアンダーレイのセッションで実施・検証される。合成の標準的な構造(レイヤリング)そのものに由来する証明義務である。 - **inherent property**: 合成規則(標準化されたレイヤリング・サブダクションの実装がユーザー選択フィールドの書き換えを一切行わないという規則)に従う限り自動的に成り立ち、個別の検証を要さない性質。第6章はForwarding transparency(フォワーダやミドルボックスが送信元・宛先・セッション識別子を書き換えないこと)をこの例として挙げる。 3つの例のうちフローアフィニティオーバーレイだけは、2つのネットワークがサブダクションで合成されているため関心事のきれいな分離を持たず、検証には2つのネットワークを合わせて考える必要がある。ただしこの場合も、形式モデルを検証対象のクラスに特殊化し自動化ツールで定理を証明することで、実ネットワークの検証をその定理の仮定を満たすかどうかの確認へと単純化できることが示される。(Source: [[@2024__PrincetonUP__The Real Internet Architecture - Chapter 6 Ideas for a Better Internet]] ch.6 §6.3.1.4, §6.3.2.2, §6.3.3) ## 横断的知見 - **「正しさの性質を分解し、それぞれに適した検証手法を割り当てる」という設計思想は、ネットワーク検証とストレージシステム検証という全く異なる領域で独立に採用されている**: 第6章のモジュラー検証は、ネットワーク合成の境界(intra-network・standard-layering・inherent property)に沿って性質を分割し、network verification・component verification(ミドルボックスのプログラム検証)・暗号学的証明(IPsecのSource validity・VPN link safety)という異なる検証技術をパターンごとに割り当てる(§6.3.2.2 表6.2)。[[軽量形式手法]]が蓄積するAmazon S3 ShardStoreの事例は、逐次クラッシュなし・逐次クラッシュあり・並行クラッシュなしという正しさの特性を分解し、それぞれに property-based テストとstateless model checkingを割り当てる。両者は対象領域(ネットワークサービス対キーバリューストレージ)も分解軸(合成構造の境界対クラッシュ・並行性の組み合わせ)も異なるが、「単一の万能な検証技術に頼るのではなく、性質の種類ごとに検証責任を分割し専用の技術を割り当てることでスケーラビリティを得る」という設計原理は共通している。(Source: [[@2024__PrincetonUP__The Real Internet Architecture - Chapter 6 Ideas for a Better Internet]] ch.6 §6.3.2.2, [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]]) - **「完全な形式検証はスケールしない」という診断は、ソフトウェア工学一般とネットワークアーキテクチャという異なる時代・異なる領域で独立に確認されている**: [[形式手法]]が蓄積するSWEBOK Straw Man Appendix I(1998)は、証明義務の生成・解消による完全な形式証明を「Advanced」(実務で広く使われる段階に達していない)に分類した。第6章(2024)は、これとは独立に「ネットワーク検証は既に活発な研究領域だが、検証されている性質は低レベルで、分散システムやユーザーが必要とする性質とは弱くしか関係しない」「スケーラビリティは切実な懸念である」と診断する(ch.6 §6.3冒頭)。分野もアプローチも異なる2つのソースが、「性質の複雑さ・システムの規模が増すと完全な形式検証は実務的な壁にぶつかる」という同じ限界に到達しており、いずれもその打開策として——完全な証明の追求ではなく——モジュール性による分割(前者は実装言語ベースの軽量な経験的検証、後者は合成構造に沿った検証範囲の限定)を選んでいる点でも収斂する。(Source: [[@2024__PrincetonUP__The Real Internet Architecture - Chapter 6 Ideas for a Better Internet]] ch.6 §6.3, [[@1998__IEEECS__SWEBOK Straw Man - Appendix I Draft Classification of Knowledge on Formal Methods]]) - **モジュール境界を検証の足場としてだけでなくセキュリティ実施の足場としても使うという発想は、Saltzer & Schroederの「完全な仲介」原則の具体化として読める**: [[セキュリティ設計原則]]が定式化するComplete mediation(すべての操作について真正性・完全性・認可を検査せよ)は抽象的な原則にとどまるが、第6章はこれをネットワークアーキテクチャの具体的な機構として与える——レイヤリング境界を横切るすべてのパケットは、アンダーレイの明確なセッションで受信されオーバーレイの明確なリンク上で受信されたことが分かるため、境界そのものがprovenance付与と検査の自然な実施点になる(ch.6 §6.3)。第6章はこれを「通常見られない多くのセキュリティチェックを促す」効果と「カスタムで再利用不能なコードのアタックサーフェスを縮小する」効果の2つに整理しており、後者はセキュリティ設計原則が挙げるEconomy of mechanism・Minimize common mechanismの縮小版とも解釈できる。(Source: [[@2024__PrincetonUP__The Real Internet Architecture - Chapter 6 Ideas for a Better Internet]] ch.6 §6.3, [[@2009__MITOCW__Principles of Computer System Design - Chapter 11 Information Security]] ch.11 §11.1.4) ## 未解決の問い - 実ネットワークアーキテクチャのサービス性質は、この抽象的・モジュラーな方法で特定できるか。実際の解析は個々のネットワークに閉じてスケーラブルになるか。(第6章自身が§6.3.4で提起する研究アジェンダ、Source: ch.6 §6.3.4) - データプレーンのモジュール性(フォワーディングテーブルの分割)は、制御プレーンのモジュール性(フォワーディングテーブルを生成するロジックの分割)に波及するか。フォワーディングテーブル自体でなく制御プレーンを直接検証する方向へ進めるか。(Source: ch.6 §6.3.4, §6.5) - ネットワーク境界での期待性質の自動チェックは実現可能で、実際のセキュリティ脅威を減らせるか。(Source: ch.6 §6.3.4) - 軽量形式手法(ShardStoreの実装言語ベース参照モデル)のような経験的検証技法は、ネットワーク合成のモジュラー検証にも転用できるか。両者は「性質を分解する」発想を共有するが、第6章はフォワーディングテーブルの静的解析、ShardStoreはproperty-basedテストという異なる技術基盤に立っており、この2つの技術系列を橋渡しする研究はまだ無い。 - 暗号アルゴリズムの証明とネットワークのフォワーディング解析という異なる検証技術のインターフェースをどう形式化すべきか。第6章はこの「seam(継ぎ目)」にセキュリティ脆弱性の余地がないようにすべきだと述べるが、具体的な形式化手法は示していない。(Source: ch.6 §6.3.4) ## 関連 - ソース: [[@2024__PrincetonUP__The Real Internet Architecture - Chapter 6 Ideas for a Better Internet]](ch.6 §6.3) / [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]] / [[@1998__IEEECS__SWEBOK Straw Man - Appendix I Draft Classification of Knowledge on Formal Methods]] / [[@2009__MITOCW__Principles of Computer System Design - Chapter 11 Information Security]] - 概念: [[形式手法]] / [[軽量形式手法]] / [[セキュリティ設計原則]] / [[エンドツーエンド論]] - 書籍: [[The Real Internet Architecture]] ## 出典 - Pamela Zave, Jennifer Rexford, *The Real Internet Architecture*, Princeton University Press, 2024, Chapter 6, §6.3.