Analyse des principes de Binius STARKs et réflexion sur son optimisation

1 Introduction

Une des principales raisons de l'inefficacité des STARKs est que la plupart des valeurs dans les programmes réels sont relativement petites, comme les index dans les boucles for, les valeurs booléennes, les compteurs, etc. Cependant, pour garantir la sécurité des preuves basées sur les arbres de Merkle, l'utilisation du codage de Reed-Solomon pour étendre les données entraîne l'occupation de nombreux valeurs redondantes dans tout le domaine, même si la valeur originale elle-même est très petite. Pour résoudre ce problème, réduire la taille du domaine est devenu une stratégie clé.

La largeur de code des STARKs de 1ère génération est de 252 bits, celle des STARKs de 2ème génération est de 64 bits, et celle des STARKs de 3ème génération est de 32 bits, mais la largeur de code de 32 bits présente encore un grand espace de gaspillage. En revanche, le domaine binaire permet d'opérer directement sur les bits, avec un encodage compact et efficace sans aucun espace gaspillé, c'est-à-dire la 4ème génération de STARKs.

Comparé aux découvertes récentes sur les corps finis comme Goldilocks, BabyBear et Mersenne31, la recherche sur les corps binaires remonte aux années 1980. Actuellement, les corps binaires sont largement utilisés en cryptographie, des exemples typiques incluent :

• Norme de chiffrement avancée ( AES ), basé sur le domaine F28;

• Code d'authentification de message Galois ( GMAC ), basé sur le domaine F2128;

• QR code, utilisant un codage Reed-Solomon basé sur F28;

• Le protocole FRI original et le protocole zk-STARK, ainsi que la fonction de hachage Grøstl qui a atteint la finale de SHA-3, basée sur le domaine F28, est un algorithme de hachage très adapté à la récursivité.

Lorsqu'un domaine plus petit est utilisé, l'opération d'extension de domaine devient de plus en plus importante pour garantir la sécurité. Le domaine binaire utilisé par Binius doit entièrement dépendre de l'extension de domaine pour assurer sa sécurité et sa praticité. La plupart des polynômes impliqués dans les calculs des Prover n'ont pas besoin d'entrer dans l'extension de domaine, mais peuvent simplement fonctionner sous le domaine de base, réalisant ainsi une grande efficacité dans le petit domaine. Cependant, les vérifications de points aléatoires et les calculs FRI doivent encore s'approfondir dans un domaine d'extension plus grand pour garantir la sécurité requise.

Lors de la construction d'un système de preuve basé sur un domaine binaire, il existe 2 problèmes pratiques : lors du calcul de la représentation de la trace dans les STARKs, la taille du domaine utilisé doit être supérieure au degré du polynôme ; lors de l'engagement de l'arbre de Merkle dans les STARKs, il est nécessaire de faire un codage de Reed-Solomon, et la taille du domaine utilisé doit être supérieure à la taille après l'extension du codage.

Binius a proposé une solution innovante pour traiter ces deux problèmes, en représentant les mêmes données de deux manières différentes : d'abord, en utilisant des polynômes multivariés ( spécifiquement des polynômes multilinéraires ) à la place des polynômes univariés, en représentant l'ensemble de la trajectoire de calcul par leurs valeurs sur des "hyper-cubes" ( hypercubes ) ; ensuite, étant donné que la longueur de chaque dimension de l'hyper-cube est de 2, il n'est pas possible de procéder à une extension standard de Reed-Solomon comme dans le cas des STARKs, mais on peut considérer l'hyper-cube comme un carré ( square ), et effectuer une extension de Reed-Solomon basée sur ce carré. Cette méthode améliore considérablement l'efficacité du codage et la performance de calcul tout en garantissant la sécurité.

2 Analyse des principes

La construction de la plupart des systèmes SNARKs actuels comprend généralement les deux parties suivantes :

• Preuve d'oracle interactif polynomiale d'information théorique ( Information-Theoretic Polynomial Interactive Oracle Proof, PIOP ) : PIOP, en tant que système de preuve central, transforme les relations de calcul d'entrée en équations polynomiales vérifiables. Différents protocoles PIOP, à travers leur interaction avec le vérificateur, permettent au prouveur d'envoyer progressivement des polynômes, de sorte que le vérificateur puisse vérifier si le calcul est correct en interrogeant un petit nombre de résultats d'évaluation de polynômes. Les protocoles PIOP existants incluent : PLONK PIOP, Spartan PIOP et HyperPlonk PIOP, qui ont chacun des manières différentes de traiter les expressions polynomiales, influençant ainsi les performances et l'efficacité de l'ensemble du système SNARK.

• Schéma d'engagement polynomial ( Polynomial Commitment Scheme, PCS ) : Le schéma d'engagement polynomial est utilisé pour prouver si une égalité polynomiale générée par PIOP est valide. Le PCS est un outil cryptographique, grâce auquel le prouveur peut s'engager sur un certain polynôme et vérifier plus tard le résultat de l'évaluation de ce polynôme, tout en cachant d'autres informations sur le polynôme. Les schémas d'engagement polynomial courants incluent KZG, Bulletproofs, FRI ( Fast Reed-Solomon IOPP ) et Brakedown, entre autres. Différents PCS ont des performances, une sécurité et des cas d'utilisation différents.

Selon les besoins spécifiques, choisissez différents PIOP et PCS, et combinez-les avec un domaine fini ou une courbe elliptique appropriée, pour construire des systèmes de preuve avec différentes propriétés. Par exemple:

• Halo2 : combiné de PLONK PIOP et de Bulletproofs PCS, basé sur la courbe Pasta. Halo2 a été conçu en mettant l'accent sur l'évolutivité et l'élimination de la configuration de confiance dans le protocole ZCash.

• Plonky2 : combine PLONK PIOP et FRI PCS, et est basé sur le domaine Goldilocks. Plonky2 est conçu pour réaliser une récursivité efficace. Lors de la conception de ces systèmes, le PIOP et le PCS choisis doivent correspondre au champ fini ou à la courbe elliptique utilisée, afin d'assurer la correction, la performance et la sécurité du système. Le choix de ces combinaisons affecte non seulement la taille des preuves SNARK et l'efficacité de la vérification, mais détermine également si le système peut réaliser la transparence sans configuration de confiance préalable, ainsi que sa capacité à supporter des fonctionnalités d'extension telles que les preuves récursives ou les preuves agrégées.

Binius: HyperPlonk PIOP + Brakedown PCS + champs binaires. Plus précisément, Binius comprend cinq technologies clés pour réaliser son efficacité et sa sécurité. Tout d'abord, l'arithmétique basée sur les tours de champs binaires (towers of binary fields) constitue la base de son calcul, permettant d'effectuer des opérations simplifiées dans le champ binaire. Deuxièmement, Binius a adapté le contrôle de produit et de permutation de HyperPlonk dans son protocole de preuve d'Oracle interactif (PIOP), garantissant une vérification de cohérence sécurisée et efficace entre les variables et leurs permutations. Troisièmement, le protocole introduit une nouvelle preuve de décalage multilinéraire, optimisant l'efficacité de la validation des relations multlinéaires sur de petits champs. Quatrièmement, Binius utilise une version améliorée de la preuve de recherche Lasso, offrant flexibilité et sécurité robuste au mécanisme de recherche. Enfin, le protocole utilise un schéma d'engagement polynomiale sur petits champs (Small-Field PCS), lui permettant de réaliser un système de preuve efficace sur le champ binaire, tout en réduisant les frais généralement associés aux grands champs.

2.1 Domain fini : arithmétisation basée sur les tours de champs binaires

Le domaine binaire en tour est la clé pour réaliser des calculs rapides et vérifiables, principalement en raison de deux aspects : le calcul efficace et l'arithmétique efficace. Le domaine binaire supporte essentiellement des opérations arithmétiques très efficaces, ce qui en fait un choix idéal pour les applications cryptographiques sensibles aux performances. En outre, la structure du domaine binaire supporte un processus d'arithmétisation simplifié, c'est-à-dire que les opérations effectuées sur le domaine binaire peuvent être représentées sous une forme algébrique compacte et facile à vérifier. Ces caractéristiques, associées à la capacité de tirer pleinement parti de ses caractéristiques hiérarchiques grâce à la structure en tour, rendent le domaine binaire particulièrement adapté à des systèmes de preuve évolutifs tels que Binius.

Le terme "canonique" fait référence à la représentation unique et directe des éléments dans le domaine binaire. Par exemple, dans le domaine binaire de base F2, toute chaîne de k bits peut être directement mappée à un élément de domaine binaire de k bits. Cela diffère des domaines premiers, qui ne peuvent pas fournir cette représentation canonique dans un nombre de bits donné. Bien qu'un domaine premier de 32 bits puisse être contenu dans 32 bits, ce n'est pas le cas pour chaque chaîne de 32 bits, car elles ne correspondent pas toutes de manière unique à un élément de domaine, tandis que le domaine binaire offre cette commodité de mappage un à un. Dans le domaine premier Fp, les méthodes de réduction courantes incluent la réduction de Barrett, la réduction de Montgomery, ainsi que des méthodes de réduction spéciales pour des domaines finis spécifiques comme Mersenne-31 ou Goldilocks-64. Dans le domaine binaire F2k, les méthodes de réduction courantes incluent des réductions spéciales ( comme celles utilisées dans AES ), la réduction de Montgomery ( comme utilisée dans POLYVAL ), et la réduction récursive ( comme Tower ). Le document "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" souligne que le domaine binaire n'introduit pas de retenue dans les opérations d'addition et de multiplication, et que l'opération de carré dans le domaine binaire est très efficace, car elle suit la règle simplifiée (X + Y )2 = X2 + Y2.

Comme indiqué dans la figure 1, une chaîne de 128 bits : cette chaîne peut être interprétée de plusieurs manières dans le contexte du domaine binaire. Elle peut être considérée comme un élément unique dans un domaine binaire de 128 bits, ou être analysée comme deux éléments de domaine de tour de 64 bits, quatre éléments de domaine de tour de 32 bits, 16 éléments de domaine de 8 bits, ou 128 éléments de domaine F2. Cette flexibilité de représentation ne nécessite aucun coût de calcul, juste un changement de type de la chaîne de bits (typecast), ce qui est une propriété très intéressante et utile. De plus, les petits éléments de domaine peuvent être empaquetés en éléments de domaine plus grands sans coût de calcul supplémentaire. Le protocole Binius tire parti de cette caractéristique pour améliorer l'efficacité du calcul. De plus, l'article "On Efficient Inversion in Tower Fields of Characteristic Two" explore la complexité du calcul des opérations de multiplication, de mise au carré et d'inversion dans un domaine binaire de tour de n bits ( décomposable en sous-domaines de m bits ).

2.2 PIOP: Version modifiée du produit HyperPlonk et Vérification de permutation------Applicable aux domaines binaires

La conception de PIOP dans le protocole Binius s'inspire de HyperPlonk et utilise une série de mécanismes de vérification clés pour valider la correcte des polynômes et des ensembles multivariés. Ces vérifications clés comprennent :

1. GateCheck : vérifie si le témoin secret ω et l'entrée publique x satisfont la relation de calcul du circuit C(x,ω)=0, afin de garantir le bon fonctionnement du circuit.

2. PermutationCheck : Vérifie si les résultats d'évaluation des deux polynômes multivariables f et g sur le cube hyperbolique booléen sont une relation de permutation f(x) = f(π(x)), afin d'assurer la cohérence des permutations entre les variables du polynôme.

3. LookupCheck : Vérifiez si l'évaluation du polynôme se trouve dans la table de recherche donnée, c'est-à-dire f(Bµ) ⊆ T(Bµ), assurez-vous que certaines valeurs se trouvent dans la plage spécifiée.

4. MultisetCheck : Vérifie si deux ensembles multivariables sont égaux, c'est-à-dire {(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H, garantissant la cohérence entre plusieurs ensembles.

5. ProductCheck : Vérifier si l'évaluation du polynôme rationnel sur l'hypercube booléen est égale à une valeur déclarée ∏x∈Hµ f(x) = s, afin de garantir l'exactitude du produit polynomial.

6. ZeroCheck : Vérifier si un polynôme multivariable en un point arbitraire sur le cube hyperbolique booléen est nul ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, afin d'assurer la distribution des zéros du polynôme.

7. SumCheck : Vérifie si la somme d'un polynôme multivarié est égale à la valeur déclarée ∑x∈Hµ f(x) = s. En transformant le problème d'évaluation d'un polynôme multivarié en évaluation d'un polynôme à une seule variable, cela réduit la complexité computationnelle pour le vérificateur. De plus, SumCheck permet le traitement par lots, en introduisant des nombres aléatoires pour construire des combinaisons linéaires afin de réaliser le traitement par lots de plusieurs instances de vérification de somme.

8. BatchCheck : basé sur SumCheck, vérifie la validité des évaluations de plusieurs polynômes multivariables afin d'améliorer l'efficacité du protocole.

Bien que Binius et HyperPlonk aient de nombreuses similitudes dans la conception du protocole, Binius apporte des améliorations dans les 3 domaines suivants :

• Optimisation de ProductCheck : dans HyperPlonk, ProductCheck exige que le dénominateur U soit non nul partout sur l'hypercube, et que le produit soit égal à une valeur spécifique ; Binius simplifie ce processus de vérification en spécialisant cette valeur à 1, réduisant ainsi la complexité de calcul.

• Gestion des problèmes de division par zéro : HyperPlonk n'a pas réussi à traiter correctement les cas de division par zéro, ce qui empêche d'affirmer que U est non nul sur l'hypercube ; Binius a correctement traité ce problème, même lorsque le dénominateur est zéro, le ProductCheck de Binius peut continuer à fonctionner, permettant de s'étendre à n'importe quelle valeur de produit.

• Vérification de permutation inter-colonnes : HyperPlonk n'a pas cette fonctionnalité ; Binius prend en charge la vérification de permutation entre plusieurs colonnes, ce qui permet à Binius de gérer des cas de permutation de polynômes plus complexes.

Ainsi, Binius a amélioré le mécanisme existant de PIOPSumCheck, augmentant la flexibilité et l'efficacité du protocole, en particulier lors du traitement de la vérification de polynômes multivariés plus complexes, offrant un support fonctionnel plus fort. Ces améliorations non seulement résolvent les limitations de HyperPlonk, mais jettent également les bases pour de futurs systèmes de preuve basés sur des corps binaires.

2.3 PIOP : nouvel argument de décalage multilinéraire ------ applicable à l'hypercube booléen

Dans le protocole Binius, la construction et le traitement des polynômes virtuels sont l'une des technologies clés, capables de générer et d'opérer efficacement des polynômes dérivés de poignées d'entrée ou d'autres polynômes virtuels. Voici deux méthodes clés :

• Packing: Cette méthode optimise l'opération en regroupant les éléments plus petits situés à des positions adjacentes dans l'ordre lexicographique en éléments plus grands. L'opérateur Pack cible des blocs de taille 2κ et les combine en un domaine de haute dimension.