Analyse des principes 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 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 de l'encodage 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 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 d'opérer directement sur les bits, rendant le codage compact, efficace et sans espace gaspillé, c'est-à-dire les STARKs de quatrième génération.

Comparé aux domaines finis récemment découverts par des recherches telles que Goldilocks, BabyBear et Mersenne31, l'étude des domaines binaires remonte aux années 1980. Actuellement, les domaines binaires sont largement utilisés en cryptographie, des exemples typiques incluent :

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

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

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

• Les protocoles FRI et zk-STARK d'origine, 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 particulièrement adapté à la récursivité.

Lorsqu'un domaine plus petit est utilisé, 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 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 domaine, mais doivent simplement opérer dans 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 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 dans l'arbre de Merkle des STARKs, un codage de Reed-Solomon doit être effectué, et la taille du domaine utilisée doit être supérieure à la taille après 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 ( spécifiquement des polynômes multilinaires ) à la place de polynômes univariés, en représentant l'ensemble de la trajectoire de calcul par leurs valeurs sur les "hyper-cubes" (; ensuite, étant donné que la longueur de chaque dimension de l'hyper-cube est de 2, il n'est pas possible de procéder à une extension Reed-Solomon standard comme avec les STARKs, mais l'hyper-cube peut être considéré comme un carré ), sur la base duquel une extension Reed-Solomon peut être effectuée. 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 :

• Preuve d'oracle interactif polynomial en théorie de l'information (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP) : Le PIOP, en tant que 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 grâce à l'interaction avec le vérificateur, permettant à ce dernier de 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, chacun ayant une manière différente de traiter les expressions polynomiales, ce qui affecte 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 égalité polynomiale générée par PIOP est valide. Le PCS est un outil cryptographique qui permet à un 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 ont des performances, des niveaux de sécurité et des cas d'utilisation 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, pour construire des systèmes de preuve avec différentes propriétés. Par exemple:

• Halo2 : combiné avec PLONK PIOP et Bulletproofs PCS, basé sur la courbe Pasta. Halo2 est conçu avec un accent sur l'évolutivité et la suppression de la configuration de confiance du protocole ZCash.

• Plonky2 : utilise PLONK PIOP associé à FRI PCS et basé sur le domaine de Goldilocks. Plonky2 a été 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 champ 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 atteindre la transparence sans nécessiter de configuration de confiance, ainsi que la possibilité de prendre en charge 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é. Premièrement, la construction arithmétique basée sur les tours de domaines binaires (towers of binary fields) constitue la base de ses calculs, permettant d'effectuer des opérations simplifiées dans le domaine binaire. Deuxièmement, Binius a adapté le contrôle de produit et de permutation de HyperPlonk dans son protocole de preuve Oracle interactif (PIOP), garantissant une vérification sécurisée et efficace de la cohérence 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 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 le schéma d'engagement polynomial sur de petits domaines (Small-Field PCS), lui permettant de mettre en œuvre 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 Domain fini : arithmétisation basée sur les tours des corps 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é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 supporte 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" fait référence à la représentation unique et directe des éléments dans un 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 cette représentation canonique dans un nombre de bits donné. Bien qu'un champ 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 de champ, alors que le champ binaire a cette commodité de mappage 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écifiques pour des champs finis particuliers tels que Mersenne-31 ou Goldilocks-64. Dans le champ binaire F2k, les méthodes de réduction courantes incluent 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 utilisée dans Tower ). Le papier "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" indique que le champ binaire ne nécessite pas d'introduction de retenue dans les opérations d'addition et de multiplication, et que l'opération de mise au carré dans le champ binaire est très efficace, car elle suit la règle simplifiée (X + Y )2 = X2 + Y2.

Comme illustré à 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 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 n'implique 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, des é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 exploite 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 des opérations de multiplication, d'élévation au carré et d'inversion dans les domaines binaires de tour de n bits ( décomposables en sous-domaines de m bits ).

( 2.2 PIOP: version adaptée du produit HyperPlonk et Vérification de Permutation------appliqué au domaine binaire

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 l'exactitude des polynômes et des ensembles multivariables. Ces vérifications essentielles comprennent :

1. GateCheck : Vérifiez si le témoin de confidentialité ω et l'entrée publique x satisfont la relation d'opération du circuit C)x,ω###=0, pour garantir le bon fonctionnement du circuit.

2. PermutationCheck : Vérifie si les résultats d'évaluation des deux polynômes multivariables f et g sur l'hypercube boolé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érifier si l'évaluation du polynôme se trouve dans la table de recherche donnée, c'est-à-dire f)Bµ) ⊆ T(Bµ), s'assurer 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érifiez si l'évaluation d'un polynôme rationnel sur le cube hypercubique 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 multivariable est nul à 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 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 évaluation d'un polynôme univarié, cela réduit la complexité de calcul pour le vérificateur. De plus, SumCheck permet également 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 somme.

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

Bien que Binius et HyperPlonk présentent de nombreuses similitudes dans la conception des protocoles, Binius apporte des améliorations dans les trois 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é de calcul.

• Gestion des problèmes de division par zéro : HyperPlonk n'a pas réussi à gérer 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 nul, 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 traiter des cas de permutation polynomiale 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 vérifications de polynômes multivariés plus complexes, offrant un support fonctionnel plus robuste. Ces améliorations ne se contentent pas de résoudre les limitations de HyperPlonk, mais jettent également les bases pour de futurs systèmes de preuve basés sur des corps binaires.

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

• Packing: Cette méthode passe par