Anthropic développe une technique de vérification formelle des logiciels existants à l'aide de l'IA

La société Anthropic a présenté les résultats d'expériences sur l'utilisation de modèles d'IA pour la vérification formelle de la fiabilité et de la sécurité des projets existants. Au cours de l'expérience, des preuves mathématiques de l'absence d'erreurs de gestion de la mémoire ont été générées à l'aide de modèles d'IA pour 123 bibliothèques open source testées dans l'infrastructure OSS Fuzz.

La vérification a été effectuée au niveau du code assembleur compilé pour l'architecture RISC-V. Le volume total des preuves générées a atteint environ 180 millions de lignes de code pour le système de vérification Rocq Prover (environ 600 000 lignes pour un fichier binaire avec 18 000 instructions RISC-V). Les preuves ont été établies par la conversion automatique des tests fuzzing existants en spécifications formelles, après quoi le modèle d'IA Claude a prouvé qu'aucun plantage ne se produit dans le programme avec n'importe quelle entrée allant jusqu'à 64 Mo.

Dans le processus de construction des preuves, le modèle d'IA a pu identifier et préparer des corrections pour des centaines d'erreurs qui n'avaient pas été remarquées lors des tests fuzzing. Parmi celles-ci, des vulnérabilités entraînant un dépassement de tampon lors du traitement de certaines entrées (par exemple, CVE-2026-56132 dans libexpat), ainsi que des erreurs logiques. De plus, le modèle d'IA a été utilisé pour prouver que l'implémentation de l'algorithme zlib dans le noyau Linux est conforme à la spécification RFC 1950.

Un interpréteur pour un sous-ensemble du langage Python a également été généré en Rust, pour lequel une preuve formelle de conformité à la sémantique de CPython a été préparée à l'aide des outils Verus. Pour comparer le comportement avec CPython, plus de 1,7 million de programmes Python générés aléatoirement ont été exécutés. Dans 99,95 % des cas, les résultats d'exécution de ces programmes dans la nouvelle implémentation et dans CPython ont été identiques, et les divergences observées se sont révélées être des cas limites connus.

La vérification formelle réalisée garantit la conformité aux spécifications, mais n'exclut pas totalement l'émergence de problèmes de sécurité, car les risques liés à la concurrence, au liage dynamique et au comportement anormal du matériel réel ne sont pas formalisés. L'avantage clé de l'approche proposée réside dans le travail direct avec les fichiers binaires, ce qui permet de se passer de la nécessité de réécrire le code existant dans des langages formellement vérifiables.

Source : opennet.ru