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プロトコルに成功裏に適用され、1万行を超えるCoqコードの機械的証明を完了し、安全性と活性の検証コード量はそれぞれ4000行と1700行に達しています。邵中教授は講演の中で次のように指摘しました："現在、PoSコンセンサスプロトコルは一般的に安全性、活性、分散化の三者を同時に満たすことが難しいというジレンマに直面しています。LiDOモデルはまさにこのジレンマを打破するために提案された体系的な設計方案です。"

邵中教授が率いるチームが開発したCertiKOSは、世界初の形式的検証を通じて「バグのない」オペレーティングシステムであり、「サイバー物理システムの安全性におけるマイルストーン」と称賛されています。この成果は、セキュリティ分野での技術的基盤を確立するだけでなく、システムセキュリティ分野における深い蓄積をも示しています。近年、邵中教授はブロックチェーンセキュリティに注力し、2017年に弟子の顧荣辉教授と共にブロックチェーンセキュリティ会社を設立し、形式的検証技術をスマートコントラクトとオンチェーンプロトコルのセキュリティ保証に導入し、数十億ドル規模の暗号資産の安全を守っています。

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

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