Web3学者峰会：イェール大学の教授がLiDOモデルを公開し、コンセンサスのプロトコルの安全性向上を支援

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企業とエコシステムの長期的な発展戦略をより良くサポートすることを目指していると述べました。

講演の終了時に、邵中教授は次のように強調しました："信頼でき、安全で、検証可能なネットワークプロトコルスタックは、真の分散型未来への重要な道筋となるでしょう。"この見解は、Web3技術の発展と安全保障を推進する上でのLiDOモデルの重要性を強調しています。

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