Points forts du sommet des chercheurs Web3 : Modèle de vérification de la sécurité du nouveau protocole de consensus rendu public pour la première fois

Lors du sommet des académiciens Web3 de 2025 qui s'est tenu récemment, un professeur du département d'informatique de l'université de Yale a prononcé un discours intitulé "Sécurité et preuve d'activité des protocoles de consensus affinés : LiDO et son cadre d'extension". Il a présenté pour la première fois au public le modèle LiDO développé par son équipe et le cadre d'extension LiDO-DAG. Cette innovation vise à fournir une sécurité et une preuve d'activité vérifiables mécaniquement pour des protocoles de consensus Byzantine Fault Tolerance (BFT) complexes, établissant ainsi une base technique pour le développement de la fiabilité et de l'évolutivité de l'écosystème Web3.

Lors de son discours, le professeur a souligné que, bien que les protocoles de consensus existants (tels que PBFT, Jolteon) soient largement utilisés, leur complexité de mise en œuvre entraîne souvent des risques de sécurité potentiels. Pour résoudre ce problème, le modèle LiDO a innové en proposant un cadre de vérification à trois niveaux.

1. Couche d'abstraction de sécurité : mapper le protocole à une machine d'état linéarisée, assurant la cohérence des journaux (sécurité) ;
2. Couche de garantie active : introduction du mécanisme "Pacemaker", qui résout les problèmes de latence réseau grâce à des diffusions de dépassement de délai et à une synchronisation des tours ;
3. Couche d'extension DAG : prend en charge les nouveaux protocoles DAG émergents tels que Narwhal et 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écaniques en Coq, dont la quantité de code pour la vérification de la sécurité et de l'activité atteint respectivement 4 000 et 1 700 lignes. Le conférencier a souligné : "Actuellement, les protocoles de consensus PoS font face à la difficulté de concilier sécurité, activité et décentralisation. Le modèle LiDO est justement une proposition de conception systémique pour surmonter cette limitation."

Ce professeur a dirigé une équipe qui a développé le premier système d'exploitation "sans faille" CertiKOS au monde grâce à la vérification formelle, salué comme un "jalon de la sécurité des systèmes cyber-physiques". Cet accomplissement a non seulement jeté les bases techniques de la société de sécurité qu'il a fondée par la suite, mais a également démontré son expertise dans le domaine de la sécurité des systèmes. Ces dernières années, il a concentré ses recherches sur la sécurité de la blockchain, s'efforçant d'appliquer 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 plusieurs centaines de milliards.

LiDO a actuellement achevé la conception du modèle et la vérification formelle, et commence à explorer les possibilités d'intégration avec les principales chaînes publiques et les protocoles décentralisés. Le conférencier a déclaré qu'ils s'engagent à valider les mécanismes clés dans Web3.0 pour fournir des produits et 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 la présentation, il a souligné : "Une pile de protocoles réseau fiable, sécurisée et vérifiable sera le chemin clé vers un véritable avenir décentralisé."