Microsoft Research dévoile Magnetar : une zkVM 10–39 fois plus rapide que ses concurrentes

Microsoft Research a présenté Magnetar, une zero-knowledge virtual machine qui prouve l'exécution de programmes ordinaires en Rust, Go et C. Le programme s'exécute normalement et fournit, avec son résultat, une courte preuve que ce code, appliqué à ces entrées, a bien produit cette sortie. La vérification prend environ 12 millisecondes. Sur un ordinateur portable, Magnetar traite 7,2–8,7 millions d'instructions processeur par seconde et devance en moyenne de 10–39 fois les zkVM comparables les plus rapides. L'auteur des travaux est Srinath Setty, chercheur principal senior et responsable d'équipe chez Microsoft Research.

Trois problèmes qu'on n'arrivait pas à résoudre en même temps

Les preuves à divulgation nulle de connaissance ont été inventées dans les années 1980, mais elles ne sont jamais devenues un outil universel. Trois obstacles s'y opposaient, et chacun ne pouvait être levé qu'au détriment des autres.

Le premier est l'efficacité. Jusqu'ici, générer une preuve exigeait des millions de fois plus de calcul que l'exécution du programme lui-même. Le deuxième est la commodité. Beaucoup de systèmes obligent le développeur à réécrire à la main son programme sous forme de circuit cryptographique (circuit), ce qui prend des mois ; chaque modification de l'application impose un nouveau circuit et de nouvelles sources de bugs. L'alternative universelle consiste à prouver l'exécution d'un processeur ordinaire, mais elle a longtemps coûté trop cher en vitesse ou en sécurité.

Le troisième est le socle cryptographique. Beaucoup de systèmes reposent sur des courbes elliptiques, qu'un ordinateur quantique suffisamment puissant peut casser. Les variantes post-quantiques s'appuient soit sur des réseaux euclidiens, soit sur de nouvelles fonctions de hachage conçues pour rendre la preuve peu coûteuse, soit sur des conjectures non démontrées concernant les codes correcteurs d'erreurs. Dans ces systèmes, la vitesse s'obtient au prix d'hypothèses fortes.

Dix ans de briques : de quoi Magnetar est fait

Magnetar est l'aboutissement de plus de dix ans de travaux chez Microsoft Research. Les chercheurs ont avancé par étapes, chaque travail réglant une partie du problème :

• Spartan (2019) a remis en avant l'approche sum-check et l'a rendue utilisable pour des programmes généralistes, sans configuration de confiance (trusted setup) ; il accepte différents blocs cryptographiques.
• Phalanx (2021) exploite la répétitivité, par exemple un même cycle d'instructions processeur, et prouve les calculs environ un ordre de grandeur plus vite que Spartan. La description du processeur dans Magnetar repose sur cette idée.
• Nova, HyperNova, NeutronNova, Neo et SuperNeo interrompent prématurément la preuve Spartan et replient les résultats partiels, ce qui rend la preuve de calculs de n'importe quelle taille nettement moins coûteuse.
• Brakedown (2021) est un schéma d'engagement rapide fondé sur des fonctions de hachage ; associé à Spartan, il a donné la première variante dont la sécurité repose sur des hachages standard.
• Spice, Lasso, Nebula, Twist and Shout ont rendu peu coûteuses les opérations sur la mémoire, sur lesquelles repose un processeur généraliste.
• Jolt a montré qu'en combinaison avec Spartan, on peut prouver efficacement l'exécution d'un processeur entier.
• Vega a appliqué ces idées à l'identité numérique : des faits tirés d'un document officiel se prouvent en moins d'un dixième de seconde.
• BinarySpartan a transposé Spartan dans des corps binaires, où la logique du processeur et les fonctions de hachage standard s'expriment efficacement.
• Ligerito est un schéma d'engagement de type Brakedown, avec des preuves nettement plus courtes.
• Ring switching permet de s'engager efficacement sur des vecteurs de bits.

Vitesse et sécurité en chiffres

Magnetar prouve l'exécution de RISC-V, une architecture ouverte pour laquelle il existe des compilateurs matures pour pratiquement tous les grands langages. Le développeur écrit son programme en Rust, Go ou C, le compile et obtient une preuve sans avoir à le réécrire sous forme de circuits. Une politique métier, un pipeline de données ou un interpréteur de machine virtuelle Ethereum : ce sont tous des programmes ordinaires.

Principaux indicateurs :

• 7,2–8,7 millions d'instructions processeur par seconde sur un ordinateur portable ;
• 9,5–12,8 millions de cycles par seconde dans la version optimisée, ce qui multiplie par environ 1,3 tous les gains annoncés ;
• 10–39 fois plus rapide en moyenne que les zkVM existantes les plus rapides, sur 15 programmes de test, du hachage cryptographique aux transferts de jetons dans un petit interpréteur EVM ;
• plus de 300 fois plus rapide que deux autres systèmes sur le test de transfert de jetons ;
• vérification de la preuve en 12 ms environ.

La sécurité de Magnetar repose sur une fonction de hachage standard comme SHA-256 ou SHA-3. Il ne nécessite ni courbes elliptiques, ni réseaux euclidiens, ni fonctions de hachage spécialisées, ni configuration de confiance, ni conjectures non démontrées sur les codes. Les fonctions de hachage sont les primitives les mieux étudiées en cryptographie ; les signatures à base de hachage, que le NIST a standardisées comme option post-quantique conservatrice, s'appuient sur elles. Pour Microsoft, c'est aussi une question de cohérence avec le programme Quantum Safe, censé faire migrer les produits vers la cryptographie post-quantique d'ici 2029.

L'architecture elle-même apporte un autre avantage. La vérification d'une preuve se compose essentiellement de hachages et d'arithmétique dans des corps binaires, c'est-à-dire d'opérations que Magnetar prouve efficacement. Pour lui, la vérification devient donc une charge de travail ordinaire, et le système peut prouver des calculs de n'importe quelle taille par morceaux, puis assembler ces morceaux. Cela permet aussi de prouver des systèmes à longue durée de vie, comme un registre ou une blockchain.

À quoi cela peut servir en pratique

Le scénario le plus proche pour l'IA concerne les agents. Un agent qui agit au nom d'un utilisateur peut joindre à chaque action une preuve qu'elle respectait la politique qui lui a été assignée. Le vérificateur n'a pas à faire confiance à l'opérateur de l'agent ni à lire ses logs. Les établissements financiers réglementés pourront prouver le traitement correct des transactions sans les divulguer.

Pour les ingénieurs, l'essentiel est ailleurs : le ticket d'entrée baisse. Si une équipe maintient déjà du code en Rust, Go ou C, elle n'a pas besoin d'un spécialiste en cryptographie pour écrire des circuits. Reste à savoir quels résultats les entreprises voudront vérifier plutôt que de les accepter sur parole. Microsoft Research invite à discuter des cas d'usage ; l'article technique, qui détaille la conception, l'analyse de sécurité et les mesures, s'intitule « Magnetar: High-speed post-quantum RV64 zkVM from standard hashes ».