Lors du sommet des chercheurs Web3, le professeur Shao Zhong a présenté le modèle LiDO, promouvant la vérification de la sécurité du protocole de consensus.

La conférence des chercheurs Web3 de 2025 s'est tenue récemment, le professeur Shao Zhong du département d'informatique de l'université de Yale a présenté un discours intitulé "Sécurité et preuve d'activité des protocoles de consensus affinés : LiDO et son extension". Il a dévoilé pour la première fois le modèle LiDO développé par son équipe et le cadre d'extension LiDO-DAG, cette réalisation révolutionnaire vise à fournir des preuves de sécurité et d'activité vérifiables de manière mécanisée pour les protocoles de consensus tolérants aux pannes byzantines (BFT) complexes, établissant ainsi une base technique pour la fiabilité et le développement à grande échelle de l'écosystème Web3.

Le professeur Shao Zhong a souligné dans son discours que les protocoles de consensus existants tels que PBFT et Jolteon, bien que largement utilisés, cachent souvent des vulnérabilités potentielles en raison de leur complexité d'implémentation. Pour résoudre ce problème, le modèle LiDO propose de manière innovante un cadre de validation en trois couches :

1. Couche d'abstraction de sécurité : mapper le protocole en une machine d'état linéaire, garantir la cohérence des journaux (sécurité) ;
2. Couche de garantie active : introduction du mécanisme "Pacemaker" pour résoudre le problème de latence réseau grâce à une diffusion par dépassement de délai et à la synchronisation des tours ;
3. Couche d'extension DAG : supporte les 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 dix mille lignes de code Coq pour la preuve mécanisée, dont les volumes de code pour la vérification de la sécurité et de l'activité atteignent respectivement 4000 lignes et 1700 lignes. Le professeur Zhao Zhong a souligné : "Actuellement, les protocoles de consensus PoS font face à la difficulté d'atteindre simultanément la sécurité, l'activité et la décentralisation. Le modèle LiDO est précisément une solution de conception systématique proposée pour surmonter ce goulot d'étranglement."

En tant que principal développeur de CertiKOS, le premier système d'exploitation "sans faille" au monde ayant passé une vérification formelle, le professeur Shao Zhong a accumulé une expérience approfondie dans le domaine de la sécurité des systèmes. Cet accomplissement a non seulement jeté des bases solides pour ses recherches ultérieures, mais a également mis en lumière sa contribution exceptionnelle dans le domaine de la sécurité des systèmes. Ces dernières années, le professeur Shao Zhong a recentré ses recherches sur la sécurité blockchain et a cofondé en 2017 une entreprise de sécurité avec des partenaires, consacrée à l'application de la technologie de vérification formelle à la protection de la sécurité des contrats intelligents et des protocoles en chaîne, fournissant une protection sécuritaire pour des actifs cryptographiques d'une valeur de milliers de milliards.

Le modèle LiDO a maintenant terminé sa conception et sa validation formelle, et a commencé à explorer la possibilité d'intégration avec les principales chaînes publiques et les protocole décentralisés. Le professeur Shao Zhong a déclaré qu'ils s'engagent à valider les mécanismes clés dans le Web3.0 pour fournir des produits et des services sur l'ensemble du cycle, afin 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é."