Zcash termine la vérification formelle d’Ironwood et publie la suppression des faux risques liés à la falsification de ZEC via le théorème de Lean

Le programme Tachyon de Zcash a annoncé le 29 juillet avoir achevé la validation formelle du pool d’écran Ironwood, et publié une preuve de validation assistée par machine, comprenant plus de 2 700 théorèmes rédigés avec le langage de programmation Lean. Cette vérification a établi une propriété de sécurité appelée « intégrité des soldes », en écartant efficacement, dans le cadre de ses hypothèses cryptographiques établies, la possibilité de failles de falsification indétectables pour Ironwood.

Validation formelle terminée pour le programme Tachyon : plus de 2 700 théorèmes Lean

Le travail de validation formelle du programme Tachyon a été réalisé en collaboration par trois chercheurs et une équipe de cryptographes, sur une durée d’un peu plus d’un mois ; la preuve de validation assistée par machine publiée au final contient plus de 2 700 théorèmes, tous rédigés avec le langage de programmation Lean. L’enjeu de cette vérification réside dans le fait qu’il s’agit d’une « validation assistée par machine » — c’est-à-dire que l’ordinateur vérifie automatiquement la justesse de chaque étape logique, plutôt que de s’appuyer uniquement sur une revue manuelle, ce qui apporte une certitude plus élevée.

Tachyon indique que la validation achevée établit une garantie mathématique selon laquelle le pool d’écran Ironwood ne contient pas de failles de falsification indétectables dans le cadre de ses hypothèses cryptographiques établies.

Propriété de sécurité « intégrité des soldes » : une garantie mathématique contre les paiements excédentaires du pool protégé

« Intégrité des soldes (Balance Integrity) » est la propriété de sécurité centrale établie par cette validation formelle, dont la définition mathématique est la suivante : le montant payé par le pool d’Ironwood protégé ne dépassera pas le montant déposé publiquement. Pour réaliser cette propriété, les composants inclus dans le travail de vérification sont les suivants :

· Le système de preuves à connaissance nulle (ZK) d’Ironwood

· Règles de circuit : les règles de calcul de base qui constituent la logique d’Ironwood

· Comptabilité au niveau du registre : mécanisme de suivi et de tenue de registres des fonds à l’échelle de l’ensemble de la couche réseau

À noter que cette preuve ne couvre pas les mécanismes de protection de confidentialité indépendants d’Ironwood ; les chercheurs indiquent que la protection de la confidentialité constitue une propriété de sécurité distincte, nécessitant une validation séparée.

Contexte de la faille d’Orchard et mécanisme comptable public de « porte tournante »

La cause directe de la mise en place du pool d’écran Ironwood est la faille découverte dans le pool de sécurité Orchard — une faille qui, en théorie, pourrait empêcher la détection d’actions de falsification de ZEC, mettant ainsi en danger l’intégrité de l’offre de Zcash. Zcash a introduit Ironwood dans la mise à niveau de la version NU6.3 ; les développeurs indiquent ne pas avoir trouvé de preuve que des failles aient été effectivement exploitées, et le nouveau pool d’écran vise à rétablir la confiance du public dans l’intégrité de l’offre de Zcash.

Les fonds transférés d’Orchard doivent passer par un point de contrôle comptable public appelé « porte tournante (Revolving Door) », afin d’empêcher l’entrée de tout jeton excédentaire hypothétique dans Ironwood ; à mesure que les fonds continuent de quitter Orchard, ce processus pourrait également fournir progressivement davantage de preuves permettant d’évaluer si l’ancien pool a déjà été abusé.

Questions fréquentes

Combien de théorèmes la validation formelle d’Ironwood du programme Tachyon contient-elle et quels outils ont été utilisés pour la réaliser ?

D’après l’annonce du programme Tachyon, cette validation formelle contient plus de 2 700 théorèmes, tous rédigés avec le langage de programmation Lean ; elle a été réalisée en un peu plus d’un mois par trois chercheurs et une équipe de cryptographes ; le résultat final est une preuve mathématique validée par machine, dans laquelle l’ordinateur vérifie automatiquement chaque étape logique.

Que garantit concrètement la propriété de sécurité « intégrité des soldes » ?

« Intégrité des soldes » garantit que le montant payé par le pool d’Ironwood protégé ne dépasse pas le montant déposé publiquement ; cette validation couvre tous les composants nécessaires pour réaliser cette propriété, y compris le système de preuves à connaissance nulle d’Ironwood, les règles de circuit et la comptabilité au niveau du registre ; toutefois, cette validation ne couvre pas les mécanismes de protection de confidentialité indépendants d’Ironwood.

Pourquoi Zcash doit-il introduire Ironwood, et la faille d’Orchard a-t-elle déjà été exploitée ?

Ironwood a été introduit par Zcash dans la mise à niveau de la version NU6.3 afin de répondre à une faille découverte dans le pool de sécurité Orchard — une faille qui, en théorie, pourrait empêcher la détection d’actions de falsification de ZEC ; les développeurs de Zcash indiquent ne pas avoir trouvé de preuve que cette faille ait été effectivement exploitée, et le nouveau pool d’écran vise à rétablir la confiance du public dans l’intégrité de l’offre de Zcash.