Zcash termine la vérification formelle d’Ironwood : 2 700 nouvelles preuves de théorèmes pour un pool de confidentialité sans failles de faux jetons

L’équipe de recherche de Zcash a achevé la vérification formelle du nouveau pool de confidentialité Ironwood, avec une preuve rédigée en langage Lean et comprenant plus de 2 700 théorèmes vérifiés par machine, afin de démontrer que le nouveau pool ne présente aucun bug de « fausse monnaie » indétectable sous ses hypothèses cryptographiques annoncées.
(Contexte : progression récente de la mise à niveau Ironwood de Zcash : plusieurs organisations ont atteint un consensus, la vérification formelle et l’audit avançant en parallèle)
(Ajout de contexte : lancement du client de nœud Zcash Zakura : synchronisation 5 fois plus rapide, avec l’objectif à long terme d’atteindre 50 000 TPS niveau Visa)

Table des matières

Toggle

• Les garanties mathématiques construites à partir de 2 700 théorèmes
• D’Orchard à Ironwood : la voie de mise à niveau de Zcash
• La signification de la vérification formelle : plus rigoureuse que les audits traditionnels

L’équipe de recherche de Zcash a achevé la vérification formelle du nouveau pool de confidentialité Ironwood et a publié, mardi, des preuves vérifiées par machine fondées sur l’annonce officielle de Project Tachyon, confirmant que le nouveau pool ne présente aucun bug de fausse monnaie indétectable dans le cadre des hypothèses cryptographiques revendiquées.

Les garanties mathématiques construites à partir de 2 700 théorèmes

D’après l’annonce de Project Tachyon, cette preuve est rédigée en langage Lean, et comprend plus de 2 700 théorèmes, réalisés en plus d’un mois par trois équipes de recherche et des cryptographes. La preuve établit une propriété de sécurité appelée « intégrité de l’équilibre » (balance integrity), garantissant que le pool de confidentialité ne paie pas plus que la valeur rendue publique à l’entrée.

Les chercheurs indiquent que la preuve couvre le système de preuves à connaissance nulle d’Ironwood, les règles de circuit et la comptabilité au niveau du registre, mais ne comprend pas les garanties de confidentialité indépendantes d’Ironwood.

D’Orchard à Ironwood : la voie de mise à niveau de Zcash

Ironwood est introduit via la mise à niveau NU6.3 de Zcash, dans le but de répondre à une vulnérabilité découverte dans le pool de confidentialité Orchard, qui pourrait théoriquement conduire à des fausses monnaies ZEC indétectables. Les développeurs de Zcash affirment qu’il n’existe actuellement aucune preuve que la vulnérabilité ait été exploitée.

Les fonds passant d’Orchard à Ironwood doivent passer par un point de contrôle comptable public appelé « tourniquet » (turnstile), conçu pour empêcher que n’importe quelles pièces « hypothétiques » en excès n’entrent dans le nouveau pool. À mesure que les fonds quittent Orchard, ce processus fournit aussi de plus en plus d’éléments de preuve, permettant de déterminer si l’ancien pool a déjà été exploité.

La signification de la vérification formelle : plus rigoureuse que les audits traditionnels

La vérification formelle (formal verification) diffère des audits de code traditionnels : ce n’est pas une vérification manuelle ligne par ligne, mais une démonstration mathématique que le code est correct dans toutes les situations possibles. Le langage Lean est un outil très populaire dans le domaine de la vérification formelle ces dernières années, avec des résultats validés dans plusieurs projets cryptographiques.

Cette fois, le travail de vérification formelle de Zcash couvre les composants essentiels d’Ironwood, ce qui signifie que la « comptabilité de base » du nouveau pool de confidentialité bénéficie désormais d’une garantie mathématique, et non d’un simple audit manuel. Pour Zcash, qui vient de traverser un incident de fausse monnaie, il s’agit d’une étape essentielle pour rétablir la confiance du marché.