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

Dit onderzoek toont aan dat AI-generatiecode in beveiligingskritieke domeinen door 55,8% van de gevallen kwetsbaar is, waarbij zes van de zeven onderzochte modellen een onvoldoende cijfer behalen en bestaande industriële tools 97,8% van de wiskundig bewezen kwetsbaarheden missen.

De kern

"Gebroken bij Standaard": Wat deze studie ons vertelt over AI en veilige code

Stel je voor dat je een supersterke, ongelofelijk snelle kok hebt die elk recept dat je bedenkt, in een seconde kan maken. Je vraagt hem: "Maak een taart die veilig is voor mensen met een suikerallergie." Hij maakt direct een prachtige taart. Maar als je erin bijt, blijkt er toch suiker in te zitten. En niet alleen dat: de kok heeft dit elke keer gedaan, zelfs als je hem herhaaldelijk hebt gevraagd: "Zorg dat er geen suiker in zit!"

Dat is precies wat deze studie, getiteld "Broken by Default" (Gebroken bij Standaard), ontdekt heeft over de AI's die vandaag de dag programmeren voor ons.

Hier is de uitleg in gewone taal, met een paar handige vergelijkingen:

1. Het Experiment: De "Kookwedstrijd"

De onderzoekers (van Cobalt AI) hebben 7 van 's werelds slimste AI-programma's (zoals GPT-4o, Gemini en Claude) een uitdaging gegeven. Ze kregen 500 specifieke vragen over het schrijven van code voor veilige systemen (zoals wachtwoorden, banktransacties en geheugenbeheer).

• De vraag: "Schrijf een programma dat X doet."
• De taak: De AI moest de code schrijven alsof het voor een echte, veilige applicatie was.
• Het resultaat: Ze kregen in totaal 3.500 stukken code.

2. De Grote Ontdekking: De "Gaten" in de Muur

Normaal gesproken kijken mensen of software veilig is door te zoeken naar bekende fouten (zoals "oh, hier staat een slechte wachtwoordfunctie"). Maar deze onderzoekers gebruikten een heel andere methode: een wiskundige "super-rekenmachine" (Z3) die de code als een wiskundig probleem bekijkt.

Ze vroegen de rekenmachine: "Is er een manier om deze code te hacken?"

• Het schokkende antwoord: Ja. In 55,8% van de gevallen kon de code worden gehackt.
• De "Kwaliteitsscore": Als je dit als schoolcijfers zou zien, scoort de beste AI een D (Gemini 2.5 Flash) en de slechtste een F (GPT-4o). Geen enkele AI haalde een C of beter.
• De bewijzen: Het is geen gok. De rekenmachine gaf zelfs het exacte getal dat je moest invoeren om de code te laten crashen. En toen ze dat getal echt invoerden, crashte de software inderdaad, net als een auto die uit elkaar valt als je te hard over een drempel rijdt.

3. Waarom is dit zo erg? (De "Onzichtbare" Gaten)

Je zou denken: "Wacht, er zijn toch al tools die fouten vinden?"
De onderzoekers testten 6 beroemde, dure software-tools die bedrijven gebruiken om fouten te vinden.

• Het resultaat: Deze tools vonden slechts 7,6% van de fouten.
• De vergelijking: Stel je voor dat je een huis bouwt met een AI. De AI bouwt een muur met een gat van 1 meter breed. De bestaande tools kijken naar de muur en zeggen: "Ziet er prima uit!" terwijl de "super-rekenmachine" schreeuwt: "Er is een gat!"
• De oorzaak: De fouten die de AI maakt, zijn vaak heel subtiel (zoals een rekenfout bij het berekenen van hoeveel geheugen er nodig is). De oude tools zoeken naar bekende patronen, maar deze AI-fouten zijn wiskundig bewezen onmogelijk te vinden zonder de "super-rekenmachine".

4. De "Gezonde Verstand"-Paradox

Een van de meest verbluffende ontdekkingen is dit:
De onderzoekers gaven de AI's hun eigen foutieve code terug en vroegen: "Kijk eens naar deze code. Zie je een fout?"

• Het antwoord: De AI's zagen de fouten 79% van de tijd! Ze konden het probleem perfect analyseren.
• Het probleem: Maar toen ze de code moesten schrijven, maakten ze dezelfde fouten weer.
• De analogie: Het is alsof een kok die perfect kan vertellen waarom een taart niet goed is ("Je hebt te veel suiker gebruikt!"), maar die bij het bakken zelf weer te veel suiker toevoegt. Ze weten het, maar ze doen het niet.

5. Helpt "Wees voorzichtig" dan?

De onderzoekers probeerden het AI's te vertellen: "Schrijf veilige code, pas op voor gaten!"

• Het resultaat: Het hielp nauwelijks. De fouten bleven bijna even vaak voorkomen.
• De nuance: In een specifiek, kleiner experiment met slechts 50 prompts (een subgroep van de totale 500), zagen ze dat het geven van een veiligheidsinstructie de fouten met ongeveer 4 punten verminderde. Dit klinkt misschien als een verbetering, maar het betekent ook dat zelfs met die extra instructie de AI nog steeds in de meerderheid van de gevallen onveilige code produceerde.
• De les: Het probleem zit niet in de instructie, maar in hoe de AI is opgeleid. De AI heeft geleerd van bestaande code op internet, en daar zitten helaas al veel fouten in. De AI heeft deze fouten "geleerd" als normaal gedrag.

Wat betekent dit voor jou?

Als je AI gebruikt om software te schrijven (vooral voor veiligheid, bankzaken of kritieke systemen):

1. Vertrouw niet blind: AI-code is standaard "gebroken" op het gebied van veiligheid.
2. Geen snelle fix: Zeggen "maak het veilig" in je prompt lost het probleem niet op.
3. Geen oude tools: De huidige software die fouten opzoekt, mist de meeste gevaren die door AI worden gemaakt.
4. Menselijke controle is nodig: Je hebt echt een menselijke expert (of geavanceerde wiskundige controle) nodig om te checken of de code echt veilig is.

Kortom: AI is een geweldige assistent, maar op het gebied van veiligheid is het momenteel als een beginnende timmerman die mooie meubels maakt, maar vergeet te controleren of de schroeven stevig genoeg zijn. Totdat we betere manieren vinden om dit te controleren, moeten we elke AI-gegenereerde code behandelen alsof hij een verborgen valkuil heeft.

Technische samenvatting

Titel

Broken by Default: Een formeel verificatiestudie van beveiligingskwetsbaarheden in door AI gegenereerde code

1. Het Probleem

AI-coding-assistenten worden steeds vaker gebruikt om productiekode te genereren in beveiligingsgevoelige domeinen (zoals webbackends, ingebouwde systemen en cryptografische bibliotheken). Echter, de mate waarin de output van deze modellen kwetsbaar is, blijft ongekwantificeerd. Bestaande onderzoeken vertrouwen vaak op statische patroonherkenning of handmatige inspectie, technieken die niet definitief kunnen vaststellen of een kwetsbaarheid daadwerkelijk uitbuitbaar is (exploitability). Er bestaat een kloof tussen het genereren van code en het kunnen bewijzen dat deze code veilig is.

2. Methodologie

De auteurs (Dominik Blain en Maxime Noiseux van Cobalt AI) hebben een rigoureuze studie uitgevoerd met de volgende methodologische pijlers:

• Dataset: Er zijn 3.500 code-artefacten gegenereerd door 7 toonaangevende Large Language Models (LLMs) (waaronder GPT-4o, Gemini 2.5 Flash, Claude Haiku 4.5, Llama 3.3/4, en Mistral Large) op basis van 500 beveiligingskritische prompts. Deze prompts zijn verdeeld over 5 CWE-categorieën:
  • Geheugenbeheer (MEM)
  • Integer-aritmetiek (INT)
  • Authenticatie (AUTH)
  • Cryptografie (CRYPTO)
  • Invoerbehandeling (INP)
• Formele Verificatie (Z3 SMT): In plaats van alleen patroonmatching, gebruiken de auteurs de Z3 SMT-solver (Satisfiability Modulo Theories) via hun eigen COBALT-analyspijplijn.
  • Kwetsbaarheidscondities worden omgezet in wiskundige formules.
  • Als Z3 een "SAT" (satisfiable) resultaat retourneert, betekent dit dat er een concreet bewijs (witness) bestaat dat de kwetsbaarheid uitbuitbaar is. Dit levert een "ground-truth" op.
• Runtime Validatie: Geselecteerde bevindingen werden geverifieerd met GCC AddressSanitizer (ASAN). De uit Z3 gehaalde bewijswaarden werden als concrete input gebruikt om runtime-crashes (zoals heap-buffer overflows) te triggeren.
• Ablatie- en Vergelijkingsstudies:
  • Veilige Prompts: Het toevoegen van expliciete beveiligingsinstructies aan de prompt. Let op: Deze ablatiestudie werd uitgevoerd op een sub-corpus van 50 prompts (v1), niet op het volledige benchmark van 500 prompts.
  • Tool Vergelijking: Een vergelijking met zes industriestandaard tools (Semgrep, Bandit, Cppcheck, Clang Static Analyzer, FlawFinder, CodeQL).
  • Generatie-Review Asymmetrie: Het testen of modellen hun eigen kwetsbare code kunnen herkennen wanneer ze gevraagd worden om deze te reviewen.

3. Belangrijkste Resultaten

Algemene Kwetsbaarheidspercentages

• Het gemiddelde percentage kwetsbare artefacten over alle modellen bedraagt 55,8%.
• GPT-4o scoort het slechtst met 62,4% kwetsbaarheden (Gradering: F).
• Gemini 2.5 Flash scoort het best met 48,4% (Gradering: D).
• Geen enkel model behaalt een graad beter dan D.
• Van de 3.500 artefacten zijn 1.055 kwetsbaarheden formeel bewezen uitbuitbaar via Z3 SAT-witnesses.

Categorie-gebonden Resultaten

• Integer-aritmetiek (CWE-190/195) vertoont het hoogste falingspercentage (87%), voornamelijk door het ontbreken van overflow-bescherming bij geheugenallocatie (malloc(n * sizeof(T))).
• Geheugenallocatie volgt met 67%.
• Cryptografie en authenticatie tonen lagere, maar nog steeds aanzienlijke percentages.

Validatie en Tooling

• Runtime Bevestiging: Van 7 geselecteerde voorbeelden veroorzaakten 6 daadwerkelijke runtime-crashes (gebeurden bij ASAN), wat bewijst dat de Z3-witnesses reële uitbuitingen zijn.
• Tooling Gap: Industriestandaard tools (Semgrep, CodeQL, etc.) detecteren slechts 7,6% van de artefacten. Ze missen 97,8% van de formeel bewezen Z3-kwetsbaarheden.
  • Reden: Bestaande tools gebruiken patroonmatching of dataflow-analyse, maar kunnen geen wiskundige redenering uitvoeren over bit-vector aritmetiek om te bewijzen dat een variabele n een overflow kan veroorzaken.

Generatie-Review Asymmetrie

• Wanneer modellen hun eigen kwetsbare code terugkregen om te reviewen, identificeerden ze 78,7% van de fouten correct.
• Dit onthult een fundamenteel probleem: modellen hebben de kennis om kwetsbaarheden te herkennen, maar passen deze kennis niet spontaan toe tijdens het generatieproces.

Invloed van Prompts

• Het toevoegen van expliciete beveiligingsinstructies ("schrijf veilige code") verlaagde het gemiddelde kwetsbaarheidspercentage slechts met 4 punten (van 64,8% naar 60,8%).
• Belangrijke nuance: Deze meting is gebaseerd op een ablatiestudie uitgevoerd op een sub-corpus van 50 prompts (v1), niet op het volledige benchmark van 500 prompts.
• Dit suggereert dat de kwetsbaarheden diep verankerd zijn in de trainingsdata en generatieprioriteiten van de modellen, en niet opgelost kunnen worden met simpele prompt-engineering.

4. Kernbijdragen

1. Methodologische Innovatie: Toepassing van formele verificatie (Z3 SMT) op AI-code om wiskundig bewijs van uitbuitbaarheid te leveren, in plaats van te vertrouwen op heuristieken.
2. Uitgebreide Benchmark: Een dataset van 3.500 artefacten over 7 frontier-modellen, wat de grootste en meest rigoureuze studie tot nu toe is.
3. Runtime Validatie: Het koppelen van formele bewijzen aan daadwerkelijke crashes via AddressSanitizer.
4. Tooling Kruisverificatie: Het aantonen dat bestaande industriestandaard tools structureel blind zijn voor de meest voorkomende AI-gegenereerde kwetsbaarheden (integer overflows in allocatie).

5. Betekenis en Conclusie

De studie concludeert dat AI-coding-assistenten "broken by default" zijn voor beveiligingskritische taken.

• Veiligheid is niet gegarandeerd: Zelfs de beste modellen genereren in bijna de helft van de gevallen kwetsbare code.
• Prompt-engineering is onvoldoende: Het toevoegen van beveiligingsinstructies is geen effectieve mitigatie.
• Bestaande tools falen: Developers kunnen niet vertrouwen op Semgrep, CodeQL of Clang SA om deze specifieke kwetsbaarheden op te vangen.
• Aanbeveling: Voor beveiligingskritische code (vooral C/C++) moet formele verificatie of menselijke audit verplicht worden gesteld. AI-code moet worden behandeld als onbeoordeelde code die expliciet op geheugenveiligheid moet worden gecontroleerd.

De auteurs pleiten ervoor dat formele verificatie via SMT-solvers een standaardcomponent wordt in elke AI-code-reviewpijplijn voor systemen die gevoelig zijn voor geheugenproblemen.