Proving Circuit Functional Equivalence in Zero Knowledge

Cet article présente ZK-CEC, le premier cadre de vérification formelle respectant la vie privée, qui permet de prouver l'équivalence fonctionnelle d'une propriété intellectuelle matérielle secrète par rapport à une spécification publique sans révéler le design, en surmontant les limites des méthodes de simulation et en garantissant la sécurité des preuves à connaissance nulle.

L'essentiel

🕵️‍♂️ Le Dilemme du Constructeur de Châteaux de Sable

Imaginez deux personnages :

1. Le Vendeur (le Prover) : Un architecte génial qui a construit un château de sable unique et complexe. Il veut le vendre, mais il a un secret : il ne veut pas montrer les plans détaillés, car il a peur qu'on lui vole son idée.
2. L'Acheteur (le Verifier) : Un riche collectionneur qui veut acheter le château. Il a une exigence : il veut être absolument certain que le château est solide, qu'il n'y a pas de pièges cachés (des "chevaux de Troie" qui pourraient faire s'effondrer le château plus tard), et qu'il correspond exactement à la maquette publique qu'il a commandée.

Le problème ?

• Si le Vendeur montre les plans, l'Acheteur pourrait les copier (piratage).
• Si le Vendeur ne montre rien, l'Acheteur a peur qu'il ait triché en mettant du sable mouillé à la place du sable dur (arnaques).

Jusqu'à présent, les solutions existaient soit en montrant tout (risque de vol), soit en faisant des tests aléatoires (comme donner un coup de pied au château pour voir s'il tient). Mais un coup de pied ne suffit pas : un piège malin pourrait être caché juste à côté, là où on ne tape pas.

🪄 La Solution Magique : ZK-CEC (Le "Voyageur Invisible")

Les auteurs de cet article, Sirui Shen et ses collègues, ont inventé un nouveau système appelé ZK-CEC. C'est comme un magicien qui peut prouver qu'un secret est vrai sans jamais révéler le secret lui-même.

Voici comment cela fonctionne, étape par étape, avec des analogies :

1. Le "Miroir de Vérité" (La Vérification Formelle)

Au lieu de tester le château au hasard, le système utilise une logique mathématique stricte. Imaginez que vous placez le château du Vendeur à côté d'une maquette officielle (publique).

• Si les deux sont identiques, tout va bien.
• S'il y a une différence, même minuscule, un "miroir magique" (appelé miter circuit) s'allume en rouge.
• Le but est de prouver que ce miroir ne s'allumera jamais, peu importe comment on regarde le château. C'est une garantie mathématique totale, pas juste un test.

2. Le Problème du "Secret" (Pourquoi c'était difficile avant)

Les magiciens précédents (les protocoles de preuve à divulgation nulle de connaissance, ou ZKP) savaient prouver des choses, mais ils avaient un défaut : ils supposaient que la "maquette" était publique.
Si le Vendeur cachait la maquette elle-même, un tricheur aurait pu dire : "Regardez, mon château est parfait par rapport à ma maquette secrète !" alors qu'en réalité, il avait inventé une maquette bidon juste pour l'occasion. Le magicien ne pouvait pas vérifier si la maquette secrète était vraie ou fausse.

3. Le Nouveau Plan (Le "Blueprint")

Les auteurs ont résolu ce problème en divisant le puzzle en deux parties :

• La Partie Publique : La maquette officielle et les règles du jeu (connues de tous).
• La Partie Secrète : Le château du Vendeur (caché).

Leur astuce géniale est de prouver que l'intersection entre la maquette publique et le château secret est impossible à contredire.
Imaginez que le Vendeur doit prouver : "Mon château secret et votre maquette publique sont si parfaitement alignés qu'il est mathématiquement impossible qu'ils soient différents."

Pour éviter la triche, le système vérifie trois choses en secret :

1. La maquette publique est valide (elle existe vraiment).
2. Le château secret est cohérent (il ne s'effondre pas sur lui-même).
3. Ils ne se contredisent que là où ils doivent se rencontrer (les portes et fenêtres), et pas ailleurs.

Si ces trois conditions sont remplies, le magicien peut dire : "Je vous assure à 100% que votre château secret est conforme à la maquette, sans jamais avoir vu un seul grain de sable du château."

🚀 Les Résultats (La Preuve par l'Exemple)

Les chercheurs ont construit ce système (appelé ZK-CEC) et l'ont testé sur des circuits électroniques réels, comme des composants de cryptographie (AES) ou des calculateurs.

• La vitesse : C'est rapide ! Pour des circuits complexes, ils ont réussi à faire la preuve en quelques secondes ou minutes.
• L'optimisation : Ils ont même trouvé un moyen de "compresser" la preuve, comme plier une grande carte pour qu'elle rentre dans une enveloppe, ce qui a rendu le processus jusqu'à 3 fois plus rapide.

💡 En Résumé

Ce papier propose une nouvelle façon de faire confiance dans le monde du matériel informatique.

• Avant : "Montre-moi tout, ou je ne te fais pas confiance." (Guerre entre le secret et la sécurité).
• Avec ZK-CEC : "Je peux te prouver que mon secret est parfait pour toi, sans jamais te montrer mon secret."

C'est comme si un architecte pouvait prouver à un client que son immeuble secret est parfaitement aux normes de sécurité, sans jamais avoir à ouvrir les plans de l'immeuble. Cela permet de construire un marché mondial de puces électroniques plus sûr, où l'on peut acheter des composants sans craindre les virus cachés ni voler les idées des inventeurs.

Résumé technique

1. Problématique et Contexte

L'écosystème moderne des circuits intégrés (CI) repose de plus en plus sur l'intégration de propriété intellectuelle (IP) de tiers (3PIP). Cette pratique introduit des risques de sécurité majeurs, tels que les chevaux de Troie matériels, les portes dérobées et les bogues de conception intentionnels.

Le défi central réside dans le verrou de confiance entre les vendeurs d'IP (qui ne veulent pas révéler leur conception propriétaire) et les intégrateurs de systèmes (qui doivent garantir l'absence de malveillances).

• Limites des solutions existantes : Les méthodes actuelles de vérification préservant la vie privée sont basées sur la simulation (utilisant le chiffrement homomorphe ou des machines virtuelles à connaissance nulle - zkVM). La simulation ne peut pas garantir formellement l'absence de tous les cas limites ou de trojans sophistiqués activés uniquement dans des conditions rares.
• Limites des méthodes formelles : La vérification formelle (comme le Combinational Equivalence Checking ou CEC) offre des garanties mathématiques, mais les protocoles existants à connaissance nulle (comme ZKUNSAT) supposent que la formule logique à vérifier est publique. Si la formule est secrète, un prover malveillant pourrait prouver des propriétés sur une formule falsifiée, brisant la sonorité (soundness) du protocole.

2. Méthodologie : ZK-CEC

Les auteurs proposent ZK-CEC, le premier cadre de vérification formelle préservant la confidentialité pour les circuits matériels. L'approche repose sur la combinaison de la vérification formelle et des preuves à connaissance nulle (ZKP) basées sur l'évaluation linéaire aveugle de vecteurs (VOLE).

A. Le Blueprint (Plan Général)

Pour résoudre le dilemme de la sonorité avec des formules secrètes, les auteurs proposent une nouvelle approche de vérification de propriétés :

1. Séparation des formules : La formule globale est divisée en une partie publique ($\Phi_{pub}$, représentant la spécification et la structure du miter) et une partie secrète ($\Phi_{sec}$, l'implémentation de l'IP).
2. Objectif : Prouver que la conjonction de la formule secrète et de la propriété publique est insatisfiable (UNSAT), c'est-à-dire $\Phi_{sys} \land \Phi_{prop} \models \bot$.
3. Conditions de sonorité : Pour éviter qu'un prover ne falsifie la preuve, le protocole vérifie quatre propriétés critiques :
   • P1 : La partie publique est correcte et satisfiable.
   • P2 : La formule globale (miter) est insatisfiable (prouvée via une preuve de réfutation).
   • P3 : La partie secrète est satisfiable (elle ne contient pas de contradictions internes).
   • P4 : Les variables secrètes et publiques sont isolées, sauf aux interfaces définies (pas de chevauchement non autorisé).

B. Protocole Technique

Le protocole $\Pi_{ZK-CEC}$ est composé de quatre sous-protocoles construits sur des fonctionnalités idéales ZK (basées sur VOLE) :

1. Encodage Polynomial : Les clauses CNF sont encodées comme des polynômes univariés. Les littéraux sont représentés par des racines de ces polynômes. Une opération de vérification de membre (un littéral appartient-il à une clause ?) devient une évaluation polynomiale.
2. $\Pi_{P1}$ (Vérification Publique) : Le vérificateur reconstruit localement les polynômes de la spécification publique et vérifie les engagements (commitments) du prover.
3. $\Pi_{P2}$ (Preuve d'Insatisfiabilité) : Adaptation du protocole ZKUNSAT. Le prover fournit une preuve de réfutation (séquence de résolutions) pour prouver que le circuit miter est insatisfiable. Les clauses intermédiaires sont stockées dans une mémoire en lecture seule (ZK-ROM) pour éviter la révélation de l'ordre de calcul.
4. $\Pi_{P3}$ (Preuve de Satisfiabilité) : Le prover prouve que sa partie secrète est satisfiable en fournissant une affectation valide sans révéler les valeurs, en vérifiant que chaque clause s'annule pour au moins un littéral de l'affectation.
5. $\Pi_{P4}$ (Isolation des Variables) : Prouve que les littéraux secrets n'apparaissent pas dans les clauses publiques (sauf aux interfaces), garantissant que la contradiction provient bien de l'incompatibilité fonctionnelle et non d'une erreur de modélisation.

C. Optimisation

Les auteurs proposent une optimisation de compression des résolvants. Au lieu de stocker chaque étape de résolution, seules les clauses apprises (learned clauses) critiques sont conservées. Cela réduit considérablement la taille de la preuve et le temps de calcul, avec une analyse prouvant que la reconstruction de la formule originale par le vérificateur reste computationnellement impossible (complexité factorielle).

3. Contributions Clés

1. Premier cadre ZK pour la vérification formelle matérielle : ZK-CEC est la première solution permettant de prouver l'équivalence fonctionnelle d'un IP secret par rapport à une spécification publique sans révéler la conception.
2. Blueprint de vérification de propriétés secrètes : Une méthode générale pour partitionner les formules en parties secrètes et publiques, assurant la sonorité là où les protocoles précédents échouaient.
3. Preuves de sécurité formelles : Le protocole garantit la complétude, la sonorité et la connaissance nulle (le vérificateur ne apprend que la validité de l'équivalence et la taille de la preuve, pas la structure du circuit).
4. Implémentation et Évaluation : Une implémentation complète utilisant l'outil EMP-toolkit et l'évaluation sur 37 circuits de référence (arithmétiques, cryptographiques comme AES S-Box, contrôleurs, etc.).

4. Résultats Expérimentaux

Les auteurs ont évalué ZK-CEC sur un serveur cloud avec des circuits allant de petits additeurs à des composants cryptographiques complexes.

• Performance : La vérification de l'insatisfiabilité (étape P1+P2) domine le temps d'exécution, ce qui est attendu pour un problème co-NP complet. Cependant, le protocole reste pratique pour des designs réels.
• Exemple concret : La vérification de l'équivalence d'un S-Box AES (211 littéraux, 700 clauses) prend environ 4,9 secondes (temps total).
• Impact de l'optimisation : L'optimisation de compression des preuves permet d'accélérer le temps de preuve d'un facteur allant jusqu'à 2,88x pour les circuits les plus complexes (ex: GFMul_8x8).
• Évolutivité : Les temps d'exécution et la taille des preuves montrent une relation quasi-linéaire sur une échelle log-log par rapport à la taille de la preuve de réfutation. Les limites actuelles sont liées à la mémoire vive (RAM) pour les très grands circuits générant des preuves de réfutation explosives.

5. Signification et Impact

Ce travail marque une avancée significative dans la sécurité de la chaîne d'approvisionnement matérielle :

• Il permet de débloquer le commerce d'IP en offrant une garantie formelle (et non probabiliste) de l'absence de trojans ou de bogues, sans compromettre la propriété intellectuelle.
• Il comble le fossé entre la vérification formelle (rigoureuse mais ouverte) et les preuves à connaissance nulle (privées mais souvent limitées à la simulation ou aux entrées publiques).
• Le "blueprint" proposé est extensible à d'autres domaines comme la vérification de logiciels et les systèmes cyber-physiques, offrant une nouvelle voie pour la confidentialité dans la vérification formelle.

En résumé, ZK-CEC transforme la vérification formelle en un outil viable pour les échanges commerciaux privés, assurant que "ce qui est vendu est bien ce qui est livré" sans révéler "comment cela est fait".