Web3学者サミットでイェール大学の教授が初めてLiDOモデルを公開

本日、2025 Web3 Scholars Summitが開催され、イェール大学コンピュータサイエンス学部のShao Zhong教授が「Proof of Security and Activity of Consensus Protocols Based on Refinement: LiDO and Its Extensions」と題した基調講演を行いました。 彼は初めて、彼のチームが開発した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モデルを初めて公開しました