Microsoft utilise des agents IA pour prouver mathématiquement que son code de chiffrement n'a aucun défaut

Points clés

• La bibliothèque SymCrypt de Microsoft, le moteur de cryptographie utilisé dans Windows et Azure, fait l'objet d'une vérification formelle à l'aide d'une chaîne d'outils combinant Rust, Lean et Aeneas depuis mi-2024.
• Les premiers algorithmes vérifiés sont SHA-3, une norme pour créer des empreintes numériques de données, et ML-KEM, un schéma de chiffrement post-quantique conçu pour résister aux attaques des futurs ordinateurs quantiques.
• Les agents IA, des logiciels capables d'effectuer des tâches en plusieurs étapes de manière autonome, rédigent des étapes de preuve mathématique que les ingénieurs révisent et vérifient indépendamment.
• Microsoft a rendu open-source le code vérifiéé, les spécifications et les preuves dans une branche publique de SymCrypt, mettant le travail à disposition pour un examen extérieur.
• Les algorithmes futurs prévus pour le même traitement incluent AES-GCM, FrodoKEM et ML-DSA, qui protègent tous les données dans Windows et Linux aujourd'hui.

Le code cryptographique, le logiciel qui brouille et protège les données dans chaque application, navigateur et système d'exploitation, est notoirement implacable. Une seule vérification de limites manquée, c'est-à-dire un défaut de confirmation qu'un nombre reste dans une plage sûre, peut fissurer la sécurité qui semble solide en surface. Les tests détectent de nombreux bugs. Ils ne les détectent pas tous.

Microsoft Research explore une approche différente : prouver que le code est correct, mathématiquement, avant qu'il ne soit déployé.

Le projet se concentre sur SymCrypt, la bibliothèque cryptographique open-source de Microsoft qui s'exécute dans Windows et Azure Linux. Les ingénieurs écrivent maintenant de nouveaux algorithmes cryptographiques en Rust, un langage de programmation qui exclut de familles entières d'erreurs de sécurité mémoire par conception. Ils passent ensuite ces programmes Rust à travers un outil appelé Aeneas, qui traduit le code sous une forme que l'assistant de preuve Lean peut analyser.

Lean n'est pas un chatbot. C'est un cadre de preuve formelle, un logiciel qui vérifie les arguments mathématiques comme une calculatrice vérifie l'arithmétique, sauf qu'il vérifie les preuves, et il ne commet jamais d'erreur arithmétique.

L'objectif est de produire un théorème : pour chaque entrée valide, cette implémentation retourne exactement le résultat que la norme publiée dit qu'elle devrait. Pas généralement. Toujours.

La première version publique couvre SHA-3, un algorithme standard pour créer une empreinte numérique unique de n'importe quel élément de données, et ML-KEM, un schéma d'échange de clés post-quantique. La cryptographie post-quantique signifie des algorithmes construits pour rester sécurisés même contre les ordinateurs quantiques, des machines qui pourraient casser de nombreuses méthodes de chiffrement actuelles.

Comment l'IA s'intègre-t-elle dans une preuve mathématique ?

Rédiger des preuves formelles est lent. C'est là que les agents IA interviennent.

Les agents gèrent les étapes répétitives intermédiaires, rédigeant des fragments de preuve qui relient les résultats intermédiaires. Les ingénieurs se concentrent sur les parties qui nécessitent un véritable jugement : vérifier que la spécification formelle correspond réellement à ce que la norme publiée dit, et examiner les propriétés haut niveau que le code doit satisfaire. La vérification des preuves elle-même est entièrement automatisée et déterministe, ce qui signifie que la machine accepte ou rejette la preuve. Il n'y a aucune place pour que l'agent fasse semblant.

Microsoft décrit cela comme une division claire : les agents rédigent, les humains révisent, le vérificateur de preuve décide.

Pour les personnes qui utilisent Windows, Azure ou tout service qui dépend de la pile de sécurité de Microsoft, le sens pratique est simple. Le chiffrement protégeant vos fichiers, vos données cloud et vos identifiants est tenu à une norme plus élevée que ce que seuls les tests peuvent fournir. Si les preuves réussissent, le code fait exactement ce que la norme l'exige.

La branche open-sourcée permet aux chercheurs externes d'inspecter à la fois le code Rust et les preuves côte à côte, donc les affirmations ne sont pas seulement la parole de Microsoft.

À surveiller : les annonces de versions formellement vérifiées atteignant les versions stables de Windows, et si d'autres bibliothèques de cryptographie adoptent des flux de travail de preuve assistés par IA similaires. Ce serait un véritable changement dans la façon dont l'industrie pense à la correction des logiciels.