本日開催されたWeb3 Scholars Conference 2025において、イェール大学のコンピュータサイエンス教授でありCertiKの共同創設者でもあるZhong Shao氏が「改良ベースの合意プロトコルのセキュリティと生存証明：LiDOとその拡張」と題した基調講演を行い、彼のチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを初めて公開しました。この画期的な成果は、複雑なビザンチン フォールト トレラント (BFT) コンセンサス プロトコルに機械化された検証可能なセキュリティと生存証明を提供し、Web3 エコシステムの信頼性とスケーラビリティの技術的基盤を築くことを目的としています。
この講演で、Shao Zhong教授は、既存のコンセンサスプロトコル（PBFTやJolteonなど）は広く使用されているものの、実装が複雑なため潜在的な脆弱性が隠れていることが多いと指摘しました。この問題を解決するために、LiDO モデルは革新的な 3 層の改良検証フレームワークを提案します。
- セキュリティ抽象化レイヤー: ログの一貫性 (セキュリティ) を確保するためにプロトコルを線形化されたステート マシンにマッピングします。
- アクティブ性保証レイヤー: タイムアウト ブロードキャストとラウンド同期を通じてネットワーク遅延の問題を解決する「Pacemaker」メカニズムを導入します。
- DAG 拡張レイヤー: Narwhal や Bullshark などの新しい DAG プロトコルをサポートし、リーダーレス コンセンサスの効率的な検証を実現します。
現在、LiDO は産業グレードのプロトコル Jolteon (2 段階 BFT) と複数の DAG プロトコルに正常に適用されており、10,000 行を超える Coq コードの機械化証明を完了しており、セキュリティ検証コードと活性検証コードはそれぞれ 4,000 行と 1,700 行に達しています。 「現在、PoSコンセンサスプロトコルは一般的に、セキュリティ、アクティビティ、分散化を同時に達成することが難しいというジレンマに直面しています」とShao Zhong教授は講演の中で指摘した。 「LiDO モデルは、このジレンマを打破するために提案された体系的な設計ソリューションです。」
シャオ・ジョン教授とそのチームによって開発されたCertiKOSは、正式な検証に合格した世界初の「脆弱性のない」オペレーティングシステムであり、「サイバーフィジカルシステムのセキュリティにおける画期的な出来事」として称賛されています。この成果は、セキュリティ企業 CertiK の技術的基礎を築いただけでなく、システム セキュリティ分野における同社の多大な蓄積を証明するものでもあります。近年、Shao Zhong教授はブロックチェーンのセキュリティに深く関わっています。 2017年、彼は弟子の顧栄輝教授とともにCertiKを共同設立し、スマートコントラクトとオンチェーンプロトコルのセキュリティに形式検証技術を導入し、数千億ドル相当の暗号資産のセキュリティを保護しました。
LiDOは現在、モデル設計と形式検証を完了しており、主流のパブリックチェーンや分散型プロトコルとの統合の可能性を検討し始めています。邵中教授は、CertiKはWeb3.0の主要メカニズムを検証し、フルサイクルの製品とサービスを提供して、Web3企業とエコシステムの長期的開発戦略をよりよくサポートすることに尽力していると述べた。スピーチの最後に、Shao Zhong教授は次のように強調しました。「信頼性が高く、安全で、検証可能なネットワーク プロトコル スタックは、真に分散化された未来への重要な道となるでしょう。」
