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 numériques dans les programmes réels sont relativement petites, mais pour garantir la sécurité des preuves basées sur les arbres de Merkle, l'utilisation du codage Reed-Solomon pour étendre les données entraîne de nombreuses valeurs redondantes supplémentaires occupant tout le domaine, même si la valeur d'origine elle-même est très petite. Pour résoudre ce problème, réduire la taille du domaine est devenue 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 un grand espace gaspillé. En comparaison, le domaine binaire permet des opérations directes sur les bits, avec un codage compact et efficace sans espace gaspillé, c'est-à-dire les STARKs de quatrième génération.

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

• Norme 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é.

Lorsque des champs plus petits sont utilisés, l'opération d'extension de champ devient de plus en plus importante pour garantir la sécurité. Le champ binaire utilisé par Binius doit entièrement s'appuyer sur l'extension de champ pour garantir sa sécurité et sa praticité. La plupart des polynômes impliqués dans les calculs de Prover n'ont pas besoin d'entrer dans l'extension de champ, mais peuvent fonctionner sous le champ de base, ce qui permet d'atteindre une grande efficacité dans le petit champ. Cependant, les vérifications de points aléatoires et les calculs FRI doivent encore plonger dans un champ 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 : dans les STARKs, la taille du domaine utilisée pour calculer la représentation de la trace doit être supérieure au degré du polynôme ; dans les STARKs, lors de l'engagement dans l'arbre de Merkle, il est nécessaire d'effectuer un codage de Reed-Solomon, et la taille du domaine 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 (en particulier des polynômes multilinéaires) au lieu de polynômes univariés, pour représenter l'ensemble de la trajectoire de calcul par leurs valeurs sur des "hypercubes" ; ensuite, puisque 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 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 actuelle de la plupart des systèmes SNARKs comprend généralement les deux parties suivantes :

• Preuves d'oracle interactif polynomial à information théorique (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP) : Le PIOP, en tant que système de preuve central, 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 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 traitent chacun les expressions polynomiales de manière différente, 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 équation polynomiale générée par PIOP est valide. Le PCS est un outil cryptographique qui permet au prouveur de s'engager sur un polynôme et de vérifier ultérieurement le résultat d'é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, des niveaux de 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, ce qui permet de construire des systèmes de preuve ayant différentes propriétés. Par exemple :

• Halo2 : combiné 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 PLONK PIOP en combinaison avec FRI PCS, basé sur le domaine de 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 corps fini ou à la courbe elliptique utilisés, afin d'assurer la correction, la performance et la sécurité du système. Le choix de ces combinaisons influence 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, et s'il peut soutenir des fonctionnalités d'extension telles que les preuves récursives ou les preuves agrégées.

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é. Tout d'abord, l'arithmétisation basée sur des 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 consistance sécurisée et efficace entre les variables et leurs permutations. Troisièmement, le protocole introduit un nouveau témoignage de décalage multilinéraire, optimisant l'efficacité de la vérification des relations multilinéaires sur de petits domaines. Quatrièmement, Binius utilise une version améliorée du témoignage de recherche Lasso, offrant flexibilité et sécurité robuste au mécanisme de recherche. Enfin, le protocole utilise un schéma de promesse polynomiale sur de petits domaines (Small-Field PCS), lui permettant de mettre en place un système de preuve efficace dans 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 essentiels 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 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 facile à vérifier. Ces caractéristiques, associé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" 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 du champ premier, qui ne peut pas fournir cette représentation canonique dans un nombre de bits donné. Bien qu'un champ premier de 32 bits puisse être contenu dans 32 bits, il n'est pas vrai que chaque chaîne de 32 bits corresponde de manière unique à un élément de champ, alors que le champ binaire permet 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 celle utilisée dans AES), la réduction de Montgomery (comme celle utilisée dans POLYVAL) et la réduction récursive (comme Tower). L'article "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" souligne que le champ binaire ne nécessite pas l'introduction de retenue lors des 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 champs binaires. Elle peut être considérée comme un élément unique dans un champ binaire de 128 bits, ou être décomposée en deux éléments de champ de 64 bits, quatre éléments de champ de 32 bits, seize éléments de champ de 8 bits, ou 128 éléments de champ F2. Cette flexibilité de représentation ne nécessite aucun coût de calcul, mais simplement une conversion de type de la chaîne de bits, ce qui est une propriété très intéressante et utile. De plus, les éléments de champ plus petits peuvent être encapsulés dans des éléments de champ plus grands sans frais de calcul supplémentaires. Le protocole Binius tire 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é de calcul de la multiplication, de l'élévation au carré et de l'inversion dans un champ binaire en tour de n bits (décomposable en m bits de sous-champs).

2.2 PIOP: version adaptée de HyperPlonk Product et PermutationCheck------s'applique au domaine binaire

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 comprennent :

1. GateCheck : Vérifiez si le témoin secret ω et l'entrée publique x satisfont la relation de calcul du circuit C(x,ω)=0, afin d'assurer 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 forment 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érifie si l'évaluation du polynôme est dans la table de recherche donnée, c'est-à-dire f(Bµ) ⊆ T(Bµ), en s'assurant que certaines valeurs sont dans la plage spécifiée.

4. MultisetCheck : vérifier 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 de garantir l'exactitude du produit polynômial.

6. ZeroCheck : Vérifier si un polynôme multivariable sur l'hypercube booléen en un point quelconque est nul ∏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 une évaluation de polynôme unidimensionnel, 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, construisant des combinaisons linéaires pour traiter plusieurs instances de vérification de sommes.

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

Bien que Binius et HyperPlonk partagent 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é 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 géré ce problème, même lorsque le dénominateur est nul, le ProductCheck de Binius peut continuer à fonctionner, permettant une généralisation à n'importe quelle valeur de produit.

• Vérification de permutation intercolonnes : 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 permutations polynomiales 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 multivariés plus complexes. Ces améliorations non seulement résolvent les limitations de HyperPlonk, mais jettent également les bases pour les systèmes de preuve basés sur des domaines binaires à l'avenir.

2.3 PIOP : nouvel argument de décalage multilinéaire ------ 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 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 à prendre les éléments les plus petits en position adjacente dans l'ordre lexicographique.