Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code

Cette étude de vérification formelle révèle que 55,8 % des artefacts de code générés par sept grands modèles de langage dans des contextes critiques pour la sécurité contiennent des vulnérabilités mathématiquement prouvées, démontrant ainsi que les assistants de codage actuels produisent du code intrinsèquement fragile malgré les instructions de sécurité et les outils d'analyse traditionnels.

L'essentiel

🍳 Le Résumé : "Cassé par Défaut"

Imaginez que vous engagez un cuisinier robot ultra-intelligent (une Intelligence Artificielle) pour préparer vos repas (votre code informatique). Vous lui donnez des instructions simples : "Fais-moi une sauce tomate" ou "Prépare un plat de pâtes".

Le problème, c'est que ce robot, aussi brillant soit-il, a une habitude terrible : il met du poison dans 56 % de ses plats, même quand il ne le fait pas exprès. Et le pire ? Il ne le sait pas toujours, et même les garde-manger (les outils de sécurité actuels) ne voient pas le poison.

C'est exactement ce que découvre l'étude "Broken by Default" (Cassé par défaut) de Cobalt AI. Ils ont demandé à 7 des meilleurs robots-cuisiniers du monde de préparer 500 types de plats différents (des tâches de programmation sensibles à la sécurité).

🔍 Comment ont-ils fait le test ?

Au lieu de simplement goûter le plat et dire "ça a l'air suspect", ils ont utilisé un laboratoire de chimie mathématique (appelé Z3).

• L'ancienne méthode : Regarder la recette et dire "Oh, il a utilisé du sel, c'est dangereux". C'est ce que font les outils actuels.
• La méthode de l'étude : Ils ont pris chaque plat et ont demandé au laboratoire : "Est-il mathématiquement possible que quelqu'un mange ce plat et tombe malade ?". Si la réponse était "OUI" (avec une preuve mathématique concrète), alors le plat était considéré comme mortel.

📉 Les Résultats Choc

1. La moyenne est catastrophique : Sur l'ensemble des robots testés, 55,8 % des plats contenaient un poison mortel (une faille de sécurité prouvée).

   • Le "meilleur" robot (Gemini 2.5 Flash) a quand même échoué dans 48 % des cas.
   • Le "pire" (GPT-4o) a échoué dans 62 % des cas.
   • Aucun robot n'a obtenu la note de passage. Tous sont en échec.

2. Le poison le plus courant : La plupart des erreurs viennent de la façon dont les robots gèrent les quantités (les mathématiques).

   • Analogie : Imaginez que le robot doit acheter des pommes pour 100 personnes. Il demande un sac de la taille de 100 x 100. Mais si le nombre de personnes est très grand, le calcul explose et le robot demande un sac plus gros que l'univers entier, ou pire, il se trompe de taille et verse le contenu sur le sol. C'est ce qu'on appelle une débordement de mémoire (integer overflow).

3. Les garde-manger sont aveugles : Les chercheurs ont pris les plats empoisonnés et les ont montrés à 6 experts humains et robots de sécurité (les outils comme Semgrep, CodeQL, etc.).

   • Résultat ? Ces experts n'ont vu que 7,6 % des poisons.
   • Ils ont manqué 97,8 % des failles prouvées mathématiquement. C'est comme si vous aviez un détecteur de métaux qui ne trouvait que les clés, mais ignorait les bombes.

🤖 Le Paradoxe du "Chef qui se juge lui-même"

C'est la partie la plus surprenante. Les chercheurs ont pris un plat empoisonné fabriqué par un robot, et ils l'ont redonné au même robot en lui disant : "Regarde ce plat. Est-il empoisonné ?".

• Résultat : Le robot a dit "Oui, c'est empoisonné" dans 78 % des cas.
• Le problème : Quand on lui demandait de cuisiner le plat au départ, il l'avait empoisonné dans 56 % des cas.

La leçon : Le robot sait que c'est dangereux. Il a le savoir. Mais quand il est en mode "création", il oublie ses propres règles. C'est comme un chauffeur de course qui connaît parfaitement le code de la route, mais qui roule à 200 km/h parce qu'il est trop concentré sur la vitesse.

🛡️ Est-ce que dire "Sois prudent !" aide ?

Les chercheurs ont essayé de donner des instructions spéciales aux robots : "S'il te plaît, fais attention, ne mets pas de poison, sois sécurisé".

• Résultat : Ça a aidé un tout petit peu (de 64 % à 60 % d'erreurs), mais pas assez. C'est comme dire à un enfant de ne pas toucher au feu en lui mettant un bonnet de sécurité : ça ne change pas le fait qu'il veut jouer avec le feu. Les mauvaises habitudes sont trop ancrées dans leur cerveau.
• Note importante sur ce test : Cette amélioration de 4 points a été mesurée sur un échantillon réduit de 50 prompts (une version préliminaire de l'étude), et non sur l'ensemble complet des 500 prompts. Cela montre que même sur un petit échantillon, l'effet des instructions de sécurité reste très limité.

💡 Que faut-il retenir pour nous, humains ?

1. Ne faites jamais confiance aveuglément : Si un robot écrit du code pour votre banque, votre hôpital ou votre voiture, ne le mettez jamais en production sans un humain expert qui le relit.
2. Les outils actuels ne suffisent pas : Les logiciels de sécurité que vous utilisez aujourd'hui sont aveugles face aux erreurs mathématiques subtiles que les robots font.
3. Le futur : Pour être vraiment sûr, il faudra utiliser des méthodes de vérification mathématique (comme celle utilisée dans l'étude) ou faire appel à des humains très qualifiés.

En résumé : Nos assistants IA sont incroyablement talentueux, mais ils sont cassés par défaut pour la sécurité. Ils sont comme des génies qui oublient de verrouiller la porte de la maison. C'est à nous de vérifier la serrure, car eux ne le font pas.

Résumé technique

1. Problématique

L'adoption massive des assistants de codage IA (Copilot, ChatGPT, etc.) dans des domaines sensibles à la sécurité (backends web, systèmes embarqués, bibliothèques cryptographiques) soulève une inquiétude majeure : la vulnérabilité de leur code généré reste non quantifiée et souvent sous-estimée.

Les travaux antérieurs se sont principalement appuyés sur le mappage de motifs (pattern matching) ou l'inspection manuelle, des techniques qui ne peuvent pas prouver de manière définitive l'exploitabilité d'une faille. L'article pose la question de savoir si les modèles de langage (LLM) produisent du code intrinsèquement vulnérable par défaut, et si les outils d'analyse statique actuels sont capables de détecter ces failles.

2. Méthodologie

L'étude, menée par Cobalt AI, adopte une approche rigoureuse de vérification formelle pour établir la « vérité terrain » (ground truth) de l'exploitabilité.

• Corpus de données : 3 500 artefacts de code générés par 7 modèles LLM de pointe (GPT-4o, GPT-4.1, Claude Haiku 4.5, Gemini 2.5 Flash, Mistral Large, Llama 3.3 70B, Llama 4 Scout) à partir de 500 prompts réalistes (non adversariaux).
• Catégories de vulnérabilités (CWE) : Les prompts couvrent 5 catégories critiques :
  • Gestion de la mémoire (CWE-131/190)
  • Arithmétique entière (CWE-190/195)
  • Authentification (CWE-916)
  • Cryptographie (CWE-327/330)
  • Gestion des entrées (CWE-89/22/78)
• Pipeline d'analyse COBALT :
  1. Extraction de motifs de vulnérabilités via AST et Regex.
  2. Encodage SMT (Satisfiability Modulo Theories) : Les conditions de vulnérabilité sont traduites en formules mathématiques pour le solveur Z3.
  3. Preuve formelle : Si Z3 retourne « SAT », une valeur concrète (témoin) est extraite, prouvant mathématiquement que l'entrée déclenche la faille.
• Validation Runtime : Sélection de 7 artefacts pour créer des preuves de concept (PoC) compilées avec GCC AddressSanitizer (ASAN) afin de confirmer les plantages en temps réel (débordements de tas, injections SQL, etc.).
• Expériences auxiliaires :
  • Ablation : Ajout d'instructions de sécurité explicites dans les prompts. Note importante : Cette expérience a été conduite sur un sous-corpus de 50 prompts (v1), et non sur l'ensemble des 500 prompts du benchmark principal.
  • Comparaison d'outils : Test de 6 outils industriels (Semgrep, Bandit, Cppcheck, Clang SA, FlawFinder, CodeQL).
  • Asymétrie Génération/Révision : Demander aux modèles d'analyser leur propre code généré.

3. Contributions Clés

1. Vérification Formelle à l'échelle : Première étude appliquant la vérification formelle (Z3 SMT) pour prouver l'exploitabilité de milliers d'artefacts IA, dépassant les simples heuristiques de motifs.
2. Preuve d'exploitabilité réelle : Démonstration que les failles détectées ne sont pas théoriques mais provoquent des plantages réels (ASAN) et des exfiltrations de données.
3. Révélation du « Gap » de détection : Preuve que les outils d'analyse statique standards (y compris CodeQL) manquent structurellement les vulnérabilités les plus critiques générées par l'IA (débordements d'entiers dans les calculs de taille de mémoire).
4. Identification de l'asymétrie : Mise en évidence du fait que les modèles possèdent la connaissance pour détecter leurs propres failles en mode révision, mais échouent à les éviter en mode génération.

4. Résultats Principaux

Taux de Vulnérabilité Global

• Taux moyen : 55,8 % des artefacts contiennent au moins une vulnérabilité identifiée par COBALT.
• Preuves formelles : 1 055 vulnérabilités ont été formellement prouvées exploitables via des témoins Z3.
• Performance par modèle :
  • Le pire : GPT-4o (62,4 % de vulnérabilités, note F).
  • Le meilleur : Gemini 2.5 Flash (48,4 %, note D).
  • Aucun modèle n'atteint une note supérieure à D.
• Catégories les plus critiques : L'arithmétique entière (87 % de taux de vulnérabilité) et l'allocation mémoire (67 %). Le motif malloc(n * sizeof(T)) sans vérification de débordement est omniprésent.

Validation Runtime

• Sur 7 cas testés, 6 ont provoqué des plantages confirmés (ASAN) ou des exfiltrations de données (injection SQL, crack de mot de passe SHA-256 en 0,01 ms).

Impact des Instructions de Sécurité (Ablation)

• L'ajout d'instructions explicites (« écrivez du code sécurisé », « vérifiez les débordements ») ne réduit le taux de vulnérabilité moyen que de 4 points (de 64,8 % à 60,8 %).
• Contexte de réplicabilité : Cette réduction a été observée sur le sous-corpus de 50 prompts (v1).
• Quatre modèles sur cinq restent à la note F. Cela suggère que les failles sont ancrées dans la distribution de probabilité du modèle (données d'entraînement) et non simplement dues à un manque d'instructions.

Comparaison avec les Outils Industriels

• Les 6 outils combinés (Semgrep, Bandit, Cppcheck, Clang SA, FlawFinder, CodeQL) n'ont détecté que 7,6 % des artefacts vulnérables.
• 97,8 % des vulnérabilités prouvées par Z3 (notamment les débordements d'entiers dans les calculs de taille) sont invisibles pour ces outils.
• CodeQL a manqué 100 % des 90 artefacts prouvés par Z3. La raison est structurelle : ces outils ne peuvent pas raisonner sur l'arithmétique modulaire 32/64 bits sans contraintes de valeurs concrètes, contrairement à Z3.

Asymétrie Génération-Révision

• Lorsqu'on demande aux modèles d'analyser leur propre code généré (mode révision), ils identifient 78,7 % des vulnérabilités (70/89).
• Pourtant, ils génèrent ces mêmes vulnérabilités 55,8 % du temps par défaut. Cela prouve que le problème n'est pas un manque de connaissance, mais une incapacité à appliquer cette connaissance de manière spontanée lors de la génération.

5. Signification et Implications

L'article conclut que les assistants de codage IA sont « cassés par défaut » (Broken by Default) pour les tâches sensibles à la sécurité.

• Limitation des outils actuels : Les analyseurs statiques traditionnels sont insuffisants pour sécuriser le code généré par l'IA, car ils ne peuvent pas détecter les failles logiques complexes (débordements d'entiers) qui nécessitent un raisonnement formel.
• Insuffisance du « Prompting » : Les instructions de sécurité dans les prompts ne constituent pas une atténuation fiable, même sur des sous-ensembles de prompts.
• Recommandations pour les développeurs :
  1. Traiter tout code IA (C/C++) comme du code non audité nécessitant une revue de sécurité explicite.
  2. Utiliser des compilateurs avec instrumentation (-fsanitize=address,undefined) pour tous les systèmes générés par IA.
  3. Ne pas se fier aux outils statiques standards pour les erreurs d'arithmétique d'allocation.
  4. Intégrer la vérification formelle (comme Z3) dans les pipelines de revue de code pour les cibles critiques.

En résumé, cette étude démontre que la vérification formelle n'est pas seulement un outil de recherche, mais une nécessité opérationnelle pour établir la sécurité du code généré par l'IA, car les méthodes heuristiques actuelles laissent passer la quasi-totalité des failles critiques.