Au sommet des chercheurs Web3, le professeur de Yale partage les avancées de la recherche sur la sécurité des protocoles de consensus

Lors du sommet des chercheurs Web3 de 2025, le professeur Zhao Zhong du département d'informatique de l'université de Yale a donné un discours intitulé « Preuves de sécurité et d'activité sur les protocoles de consensus affinés : LiDO et son cadre d'extension ». Il a présenté pour la première fois le modèle LiDO développé par son équipe ainsi que le cadre d'extension LiDO-DAG. Cette avancée révolutionnaire vise à fournir des preuves de sécurité et d'activité vérifiables mécaniquement pour des protocoles de consensus tolérants aux pannes byzantines (BFT), é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é lors de sa conférence que les protocoles de consensus existants (comme PBFT, Jolteon), bien qu'ils soient largement utilisés, cachent souvent des vulnérabilités potentielles en raison de leur complexité de mise en œuvre. Pour résoudre ce problème, le modèle LiDO propose de manière innovante un cadre de vérification en trois couches :

1. Couche d'abstraction de sécurité : mapper le protocole en une machine à états linéarisée, garantissant 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 à la diffusion des délais et à la synchronisation des tours ;
3. Couche d'extension DAG : prise en charge 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, complétant la preuve mécanique de plus de dix mille lignes de code Coq, avec des quantités de code de vérification de sécurité et d'activité atteignant respectivement 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 sécurité, activité et décentralisation. Le modèle LiDO est précisément une solution de conception systématique proposée pour surmonter cette difficulté."

Il convient de noter que le professeur Shao Zhong et son équipe ont développé CertiKOS, le premier système d'exploitation "sans faille" au monde ayant fait l'objet d'une vérification formelle, salué comme un "jalon de la sécurité des systèmes cyber-physiques". Cet exploit a non seulement établi son accumulation solide 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é des blockchains. En 2017, le professeur Shao Zhong et son élève le professeur Gu Ronghui ont introduit la technologie de vérification formelle dans le domaine de la garantie de sécurité des contrats intelligents et des protocoles on-chain, fournissant un soutien important à la sécurité des actifs cryptographiques.

LiDO a actuellement terminé la conception du modèle et la vérification formelle, et a commencé à explorer 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'efforcent de vérifier les mécanismes clés dans Web3.0, afin de fournir des produits et des services sur tout le 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 protocoles réseau fiable, sécurisée et vérifiable sera la clé du chemin vers un véritable avenir décentralisé."