Anthropic affirme que Claude a démontré des propriétés de sécurité dans 123 bibliothèques

Anthropic a publié des travaux de recherche le 22 octobre 2026, indiquant que Claude avait produit des preuves formelles vérifiées par machine de propriétés de sécurité au niveau du code assembleur RISC-V pour 239 points d’entrée de tests de fuzzing répartis dans 123 bibliothèques open source, dans le cadre d’une collaboration avec Theorem.

Selon Anthropic, Claude a corrigé les bogues qu’il avait trouvés, puis prouvé que les programmes se termineraient toujours normalement, sans provoquer d’erreurs de sûreté mémoire ni faire échouer d’assertions, pour toute entrée de moins de 64 MB et toute réponse modélisée du système d’exploitation Linux ainsi que toute disposition mémoire modélisée. Les preuves supposent que le programme s’exécute comme un binaire statique monothread, avec une quantité de mémoire fixe, sur un processeur RISC-V utilisant Linux. Anthropic a indiqué que les preuves totalisaient environ 180 millions de lignes de Rocq et qu’une preuve type comptait environ 600 000 lignes pour couvrir des binaires dont la longueur médiane était de 18 000 instructions RISC-V. L’entreprise a déclaré qu’à sa connaissance, il s’agissait du premier effort de grande ampleur visant à utiliser l’IA pour appliquer la vérification formelle à des logiciels en production au niveau du code assembleur.

Une partie des preuves, ainsi que les sémantiques RISC-V et du système d’exploitation qui les sous-tendent, est en cours de publication sur GitHub. Anthropic a indiqué qu’elle publiait également les composants de confiance conçus pour le projet qui ne sont pas déjà publics, les preuves complètes des tests de fuzzing n’ayant nécessité aucun correctif et les spécifications des tests de fuzzing qu’elle n’a pas pu démontrer, tout en gardant confidentielles les preuves susceptibles de révéler un bogue non corrigé.

Transformer des tests de fuzzing en preuves formelles

Cette approche convertit le test de fuzzing compilable existant de chaque bibliothèque en une spécification formelle qui encode une règle : le test ne plante jamais, quelle que soit l’entrée de moins de 64 MB. La spécification est définie à partir des instructions RISC-V compilées, en s’appuyant sur la sémantique formelle de l’ensemble d’instructions RISC-V et des processus Linux de Theorem ; le vérificateur de preuves Rocq contrôle ensuite chaque preuve achevée par rapport à la spécification. Selon Anthropic, il ne reste ainsi que trois composants auxquels les développeurs doivent faire confiance : les modèles formels de RISC-V et des processus Linux, les énoncés exacts des théorèmes et le vérificateur Rocq lui-même.

Anthropic a indiqué avoir appliqué ce processus à des centaines de projets de l’initiative OSS-Fuzz de Google, qui assure des tests de fuzzing continus pour les projets open source répondant à ses critères et instrumente automatiquement les programmes C et C++ avec AddressSanitizer, un outil qui fait planter un programme chaque fois qu’un accès mémoire est incorrect. Une annexe datée du 22 octobre 2026 détaille le théorème complet démontré : pour toutes les entrées de moins de 64 MiB et toutes les dispositions mémoire, ni le binaire instrumenté avec ASan ni le binaire non instrumenté ne provoque de faute, n’avorte ou ne présente de comportement non modélisé ; tous deux produisent des traces de lecture et d’écriture, un comportement à la sortie et un état final du système de fichiers identiques.

L’annexe indique que Claude a écrit environ un milliard de lignes de Rocq au cours de l’effort, dont environ 180 millions ont passé le vérificateur de preuves ; le point d’entrée du parseur de cJSON, qui compte 391 lignes, a fait l’objet d’une preuve de 630 000 lignes, tandis que fftw3, avec 51 000 lignes intégrées à l’édition de liens, a fait l’objet d’une preuve de 480 000 lignes. Comme Claude était autorisé à modifier le code avant d’achever une preuve, Anthropic a indiqué avoir pénalisé les correctifs, accordé un bonus pour la démonstration des entrées dont le comportement avait été modifié par un correctif, et consigné et audité les correctifs afin de décourager la manipulation du système de récompenses.

Des bogues découverts au cours des tentatives de démonstration

Anthropic indique que les tentatives de démonstration ont mis au jour des centaines de bogues, dont beaucoup qu’un outil de fuzzing aurait peu de chances de trouver. En démontrant les propriétés du point d’entrée d’une bibliothèque, Claude a découvert un sous-débordement de compteur dans un décompresseur, qui provoquait une écriture hors limites, mais uniquement avec des entrées d’environ 20 MB présentant une disposition rare et spécifique. Parmi les autres découvertes figuraient une lecture hors limites dans un décodeur d’image nécessitant une entrée de 64 MB et plus de 2 GB de mémoire, une lecture hors limites exigeant une séquence particulière d’appels via deux descripteurs du même fichier, ainsi que la redécouverte de CVE-2026-56132 dans libexpat, qui nécessitait une entrée profondément imbriquée.

Claude a également découvert des bogues logiques qui ne provoquent jamais de plantage, notamment une restriction sur les fichiers qu’une application peut charger, qui n’est pas toujours appliquée. Anthropic a indiqué que des tentatives de vérification portant sur plusieurs applications critiques largement utilisées avaient révélé un bogue logique jusque-là inconnu, présent depuis plus de dix ans, et que, lors d’un effort visant à vérifier un lecteur PDF largement utilisé, l’équipe avait découvert en une semaine autant de bogues de sécurité qu’il s’en signale généralement en un an.

Autres expériences et observations sur l’efficacité

Au-delà d’OSS-Fuzz, Anthropic a demandé à Claude de rédiger une spécification formelle de la RFC 1950, le document technique qui définit le format de compression zlib, puis de démontrer que l’implémentation zlib du noyau Linux la respecte correctement. Claude a démontré directement les propriétés du binaire compilé pour x86, à l’aide d’une sémantique formelle de l’ensemble d’instructions x86 générée par Claude. Anthropic a indiqué avoir répété le processus pour une demi-douzaine d’autres bibliothèques largement utilisées et découvert des bogues mineurs et inexploitables dans des cas limites, qui sont en cours de signalement aux projets concernés. L’entreprise a également rapporté que la génération de la sémantique x86 avait permis de repérer des centaines d’erreurs dans la documentation de référence officielle, ainsi qu’un plus petit nombre de bogues dans le matériel lui-même, et que l’exécution pas à pas de cette sémantique pouvait démarrer un espace utilisateur Ubuntu sur un noyau Linux.

Lors d’une autre expérience, Claude a créé en Rust un interpréteur couvrant une grande partie de Python et a prouvé, à l’aide de l’outil de vérification Verus, qu’il respecte la sémantique de CPython décrite dans un article universitaire. L’annexe technique indique que les 17 niveaux de l’interpréteur ont été vérifiés et que le théorème établit que « chaque fois que l’interpréteur renvoie un résultat, celui-ci correspond à celui prescrit par la sémantique formelle ». Anthropic a déclaré que des tests empiriques menés sur 1,7 million de programmes Python générés aléatoirement ont révélé un comportement identique à celui de CPython dans 99,95 % des cas ; parmi les sept bogues délibérément introduits, cinq ont résisté aux tests aléatoires, tandis que les sept ont invalidé la preuve.

Pour mesurer l’efficacité, Anthropic a créé 36 petites tâches de vérification en réduisant la taille de points d’entrée réels d’OSS-Fuzz. Les programmes obtenus comptaient de 283 à 2 491 instructions, leurs entrées étaient limitées à 64 octets et AddressSanitizer avait été remplacé par un environnement d’exécution « mini-ASan » d’environ 100 instructions. Anthropic indique qu’Opus 5.5 prouve la moitié des tâches avec environ 40 % de jetons en moins qu’Opus 5. Anthropic indique également que les agents autorisés à copier les preuves des autres dans un espace de travail partagé ont eu besoin de 17 % de jetons en moins que ceux travaillant seuls ; certains ont réussi après avoir échoué seuls auparavant, tandis que les agents travaillant seuls n’ont pas réussi à achever deux des preuves. L’entreprise a déclaré que le même effet de réutilisation s’était manifesté à grande échelle lors de l’effort mené autour d’OSS-Fuzz : les équipes d’agents copiaient les preuves achevées et les adaptaient, car une grande partie de chaque preuve porte sur le code d’initialisation commun de l’environnement d’exécution C et d’AddressSanitizer.

Limites déclarées et programme OSS Verify

Anthropic précise que ces preuves ne signifient pas que les bibliothèques sont exemptes de bogues : des bogues subsistants pourraient se trouver dans les composants de confiance ou hors du périmètre des preuves. Celles-ci portent sur des binaires RISC-V statiques à un seul fil d’exécution, liés à musl libc, alors que la plupart des utilisateurs exécutent ces bibliothèques sur x86 ou ARM et les lient dynamiquement à glibc. De plus, AddressSanitizer ne détecte pas tous les bogues liés à la sécurité mémoire. L’entreprise a déclaré s’attendre à ce que ces limites deviennent surmontables à mesure que les modèles s’améliorent.

Theorem propose gratuitement le même processus aux projets open source admissibles par l’intermédiaire de son programme OSS Verify. Pour s’inscrire, il faut envoyer une demande de fusion ajoutant les fichiers project.yaml, Dockerfile et build.sh au dépôt du programme. Theorem indique qu’elle examine les projets selon des critères semblables à ceux d’OSS-Fuzz, en donnant la priorité aux infrastructures critiques largement utilisées. Selon Theorem, les responsables de maintenance reçoivent une preuve Rocq, vérifiée par le noyau Rocq, établissant que chaque cible de fuzzing ne plante pour aucune entrée d’au plus 64 MiB. Les bogues découverts au cours de la vérification sont signalés aux responsables de maintenance par courriel, à titre confidentiel et sans échéance de divulgation ; la production des preuves peut prendre plusieurs jours. La feuille de route de Theorem vise à vérifier l’ensemble de l’écosystème Nix, y compris des infrastructures critiques comme glibc, OpenSSL et cURL.