はじめに: Gasper 合意メカニズムの最終性の正式な検証

以太坊爱好者

特邀专栏作者

2020-07-21 05:46

この記事は約4672文字で、全文を読むには約7分かかります

Gasper を形式化し、その主要な 3 つの特性を証明します。

AI要約

展開

Gasper を形式化し、その主要な 3 つの特性を証明します。

編集者注: この記事は以下から引用しましたイーサリアム愛好家 (ID: ethfans)編集者注: この記事は以下から引用しました

イーサリアム愛好家 (ID: ethfans)

Gasper は、ビーコンチェーンプロトコル (次期イーサリアム 2.0 ネットワークの基礎となるプロトコル) によって実装された抽象的なプルーフオブステークプロトコル層です。 Gasper の重要な部分は、一連のファイナリティメカニズムです。これは、トランザクションの耐久性とシステムの中断のない動作が攻撃によって損傷されないことを保証するために使用されます。

Gasper

私たちは、Runtime Verification とイーサリアム財団との長期的な協力における新たなマイルストーンを発表できることを嬉しく思います: 私たちはビーコンチェーンプロトコルをシミュレートおよび検証するための正式なフレームワークを開発し、Gasper のファイナリティの正しさを正式に証明することに成功しました。そして、これらの結果も使用しますビーコンチェーンの Gasper 抽象化実装にもこれらのプロパティがあることを実証します。モデルと証明スクリプトの両方がここにあります。

最初のレベルのタイトル

ビーコンチェーンプロトコルは、イーサリアムの将来のメジャーアップグレード「イーサリアム2.0」の中核となる新しいプルーフオブステークプロトコルセットです。ビーコンチェーンプロトコルでは、参加しているノード (または「検証者」) はすべて、システム内に預金 (ETH の形式での賭け金) を持っています。バリデーターは、ネットワークに「証明書」を送信することで、ブロックの有効性を確認し、さまざまな属性に投票します。ビーコンチェーンプロトコル自体には、バリデーターがブロックチェーンの最新の状態について合意に達するのに役立ついくつかのツールが含まれています。

Gasper は、ビーコンチェーンプロトコルにおけるファイナリティガジェットの抽象的だが正確な説明を提案し、フォーク選択ルールも定義しています。ファイナリティガジェットは、どのブロックが参加者によってファイナライズされたとみなされるかを決定するために使用されます。チェーンが分岐するときのメインチェーン。 Gasper のファイナリティは、「Casper Friendly Finality Gadget (Casper FFG)」論文に由来する概念を一般化し、「ファイナライゼーション」をより一般的な形式にしました。

副題

正当化と最終化

ファイナリティの概念は、「チェックポイントブロック」 (「エポック境界ブロック」とも呼ばれ、エポックの開始時のブロックです) にのみ関連します。検証メッセージの一部は「合理化投票」と呼ばれます。合理化投票では、検証者はソースチェックポイントブロックを後のターゲットチェックポイントブロックに関連付け、検証を開始した検証者が「現在の状態から移行できる」と信じていることを視覚的に示します。ソースチェックポイントから宛先チェックポイントの状態への変換。実際、ジャスティフィケーション投票には、(1) 投票を開始したバリデータ、(2) ソースチェックポイントとそのジャスティフィケーションの高さ、(3) ターゲットチェックポイントとそのジャスティフィケーションの高さが表示されます。

条件が満たされる場合に限り、(1) ソースチェックポイント B0 が合理化されている、(2) 過半数 (つまり、バリデータの少なくとも 2/3) も B0-B1 ソースとターゲットのペアに投票した場合、ターゲットチェックポイント B1 ソースチェックポイント B0 を介して合理化されます。

B0 はオーダー K のファイナリティ (k > 0) を達成し、大多数のバリデーターが B0 をその K 世代の子孫チェックポイント Bk に関連付けた場合に限り、B0 と Bk の間のすべてのチェックポイントがファイナライズされます。ジェネシスブロック自体は合理化されたものであり、最終的なものであると考えられることに注意してください。以下の図は、Gasper における合理化と最終化の概念を示しています。
バリデーターがプロトコルから逸脱して矛盾した投票を提出しようとすると、バリデーターにはペナルティが課され、デポジットの大部分が差し引かれます。ギャスパーは、矛盾した投票を構成するものを定義する 2 つの条件 (スラッシュ条件とも呼ばれます) を定義しています。

サラウンド投票: 検証者によって発行された投票に関連付けられた 2 つのチェックポイントは、検証者によって発行された別の投票の 2 つのチェックポイントの高さ範囲内に正確にあります。

文章

ダブル投票を開始したバリデーターは最初のスラッシュ条件に違反したとみなされ、ラップ投票を開始したバリデーターは 2 番目のスラッシュ条件に違反しました。どちらの場合でも、ルールに違反したバリデーターは多額のデポジットを差し引かれます。

副題
正確性 (正確性のプロパティ)

他の Byzantine Fault Tolerance (BFT) プロトコルと同様に、Gasper プロトコルの基礎となる重要な前提は、大多数の検証者 (2/3 以上、デポジットの金額によって定義される) が正直であり、プロトコルの要件に従うということです。この仮定の下では、Gasper には 2 つの基本的なプロパティがあります。

責任ある安全性: バリデーターの少なくとも 1/3 (デポジット額に関して) がスラッシュされない限り、異なるフォークに属する 2 つのブロックがファイナライズされることはありません。

妥当な生存性: 過去にブロックチェーンに何が起こったとしても、ブロックの最終化プロセスがデッドロックになることはありません。

さらに、バリデーターのセットが動的に変化する環境では (バリデーターがネットワークを離れ、新しいバリデーターが参加すると、アクティブなバリデーターのセットが変化する可能性があります)、3 番目のプロパティは、誰かがプロトコルのルールに違反したときを数値化します。没収できるもの：

スラッシュ可能な限界: バリデータのアクティブ化と終了パラメータ条件を制御するためにプロトコル外の条件を使用できる限り、(セキュリティを破る場合に) スラッシュできるデポジットの量には下限があることが証明できます。

動的バリデータのセット (ビーコンチェーンプロトコルが実装するもの) は、別の困難な問題を引き起こします。システムは、悪意のあるバリデータを確実に罰することができなくなりました。悪意のあるバリデータは、何か悪いことをした後、デポジット前に罰することができるためです。実際にはスラッシュされているため、ネットワークから離れます。スラッシュ可能な下限プロパティにより、アクティブなバリデータセットの可変範囲を調整し、最小限の責任レベルを維持することが可能になります。

ギャスパーのファイナリティを検証する

Gasper は、その正しさを正式に証明するために使用できる、ファイナリティの数学的で正確な記述を提供することを目的としています。この正しさは、ビーコンチェーンプロトコルのセキュリティを証明するための鍵でもあります。イーサリアムプラットフォームは大規模な金融取引システムの株価として使用されることが増えており、セキュリティ保証の前例のない重要性が浮き彫りになっています。

イーサリアム財団と協力して、Coq 証明ヘルパーを使用した動的バリデーターセットの一般条件下で、Gasper のファイナリティメカニズムを形式化しました。この条件の下で、Gasper の 3 つの重要な特性をすべて指摘し、証明します: 責任ある安全性、可能性の生存性、および大幅な下限。すべての証明は同じ Coq モデルを使用します。
ここでは、この成果について簡単に説明するだけです。詳細は次のサイトでご覧いただけます。

プロジェクトに関する技術レポート

プロジェクトの Github リポジトリ

副題

モデリングと検証の方法

最初のステップは、正式に述べ、証明したいすべての重要な特性を表現できるプロトコルのモデルを開発することです。このモデルは、Casper FFG の安全性と稼働性を検証した以前の作業に基づいて構築されています (以前のモデルは、Gasper ファイナリティメカニズムの初期バージョンを定義していました)。

このモデルには 3 つの主要な構造モジュールがあります。

\sum は合計演算子で、stake.[st_fun v] はバリデータ v に対応するステークの量を示します (st_fun は、すべてのバリデータがシステムにステークを持っている必要があると想定しています)。

さらに、動的なバリデーターのセットをシミュレートしたいため、つまり、アクティブなバリデーターのセットがブロックごとに変化する可能性があるため、抽象 (限定された) マッピング vset を宣言します: {fmap Hash -> {set Validator}}, セットが与えられた場合ブロック内のアクティブなバリデーターの数。ここで、 vset と wt を使用して、超多数セットが何であるかを定義できます。

特定のブロックで、アクティブなバリデーターのセットのサブセットの重みがセット全体の重みの 2/3 を超える場合、そのサブセットは絶対多数セットになります。

ブロックツリー。有限タイプのブロックハッシュを使用してブロック Hash:finType をシミュレートし、genesis を使用してジェネシスブロックを表します。チェックポイントブロックツリーをシミュレートするために、ブロックの親子関係 (h1 は h2 の親) を表すために h1 <~ h2 という表記を使用します。

次に、h1 <~* h2 を使用して祖先関係を定義します。h1 は h2 の祖先であり、h2 は h1 の子孫です (h1 と h2 は同じブロックにすることができます)。先祖関係の属性としては、例えば、先祖の先祖も先祖であり、父子関係の属性と同様である。

文章

副題

これらの定義とそれに対応するプロパティに基づいて、ペナルティ条件、クォーラム交差プロパティ、合理化と終了処理など、モデル内の他のすべての構造とプロパティを定義します。たとえば、プロトコル違反が発生した場合にコミュニティを没収するプロパティは、次の抽象メンバーシップ制約を使用して定義できます。

この命題は、グループをスラッシュするということは、いくつかのブロック bL および bR に 2 つの超多数グループ vL および vR が存在することを意味し、これら 2 つのグループの交差部分がスラッシュされたバリデータ (二重投票または囲み投票の開始) であることを示しています。アクティブなバリデーターのセットが常に固定されているという特別な条件下では、これらの超多数セットの共通部分の重みは、すべてのデポジットの少なくとも 1/3 であることに注意してください。

別の例は、ファイナライズ中のフォーク (つまり、セキュリティ違反) の定義です。

この命題は、2 つの矛盾するブロック b1 と b2 が両方とも最終化されることを示しています (b1 も b2 も他方の祖先ブロックではないため)。これら 2 つのブロックは、任意の合理化の高さで任意の長さのチェーンによって完成させることができます。

これらの定義と一連の結果は、説明責任の安全性、可能性のアクティビティ、および大幅な下限の 3 つの定理を指摘および証明するために使用されます。明確にするために、説明責任セキュリティ定理の定式化も次のように再定義します。

定義は単純で、「セキュリティが（ファイナライズされたフォークで）破られた場合、それはバリデータセットがスラッシュされていることを意味するに違いない」と言うだけです。この証明は、ギャスパーによって与えられた非公式な議論を機械化したものであり、なぜフォークが確定するということは、スラッシュ条件の 1 つに違反する 2 つの超多数派のグループが存在し、それらの交差がスラッシュされる必要があることを意味するのかを示しています。