Anthropic affirme que Claude a prouvé la sécurité de 123 bibliothèques

Anthropic déclare que son modèle Claude a rédigé des preuves mathématiques vérifiées par machine démontrant que le code compilé de 123 bibliothèques open source ne peut pas planter dans des conditions définies. Le modèle a également découvert des bugs qui étaient passés inaperçus pendant des années malgré des milliers de milliards de tests, selon une recherche publiée le 22 octobre par le Frontier Red Team de l'entreprise, qui a collaboré sur ce projet avec le cabinet de méthodes formelles Theorem.anthropic.com

L'entreprise qualifie cela de ce qu'elle croit être "le premier effort à grande échelle utilisant l'IA pour appliquer une vérification formelle à des logiciels de production au niveau du code assembleur". Anthropic soutient que l'IA peut désormais trouver et exploiter facilement des bugs, rendant les tests seuls insuffisants pour protéger les logiciels.anthropic.com

Des tests de fuzz aux preuves formelles

L'équipe a commencé avec des tests de fuzz issus du programme OSS-Fuzz de Google et a transformé chacun d'eux en une spécification formelle. La règle était que le test ne devait jamais planter sur aucune entrée inférieure à 64 Mo une fois compilé en code machine RISC-V. En quelques semaines, Claude a prouvé cela pour 239 points d'entrée à travers 123 bibliothèques. Les preuves totalisent environ 180 millions de lignes de code dans le langage de preuve Rocq, et une preuve typique atteint environ 600 000 lignes, selon Anthropic. Le vérificateur de preuves Rocq confirme que chaque preuve correspond à sa spécification, évitant ainsi aux développeurs de devoir examiner le code généré ligne par ligne, a rapporté Interesting Engineering.interestingengineering.com+1

Anthropic a précisé qu'un sous-ensemble des preuves est publié, accompagné de la sémantique RISC-V et Linux sous-jacente. Theorem propose d'exécuter gratuitement le même pipeline pour les projets open source éligibles via son programme OSS Verify, a rapporté Unite.AI. Theorem a également publié une compétence Claude pour aider les mainteneurs à s'inscrire.unite.ai+1

Bugs manqués par les fuzzers

La rédaction des preuves a mis en évidence des centaines de bugs, que Claude a corrigés avant de prouver la validité du code réparé. Dans un décompresseur, il a trouvé un sous-dépassement de compteur menant à une écriture hors limites, mais uniquement sur des entrées d'environ 20 Mo avec une disposition rare. Une autre lecture hors limites, dans un décodeur d'image, nécessitait une entrée de 64 Mo et plus de 2 Go de mémoire. Claude a également redécouvert une vulnérabilité connue dans libexpat et a trouvé une faille logique où une fonctionnalité destinée à restreindre les fichiers qu'une application peut charger n'était pas toujours appliquée, selon la recherche.anthropic.com

Limites de la garantie

Anthropic a averti que ces preuves ne signifient pas que les bibliothèques sont exemptes de bugs. Elles supposent un binaire statique monothread avec un budget mémoire fixe s'exécutant sur un processeur RISC-V sous Linux. Tout bug restant se situe soit en dehors du champ d'application des preuves, soit dans les composants de confiance, c'est-à-dire les modèles de matériel et de système d'exploitation, les énoncés de théorèmes et le vérificateur Rocq lui-même, a écrit l'entreprise. La plupart des systèmes déployés utilisent d'autres architectures ou configurations de processeurs, a noté Interesting Engineering.interestingengineering.com+1

Anthropic estime toujours que les aspects économiques sont en train de changer. "Nous encourageons tous les développeurs à explorer la vérification formelle avec les LLM, en particulier ceux qui ont essayé par le passé avec des modèles moins performants et ont constaté que cela ne fonctionnait pas", a écrit l'équipe.anthropic.com