4月8日、香港で開催された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コンセンサスプロトコルは一般的に、セキュリティ、アクティビティ、分散化を同時に達成するのが難しいというジレンマに直面しています」とシャオ・ジョン教授は講演の中で指摘した。 「LiDOモデルは、このジレンマを打破するために提案された体系的な設計ソリューションです。」
シャオ・ジョン教授とそのチームによって開発されたCertiKOSは、正式な検証に合格した世界初の「脆弱性のない」オペレーティングシステムであり、「サイバーフィジカルシステムのセキュリティにおける画期的な出来事」として称賛されています。この成果は、セキュリティ企業であるCertiKの技術的基礎を築いただけでなく、システムセキュリティ分野における同社の多大な蓄積を証明するものでもあります。近年、Shao Zhong教授はブロックチェーンのセキュリティに深く関わっています。 2017年に弟子の顧栄輝教授とともにCertiKを共同設立し、スマートコントラクトとオンチェーンプロトコルのセキュリティに形式検証技術を導入し、数千億ドル相当の暗号資産のセキュリティを保護しました。
LiDOは現在、モデル設計と形式検証を完了しており、主流のパブリックチェーンや分散型プロトコルとの統合の可能性を検討し始めています。邵中教授は、CertiKはWeb3.0の主要メカニズムを検証し、Web3企業とエコシステムの長期的な開発戦略をより良くサポートするためのフルサイクルの製品とサービスを提供することに尽力していると語った。スピーチの最後に、Shao Zhong教授は「信頼性が高く、安全で、検証可能なネットワーク プロトコル スタックが、真に分散化された未来への重要な道となるだろう」と強調しました。
