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

1. Introduction

Contrairement aux SNARKs basés sur les courbes elliptiques, les STARKs peuvent être considérés comme des SNARKs basés sur le hash. Une des principales raisons de l'inefficacité actuelle 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 nombreuses 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 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. Cependant, la largeur de codage de 32 bits présente encore un grand espace perdu. En comparaison, le domaine binaire permet d'opérer directement sur les bits, avec un codage compact et efficace sans aucun espace perdu, c'est-à-dire les STARKs de quatrième génération.

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

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

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

• QR code, 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 du SHA-3, basée sur le domaine F28, est un algorithme de hachage très adapté à la récursivité.

Lorsque des domaines plus petits sont utilisés, 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 réelle utilisabilité. La plupart des polynômes impliqués dans les calculs des Prover n'ont pas besoin d'entrer dans l'extension de domaine, mais doivent simplement opérer sous le domaine de base, permettant ainsi d'atteindre une grande efficacité dans de petits domaines. 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 deux problèmes pratiques : lors du calcul de la 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 codage de Reed-Solomon doit être effectué, et la taille du domaine utilisée doit être supérieure à la taille après l'extension du codage.

Binius a proposé une solution innovante qui traite ces deux problèmes 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éraires) au lieu de polynômes univariés, en représentant l'ensemble de la trajectoire de calcul par ses 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 l'hypercube peut être considéré comme un carré, permettant ainsi d'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 :

• Preuves d'oracle interactif polynomial en théorie de l'information (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP) : Le PIOP, en tant que cœur du système de preuve, transforme les relations de calcul d'entrée en égalités polynomiales vérifiables. Différents protocoles PIOP, à travers l'interaction avec le vérificateur, permettent au prouveur d'envoyer progressivement des polynômes, de sorte que le vérificateur puisse valider si le calcul est correct en interrogeant un nombre réduit 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, influençant ainsi la performance 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é polynomial générée par PIOP est valide. Le PCS est un outil cryptographique qui permet au prouveur de s'engager sur un certain polynôme et de vérifier ultérieurement les résultats 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.

En fonction des besoins spécifiques, choisissez différents PIOP et PCS, et combinez-les avec des domaines finis ou des courbes elliptiques appropriés, 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. Lors de la conception de Halo2, l'accent a été mis sur l'évolutivité et l'élimination de la configuration de confiance dans le protocole ZCash.

• Plonky2 : utilise le PLONK PIOP associé au FRI PCS et est basé sur le domaine Goldilocks. Plonky2 est conçu pour réaliser des récursions efficaces. Lors de la conception de ces systèmes, le PIOP et le PCS choisis doivent correspondre au domaine fini ou à la courbe elliptique utilisée, afin de garantir la validité, la performance et la sécurité du système. Le choix de ces combinaisons n'affecte pas seulement la taille de la preuve SNARK et l'efficacité de la vérification, mais détermine également si le système peut atteindre la transparence sans configuration de confiance préalable, et s'il peut soutenir des fonctionnalités d'extension telles que la preuve récursive ou la preuve agrégée.

Binius : HyperPlonk PIOP + Brakedown PCS + domaine binaire. Plus précisément, Binius comprend cinq technologies clés pour réaliser son efficacité et sa sécurité. Premièrement, 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. Deuxièmement, Binius adapte la vérification de produit et de permutation de HyperPlonk dans son protocole de preuve Oracle interactif (PIOP), garantissant une vérification cohérente sécurisée et efficace entre les variables et leurs permutations. Troisièmement, le protocole introduit une nouvelle preuve de décalage multilinéaire, optimisant l'efficacité de la vérification 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 pour de petits domaines (Small-Field PCS), lui permettant de réaliser un système de preuve efficace sur le domaine binaire, tout en réduisant les frais généralement associés aux grands domaines.

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

Les corps binaires en tour sont la clé pour réaliser des calculs rapides et vérifiables, principalement en raison de deux aspects : le calcul efficace et l'arithmétisation efficace. Les corps binaires soutiennent essentiellement des opérations arithmétiques très efficaces, ce qui en fait un choix idéal pour les applications cryptographiques sensibles aux performances. De plus, la structure des corps binaires soutient un processus d'arithmétisation simplifié, c'est-à-dire que les opérations exécutées sur les corps binaires peuvent être représentées sous une forme algébrique compacte et facile à vérifier. Ces caractéristiques, associées à la capacité d'exploiter pleinement les caractéristiques hiérarchiques de la structure en tour, rendent les corps binaires particulièrement adaptés à des systèmes de preuves évolutifs tels que Binius.

Le terme "canonique" fait référence à la représentation unique et directe des éléments dans le champ binaire. Par exemple, dans le champ binaire de base F2, toute chaîne de k bits peut être directement mappée à un élément de champ binaire de k bits. Cela diffère des champs premiers, qui ne peuvent pas fournir une telle représentation canonique dans un nombre de bits donné. Bien qu'un champ premier de 32 bits puisse être contenu dans 32 bits, toutes les chaînes de 32 bits ne correspondent pas nécessairement de manière unique à un élément de champ, alors que le champ binaire offre cette commodité de correspondance un-à-un. Dans le champ 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 champs finis spécifiques comme Mersenne-31 ou Goldilocks-64. Dans le champ binaire F2k, les méthodes de réduction couramment utilisées comprennent la réduction spéciale (comme utilisée 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" note que le champ binaire n'a pas besoin d'introduire des reports dans les opérations d'addition et de multiplication, et que l'opération de carré dans le champ binaire est très efficace, car elle suit la règle simplifiée (X + Y )2 = X2 + Y 2.

Comme montré 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 des domaines binaires. 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 tour de 64 bits, quatre éléments de domaine tour de 32 bits, 16 éléments de domaine tour de 8 bits, ou 128 éléments de domaine F2. Cette flexibilité de représentation ne nécessite aucun coût de calcul, c'est simplement une conversion de type (typecast) de la chaîne de bits, ce qui est une propriété très intéressante et utile. De plus, les éléments de petits domaines peuvent être empaquetés en éléments de domaines plus grands sans frais de calcul supplémentaires. Le protocole Binius tire parti de cette caractéristique pour améliorer l'efficacité du calcul. En outre, l'article "On Efficient Inversion in Tower Fields of Characteristic Two" explore la complexité de calcul des opérations de multiplication, de mise au carré et d'inversion dans un domaine binaire tour de n bits (décomposable en sous-domaines de m bits).

2.2 PIOP : Version adapté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 adopte une série de mécanismes de vérification essentiels pour valider la correction des polynômes et des ensembles multivariés. Ces vérifications essentielles 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 de deux polynômes multivariables f et g sur le cube hyperbooléen forment une relation de permutation f(x) = f(π(x)), afin d'assurer la cohérence des permutations entre les variables des polynômes.

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µ), assurant que certaines valeurs sont 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érifie si l'évaluation d'un polynôme multivarié sur le cube hypercubique booléen est égale à une valeur déclarée ∏x∈Hµ f(x) = s, afin d'assurer la validité du produit polynômial.

6. ZeroCheck : vérifier si un polynôme multivariable est nul en un point arbitraire du cube hyperbolique boolean ∏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 d'un polynôme multivariable est égale à la valeur déclarée ∑x∈Hµ f(x) = s. En transformant le problème d'évaluation d'un polynôme multivariable en un problème d'évaluation de polynôme à une variable, cela réduit la complexité de calcul pour la partie vérificatrice. De plus, SumCheck permet le traitement par lots, en introduisant des nombres aléatoires pour construire des combinaisons linéaires afin de traiter plusieurs instances de vérification de sommes.

8. BatchCheck : basé sur SumCheck, vérifie l'exactitude des évaluations 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 des protocoles, 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 sur tout l'hypercube, et que le produit doit être é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 traité ce problème correctement, même lorsque le dénominateur est zéro, le ProductCheck de Binius peut continuer à fonctionner, 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 situations de permutation polynomiale plus complexes.

Ainsi, Binius a amélioré la flexibilité et l'efficacité du protocole grâce à des modifications du mécanisme PIOPSumCheck existant, en offrant un meilleur support fonctionnel, en particulier lors du traitement de vérifications de polynômes multivariés plus complexes. 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 domaines binaires.

2.3 PIOP : nouvel argument de décalage multilinéraire ------ applicable au cube hyperbolique 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 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 :

• Emballage : Cette méthode consiste à combiner les plus petits emplacements adjacents dans l'ordre lexicographique.