CBC Casperと形式的検証
こんにちは、R&Dチームの中村(Twitter: nrryuya)です。本日、CBC Casperに関する論文: “Refinement and Verification of CBC Casper”を公開しました。
本論文はCrypto Valley Conference 2019、ポスターはIEEE S&P 2019にアクセプトされました。
CBC Casperは、Ethereumに将来的に導入される可能性があるだけではなく、理論的に美しく、次世代のコンセンサスアルゴリズムとしてたくさんのポテンシャルを秘めたプロトコルです。この記事では、 CBC Casperの基本的な事項と、今回の論文の内容について紹介します。
コンセンサスプロトコルの種類
CBC Casperの説明に入る前に、ブロックチェーンで使われるコンセンサスプロトコルにはどういうものがあるのか、簡単に説明しようと思います。まず、ブロックチェーンのコンセンサスには、(1)ブロックベース (2)チェーンベースの二種類があります。
(1)ブロックベースのコンセンサスの基本アイデアは、ブロック一つ一つに対して、それをチェーンに繋げるか否かコンセンサスをとり、合意に至ればチェーンに繋げ、至らなければスキップして次のブロックを提案させる、というものです。ブロック一つ一つ合意して行くので、基本的にはフォークは起こりません。TendermintやAlgorandなどが有名で、ブロックごとに実行されるコンセンサスアルゴリズムは、pBFTをはじめとする古典的なアルゴリズムに基づいているものが多いです。（ブロックベースという私個人的なものです。BFT-based consensusなどと呼ばれているのも時折目にします。）
一方、(2)チェーンベースのコンセンサスの基本アイデアは、ブロックの合意が確定しないまま各ノードにチェーンを伸ばさせ、その時どのチェーンを伸ばすかのルール（フォークチョイスルール）を適切に設定することで、次第に一つのチェーンに収束させる、というものです。言わずもがな、Bitcoinや現状のEthereumはこれに該当し、マイニングによりブロック生成者を選び、longest-chain rule（一番長いチェーンを伸ばす）をフォークチョイスルールとして採用しています。OuroborosなどPoSのチェーンベースのプロトコルもあります。基本的には、ファイナリティは確率的なものです。
ETH2.0で使われるCasper the Friendly Finality Gadget (FFG)は、チェーンベースのプロトコルに、(1)で使われるようなpBFTライクのプロトコルで決定的ファイナリティを与える仕組み（だからファイナリティガジェットという名前）です。PolkadotのGRANDPAもファイナリティガジェットです。
ちなみに、PoWとPoS、というのは、コンセンサスアルゴリズムの区分ではなく、どうやってシビル耐性を持たせるかという違いです。
それでは、CBC Casperはというと、(2)のチェーンベースのプロトコルになります。しかし、後述するように、決定的ファイナリティを持っています。
CBC Casper
CBC Casperは、EthereumのPoS移行のため、元々はVlad Zamfirにより考案されたコンセンサスアルゴリズムです。最新のホワイトペーパーはこちらです。
CBC Casperの他のプロトコルとの大きな違いとしては、(1) “correct-by-construction”という方法論と、(2)message justificationがあります。
(1) “Correct-by-construction”
元々VladはCasper the friendly GHOST (TFG)という名前で提案をしていました（以前のブログやホワイトペーパー参照）。CBC CasperはCasper TFGを一般化する形で作られ、それ自体は単一のコンセンサスプロトコルではなく、プロトコルを定義するフレームワークのようなものです。具体的には、CBC Casperは、コンセンサスプロトコルを5つのパラメーターにより定義します。
そして、CBC Casperから、具体的なプロトコルを作ることができます。例えば、ブロックチェーンのコンセンサスプロトコルの場合は、C (consensus values)が存在しうる全てのブロックの集合、E (estimator)がフォークチョイスルールになります。（実際には、パラメーターの指定だけではなくバリデータの戦略も定義する必要があります。） また、ブロックチェーン以外のデータ構造を採用することもできます。
“Correct-by-construction”とは、このようにコンセンサスプロトコルを定義した時に、その時点で望ましい性質が満たされているようにする方法論のことです。具体的には、コンセンサスプロトコルが最低限満たすべき二つの性質であるsafety（バリデータが矛盾した意思決定をしないこと）とliveness（バリデータがいつかは意思決定をすること）のうち、safetyに関して、CBC Casperから定義されたプロトコルは全て同じ証明が成立します。Liveness含めその他の性質は、実際に生成されたプロトコルにおいて個別に議論する形になります。
このフレームワークは非常にフレキシブルで、下図にあるような“block-and-vote”のプロトコルから、“vote-by-block”のプロトコルまで表現することができます。したがって、コンセンサスプロトコルにまつわる様々なトレードオフ (例: ファイナリティまでの時間と必要なメッセージ数の関係)を、一つの枠組みで議論することができます。
(2) Message justification
CBC Casperでは、全てのメッセージは justification、つまり、そのメッセージの送信者がそれまでに受け取ったメッセージの集合を含みます。Justificationは基本的にはフォークチョイスの証拠の役割を果たし、全てのメッセージは、それが提案もしくは投票するブロックが、そのメッセージのjustificationに対しフォークチョイスを実行した結果であるように強制されます。(そうでない場合不正なメッセージになります。)
プロトコルに従うvalidatorは、自分がそれまで送ったメッセージをjustificationに含めなければなりません。互いにjustifyしない二つのメッセージを送ることは equivocation (ビザンチン故障の一種)と言われます。Equivocationを検知できることがCBC Casperの特徴の一つで、デポジットをslashするなどにより、equivocationのインセンティブをなくし、その数を抑えることができます。
Equivocationをしないで、それまで伸ばしていた、もしくは投票していたチェーンから別のチェーンに移るには、それが正当であると示す証拠を、次のメッセージに含める必要があるということです。
また、あるバリデータのある時のjustificationは、その後に未来にわたって、そのバリデータのjustificationに含ます。これにより、十分な数のバリデータが、あるブロックの子孫のブロック提案・投票しているのをjustifyした場合、バリデータはそのブロックに「ロック」されることになります。
Equivocationの数がある閾値以下だと仮定することで、一定以上のバリデータがあるブロックにロックされたとき、そのブロックはファイナライズすることになります。こうして、CBC Casperは決定的なファイナリティを持ちます。実際にファイナライズされたブロックを検知するヒューリスティックスは、 safety oracleと呼ばれています。
実際にプロトコルを生成する場合、いつメッセージを送るか、といった、バリデータの戦略を、そのプロトコルがlivenessを持つように定める必要があります。仮説ではありますが、“vote-by-block”のプロトコルにおいては、チェーンが収束することを示すことで、livenessはほとんど示されると考えています。
CBC Casperの利点
ここまで見てきたように、CBC Casperのアドバンテージとしては、(1) 柔軟性 (2) 理論的なシンプルさが挙げられます。
また、ファイナリティの判定において、equivocationの閾値は各バリデータが自分で決めることができるため、CBC Casperのファイナリティは主観的なものです（ビットコインにおける “6 confirmation” ルールのようなものですが、equivocation fault toleranceは任意の100%に近い値に上げることができます！）。
また、CBC Casperは、Casper FFGとは異なり、finalityのサイクルはブロックごとですので、finalityのレイテンシはより早いと言えます。
CBC Casperをもっと知りたいという方は、Barnabé Monnotによるブログ 及びVitalikのブログがおすすめです。
CBC Casperの形式的検証
今回の論文の主要なコントリビューションは、定理証明支援システムIsabelle/HOLを用いて、CBC Casperに関する各種定理を証明したことです。定理証明支援システムは、論理と数学のIDEのようなもので、ペンと紙で行った証明の間違いを見つけるのを助けてくれるなど、形式的検証の強い味方です。
Isabelle/HOLの証明はオープンソースです。
具体的には、CBC Casperフレームワークの基礎をなすmessage justificationや状態遷移に関する性質の証明、それらを使ったsafety及びsafety oracleの証明を行なっています。
また、今回の論文の目的として、いくつかのドラフトペーパーやブログ記事にまたがっている既存のCBC Casperに関する研究を、学術的なフォーマットで一つの論文に整理するというのもあります。
Future work
現在は、CBC Casperから完全なブロックチェーンのプロトコルを定義し、そのlivenessを証明することに取り組んでいます。
また、Isabelleなどの定理証明システムは、証明で使われる定義からプログラムを生成する機能があり、こちらも研究の方向として興味深いと思っています。この画像はIsabelle/HOLが生成したHaskellコードの一部です。
また、Vladが取り組んでいるシャーディングへの応用も、野心的かつ興味深いです。(Vladによるスライド参照)
CBC Casperは理論的にはとてもシンプルですが、実際に実装するにはいくつかの課題があります。VitalikはETH2.0のbeacon chainの文脈で、CBC Casperをもっと扱いやすくする様々な提案をしています。
Acknowledgment
以上です！CBC Casperの生みの親であるVlad Zamfir, そして、元の論文の他の著者であるNate Rush, Aditya Asgaonkar, Georgios Piliouras, そしてもちろん、Vitalik Buterinに、最大の敬意を払います。
また、CBC Casperの形式化に最初に取り組んだYoichi Hiraiさん、今回Isabelleでの定理証明に関して多大なサポートをくださったYusuke Ishibashiさんにも感謝いたします。
最後に
CBC Casperの研究に興味のある方は、ぜひDMかWantedly経由で気軽に話を聞きに来て下さい！
