形式的検証を完了
イーサリアム2.0のデポジットコントラクトに関して、エンドツーエンドの形式的検証をクリアしていたことが明らかとなった。デポジットコントラクトは、フェーズ0に当たるビーコンチェーンでステーキングを行うためのコントラクトだ。
今回監査を行なったRuntime Verificationの公表した文書によれば、最新バージョンにて、デポジットコントラクトで発見されたバグは全て報告・承認され、適切に修正が施されたとのことだ。これはデポジット・コントラクトの立ち上げが可能になったことを意味する。
イーサリアム2.0では、コンセンサス・アルゴリズムPoSを利用した「ビーコンチェーン」が導入されるが、そのビーコンチェーンにバリデータ（承認者）としてネットワークに参画するためには、最低限の32ETHをステーキングする必要があるという。
この仕組みを機能させるためには、デポジットコントラクトに各バリデータのステーキングに関する履歴を保存する必要性はあるが、新たにデポジットされる度に、この履歴を更新するには、多大な時間と複雑性を要する。そのため、記録に適したアルゴリズム「インクリメンタル・マークル木・アルゴリズム」が開発され、それが上述のデポジットコントラクトでは利用される。
イーサリアム2.0のセキュリティを担保するためには、このアルゴリズム及びデポジットコントラクトが正しく機能することが必要不可欠とされている。今回、Runtime Verificationにより執り行われた形式的検証は、これらが正しく機能を果たすか否かが確かめられた格好となる。
この形式的検証をクリアしたことにより、イーサリアム2.0のフェーズ0のローンチに向け、また一歩前進したと言えるだろう。
参考：End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
CoinPostの注目記事
