Séminaire de Hugo Delavenne et Daniel Augot, INRIA, GRACE
Calcul vérifiable (SNARK) à base de tests de proximités à des codes de Reed-Solomon (FRI)
Cette présentation effectuée par Hugo Delavenne fait suite à celle de Daniel Augot du 12 février dernier :
https://imath.univ-tln.fr/Seminaire-de-Daniel-Augot-et-Hugo-Delavenne-INRIA-GRACE.html
Titre :
Calcul vérifiable (SNARK) à base de tests de proximités à des codes de Reed-Solomon (FRI)
Résumé :
Supposons qu’un utilisateur veuille déléguer un long calcul à un serveur puissant mais éventuellement malhonnête. Comment cet utilisateur peut-il s’assurer que le résultat du calcul est correct ? Par exemple, un utilisateur souhaite faire appliquer un lourd modèle d’IA sur une entrée, et veut vérifier que le serveur n’applique pas un modèle plus simple ou plus biaisé. Une méthode non cryptographique serait de refaire le calcul ou d’obtenir la trace d’exécution et de la vérifier, mais ce n’est pas envisageable pour un utilisateur peu puissant. La solution cryptographique est d’utiliser des SNARK (Succinct Non-interactive ARguments of Knowledge). Plus précisément, étant donné un algorithme A et une entrée x, le serveur (prouveur) peut calculer la sortie y=A(x) et générer une preuve π du fait que "y=A(x)". L’utilisateur (vérifieur) peut alors vérifier que y est correct avec les données de x, A et π plus efficacement qu’en refaisant le calcul. Les trois grandes approches de SNARK sont à base de courbes elliptiques, de codes correcteurs, et plus récemment de réseaux euclidiens. Dans cet exposé je présenterai la principale construction à base de codes de Reed-Solomon.
La première étape de construction d’un SNARK, appelée l’arithmétisation, est la réduction de la vérification d’exécution correcte de A à la vérification d’égalités polynomiales entre polynômes construits avec la trace d’exécution de A. Ces polynômes sont ensuite encodés dans des codes de Reed-Solomon, ce qui permet au prouveur de faire une preuve très efficace de ces égalités polynomiales à l’aide du lemme de Schwartz-Zippel et de tests de proximités.
Un test de proximité permet d’établir qu’un vecteur u donné est proche d’un mot de code (en distance de Hamming) tout en ne regardant qu’un nombre restreint de coordonnées aléatoirement choisies de u (query), avec une probabilité d’échec négligeable (soundness). Concrètement, le protocole interactif FRI (Fast Reed-Solomon IOPP) permet au prouveur de convaincre le vérifieur que u est proche d’un code de Reed-Solomon, avec une soundness cryptographique 2^-λ, un nombre de query O(λ log(n)), et une complexité de vérification O(λ log(n)²).