# 軽量形式手法 軽量形式手法とは、完全な形式検証(full formal verification)の健全性を追求する代わりに、自動化・使いやすさ・システムと仕様が継続的に変化する中で正しさを保ち続ける能力を優先する、実用的な検証アプローチを指す。ShardStore の事例では、実装と同じ言語(Rust)で書かれた実行可能な参照モデルを、property-based テストと stateless model checking で実装と照合することで実現される。正しさの特性(逐次クラッシュなし・逐次クラッシュあり・並行クラッシュなし)を分解し、それぞれに最も適した検証ツールを割り当てる点が特徴である(Source: [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]])。 ## 横断的知見 - **DDIA 第9章のシステムモデル分類は、ShardStore の「正しさの特性を分解する」設計思想の理論的裏付けになる**: ShardStore は逐次クラッシュなし・逐次クラッシュあり・並行クラッシュなしという 3 つの正しさの特性を分解し、それぞれに最適な検証ツール(property-based テスト・stateless model checking)を割り当てる。DDIA 第9章はこの分解の背景にある一般原理——クラッシュ停止モデル(1 回だけクラッシュし復帰しない)とクラッシュ回復モデル(任意のタイミングで繰り返しクラッシュ・復帰する)を明確に区別するシステムモデルの形式化——を提供する。「逐次クラッシュあり」は単一ノードのクラッシュ回復モデルの検証、「並行クラッシュなし」は複数ノードが同時に振る舞う場合の安全性検証に相当し、ShardStore が未解決として残す「並行クラッシュ実行」の検証困難性は、DDIA が言う「クラッシュ回復モデルと並行性を同時に扱うシステムモデルは形式化・検証コストが跳ね上がる」という一般的な傾向の具体例と解釈できる。(Source: [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]], [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "System Model and Reality") - **軽量形式手法(実装言語での参照モデル+property-based テスト)は、DDIA が挙げる決定論的シミュレーションテスト(DST)と同じ「モデル検査とは異なる経験的検証」の系譜に位置する**: DDIA 第9章はモデル検査(TLA+ 等、簡略化された仕様言語のモデルを検証)と、DST(実コードを決定論的に大量実行して検証)を対比する。ShardStore の軽量形式手法は実装と同じ言語(Rust)で参照モデルを書く点で TLA+ のような専用仕様言語を使うモデル検査とは異なるが、DST のように実行環境全体を決定論化するわけでもない中間的な位置にある——「仕様は簡略化されているが実装言語で書く」という選択は、モデル検査の抽象化コストと DST の環境制御コストの両方を部分的に回避する設計判断と言える。(Source: [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]], [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "Model checking and specification languages", "Deterministic simulation testing") - **1998年の SWEBOK Straw Man Appendix I が Research(研究段階)に分類した「形式仕様に基づくテストケース自動導出」「仕様とコードの照合」は、2021年の ShardStore で実装言語ベースの軽量な形として実務に定着している**: Appendix I はコーディングとテスト段階の形式手法トピックとして、形式仕様からのブラックボックス単体テスト導出や仕様への適合検証を Research に分類し、完全な形式証明(証明義務の生成・解消)は Advanced にとどめた。ShardStore はこの間隙を、専用の仕様言語による完全な証明ではなく、実装と同じ言語(Rust)の参照モデルに対する property-based テストと stateless model checking で埋めている。すなわち20年余りの間に、形式仕様と実装の照合という研究段階の課題は「完全な形式証明」の方向ではなく「軽量な経験的検証」の方向で実務適用が進んだと解釈できる。(Source: [[@1998__IEEECS__SWEBOK Straw Man - Appendix I Draft Classification of Knowledge on Formal Methods]], [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]]) - **「正しさの性質を分解し、それぞれに専用の検証手法を割り当てる」という設計思想は、ストレージシステムとネットワークアーキテクチャという全く異なる領域で独立に採用されている**: ShardStore は逐次クラッシュなし・逐次クラッシュあり・並行クラッシュなしという正しさの特性を分解し、それぞれに property-based テストと stateless model checking を割り当てる。*The Real Internet Architecture* 第6章が提案する[[モジュラー検証]]は、ネットワーク合成の境界(intra-network・standard-layering・inherent property)に沿って性質を分割し、network verification・component verification・暗号学的証明という異なる検証技術をパターンごとに割り当てる(第6章 表6.2)。対象領域も分解軸も異なるが、「単一の万能な検証技術に頼らず、性質の種類ごとに検証責任を分割し専用の技術を割り当てることでスケーラビリティを得る」という設計原理は共通しており、軽量形式手法がストレージシステムで確立したパターンが、ネットワークアーキテクチャという別領域でも独立に発見されていることを示す。(Source: [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]], [[@2024__PrincetonUP__The Real Internet Architecture - Chapter 6 Ideas for a Better Internet]] ch.6 §6.3.2.2) - **同じ Amazon 社内でも、システムの性質に応じて全く異なる厳密さの形式手法が選ばれている**: ShardStore(2021)はキーバリューストレージノードの正しさを、完全な数学的証明ではなく実装言語(Rust)の参照モデルに対する property-based テストと stateless model checking という軽量な経験的検証で担保する。一方 *Building Secure and Reliable Systems* 第13章が引用する Amazon の TLS 実装 s2n の事例(Chudnov et al. 2018, "Continuous Formal Verification of Amazon s2n")は、暗号プロトコルという性質上、継続的インテグレーションに組み込まれた本格的な形式検証(証明ベースのアプローチ)によって TLS の実装を検証し続けている。同一企業内で、ストレージシステムには軽量形式手法、暗号プロトコル実装にはより重い継続的形式検証というように、対象システムの性質(クラッシュ整合性 対 プロトコルの安全性証明)に応じて検証の厳密さのレベルを使い分けていることがうかがえる。これは軽量形式手法が「あらゆる場面で完全な形式検証を代替する」ものではなく、対象の性質によって適用範囲が限定されることを示す実例である。(Source: [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]], [[@2020__OReilly__Building Secure and Reliable Systems - Chapter 13 Testing Code]] ch.13 §Formal Methods) ## 未解決の問い - 軽量形式手法(実装言語ベースの参照モデル+property-based テスト)は、[[モジュラー検証]]がネットワーク合成の境界で行う静的なフォワーディングテーブル解析とは異なる技術基盤に立つ。両者の「性質を分解する」という共通発想を、実際に技術面でも橋渡しできるか(例えばネットワークの制御プレーンに軽量形式手法を適用する等)は未検討。 - s2n のような暗号プロトコル実装の継続的形式検証と、ShardStore のような軽量形式手法は、なぜ Amazon 社内で異なるアプローチを選んだのか。プロトコルの安全性証明はクラッシュ整合性の検証よりも「性質を厳密な数式で書きやすい」ためか、それとも要求される保証水準(セキュリティ対信頼性)の違いによるものか。両ソースを直接突き合わせた検討はまだない。 - 並行クラッシュ実行(並行性とクラッシュの組み合わせ)を検証する有効な自動化手法は何か。ShardStore の事例では未確立のまま残されている。 - 実装と同じ言語で参照モデルを書くアプローチは、Rust 以外の言語(例: Go・Java 製の分散ストレージシステム)でも同程度の保守コスト削減効果を持つか。 - リソース枯渇(disk space・メモリ)系の障害を、テスト環境固有のオーバーヘッドと実バグを区別しながら自動検証する手法は確立できるか。 - 軽量形式手法によって検出される不具合の分布(機能的正しさ/クラッシュ整合性/並行性)は、他の本番ストレージシステムでも同様の比率になるか。 - ShardStore の「並行クラッシュなし」の検証範囲を、DDIA が紹介する DST(FoundationDB の Flow・TigerBeetle の決定論的イベントループ)のようなアプローチに置き換えれば、未解決の「並行クラッシュ実行」の検証まで拡張できるか。両者を組み合わせたハイブリッド検証の設計は可能か。 ## 関連 - ソース: [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]] / [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] / [[@1998__IEEECS__SWEBOK Straw Man - Appendix I Draft Classification of Knowledge on Formal Methods]] / [[@2020__OReilly__Building Secure and Reliable Systems - Chapter 13 Testing Code]] - エンティティ: [[ShardStore]] / [[James Bornholt]] / [[Amazon Web Services]] - 概念: [[システムモデルと安全性・活性]] / [[TLA+]] / [[障害注入]]（DST という相補的な経験的検証技法）/ [[形式手法]] / [[モジュラー検証]](性質を分解し専用の検証手法を割り当てる設計思想を別領域(ネットワークアーキテクチャ)で共有する姉妹概念) ## 出典 - [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]] - [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]]「System Model and Reality」「Formal Methods and Randomized Testing」 - Bourque, P. et al., *Guide to the Software Engineering Body of Knowledge – A Straw Man Version*, IEEE Computer Society, 1998, Appendix I. - Pamela Zave, Jennifer Rexford, *The Real Internet Architecture*, Princeton University Press, 2024, Chapter 6, §6.3.2.2. - Heather Adkins et al. (eds.), *Building Secure and Reliable Systems*, O'Reilly Media, 2020, Chapter 13(§Formal Methods, 引用元: Chudnov, Andrey et al. 2018. "Continuous Formal Verification of Amazon s2n").