Analyse des principes des STARKs de Binius et réflexion 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, l'utilisation du codage de Reed-Solomon pour étendre les données entraîne de nombreuses valeurs redondantes supplémentaires qui 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 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 gaspillé. En revanche, le domaine binaire permet de manipuler directement les bits, avec un codage compact et efficace sans aucun espace gaspillé, c'est-à-dire les STARKs de 4ème génération.

Comparé aux travaux récents sur les 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 :

• Norme de cryptage 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 du SHA-3, basée sur le domaine F28, constituent 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 s'appuyer sur l'extension de domaine pour assurer sa sécurité et sa réelle utilisabilité. La plupart des polynômes impliqués dans les calculs de Prover n'ont pas besoin d'entrer dans l'extension de domaine, mais doivent simplement fonctionner sous le domaine de base, ce qui permet d'atteindre une grande efficacité dans un petit domaine. Cependant, les vérifications de points aléatoires et les calculs FRI doivent encore plonger dans une extension de domaine plus grande 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 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, un codage de Reed-Solomon doit être effectué, et la taille du domaine utilisé doit être supérieure à la taille après extension du codage.

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 : d'abord, en utilisant un polynôme multivarié ( qui est spécifiquement un polynôme multilinéraire ) à la place d'un polynôme à variable unique, en représentant l'ensemble de la trajectoire de calcul par ses valeurs sur les "hypercubes" ( ; ensuite, comme chaque dimension de l'hypercube a une longueur de 2, il est impossible d'effectuer une extension standard de Reed-Solomon comme avec les STARKs, mais on peut considérer l'hypercube comme un carré ), et effectuer l'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) : PIOP, en tant que cœur du système de preuve, transforme les relations de calcul en équations polynomiales vérifiables. Différents protocoles PIOP, grâce à l'interaction avec le vérificateur, permettent au prouveur d'envoyer progressivement des polynômes, permettant au vérificateur de valider la correction des calculs en interrogeant un nombre réduit de résultats d'évaluation des polynômes. Les protocoles PIOP existants incluent : PLONK PIOP, Spartan PIOP et HyperPlonk PIOP, qui traitent chacun les expressions polynomiales de manière différente, influençant ainsi les performances et l'efficacité du système SNARK dans son ensemble.

• Schéma d'engagement polynomial (Polynomial Commitment Scheme, PCS) : L'engagement polynomial est utilisé pour prouver si l'é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 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 comprennent KZG, Bulletproofs, FRI(Fast Reed-Solomon IOPP) et Brakedown, entre autres. Différents PCS ont des performances, une sécurité et des scénarios d'application différents.

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

• Halo2 : combinant PLONK PIOP et 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 : utilise une combinaison de PLONK PIOP et de FRI PCS, basé sur le domaine de Goldilocks. Plonky2 est conçu pour réaliser une récursion efficace. Lors de la conception de ces systèmes, le PIOP et le PCS choisis doivent correspondre au corps fini ou à la courbe elliptique utilisés, afin d'assurer la justesse, la performance et la sécurité du système. Le choix de ces combinaisons affecte non seulement la taille de la preuve 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, et s'il peut prendre en charge des fonctionnalités d'extension telles que la preuve récursive ou la preuve agrégée.

Binius : HyperPlonk PIOP + Brakedown PCS + domaines 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 ses calculs, permettant d'effectuer des opérations simplifiées dans le champ binaire. Ensuite, Binius a adapté l'HyperPlonk en vérification de produit et de permutation dans son protocole de preuve Oracle interactif (PIOP), garantissant un contrôle de cohérence sécurisé 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 vérification des relations multiliné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 de polynômes de petits champs (Small-Field PCS), lui permettant de réaliser un système de preuve efficace sur le champ binaire et 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

Les corps binaires en tour sont essentiels pour réaliser des calculs vérifiables rapides, principalement en raison de deux aspects : un calcul efficace et une arithmétisation efficace. Les corps binaires soutiennent essentiellement 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 soutient 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 facile à vérifier. Ces caractéristiques, combinées à la capacité d'exploiter pleinement ses caractéristiques hiérarchiques grâce à la structure en tour, rendent les corps binaires particulièrement adaptés à des systèmes de preuve évolutifs tels que Binius.

Le terme "canonical" désigne la représentation unique et directe des éléments dans le domaine binaire. Par exemple, dans le domaine binaire le plus fondamental F2, toute chaîne de k bits peut être directement mappée à un élément du 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 qui peut correspondre de manière unique à un élément du domaine, alors que le domaine binaire permet cette commodité d'un 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 tels que Mersenne-31 ou Goldilocks-64. Dans le domaine binaire F2k, les méthodes de réduction couramment utilisées 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" indique que le domaine binaire n'a pas besoin d'introduire des retenues lors des 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 + Y 2.

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 des domaines binaires. Elle peut être considérée comme un élément unique dans le 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, seize éléments de domaine de tour de 8 bits, ou 128 éléments du domaine F2. Cette flexibilité de représentation ne nécessite aucun coût de calcul, juste une conversion de type de 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 regroupé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é des calculs. De plus, l'article "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 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 essentiels pour valider l'exactitude des polynômes et des ensembles multivariés. Ces vérifications essentielles incluent :

1. GateCheck : vérifie si le témoin de confidentialité ω 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 hyperbooléen sont une relation de permutation f(x) = f(π)x((, afin d'assurer la cohérence de l'agencement entre les variables du polynôme.

3. LookupCheck : Vérifiez si l'évaluation du polynôme est dans la table de recherche donnée, c'est-à-dire f)Bµ) ⊆ T(Bµ), assurez-vous 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érifier si l'évaluation d'un polynôme rationnel sur le cube hyperbolique booléen est égale à une valeur déclarée ∏x∈Hµ f(x) = s, afin d'assurer l'exactitude du produit polynomial.

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

7. SumCheck : Vérification 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 multivarié en une évaluation de polynôme à une variable, la complexité de calcul pour le vérificateur est réduite. De plus, SumCheck permet le traitement par lots en introduisant des nombres aléatoires pour construire des combinaisons linéaires, ce qui permet de traiter plusieurs instances de vérification de somme.

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

Bien que Binius et HyperPlonk présentent de nombreuses similitudes dans la conception des protocoles, Binius a apporté des améliorations dans les 3 domaines suivants :

• Optimisation de ProductCheck : dans HyperPlonk, ProductCheck exige que le dénominateur U soit non nul 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é des calculs.

• Traitement 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 rend impossible d'affirmer que U est non nul sur l'hypercube ; Binius a correctement traité ce problème, même dans le cas où 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 traiter des cas de permutation polynomiale plus complexes.

Ainsi, Binius a amélioré la flexibilité et l'efficacité du protocole en modifiant le mécanisme PIOPSumCheck existant, offrant un meilleur support fonctionnel, en particulier lors du traitement de vérifications de polynômes multivariables plus complexes. Ces améliorations ont non seulement résolu les limitations dans HyperPlonk, mais ont également jeté 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 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 :

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