Sommet des chercheurs Web3 : un professeur de Yale dévoile le modèle LiDO, contribuant à l'amélioration de la sécurité du protocole de consensus

Lors du sommet des chercheurs Web3 de 2025, le professeur Shao Zhong du département d'informatique de l'université de Yale a donné un discours principal intitulé « Preuves de sécurité et d'activité des protocoles de consensus raffinés : LiDO et son extension ». Il a présenté pour la première fois le modèle LiDO et le cadre d'extension LiDO-DAG développés par son équipe. Ce résultat innovant vise à fournir des preuves de sécurité et d'activité vérifiables mécaniquement pour des protocoles de consensus Byzantine Fault Tolerant (BFT) complexes, établissant une base technique pour le développement de la fiabilité et de l'évolutivité de l'écosystème Web3.

Le professeur Shao Zhong a souligné dans son discours que, bien que les protocoles de consensus existants (comme PBFT, Jolteon) soient largement utilisés, leur complexité de mise en œuvre présente souvent des vulnérabilités de sécurité potentielles. Pour résoudre ce problème, le modèle LiDO a proposé un cadre innovant de vérification en trois couches :

1. Couche d'abstraction sécurisée : mapper le protocole en tant qu'état linéarisé, garantissant la cohérence des journaux (sécurité).
2. Couche de garantie d'activité : introduction du mécanisme "Pacemaker", qui résout le problème de latence réseau par diffusion de dépassement de délai et synchronisation des tours.
3. Couche d'extension DAG : support des nouveaux protocoles DAG tels que Narwhal, Bullshark, permettant une validation efficace du consensus sans leader.

Actuellement, LiDO a été appliqué avec succès au protocole industriel Jolteon (BFT à deux étapes) et à plusieurs protocoles DAG, ayant complété plus de 10 000 lignes de preuves mécanisées en Coq, dont le volume de code pour la vérification de la sécurité et de l'activité atteint respectivement 4 000 lignes et 1 700 lignes. Le professeur Shao Zhong a souligné dans son discours : "Actuellement, les protocoles de consensus PoS font face à la difficulté de concilier sécurité, activité et décentralisation. Le modèle LiDO est précisément une solution de conception systématique proposée pour briser ce dilemme."

Il convient de noter que le professeur Zhao Zhong a précédemment dirigé une équipe pour développer CertiKOS, le premier système d'exploitation "sans vulnérabilités" au monde validé par des vérifications formelles, salué comme un "jalon pour la sécurité des systèmes cyber-physiques". Cet accomplissement a non seulement établi son expertise dans le domaine de la sécurité des systèmes, mais a également fourni une base solide pour les recherches ultérieures sur la sécurité blockchain. En 2017, le professeur Zhao Zhong et son étudiant, le professeur Gu Ronghui, ont introduit la technologie de vérification formelle dans le domaine de la sécurité des contrats intelligents et des protocoles en chaîne, offrant une protection sécuritaire pour des actifs cryptographiques d'une valeur de plusieurs milliards de dollars.

Le modèle LiDO a actuellement terminé sa conception et sa vérification formelle, et explore la possibilité d'intégration avec les principales chaînes publiques et les protocoles décentralisés. Le professeur Shao Zhong a déclaré qu'ils s'engagent à valider les mécanismes clés dans le Web3.0 afin de fournir des produits et services sur l'ensemble du cycle, et de mieux soutenir la stratégie de développement à long terme des entreprises et de l'écosystème Web3.

À la fin de son discours, le professeur Shao Zhong a souligné : "Une pile de protocole réseau fiable, sécurisée et vérifiable sera le chemin clé vers un avenir véritablement décentralisé." Ce point de vue met en évidence l'importance du modèle LiDO dans le développement de la technologie Web3 et la garantie de la sécurité.