Analyse des principes de Binius STARKs et réflexions 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 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 occupant l'ensemble du 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 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 un grand nombre d'espaces gaspillés. En comparaison, le domaine binaire permet d'opérer directement sur les bits, offrant un codage compact et efficace sans aucun espace gaspillé, soit la quatrième génération de STARKs.

Comparé aux domaines finis récemment découverts tels que Goldilocks, BabyBear et 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 :

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

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

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

• Protocole FRI et zk-STARK d'origine, ainsi que la fonction de hachage Grøstl, qui est entrée en 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 dépend entièrement de l'extension de domaine pour assurer sa sécurité et sa faisabilité pratique. La plupart des polynômes impliqués dans les calculs de Prover n'ont pas besoin d'entrer dans l'extension de domaine et peuvent simplement opérer dans le domaine de base, ce qui permet d'atteindre 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 trace dans les STARKs, la taille du domaine utilisée doit être supérieure au degré du polynôme ; lors de l'engagement dans l'arbre Merkle dans les STARKs, il est nécessaire de faire un codage de Reed-Solomon, 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 pour traiter ces deux problèmes de manière distincte et représenter les mêmes données de deux manières différentes : tout d'abord, en utilisant des polynômes multivariés (plus précisément des polynômes multilinaires) à la place de polynômes à une seule variable, en représentant l'ensemble de la trajectoire de calcul par ses valeurs sur les "hypercubes" ; ensuite, étant donné que la longueur de chaque dimension de l'hypercube est de 2, il n'est pas possible de procéder à une extension standard de Reed-Solomon comme avec les STARKs, mais l'hypercube peut être considéré comme un carré, et l'extension de Reed-Solomon peut être 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 :

• Preuves d'oracle interactif polynomial (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP) : Le PIOP, en tant que système de preuve central, transforme les relations de calcul en égalités polynomiales vérifiables. Différents protocoles PIOP permettent, à travers une interaction avec le vérificateur, au prouveur d'envoyer progressivement des polynômes, permettant ainsi au vérificateur de valider la justesse des calculs en interrogeant un nombre réduit d'évaluations 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 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 au prouveur 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 différentes performances, sécurité et cas d'utilisation.

Selon les besoins spécifiques, choisissez différents PIOP et PCS, et combinez-les avec un domaine fini ou une courbe elliptique appropriée, afin 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. Halo2 a été conçu en mettant l'accent sur l'évolutivité et l'élimination du trusted setup dans le protocole ZCash.

• Plonky2 : utilise la combinaison de PLONK PIOP et de FRI PCS, basée 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ée, afin d'assurer la correction, les performances et la sécurité du système. Le choix de ces combinaisons influence non 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 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, une arithmétique basée sur des tours de domaines binaires constitue la base de ses calculs, permettant d'effectuer des opérations simplifiées dans le domaine binaire. Deuxièmement, Binius a adapté les vérifications de produits et de permutations 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é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 polynômial sur petits domaines (Small-Field PCS), lui permettant de mettre en œuvre un système de preuve efficace dans le domaine binaire et réduisant les frais généralement associés aux grands domaines.

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

Les corps binaires en tour sont la clé pour réaliser un calcul vérifiable rapide, principalement en raison de deux aspects : le calcul efficace et l'arithmétique 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 permet un processus d'arithmétisation simplifié, c'est-à-dire que les opérations effectuées sur les corps binaires peuvent être exprimé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, font des corps binaires un choix particulièrement adapté pour des systèmes de preuve évolutifs comme Binius.

Le terme "canonical" fait référence à la représentation unique et directe des éléments dans un corps binaire. Par exemple, dans le corps binaire de base F2, 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 premiers, qui ne peuvent pas fournir cette représentation canonique dans un nombre de bits donné. Bien qu'un corps premier de 32 bits puisse être contenu dans 32 bits, ce n'est pas le cas pour chaque chaîne de 32 bits, qui ne peut pas correspondre de manière unique à un élément de corps, alors que le corps binaire offre cette commodité de correspondance un à un. Dans le corps 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 corps finis spécifiques comme Mersenne-31 ou Goldilocks-64. Dans le corps 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 corps binaire ne nécessite pas l'introduction de retenues dans les 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 de simplification (X + Y )2 = X2 + Y2.

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 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, seize é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 supplémentaire, il s'agit simplement d'une conversion de type (typecast) de la chaîne de bits, ce qui est une propriété très intéressante et utile. En outre, les éléments de petit 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é des calculs. De plus, le document "On Efficient Inversion in Tower Fields of Characteristic Two" explore la complexité calculatoire des opérations de multiplication, de mise au carré et d'inversion dans un domaine binaire tour de n bits (décomposable en m bits de sous-domaines).

2.2 PIOP : version adaptée de HyperPlonk Product et PermutationCheck ------ applicable aux corps binaires

La conception de PIOP dans le protocole Binius s'inspire de HyperPlonk et utilise une série de mécanismes de vérification fondamentaux pour valider la justesse des polynômes et des ensembles multivariés. Ces vérifications fondamentales 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 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 l'hypercube booléen sont 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µ), garantissant 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 d'un polynôme rationnel sur l'hypercube booléen est égale à une certaine 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 à un point quelconque sur l'hypercube booléen ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, afin de s'assurer de 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 une évaluation d'un polynôme à une 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 traiter plusieurs instances de vérification de sommes.

8. BatchCheck : basé sur SumCheck, vérifie l'exactitude 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 des protocoles, Binius a amélioré les trois aspects 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.

• 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 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 intercolonnes : HyperPlonk ne prend pas en charge cette fonction ; Binius prend en charge la vérification de permutation entre plusieurs colonnes, ce qui permet à Binius de gérer des cas de permutation polynomiale plus complexes.

Ainsi, Binius a amélioré la flexibilité et l'efficacité du protocole grâce à des améliorations apportées au mécanisme PIOPSumCheck existant, offrant un soutien fonctionnel plus fort lors du traitement de validations de polynômes multivariables plus complexes. Ces améliorations non seulement résolvent les limitations de HyperPlonk, mais posent également les bases pour de futurs systèmes de preuves basés sur des domaines binaires.

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 optimise l'opération en regroupant les plus petits éléments adjacents dans l'ordre lexicographique en éléments plus grands. L'opérateur Pack cible des blocs de taille 2κ et les regroupe.