Au sommet des chercheurs Web3, le professeur de Yale révèle un nouveau modèle de sécurité du protocole de consensus

Lors du récent sommet des chercheurs Web3 de 2025, le professeur Shao Zhong du département d'informatique de l'université de Yale a donné un discours captivant, présentant le modèle LiDO et le cadre d'extension LiDO-DAG développés par son équipe. Cette réalisation innovante vise à fournir une sécurité et une preuve de vivacité vérifiables mécaniquement pour le protocole de consensus Byzantine Fault Tolerance (BFT) complexe, établissant ainsi une base technique solide pour le développement de la fiabilité et de l'évolutivité de l'écosystème Web3.

Le professeur Shao Zhong a souligné lors de sa présentation que, bien que les protocoles de consensus existants (tels que PBFT, Jolteon) soient largement utilisés, leur complexité d'implémentation cache souvent des vulnérabilités de sécurité potentielles. Pour résoudre ce problème, le modèle LiDO a proposé un cadre de vérification en trois couches innovant :

1. Couche d'abstraction de sécurité : mapper le protocole en une machine d'état linéarisée, assurant la cohérence des journaux ;
2. Couche de garantie active : introduction du mécanisme "Pacemaker", qui résout le problème de latence du réseau par la diffusion de dépassement de délai et la synchronisation des tours ;
3. Couche d'extension DAG : prend en charge des protocoles DAG émergents tels que Narwhal et Bullshark, réalisant une validation de consensus efficace sans leader.

Actuellement, LiDO a été appliqué avec succès au protocole industriel Jolteon (BFT à deux étapes) ainsi qu'à plusieurs protocoles DAG, ayant réalisé plus de dix mille lignes de preuves mécaniques Coq. Parmi celles-ci, le volume de code pour la vérification de la sécurité et de l'activité a respectivement atteint 4000 lignes et 1700 lignes. Le professeur Shao Zhong a souligné dans son discours : "Actuellement, les protocoles de consensus PoS font face à la difficulté de concilier la sécurité, l'activité et la décentralisation. Le modèle LiDO est précisément une solution de conception systémique proposée pour briser cette impasse."

Le CertiKOS développé par le professeur Shao Zhong et son équipe a été salué comme un "jalon de la sécurité des systèmes cyber-physiques". C'est le premier système d'exploitation "sans vulnérabilité" au monde ayant fait l'objet d'une vérification formelle. Cet exploit démontre non seulement l'accumulation approfondie de l'équipe dans le domaine de la sécurité des systèmes, mais établit également une solide base technique pour leurs recherches futures. En 2017, le professeur Shao Zhong et son étudiant, le professeur Gu Ronghui, ont conjointement 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écurisée à des actifs cryptographiques d'une valeur de plusieurs centaines de milliards de dollars.

Le modèle LiDO a maintenant terminé sa conception et sa validation formelle, et a commencé à explorer les possibilités 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 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 des écosystèmes 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 véritable avenir décentralisé." Ce point de vue met en lumière sa profonde compréhension des orientations de développement de la technologie Web3, tout en offrant de nouvelles pistes de réflexion sur la sécurité des systèmes blockchain et décentralisés à l'avenir.