Zcash termine la vérification formelle d’Ironwood : des règles de preuve fondées sur 2 700 théorèmes excluent la contrefaçon indétectable

D’après Project Tachyon, mardi, des chercheurs de Zcash ont achevé la vérification formelle d’Ironwood, en publiant une preuve vérifiée par machine qui montre que le nouveau pool protégé du réseau ne contient pas de bugs de contrefaçon indétectables dans le cadre de ses hypothèses cryptographiques définies.

La preuve, écrite dans le langage de programmation Lean, comprend plus de 2 700 théorèmes et a été finalisée par trois équipes de chercheurs et de cryptographes sur plus d’un mois. Les travaux établissent l’intégrité de l’équilibre, garantissant que le pool protégé ne peut pas verser plus de valeur que celle qui y a été introduite publiquement. La preuve couvre le système de preuve à divulgation nulle d’Ironwood, les règles des circuits et la comptabilité au niveau du registre, bien qu’elle ne traite pas des garanties de confidentialité.