アルゴランドをフォーマルに検証：鋼鉄のチェーンを補強（モデリングと安全性） by Runtime Verification
投稿日: 2019年6月18日 投稿者: Musab Alturki, Brandon Moore, Karl Palmskog, Lucas Pena
今年（2019年）初め、Runtime Verificationはアルゴランドのコンセンサス・プロトコルの検証を依頼されました。この取り組みの最初の部分、すなわちプロトコルのモデリングとその安全性定理の証明が成功裏に完了したことを報告します。具体的には、証明アシスタント（Coq）を用いて、プロトコルがフォークしないことが数学的に保証される仮定を系統的に特定しました。
エンゲージメントの概要に入る前に、まずアルゴランドの簡単な紹介をします。アルゴランドは、MIT教授でチューリング賞受賞者のシルビオ・ミカリによって設立され、ブロックチェーン分野で最も強力なチームの1つを構築しています。アルゴランドの中心はアルゴランド・コンセンサス・プロトコルであり、真の分散型でありながら効率的で安全かつスケーラブルな運用を約束するPure PoS（Proof of Stake）プロトコルです。Pure PoSにおける基本的な考え方は、システムの安全性を、特定の小さなサブセットのノードに依存したり、資産をロックしてユーザーにペナルティを与えることなく、誠実なユーザーによって全ステークの超多数が保有されていることのみに依存させることです。アルゴランドのコンセンサス・プロトコルは、スケーラビリティ、分散化、セキュリティの3つを特徴としています。アルゴランドの内部構造に興味のある読者は、アルゴランド・チームがMediumで公開した有益な記事を確認することが推奨されます。
エンゲージメントの概要
ここでは、エンゲージメントのハイレベルな概要のみを説明します。完全な詳細については、以下を参照してください。
プロジェクトに付随する拡張技術報告書
プロジェクトのGithubリポジトリ
この契約では、まずプロトコルのフォーマルなモデルを構築し、プロトコル設計がその要件を満たすための前提条件を突き止めることが必要でした。最高レベルの保証を実現するために、数学者が定理を証明するのと同じように、表現力豊かなフォーマル論理体系の中でシステムをモデル化・仕様化し、検証を行う演繹的検証を選択しました。下図は、システム解析の様々なアプローチを、必要な労力と保証度の関数として表したものです。
アルゴランドのコンセンサス・プロトコルは、一連のラウンドを経て進行します。各ラウンドで、ノードはブロックチェーンに追加するブロックを認証します。ネットワークが分割（partitioned）されている場合、ブロックを認証するためにいくつかの試行（ピリオドと呼ばれる）が必要な場合があります。詳細は、Algorand Blockchain Features Specificationとアルゴランドに関するこのジャーナルペーパーを参照してください。プロトコル自体は、ノード・レベルの動作とネットワーク・レベルの動作（敵対者の動作を含む）の両方を包含しており、プロトコルの関連する特性を表現し検証できるようにするには、かなりの量の詳細をモデル化する必要があることを意味しています。
私たちは、アルゴランド・コンセンサス・プロトコルのモデルをCoqで開発し、その多くの特性を証明しました。そして、最終的に、ネットワークが分割されている（つまり、メッセージ遅延が任意に大きい）場合でも、2つの正直なノードが2つのブロックを認証しないという非同期安全特性を示すために使用されました。このモデルの核となるのはglobal stateの遷移関係です。この関係は、プロトコルのglobal stateが1ステップでどのように別の状態に遷移するかを帰納的に定義するものです。
このモデルにおいて、ある種の事象が発生したことを主張するほとんどの文は、ある条件を満たす可能性のあるトレース上の命題として指定されます。すなわち、state g(i)をi番目のstate、g(i+1)を(i+1)番目のstateとすると、g(i)とg(i+1)の順序対はglobal移行関係に属すことになります。このように、パスの性質をトレース上の命題として指定することで、具体的な初期状態（または初期状態の集合）を仮定することなく、その性質が何であるかを一般的に定義することができます。また、性質が成立するために必要な条件は、考慮するトレースの状態に対する制約として指定することができます。
エンゲージメントの成果
本契約の主要な成果は、非同期安全性定理の厳密な形式化と証明です。この定理は、同じラウンドからの2つの証明書は同じブロックのためのものでなければならない、つまり、フォークは許されないと断言します。または、Coqで正式には：
前提条件state_before_round r g0は、ラウンドrにユーザがまだ入っていないときに、トレースが歴史上十分長く遡ることを述べ、is_trace g0 traceは、トレースがg0から始まるglobal stateの有効シーケンスであり、連続状態の各ペアがglobal遷移関係を満足することを述べていることに注意してください。定理の証明は、それ自体がより小さなレンマに分解された個々の結果に構成されています（合計約170のレンマがある）。
第二の主要な成果は、必要な仮定を正確に規定し、これらの仮定が安全性の成立に十分であることを示したことです。仮定は、設計の実装を展開する際や、実装の上に構築されるシステムで考慮すべき非常に重要なものです。仮定は、有限のノード集合やメッセージ・ペイロードで使用される有限の値集合などのモデル・パラメータとして、またはメッセージ遅延がどのように制限されるかに関する仮定や、ステークスの超多数を保有するノードの誠実さに関する仮定など、より精巧な仮説（または公理）として指定されます。
今後について
我々が開発したモデルは、アルゴランド・コンセンサス・プロトコルのダイナミクスを、我々が検証した性質と直交する形で捉えた汎用的なものです。つまり、このモデルは非同期安全性以外のシステムの他の特性、特に重要なのはliveness（すなわち、ブロックが毎ラウンド認証されること）を検証するために容易に使用することができます。実際、プロトコルについて示され、安全性の証明に使用された小さな結果の多くは、liveness証明の努力に不可欠な要素を構成すると予想されます。
このプロジェクトでは、アルゴランドの専門家（Jing Chen、Nickolai Zeldovich、Victor Luchangco）と協働することができました。
元記事：https://runtimeverification.com/blog/formally-verifying-algorand-reinforcing-a-chain-of-steel-modeling-and-safety
Comments