Sécurité de l’IA
Anthropic et Theorem présentent des preuves écrites par IA pour des cibles de fuzzing ouvertes
Claude a produit des preuves vérifiées par machine pour 239 points d’entrée dans 123 bibliothèques, avec des limites explicites de binaires, entrées, mémoire et comportement.
Anthropic a publié le 22 octobre une recherche menée avec Theorem, indiquant que Claude avait produit des preuves formelles de sécurité pour 239 points d’entrée de tests de fuzzing dans 123 bibliothèques à code source ouvert. Les travaux transforment des tests existants en énoncés mathématiques sur des programmes compilés, puis font valider les arguments générés par un vérificateur indépendant. Le modèle a également trouvé et corrigé des bogues qui empêchaient ces énoncés d’être vrais.
Les garanties s’appliquent dans un environnement d’exécution défini : des binaires RISC-V statiques et monofils, liés à musl, fonctionnant dans un modèle de processus Linux avec des budgets mémoire fixes. L’annexe technique précise des entrées inférieures à 64 MiB, et la documentation du pilote de Theorem indique que les fichiers de cette taille ou plus sont refusés. Les prémisses du théorème déterminent également les réponses du système d’exploitation, les dispositions mémoire et les conditions de ressources couvertes.
Le processus utilise le harnais de fuzzing existant de la bibliothèque, dont les assertions peuvent représenter des propriétés comme la réussite d’une compression puis d’une décompression. Il compare les binaires ordinaires à des versions contenant des contrôles d’instrumentation de détection d’erreurs et raisonne sur leur comportement observable. L’annexe inclut parmi les plantages les fautes, les arrêts de type abort et les comportements absents du modèle de processus. Claude construit les arguments dans Rocq, dont le noyau vérifie s’ils établissent les énoncés demandés.
La frontière de confiance reste concentrée dans les modèles formels de machine et de processus, les énoncés exacts des théorèmes et le vérificateur lui-même, y compris les outils auxiliaires et l’environnement nécessaires pour vérifier chaque binaire. La couverture suit le code accessible depuis le point d’entrée choisi et les contrôles présents dans le binaire. Les propriétés extérieures à ces contrôles et les différences entre le modèle et le matériel ou les systèmes d’exploitation déployés restent pertinentes pour appliquer un résultat à un logiciel en production.
La correction du code a introduit un autre défi : un agent pouvait faciliter une preuve d’absence de plantage en supprimant un comportement utile du programme. Anthropic indique que l’expérience pénalisait chaque correctif et accordait des points supplémentaires pour démontrer quelles entrées une modification affectait et à quel point cet ensemble était restreint. Les chercheurs ont aussi enregistré et audité les correctifs pour repérer ces raccourcis. Après une modification, la spécification était régénérée et le modèle tentait de prouver l’énoncé sur le programme révisé.
Le matériel public ne représente qu’une partie des résultats. Au moment de l’examen, le dépôt de preuves de Theorem répertoriait 60 points d’entrée dans 25 bibliothèques, vérifiés avec Rocq 9.2.0. Il fixe les binaires compilés et consigne les énoncés et hypothèses associés. La version publiée contient des preuves de concordance, qui comparent les comportements et excluent les erreurs spécifiées ; elles peuvent toutefois autoriser une exécution qui ne se termine jamais. La terminaison demande un théorème distinct.
La discussion d’experts dans l’annexe d’Anthropic décrit des preuves bien plus prolixes que celles qu’écrirait habituellement un spécialiste humain. Les agents détaillaient à répétition registres, adresses mémoire et branches d’exécution, tout en développant certaines abstractions connues. L’analyse considère l’amélioration de la structure modulaire comme une question ouverte pour étendre cette approche à des programmes plus complexes. Elle distingue la validité mathématique d’une preuve de l’efficacité et de l’organisation de sa production.
Theorem propose également son processus OSS Verify gratuitement aux projets ouverts remplissant les conditions. L’éligibilité est examinée individuellement selon la maintenance, l’usage, la licence et la place du projet sur des frontières de sécurité ou sous d’autres logiciels. Le programme privilégie les infrastructures largement utilisées et signale les bogues découverts en privé aux responsables de maintenance. Sa documentation indique que les preuves peuvent prendre plusieurs jours et être actualisées après leur achèvement, chaque résultat restant lié à des versions compilées précises du programme.