Web3学者峰会でイェール大学教授がコンセンサスプロトコルの安全性研究の進展を共有

2025年のWeb3学者サミットで、イェール大学コンピュータサイエンス学部の教授であるシャオ・ジョンは、「細化されたコンセンサスプロトコルの安全性と活性証明：LiDOとその拡張」というタイトルの基調講演を行い、彼のチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを初めて公開しました。この画期的な成果は、複雑なビザンチン耐障害（BFT）コンセンサスプロトコルに対して機械的に検証可能な安全性と活性証明を提供することを目的としており、Web3エコシステムの信頼性とスケールアップの発展のための技術的基盤を築くものです。

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

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

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

注目すべきは、邵中教授が率いるチームが開発したCertiKOSが、世界初の形式的検証を通じて「バグのない」オペレーティングシステムであり、「サイバー物理システムの安全性におけるマイルストーン」と評されていることです。この成果は、システムセキュリティ分野における深い蓄積を確立しただけでなく、その後のブロックチェーンセキュリティ研究に対しても強固な基盤を提供しました。2017年、邵中教授とその弟子の顧荣辉教授は、形式的検証技術をスマートコントラクトとオンチェーンプロトコルのセキュリティ保証の分野に導入し、暗号資産の安全性に重要なサポートを提供しました。

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

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