Le professeur de Yale dévoile pour la première fois le modèle LiDO lors du sommet des chercheurs Web3

La conférence des chercheurs Web3 de 2025 se tient aujourd'hui, le professeur Shao Zhong du département d'informatique de l'université de Yale a présenté un discours principal intitulé "Preuve de sécurité et de vivacité des protocoles de consensus affinés : LiDO et son extension". Il a révélé pour la première fois le modèle LiDO développé par son équipe et le cadre d'extension LiDO-DAG, cette avancée révolutionnaire vise à fournir des preuves de sécurité et de vivacité vérifiables de manière mécanique pour les protocoles de consensus tolérants aux pannes byzantines (BFT), établissant ainsi une pierre angulaire technique pour la fiabilité et le développement à grande échelle de l'écosystème Web3.

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

1. Couche d'abstraction de sécurité : mapper le protocole en une machine à états linéarisée, assurant 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 en cas de dépassement de délai et à la synchronisation des tours ;
3. Couche d'extension DAG : prend en charge les nouveaux protocoles DAG émergents tels que Narwhal et Bullshark, permettant une vérification efficace sans consensus de leader.

Actuellement, LiDO a été appliqué avec succès au protocole de niveau industriel Jolteon (BFT à deux étapes) et à plusieurs protocoles DAG, complétant plus de dix mille lignes de preuves mécaniques de code Coq, avec respectivement 4000 lignes pour la vérification de la sécurité et 1700 lignes pour la vérification de l'activité. Le professeur Zhao Zhong a souligné lors de sa présentation : "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 proposition de conception systématique visant à briser cette impasse."

En tant que développeur de CertiKOS, le premier système d'exploitation "sans vulnérabilités" au monde vérifié formellement, le professeur Shao Zhong a accumulé une vaste expérience dans le domaine de la sécurité des systèmes. Cet accomplissement a été qualifié de "jalon dans la sécurité des systèmes cyber-physiques". Ces dernières années, le professeur Shao Zhong a réorienté ses recherches vers la sécurité des blockchains, et en 2017, il a cofondé une entreprise de sécurité avec son disciple, le professeur Gu Ronghui, introduisant la technologie de vérification formelle pour garantir la sécurité des contrats intelligents et des protocoles on-chain, fournissant une protection sécuritaire pour des actifs cryptographiques de plusieurs milliards de dollars.

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

À la fin de son discours, le professeur Shao Zhong a souligné : "Un ensemble de protocoles réseau fiable, sécurisé et vérifiable sera la clé pour accéder à un véritable avenir décentralisé."