💻 computer science

GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation

Cet article identifie et corrige deux écarts critiques dans l'implémentation de l'algorithme d'Euclide étendu de Go qui compromettent la génération de clés RSA, prouvant par la suite la correction et la terminaison du code corrigé à l'aide des outils de vérification Gobra et Lean tout en démontrant comment les agents d'IA peuvent aider à affiner les preuves formelles.

Auteurs originaux : Linard Arquint

Publié 2026-06-05

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Linard Arquint

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous construisez un coffre-fort numérique hautement sécurisé (comme ceux utilisés pour la banque en ligne ou la messagerie sécurisée). Pour verrouiller et déverrouiller ce coffre-fort, vous avez besoin d'une clé mathématique très spécifique et complexe. Dans le monde de l'informatique, cette clé est générée en utilisant une recette appelée l'algorithme du Plus Grand Commun Diviseur (PGCD) étendu.

Ce document traite d'une équipe de chercheurs qui est allée dans la « cuisine » du langage de programmation Go (un outil populaire utilisé pour construire des logiciels) pour vérifier si la recette de cette clé était suivie correctement. Ils ont découvert que la recette avait été légèrement altérée, et ils l'ont corrigée tout en prouvant mathématiquement que la nouvelle version fonctionne parfaitement.

Voici l'histoire de leur découverte, décomposée en parties simples :

1. L'erreur de « Copier-Coller »

Les développeurs de Go voulaient mettre à jour leur logiciel pour répondre à des normes de sécurité gouvernementales strictes. Pour ce faire, ils ont pris une recette provenant d'une source fiable et bien connue appelée BoringSSL (une bibliothèque sécurisée utilisée par Google) et l'ont « portée » (traduite) en Go.

Imaginez que c'est comme si un chef célèbre vous donnait une recette secrète pour un gâteau. Vous décidez de réécrire la recette de votre propre main pour la rendre plus facile à lire. Le document affirme qu'en réécant la recette, les développeurs de Go ont accidentellement modifié deux étapes importantes.

Le Problème : La recette originale avait une règle stricte : « Si vous ajoutez ces deux nombres, et que le résultat est trop grand, vous devez soustraire une quantité spécifique des deux nombres en même temps. » Cela empêche le gâteau de s'effondrer.
Le Bug : La version Go effectuait cette vérification de « trop grand » séparément pour chaque nombre. C'était comme vérifier la farine et le sucre indépendamment. Cela brisait l'équilibre mathématique (les « invariants ») qui garantit que la clé est correcte.
La Surprise : Trois experts humains différents ont examiné le code et n'ont pas vu cette erreur. Elle était si subtile qu'elle a échappé au filet de sécurité.

2. L'ingrédient « Trop Grand »

Le second problème concernait la taille des ingrédients autorisés.

La Règle : La recette originale disait : « Le premier ingrédient doit toujours être plus petit que le second. »
Le Changage : La version Go permettait au premier ingrédient d'être plus grand que le second.
La Correction : Les chercheurs n'ont pas eu besoin de modifier le code pour cela. Au lieu de cela, ils ont dû mettre à jour la « preuve » (la garantie mathématique) pour montrer que la recette fonctionne toujours avec des ingrédients plus grands.

3. Le Détective Magique (Gobra)

Pour prouver qu'ils avaient corrigé les bugs, les chercheurs ont utilisé un outil appelé Gobra.

L'Analogie : Imaginez un inspecteur robotique super strict et hyper attentif. Vous lui donnez le code et une liste de règles (spécifications). Le robot ne se contente pas d'exécuter le code ; il simule chaque façon possible dont le code pourrait s'exécuter, vérifiant chaque chemin pour s'assurer qu'il ne viole jamais les règles.
Le Résultat : Le robot a confirmé qu'une fois le « bug de synchronisation » corrigé, le code était 100 % correct. En fait, parce que la correction a supprimé des étapes inutiles, le nouveau code s'exécute en réalité 24 % plus vite que la version buggée.

4. L'Assistant IA

Les chercheurs n'ont pas fait tout le travail difficile seuls. Ils ont utilisé un agent d'IA (un programme informatique intelligent) pour les aider.

Comment cela fonctionnait : L'IA agissait comme un apprenti infatigable. Quand le robot inspecteur (Gobra) disait : « Cette partie n'a pas de sens », l'IA suggérait des modifications aux règles ou au code.
Le Piège : L'IA supposait initialement que le code était parfait et essayait de forcer les mathématiques à correspondre. Les chercheurs humains ont dû lui dire : « Non, le code est réellement faux ; cherche la différence. » Une fois que l'IA a compris cela, elle est devenue incroyablement utile, suggérant des corrections et aidant à écrire les preuves mathématiques.

5. La Conclusion

Le document conclut par trois leçons principales :

Même les experts font des erreurs subtiles : Trois réviseurs humains ont manqué un bug critique qu'un outil de preuve formelle a trouvé.
La vérification formelle est puissante : Utiliser un outil comme Gobra, c'est comme avoir une garantie mathématique que votre code fonctionne, plutôt que d'espérer simplement qu'il fonctionne parce qu'il a passé quelques tests.
L'IA est un excellent partenaire : L'IA peut aider les humains à écrire ces preuves complexes, mais les humains doivent toujours guider l'IA pour qu'elle remette en question le code plutôt que de simplement l'accepter.

En bref : Les chercheurs ont trouvé une faille cachée dans un algorithme de sécurité critique dans la bibliothèque standard de Go, l'ont corrigée, ont prouvé mathématiquement que la correction fonctionne, et ont montré que la correction rend en fait le logiciel plus rapide. Ils ont fait cela en combinant l'intuition humaine, des outils de preuve automatisés et l'assistance de l'IA.

Résumé Technique : GCD : Garbled, Corrected, Demonstrandum

Énoncé du Problème

L'article traite de la correction et de la vérification de l'implémentation de l'algorithme d'Euclide étendu (GCD étendu) au sein de la bibliothèque standard de Go (crypto/internal/fips140/bigmod). Cette implémentation est critique pour la génération de paires de clés RSA, un composant fondamental pour TLS, SSH et PGP. L'implémentation Go a été introduite dans Go 1.24 pour supporter nativement la conformité FIPS 140-3, remplaçant ainsi la dépendance à BoringSSL.

Les auteurs ont identifié une divergence critique : bien que le code Go soit présenté comme un port direct de l'implémentation de BoringSSL (qui est formellement vérifiée via l'assistant de preuve Rocq via Fiat Cryptography), la version Go contenait des déviations subtiles. Ces déviations ont brisé les invariants mathématiques de l'algorithme, compromettant potentiellement la correction du calcul de l'inverse modulaire requis pour les clés privées RSA. De plus, l'implémentation Go permettait un domaine d'entrée plus large que la version prouvée de BoringSSL, invalidant les hypothèses de preuve existantes.

Méthodologie

Les auteurs ont employé une approche de vérification de programmes déductive utilisant Gobra, un vérificateur de Go basé sur la logique de séparation. La méthodologie comprenait :

Spécification Formelle : Les auteurs ont formalisé les spécifications en langage naturel des fonctions Go (extendedGCD, InverseVarTime, GCDVarTime) en spécifications Gobra, incluant les préconditions, les postconditions et les invariants de boucle.
Analyse des Écarts : En tentant de vérifier le code Go existant par rapport aux spécifications dérivées de la preuve de BoringSSL, les auteurs ont identifié deux classes majeures de déviations :
- Soustractions Non Synchronisées : L'implémentation Go mettait à jour les coefficients de Bézout ( $A, B, C, D$ ) indépendamment selon des conditions locales, alors que l'implémentation de référence exigeait des réductions synchronisées pour maintenir les invariants de boucle.
- Expansion du Domaine d'Entrée : L'implémentation Go autorisait des entrées où $a \ge n$ , violant la précondition $a < n$ requise par la preuve originale.
Construction de la Preuve :
- Correction du Code : Les auteurs ont proposé une correction pour les soustractions non synchronisées afin d'aligner la logique de Go avec les invariants mathématiques.
- Adaptation de la Preuve : Ils ont porté la preuve existante de BoringSSL de Rocq vers Gobra. Pour la déviation du domaine d'entrée, ils ont assoupli les invariants et les postconditions pour couvrir le cas où $a \ge n$ , prouvant que la valeur du GCD reste correcte même si la propriété de l'inverse modulaire ne tient pas dans ce cas spécifique.
- Vérification Hybride : Pour les lemmes d'arithmétique non linéaire que le solveur SMT Z3 (utilisé par Gobra) ne pouvait pas traiter, les auteurs ont utilisé l'assistant de preuve Lean pour prouver des lemmes clés et les ont importés dans Gobra en tant que lemmes trusted (de confiance).
Vérification Assistée par IA : Les auteurs ont utilisé un agent IA (Claude Code d'Anthropic) pour affiner de manière itérative les invariants et les lemmes en fonction des messages d'erreur de Gobra, réduisant considérablement l'effort manuel de construction de la preuve.

Principales Contributions

Découverte de Bugs : L'article révèle deux déviations subtiles mais critiques dans l'implémentation du GCD étendu de Go qui brisent les invariants algorithmiques. Ces bugs étaient présents dans un code ayant subi plusieurs revues et affirmé être un port direct d'une implémentation vérifiée.
Optimisation des Performances : La correction proposée pour la déviation de soustraction non synchronisée restaure non seulement la correction, mais entraîne également une accélération moyenne de 24 % (moyenne géométrique) en éliminant les allocations de mémoire inutiles et les opérations redondantes dans le corps de la boucle.
Vérification Formelle de la Crypto Go : Les auteurs ont vérifié avec succès l'implémentation corrigée de Go, sa terminaison et sa correction par rapport aux spécifications formelles en utilisant Gobra. Il s'agit de la première vérification formelle de ce composant spécifique dans la bibliothèque standard de Go.
Portage et Généralisation de la Preuve : Ils ont réussi à porter une preuve de Rocq (Fiat Cryptography) vers Gobra et à la généraliser pour couvrir le domaine d'entrée plus large permis par l'implémentation de Go.
IA dans la Vérification : Ce travail démontre l'efficacité des agents IA pour faciliter la vérification formelle en itérant de manière autonome sur les spécifications et en identifiant les causes racines des échecs de preuve (par exemple, en suggérant que la réduction indépendante des coefficients était le problème).

Résultats

Correction : L'implémentation corrigée a été vérifiée avec succès en 16,9 secondes sur un ordinateur portable standard. La vérification couvre la fonction extendedGCD et ses clients InverseVarTime et GCDVarTime.
Performance : Les benchmarks sur diverses tailles de limbs (64 à 8192 bits) ont montré que l'implémentation vérifiée est systématiquement plus rapide que l'originale. L'accélération moyenne était de 23,98 %, avec des améliorations allant de 15,6 % à 36 % selon la taille des entrées. L'accélération est attribuée aux mises à jour en place et à l'élimination des allocations de buffers intermédiaires.
Divulgation et Impact : Les auteurs ont divulgué les déviations aux mainteneurs de la cryptographie de Go. Les mainteneurs ont confirmé que, bien que ces déviations puissent théoriquement conduire à des inverses modulaires incorrects, des vérifications défensives dans le code de génération de clés RSA détecteraient ces erreurs et renverraient une erreur plutôt qu'une clé incorrecte, limitant l'impact à la disponibilité plutôt qu'à la sécurité. Les corrections sont en cours d'examen pour inclusion dans la bibliothèque standard de Go.
Intégration Continue : Grâce au temps de vérification rapide, la preuve a été intégrée au flux de travail d'intégration continue (CI) du projet pour vérifier automatiquement toute déviation future.

Signification et Revendications

L'article affirme que son travail met en évidence trois idées principales :

Bugs Subtils dans le Code Revu : Même un code bien revu, surtout lorsqu'il est présenté comme un port direct d'une implémentation vérifiée, peut contenir des bugs subtils qui brisent les invariants.
Puissance de la Vérification Formelle : La vérification formelle est un outil puissant pour découvrir ce type de bugs que les tests et la revue manuelle pourraient manquer.
Rôle des Agents IA : Les agents IA peuvent faciliter efficacement le processus de vérification en affinant de manière itérative les invariants et les lemmes sur la base des retours du vérificateur, bien que la supervision humaine reste nécessaire pour le nettoyage final et la compréhension structurelle.

Les auteurs soulignent que leur travail comble l'écart entre l'implémentation et sa preuve. En vérifiant directement le code Go plutôt qu'en se basant sur l'existence d'une preuve pour une autre implémentation (BoringSSL), ils garantissent que le code spécifique exécuté en production est mathématiquement sain. Ils notent également que, bien qu'ils s'appuient sur des fonctions trusted pour les opérations de bas niveau sur les bits, l'argument de correction globale est décomposé en composants petits et révisables, augmentant la confiance dans la fiabilité du système.