Des failles découvertes dans six bibliothèques déjà vérifiées par l'IA d'Anthropic

GenProof a découvert des bugs dans six bibliothèques examinées par Anthropic et lance QuickProof pour rendre la vérification formelle plus accessible.

Une preuve mathématique peut être parfaitement correcte et laisser passer un bug. C'est le paradoxe mis en évidence par GenProof, un nouveau laboratoire de recherche spécialisé dans la vérification formelle des logiciels. Ses chercheurs affirment avoir découvert des erreurs dans six bibliothèques open source dont certaines propriétés avaient déjà été démontrées par Claude, dans le cadre d'un programme mené par Anthropic et Theorem. Les preuves précédentes ne seraient pas fausses : elles auraient simplement vérifié des propriétés insuffisantes pour détecter les erreurs découvertes.

Fondé notamment par Alex Pokras, le laboratoire accompagne son lancement de deux outils, QuickProof et QuickMaths. Le premier cherche à rendre la vérification formelle accessible aux développeurs sans expertise particulière en mathématiques. Le second organise plusieurs agents IA pour résoudre des problèmes de démonstration dans Lean. Selon le registre public des découvertes, les recherches du laboratoire couvrent 111 projets et totalisent 352 bugs identifiés, dont 134 corrigés et 212 ayant fait l'objet de signalements publics. Ces chiffres correspondent à l'état du registre communiqué au lancement et incluent des problèmes de gravité très variable. Une preuve correcte peut vérifier la mauvaise chose

La vérification formelle consiste à démontrer mathématiquement qu'un programme respecte une propriété précise, pour toutes les entrées autorisées par cette propriété. Contrairement aux tests classiques, qui examinent un nombre limité de situations, une démonstration peut couvrir un ensemble complet de comportements définis par sa spécification.

Le problème vient précisément de cette spécification. Démontrer qu'un logiciel ne plante jamais ne garantit pas qu'il renvoie le bon résultat. Une fonction de compression peut produire un fichier incorrect sans provoquer d'erreur d'exécution. Une bibliothèque de calcul peut retourner une valeur erronée tout en respectant les contraintes de sécurité mémoire qui lui ont été imposées.

Le 22 octobre, Anthropic et Theorem avaient publié les résultats d'un programme dans lequel Claude avait démontré des propriétés de sécurité sur 239 points d'entrée appartenant à 123 bibliothèques open source. Les chercheurs avaient travaillé directement sur des exécutables RISC-V, avec environ 180 millions de lignes de preuves vérifiées par Rocq, un assistant de preuve formelle.

La démarche visait principalement à établir que certains programmes ne pouvaient pas planter dans les conditions définies par les tests utilisés comme spécifications. Les auteurs reconnaissaient eux-mêmes que ces garanties ne couvraient ni l'ensemble des fonctionnalités des bibliothèques ni tous leurs environnements d'exécution.

L'équipe de GenProof a repris six bibliothèques figurant dans cette publication : zstd, OpenSSL, libpcap, zlib, Mbed TLS et coturn. Des erreurs ont été identifiées dans chacune d'elles, sans invalider les démonstrations précédentes. L'analyse publiée souligne une différence fondamentale entre prouver qu'un programme s'exécute sans incident et démontrer qu'il accomplit correctement la tâche attendue. Des bugs dans Redis, Linux et des bibliothèques historiques

L'une des découvertes les plus documentées concerne Redis, un logiciel largement employé pour stocker et manipuler des données en mémoire. Un changement introduit dans la version 8.8 a modifié le traitement de certaines tailles d'entrées dans le format interne listpack.

Ce changement pouvait rendre illisibles des données pourtant valides, enregistrées avec Redis 8.6 ou une version antérieure. Dans certaines conditions, une simple lecture après mise à jour provoquait l'arrêt du serveur. Avec des paramètres particuliers, les entrées pouvaient devenir invisibles puis être enregistrées sous forme de doublons. Le problème a fait l'objet du signalement Redis n°16078, suivi d'une correction.

Les tests habituels ne détectaient pas nécessairement cette incompatibilité, puisqu'ils vérifiaient généralement qu'une même version pouvait relire les données qu'elle venait d'écrire. En examinant toutes les représentations autorisées par la spécification du format, les chercheurs ont identifié trois tailles particulières à l'origine du dysfonctionnement.

D'autres investigations ont porté sur le noyau Linux. Le laboratoire affirme avoir découvert un défaut ancien, potentiellement exploitable à distance pour provoquer l'arrêt d'un appareil vulnérable, dans un composant qu'Anthropic et Theorem avaient précédemment étudié. Une demande d'identifiant CVE a été déposée, mais le registre consulté ne fournit pas encore de référence attribuée. La portée exacte de cette vulnérabilité reste donc à considérer comme une affirmation du laboratoire, dans l'attente des éléments techniques et des validations publiques correspondants.

Les travaux concernent également des composants très répandus comme zlib, OpenSSL, nginx et des bibliothèques de traitement de données. Certains signalements ont déjà été corrigés par les responsables des projets, d'autres restent à l'état de confirmation ou d'examen. Le détail des investigations publié par GenProof distingue les erreurs de fonctionnement ordinaires des vulnérabilités susceptibles d'avoir des conséquences sur la sécurité. Écrire un test en C pour obtenir une preuve mathématique

L'une des principales difficultés de la vérification formelle réside dans la rédaction de spécifications compréhensibles par un assistant de preuve. Cette étape demande traditionnellement une maîtrise de langages spécialisés, ce qui limite son adoption dans les équipes de développement classiques.

Avec QuickProof, GenProof propose une interface fondée sur le langage C. Le développeur décrit la propriété attendue dans un petit programme qui ressemble à un test unitaire. Pour une bibliothèque de compression, il peut demander que les données obtenues après compression puis décompression soient identiques aux données initiales.

La différence intervient dans la définition des