Claude et la vérification de sécurité

OOndine

Dans une recherche publiée jeudi, Anthropic indique que Claude a produit, en collaboration avec Theorem, des preuves formelles vérifiées par machine pour 239 points d’entrée de tests de fuzzing dans 123 bibliothèques open source, au niveau du code assembleur RISC-V, selon Unite.AI. Anthropic indique que Claude a corrigé les bogues détectés, puis prouvé que les programmes terminent normalement, sans erreur de sûreté mémoire ni assertion échouée, pour toute entrée de moins de 64 mégaoctets et dans les conditions Linux modélisées. Le travail a généré environ 180 millions de lignes de preuves dans le langage Rocq, en quelques semaines et sans ingénierie manuelle des preuves. Les chercheurs ont néanmoins fourni les modèles, les outils, les bancs de test et la conception de la vérification, précise AlphaSignal. Selon les chercheurs, le processus aurait aussi révélé puis permis de corriger des défauts qui seraient passés inaperçus malgré des campagnes répétées de fuzzing, dont un bogue logique ancien et la vulnérabilité CVE-2026-56132. Anthropic et Theorem ont publié en accès libre les preuves, les sémantiques et un outil Claude associé au projet. Ces résultats apportent des garanties précises, mais elles se limitent aux entrées de moins de 64 mégaoctets et aux conditions Linux modélisées. Les preuves concernent des points d’entrée et des conditions définis, et ne constituent pas une garantie générale de sécurité pour les bibliothèques concernées.