Web3学者峰会上耶鲁教授分享コンセンサスプロトコル安全性新モデル

最近、2025年Web3学者サミットが予定通り開催されました。会議では、イェール大学コンピュータサイエンス学科の教授である邵中が、「細化されたコンセンサスプロトコルの安全性と活性証明：LiDOおよびその拡張」に関する基調講演を行い、初めてそのチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを一般に紹介しました。この革新的な成果は、複雑なビザンチン耐障害（BFT）コンセンサスプロトコルに対して機械的に検証可能な安全性と活性証明を提供することを目的としており、Web3エコシステムの信頼性とスケーラビリティの発展に技術基盤を築くものです。

邵中教授は講演の中で、既存のコンセンサスプロトコル（PBFT、Jolteonなど）が広く利用されているにもかかわらず、その実装の複雑さから潜在的な脆弱性を隠していることを指摘しました。この問題を解決するために、LiDOモデルは革新的な三層の細分化検証フレームワークを提案しました：

1. セキュリティ抽象層：プロトコルを線形化された状態機械にマッピングし、ログの一貫性（安全性）を確保する；
2. 活性保障層："Pacemaker"メカニズムを導入し、タイムアウトブロードキャストとラウンド同期でネットワーク遅延問題を解決する；
3. DAG拡張層：Narwhal、Bullsharkなどの新興DAGプロトコルをサポートし、リーダーなしのコンセンサスによる効率的な検証を実現します。

現在、LiDOは産業レベルのプロトコルJolteon（二段階BFT）および複数のDAGプロトコルに成功裏に適用され、10,000行を超えるCoqコードの機械的証明を完了しました。その中で、安全性と活性の検証のコード量はそれぞれ4,000行および1,700行に達します。邵中教授は講演で次のように強調しました："現在、PoSコンセンサスプロトコルは安全性、活性、非中央集権の三者を同時に満たすことが難しいというジレンマに直面しています。LiDOモデルは、このジレンマを打破するために提案された体系的設計案です。"

言及すべきは、邵中教授が率いるチームが以前に開発したCertiKOSであり、これは世界初の形式的検証を通じて"脆弱性のない"オペレーティングシステムであり、"ネットワーク物理システムの安全性のマイルストーン"と称賛されています。この成果は、システムセキュリティ分野における深い蓄積を示すだけでなく、その後のブロックチェーンセキュリティ分野での研究の基盤を築くものです。2017年、邵中教授と彼の弟子である顧荣辉教授は共同で形式的検証技術をスマートコントラクトとオンチェーンプロトコルのセキュリティ保証分野に導入し、数千億ドル規模の暗号資産に安全保障を提供しました。

LiDOモデルは現在、設計と形式的検証を完了し、主流のパブリックチェーンおよび分散型プロトコルとの統合の可能性を探求し始めています。邵中教授は、Web3.0における重要なメカニズムの検証に取り組んでおり、全周期の製品とサービスを提供し、Web3企業とエコシステムの長期的な発展戦略をより良くサポートすることを目指しています。講演の終わりに、邵中教授は強調しました："信頼できる、安全で、検証可能なネットワークプロトコルスタックは、真の分散型未来への重要な道筋となるでしょう。"

! CertiKの共同創設者であるShao Zhong教授は、Web3 Scholars Summitに出席し、LiDOモデルを初めて公開しました