Analyse des principes des STARKs de Binius et réflexions sur leur 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 indices 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, lorsque l'on utilise le codage de Reed-Solomon pour étendre les données, de nombreuses valeurs redondantes supplémentaires occupent 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 codage des STARKs de première génération est de 252 bits, celle des STARKs de deuxième génération est de 64 bits, et celle des STARKs de troisième génération est de 32 bits, mais la largeur de codage de 32 bits présente encore beaucoup d'espace gaspillé. En comparaison, le domaine binaire permet d'opérer directement sur les bits, avec un codage compact et efficace sans espace gaspillé, c'est-à-dire la quatrième génération de STARKs.

Comparé aux découvertes récentes de corps finis tels que 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 :

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

• Galois Message Authentication Code ( GMAC ), basé sur le domaine F2128;

• Code QR, utilisant le codage Reed-Solomon basé sur F28 ;

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

Lorsqu'on utilise des domaines plus petits, 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 s'appuyer entièrement sur 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 dans 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 plonger 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 trace dans les STARKs, la taille du domaine utilisée doit être supérieure au degré du polynôme ; lors de l'engagement de l'arbre de Merkle dans les STARKs, un encodage de Reed-Solomon doit être effectué, et la taille du domaine utilisée doit être supérieure à la taille après l'extension de l'encodage.

Binius a proposé une solution innovante qui traite ces deux problèmes séparément et représente les mêmes données de deux manières différentes : premièrement, en utilisant des polynômes multivariés (plus précisément des polynômes multilinéaires) au lieu de polynômes univariés, en représentant l'ensemble de la trajectoire de calcul par leurs valeurs sur des "hypercubes" ; deuxièmement, étant donné que la longueur de chaque dimension de l'hypercube est de 2, il n'est pas possible d'effectuer une extension de Reed-Solomon standard comme avec les STARKs, mais on peut considérer l'hypercube comme un carré et effectuer une extension de Reed-Solomon basée sur ce carré. Cette méthode améliore considérablement l'efficacité du codage et les performances 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 Interactive Polynômiale Théorique de l'Information (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP) : Le PIOP, en tant que noyau du système de preuve, transforme les relations de calcul en égalités polynomiales vérifiables. Différents protocoles PIOP permettent au prouveur d'envoyer progressivement des polynômes par l'interaction avec le vérificateur, de sorte que le vérificateur puisse valider si le calcul est correct en interrogeant un petit nombre de résultats d'évaluation de polynômes. Les protocoles PIOP existants incluent : PIOP PLONK, PIOP Spartan et PIOP HyperPlonk, qui traitent chacun les expressions polynomiales de manière différente, ce qui influence 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 l'égalité polynomiale générée par PIOP est valide. Le PCS est un outil cryptographique qui permet à un prouvant de s'engager sur un certain polynôme et de vérifier ultérieurement 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 présentent des performances, une sécurité et des scénarios d'application variés.

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

• Halo2 : combinant PLONK PIOP et Bulletproofs PCS, basé sur la courbe Pasta. La conception de Halo2 se concentre sur l'évolutivité et l'élimination de la configuration de confiance dans le protocole ZCash.

• Plonky2 : utilise la combinaison de PLONK PIOP et de FRI PCS, et est basé sur le domaine de Goldilocks. Plonky2 est conçu pour réaliser des récursions efficaces. Lors de la conception de ces systèmes, les PIOP et PCS sélectionnés doivent correspondre au corps fini ou à la courbe elliptique utilisés pour garantir la validité, 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 une transparence sans configuration de confiance préalable, et s'il peut prendre en charge des fonctionnalités d'extension telles que les preuves récursives ou les preuves d'agrégation.

Binius : HyperPlonk PIOP + Brakedown PCS + domaine binaire. Concrètement, 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 domaines binaires constitue la base de son calcul, permettant d'effectuer des opérations simplifiées dans le domaine binaire. Ensuite, Binius a adapté la vérification de produit et de permutation de HyperPlonk dans son protocole de preuve 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 multilinéaires sur de petits domaines. 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 polynomial de petit domaine (Small-Field PCS), lui permettant de réaliser un système de preuve efficace sur le domaine binaire et réduisant les frais généralement associés aux grands domaines.

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

Les corps binaires en tour sont essentiels pour réaliser des calculs vérifiables rapides, principalement en raison de deux aspects : le calcul efficace et l'arithmétisation efficace. Les corps binaires prennent essentiellement en charge des opérations arithmétiques hautement efficaces, ce qui en fait un choix idéal pour les applications cryptographiques sensibles aux performances. De plus, la structure des corps binaires prend en charge un processus d'arithmétisation simplifié, c'est-à-dire que les opérations effectuées sur les corps binaires peuvent être représentées sous une forme algébrique compacte et facilement vérifiable. Ces caractéristiques, combinées à la capacité d'exploiter pleinement ses propriétés hiérarchiques grâce à une structure en tour, rendent les corps binaires particulièrement adaptés à des systèmes de preuve évolutifs tels que Binius.

Le terme "canonical" fait référence à la représentation unique et directe d'un élément dans un corps binaire. Par exemple, dans le corps binaire F2 le plus simple, toute chaîne de k bits peut être directement mappée à un élément de corps binaire de k bits. Cela diffère des corps de nombres premiers, où il n'est pas possible de fournir cette représentation canonique dans un nombre de bits donné. Bien qu'un corps de nombres premiers de 32 bits puisse être contenu dans 32 bits, ce n'est pas le cas pour chaque chaîne de 32 bits pouvant correspondre de manière unique à un élément de corps, tandis que le corps binaire permet cette commodité de correspondance un à un. Dans le corps de nombres premiers 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 corps finis spécifiques tels que Mersenne-31 ou Goldilocks-64. Dans le corps 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 dans Tower). L'article "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" indique que dans le corps binaire, aucune retenue n'est nécessaire lors des opérations d'addition et de multiplication, et que l'opération de carré dans le corps binaire est très efficace car elle suit la règle simplifiée (X + Y )2 = X2 + Y 2.

Comme illustré 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 d'un domaine binaire. Elle peut être considérée comme un élément unique dans un domaine binaire de 128 bits, ou être décomposée en deux éléments de domaine de tour de 64 bits, quatre éléments de domaine de tour de 32 bits, seize éléments de domaine de tour de 8 bits, ou 128 éléments de domaine F2. Cette flexibilité de représentation ne nécessite aucun coût de calcul supplémentaire, 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 éléments de petit domaine peuvent être emballés en éléments de domaine plus grands sans coût de calcul supplémentaire. Le protocole Binius a tiré parti de cette caractéristique pour améliorer l'efficacité des calculs. En outre, le document « On Efficient Inversion in Tower Fields of Characteristic Two » explore la complexité computationnelle des opérations de multiplication, de mise au carré et d'inversion dans un domaine binaire de tour de n bits (décomposable en un sous-domaine de m bits).

2.2 PIOP : Version adaptée du produit HyperPlonk et PermutationCheck ------ Applicable aux corps binaires

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

1. GateCheck : vérifier 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 de deux polynômes multivariés f et g sur le cube hyperbolique booléen forment une relation de permutation f(x) = f(π(x)), afin de garantir la cohérence des permutations entre les variables du polynôme.

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

4. MultisetCheck : Vérifie si deux ensembles de variables multiples 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 d'un polynôme à coefficients rationnels sur l'hypercube booléen est égale à une valeur déclarée ∏x∈Hµ f(x) = s, afin de garantir la validité du produit polynomial.

6. ZeroCheck : Vérifie si un polynôme multivariable à plusieurs variables est nul en un point quelconque sur l'hypercube booléen ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, afin de garantir la distribution des zéros du polynôme.

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

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

Bien que Binius et HyperPlonk aient de nombreuses similitudes dans la conception du protocole, Binius a amélioré les 3 aspects suivants :

• Optimisation de ProductCheck : dans HyperPlonk, ProductCheck exige que le dénominateur U soit partout non nul sur le cube 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 du problème 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 à traiter, permettant une généralisation à 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 d'arrangements polynomiaux plus complexes.

Ainsi, Binius a amélioré le mécanisme PIOPSumCheck existant, 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 ainsi un soutien fonctionnel plus robuste. Ces améliorations non seulement résolvent les limitations de HyperPlonk, mais établissent également une base pour les futurs systèmes de preuve basés sur des domaines 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, permettant de générer et de manipuler 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 :

• Emballage :