Le 8 avril, lors de la Conférence des chercheurs Web3 2025 (Web3 Scholars Conference 2025) tenue à Hong Kong, le professeur du département d'informatique de l'Université de Yale et co-fondateur de CertiK, Zhao Zhong, a prononcé un discours intitulé « Sécurité et preuve d'activité des protocoles de consensus affinés : LiDO et son cadre d'extension ». C'est la première fois qu'il a présenté le modèle LiDO développé par son équipe ainsi que le cadre d'extension LiDO-DAG. Ce résultat révolutionnaire vise à fournir des preuves de sécurité et d'activité vérifiables de manière mécanique pour des protocoles de consensus complexes tolérants aux fautes byzantines (BFT), établissant ainsi une pierre angulaire technique pour la fiabilité et le développement à grande échelle de l'écosystème Web3.
Dans cette présentation, le professeur Shao Zhong a souligné 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.
Couche d'abstraction de sécurité : mapper le protocole en une machine à états linéarisée, garantissant la cohérence des journaux (sécurité) ;
Couche de garantie active : Introduction du mécanisme "Pacemaker", qui résout le problème de latence du réseau grâce à la diffusion en cas de dépassement de délai et à la synchronisation des tours ;
DAG couche d'extension : prend en charge des protocoles DAG émergents tels que Narwhal, Bullshark, pour réaliser une validation efficace du Consensus sans leader.
À l’heure actuelle, LiDO a été appliqué avec succès au protocole de qualité industrielle Jolteon (BFT à deux étages) et à plusieurs protocoles DAG, complétant la preuve mécanisée de plus de 10 000 lignes de code Coq, avec 4 000 lignes de sécurité et 1 700 lignes de code de vérification d’activité. « À l’heure actuelle, les protocoles de consensus PoS sont généralement confrontés au dilemme de la sécurité, de la viabilité et de la décentralisation », a souligné le professeur Shao Zhong dans son discours. « Le modèle LiDO est une solution de conception systématique pour résoudre ce dilemme. »
CertiKOS, développé par le professeur Shao Zhong et son équipe, est le premier système d’exploitation « sans vulnérabilité » au monde qui a passé avec succès une vérification formelle et a été salué comme une « étape importante dans la sécurité des systèmes cyber-physiques ». Cette réalisation jette non seulement les bases de la technologie de l’entreprise de sécurité CertiK, mais démontre également sa vaste expérience dans le domaine de la sécurité des systèmes. Ces dernières années, le professeur Shao Zhong s’est profondément impliqué dans la sécurité de la blockchain et a cofondé CertiK avec son disciple, le professeur Gu Ronghui, en 2017, introduisant une technologie de vérification formelle dans la sécurité des contrats intelligents et des protocoles on-chain, et escortant la sécurité de centaines de milliards de dollars d’actifs cryptographiques.
LiDO a terminé la conception du modèle et la vérification formelle, et a commencé à explorer la possibilité d’intégration avec les chaînes publiques traditionnelles et les protocoles décentralisés. Le professeur Shao Zhong a déclaré que CertiK s’engageait à vérifier les mécanismes clés du Web3.0 afin de fournir des produits et des services à cycle complet afin de mieux soutenir les stratégies 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 protocoles réseau fiable, sécurisée et vérifiable sera la clé vers un avenir véritablement décentralisé. ”
Le contenu est fourni à titre de référence uniquement, il ne s'agit pas d'une sollicitation ou d'une offre. Aucun conseil en investissement, fiscalité ou juridique n'est fourni. Consultez l'Avertissement pour plus de détails sur les risques.
Le co-fondateur de CertiK, le professeur Shao Zhong, a assisté au sommet des chercheurs Web3 et a présenté pour la première fois le modèle LiDO.
Le 8 avril, lors de la Conférence des chercheurs Web3 2025 (Web3 Scholars Conference 2025) tenue à Hong Kong, le professeur du département d'informatique de l'Université de Yale et co-fondateur de CertiK, Zhao Zhong, a prononcé un discours intitulé « Sécurité et preuve d'activité des protocoles de consensus affinés : LiDO et son cadre d'extension ». C'est la première fois qu'il a présenté le modèle LiDO développé par son équipe ainsi que le cadre d'extension LiDO-DAG. Ce résultat révolutionnaire vise à fournir des preuves de sécurité et d'activité vérifiables de manière mécanique pour des protocoles de consensus complexes tolérants aux fautes byzantines (BFT), établissant ainsi une pierre angulaire technique pour la fiabilité et le développement à grande échelle de l'écosystème Web3.
Dans cette présentation, le professeur Shao Zhong a souligné 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.
Couche d'abstraction de sécurité : mapper le protocole en une machine à états linéarisée, garantissant la cohérence des journaux (sécurité) ;
Couche de garantie active : Introduction du mécanisme "Pacemaker", qui résout le problème de latence du réseau grâce à la diffusion en cas de dépassement de délai et à la synchronisation des tours ;
DAG couche d'extension : prend en charge des protocoles DAG émergents tels que Narwhal, Bullshark, pour réaliser une validation efficace du Consensus sans leader.
À l’heure actuelle, LiDO a été appliqué avec succès au protocole de qualité industrielle Jolteon (BFT à deux étages) et à plusieurs protocoles DAG, complétant la preuve mécanisée de plus de 10 000 lignes de code Coq, avec 4 000 lignes de sécurité et 1 700 lignes de code de vérification d’activité. « À l’heure actuelle, les protocoles de consensus PoS sont généralement confrontés au dilemme de la sécurité, de la viabilité et de la décentralisation », a souligné le professeur Shao Zhong dans son discours. « Le modèle LiDO est une solution de conception systématique pour résoudre ce dilemme. »
CertiKOS, développé par le professeur Shao Zhong et son équipe, est le premier système d’exploitation « sans vulnérabilité » au monde qui a passé avec succès une vérification formelle et a été salué comme une « étape importante dans la sécurité des systèmes cyber-physiques ». Cette réalisation jette non seulement les bases de la technologie de l’entreprise de sécurité CertiK, mais démontre également sa vaste expérience dans le domaine de la sécurité des systèmes. Ces dernières années, le professeur Shao Zhong s’est profondément impliqué dans la sécurité de la blockchain et a cofondé CertiK avec son disciple, le professeur Gu Ronghui, en 2017, introduisant une technologie de vérification formelle dans la sécurité des contrats intelligents et des protocoles on-chain, et escortant la sécurité de centaines de milliards de dollars d’actifs cryptographiques.
LiDO a terminé la conception du modèle et la vérification formelle, et a commencé à explorer la possibilité d’intégration avec les chaînes publiques traditionnelles et les protocoles décentralisés. Le professeur Shao Zhong a déclaré que CertiK s’engageait à vérifier les mécanismes clés du Web3.0 afin de fournir des produits et des services à cycle complet afin de mieux soutenir les stratégies 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 protocoles réseau fiable, sécurisée et vérifiable sera la clé vers un avenir véritablement décentralisé. ”