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

Lo studio "Broken by Default" dimostra tramite verifica formale che il 55,8% del codice generato da sette modelli linguistici avanzati contiene vulnerabilità di sicurezza matematicamente provate, rivelando che gli strumenti di sicurezza attuali ne individuano solo una frazione minima e che le istruzioni esplicite non riescono a mitigare efficacemente il rischio.

L'essenziale

Immagina di aver appena assunto il programmatore più intelligente e veloce del mondo. È un genio che scrive codice per te in un istante, 24 ore su 24. Ti chiede di scrivere una funzione per gestire i soldi, un sistema di sicurezza o un database. Lui lo fa subito.

Purtroppo, questo studio ci dice una cosa sconvolgente: questo genio è distratto e scrive codice pericoloso più della metà delle volte.

Ecco i punti chiave, spiegati con delle metafore:

1. Il "Genio Distratto" (I Risultati Principali)

Gli autori hanno chiesto a 7 diversi modelli di intelligenza artificiale (tra cui i più famosi come GPT-4o, Claude e Gemini) di scrivere 500 pezzi di codice su temi delicati (come la gestione della memoria o la crittografia).

• Il risultato: In media, 56 volte su 100, il codice prodotto conteneva un buco di sicurezza grave.
• La metafora: È come se tu chiedessi a un architetto di costruire 100 ponti. Di questi, 56 crollerebbero appena ci passi sopra con un'auto. Il modello migliore (Gemini) ne ha "salvati" solo 52 su 100, mentre il peggiore (GPT-4o) ne ha rovinati 62. Nessuno ha raggiunto un livello di sicurezza accettabile.

2. La "Prova Matematica" (Non sono solo sospetti)

Fino ad oggi, molti studi dicevano: "Ehi, questo codice sembra strano, forse è pericoloso".
Questo studio ha fatto di più. Ha usato un super-calcolatore matematico chiamato Z3 (immaginalo come un detective che non si accontenta di "sembra", ma vuole la prova fisica).

• Cosa ha fatto: Il detective Z3 ha preso il codice generato dall'AI e ha detto: "Dimostrami matematicamente che se inserisco questo numero specifico, il sistema si rompe".
• Il verdetto: L'AI ha fallito. Il detective ha trovato 1.055 prove matematiche che il codice si poteva hackerare. Non è un "forse", è un "sicuro".
• La verifica reale: Hanno anche provato a rompere il codice nella vita reale (come un test crash di un'auto) e 6 volte su 7 il codice si è effettivamente rotto, confermando che i buchi erano reali.

3. Il "Furto di Abitudini" (Perché succede?)

Perché un'intelligenza così avanzata sbaglia così tanto?

• La metafora: Immagina che l'AI sia uno studente che ha letto tutti i libri di codice mai scritti su internet. Il problema è che la maggior parte del codice scritto dagli umani in passato (specialmente in C/C++) conteneva errori di sicurezza. L'AI ha imparato a memoria questi errori, pensando che fossero la norma.
• Il risultato: Quando le chiedi di scrivere codice sicuro, lei riproduce le "cattive abitudini" che ha imparato dai suoi libri di testo. È come se un cuoco che ha mangiato solo cibo spazzatura per anni, provasse a cucinare una cena sana: sa come si fa, ma il suo istinto lo porta a mettere troppo sale e zucchero.

4. Il "Falso Amico" (I Prompt di Sicurezza)

Molti pensano: "Basta chiedere gentilmente all'AI di stare attenta!".

• L'esperimento: Hanno provato a dire all'AI: "Per favore, scrivi codice sicuro, controlla gli errori, sii prudente".
• Il risultato: È stato inutile. Il codice è rimasto pericoloso quasi quanto prima.
• La metafora: È come dire a un bambino che corre in strada: "Per favore, corri piano e guarda le macchine". Se il bambino ha l'abitudine di correre, un semplice "per favore" non basta a cambiare il suo comportamento istintivo. Le istruzioni di sicurezza sono state ignorate dal "cervello" dell'AI.
• Un dettaglio importante: Quando gli autori hanno analizzato più da vicino questo fenomeno su un piccolo gruppo di 50 richieste (un sottogruppo del test totale), hanno visto che rimuovere queste istruzioni di sicurezza faceva peggiorare le prestazioni di circa 4 punti. Questo conferma che, anche su piccola scala, l'AI tende a ignorare le richieste di prudenza, ma il dato principale si riferisce all'intero test su larga scala.

5. I "Controllori del Pass" (Gli Strumenti di Sicurezza)

C'è un altro problema: gli strumenti che usiamo oggi per controllare il codice (come antivirus o scanner di sicurezza) non vedono questi errori.

• La metafora: Immagina di avere un ispettore di sicurezza che controlla se le porte sono chiuse. L'AI però non ha lasciato la porta aperta; ha costruito il muro con dei mattoni che si sgretolano se ci metti sopra un peso specifico. L'ispettore guarda la porta e dice: "Tutto ok!", mentre il muro crolla.
• Il dato: Gli strumenti professionali hanno trovato solo il 7% degli errori. Il 98% degli errori provati matematicamente dall'AI erano invisibili a questi strumenti.

6. Il "Paradosso del Critico" (L'AI sa di sbagliare)

Questa è la parte più strana e inquietante.

• L'esperimento: Hanno preso il codice sbagliato generato dall'AI e lo hanno rimandato alla stessa AI, chiedendole: "C'è un errore qui?".
• Il risultato: L'AI ha detto: "Sì, c'è un errore!" nel 79% dei casi.
• Il paradosso: L'AI sa come scrivere codice sicuro e sa riconoscere gli errori quando li vede, ma quando deve scrivere il codice da zero, non lo fa. È come un professore di guida che sa esattamente come si guida in sicurezza, ma quando sale alla guida lui stesso, sbaglia frenate e sterzate.

In sintesi: Cosa dobbiamo fare?

Lo studio conclude con un messaggio forte: Non fidarsi ciecamente dell'AI per il codice critico.

1. L'AI scrive codice "rotto" di default.
2. Chiederle di stare attenta non basta.
3. Gli strumenti attuali non la controllano abbastanza bene.
4. Serve una verifica umana o matematica molto rigorosa prima di usare quel codice.

È come se avessimo trovato un nuovo tipo di cemento che sembra solido ma crolla sotto un peso specifico. Finché non impariamo a testarlo con metodi matematici (come fa questo studio), non dovremmo usarlo per costruire grattacieli.

Sommario tecnico

Titolo: Broken by Default: Uno studio di verifica formale sulle vulnerabilità di sicurezza nel codice generato dall'IA

1. Il Problema

L'adozione rapida degli assistenti di codifica basati sull'IA (come GitHub Copilot, ChatGPT, Claude e Gemini) ha trasformato i flussi di lavoro di sviluppo software, con un utilizzo crescente in domini sensibili alla sicurezza (backend web, sistemi embedded, librerie crittografiche). Tuttavia, l'exploitabilità del codice generato da questi modelli rimane un "buco nero" non quantificato.
La ricerca precedente si è basata prevalentemente su:

• Matching di pattern statici: Tecniche che identificano vulnerabilità basandosi su firme note, ma che non possono dimostrare l'effettiva sfruttabilità.
• Ispezione manuale: Soggetta a errori umani e non scalabile.
• Mancanza di prove matematiche: Nessuno studio precedente ha fornito una prova formale che un output specifico dell'IA contenga una vulnerabilità sfruttabile con un input concreto.

2. Metodologia

Gli autori hanno condotto uno studio empirico su larga scala utilizzando una pipeline di analisi chiamata COBALT, integrata con un risolutore SMT (Satisfiability Modulo Theories) chiamato Z3.

• Dataset: 3.500 artefatti di codice generati da 7 modelli LLM all'avanguardia (GPT-4o, GPT-4.1, Claude Haiku 4.5, Gemini 2.5 Flash, Mistral Large, Llama 3.3 70B, Llama 4 Scout) su 500 prompt di sicurezza (100 per ciascuna delle 5 categorie CWE: Gestione della Memoria, Aritmetica Interi, Autenticazione, Crittografia, Gestione Input).
• Pipeline COBALT:
  1. Estrazione Pattern: Identificazione di siti vulnerabili candidati tramite AST e Regex.
  2. Codifica Z3 SMT: Le condizioni di vulnerabilità (es. overflow intero) vengono codificate come formule logiche. Il solver Z3 verifica se esiste un input concreto che soddisfa la condizione di errore.
  3. Estrazione del "Witness": Se Z3 restituisce SAT (soddisfacibile), viene estratto un valore concreto (es. un numero specifico) che dimostra matematicamente l'exploitabilità.
• Validazione Runtime: 7 vulnerabilità rappresentative sono state testate compilando Proof-of-Concept (PoC) con GCC AddressSanitizer (ASAN) per confermare crash reali in memoria.
• Esperimenti Ausiliari:
  • Ablazione Prompt: Confronto tra prompt standard e prompt con istruzioni di sicurezza esplicite. Nota importante: Questo esperimento di ablazione è stato condotto su un sotto-corpus di 50 prompt (v1), non sull'intero benchmark di 500 prompt, per garantire la replicabilità e la gestione delle risorse computazionali.
  • Confronto Strumenti: Test di 6 strumenti industriali (Semgrep, Bandit, Cppcheck, Clang SA, FlawFinder, CodeQL) sugli stessi artefatti.
  • Asimmetria Generazione-Revisione: Test se i modelli riescono a identificare le proprie vulnerabilità quando gli viene chiesto di revisionare il codice.

3. Contributi Chiave

1. Verifica Formale su Larga Scala: Primo studio che applica la verifica formale (Z3 SMT) per stabilire la "ground-truth" (verità fondamentale) dell'exploitabilità del codice generato dall'IA, superando i limiti del semplice matching di pattern.
2. Benchmark Multi-Modello: Valutazione simultanea di 7 modelli frontier su prompt identici, fornendo un confronto oggettivo delle prestazioni di sicurezza.
3. Dimostrazione del Divario Strutturale: Evidenzia che gli strumenti di analisi statica industriali attuali sono strutturalmente incapaci di rilevare specifiche classi di vulnerabilità (overflow in aritmetica di allocazione) che l'IA genera frequentemente.
4. Prova di Asimmetria Cognitiva: Dimostra che i modelli possiedono la conoscenza per rilevare le vulnerabilità in modalità "revisione", ma falliscono sistematicamente nell'applicare tale conoscenza durante la "generazione".

4. Risultati Principali

• Tasso di Vulnerabilità Elevato:

  • La media di vulnerabilità tra tutti i modelli è del 55,8%.
  • GPT-4o ha il tasso più alto (62,4%, voto F).
  • Gemini 2.5 Flash ha le prestazioni migliori (48,4%, voto D).
  • Nessun modello ha raggiunto un voto migliore di D (nessuno sotto il 45% di vulnerabilità).
  • Sono stati trovati 1.055 casi formalmente provati sfruttabili tramite Z3.

• Categorie Critiche:

  • L'Aritmetica Interi (CWE-190/195) presenta il tasso di fallimento più alto (87%), principalmente a causa della mancata gestione degli overflow nei calcoli di dimensione per malloc.
  • La Gestione della Memoria (CWE-131/190) segue con il 67%.

• Validazione Runtime:

  • 6 su 7 vulnerabilità selezionate hanno causato crash reali confermati da AddressSanitizer (es. heap-buffer-overflow, SQL injection funzionante).
  • Un caso di hashing password debole (SHA-256) è stato crackato in 0,01ms.

• Inefficacia delle Istruzioni di Sicurezza:

  • L'aggiunta di prompt espliciti ("scrivi codice sicuro") ha ridotto il tasso di vulnerabilità media solo del 4% (da 64,8% a 60,8%). Questo risultato è stato ottenuto analizzando un sotto-corpus di 50 prompt (v1) durante l'esperimento di ablazione.
  • Quattro modelli su cinque sono rimasti con voto F. Le istruzioni non sembrano sovrascrivere i pattern di memoria appresi dai dati di addestramento.

• Il Divario degli Strumenti (RQ5):

  • La combinazione di 6 strumenti industriali ha rilevato solo il 7,6% degli artefatti vulnerabili.
  • Hanno mancato il 97,8% delle vulnerabilità formalmente provate da Z3.
  • CodeQL, uno strumento semantico avanzato, ha rilevato 0 su 90 (100% di fallimento) delle vulnerabilità Z3-proven, dimostrando che l'overflow in aritmetica di allocazione è strutturalmente invisibile all'analisi dei flussi di dati senza ragionamento aritmetico concreto.

• Asimmetria Generazione-Revisione (RQ6):

  • Quando il codice vulnerabile generato è stato re-inserito nel modello per una revisione, il modello ha identificato correttamente la vulnerabilità nel 78,7% dei casi.
  • Tuttavia, genera lo stesso codice vulnerabile nel 55,8% dei casi di default. Questo indica che il problema non è la mancanza di conoscenza, ma un fallimento nell'applicazione spontanea durante la generazione.

5. Significato e Implicazioni

• Codice "Rotto" di Default: Gli assistenti di codifica attuali producono codice insicuro di default in domini critici. Non è un problema di configurazione, ma intrinseco alla generazione.
• Insufficienza dei Prompt: Aggiungere istruzioni di sicurezza ai prompt non è una mitigazione sufficiente; il problema risiede nei prior di generazione del modello, non nella superficie di istruzione.
• Necessità di Verifica Formale: Gli strumenti statici tradizionali (pattern matching, analisi dei flussi) sono inadeguati per il codice generato dall'IA, specialmente per gli overflow interi. La verifica formale (SMT) è l'unico metodo per stabilire la sfruttabilità reale su larga scala.
• Raccomandazioni per gli Sviluppatori:
  1. Trattare il codice C/C++ generato dall'IA come codice non revisionato che richiede audit di sicurezza espliciti.
  2. Utilizzare compilatori con sanitizzatori (-fsanitize=address,undefined) su tutto il codice generato.
  3. Non fare affidamento su strumenti come Semgrep, CodeQL o Cppcheck per rilevare overflow in calcoli di allocazione generati dall'IA.
  4. Integrare la verifica formale o la revisione umana per l'aritmetica di allocazione.

Conclusione: Lo studio conclude che l'IA per la codifica è "rotta di default" per quanto riguarda la sicurezza. La metodologia di verifica formale tramite Z3 non è solo uno strumento di ricerca, ma dovrebbe diventare un componente obbligatorio in qualsiasi pipeline di revisione del codice AI che operi su target sensibili alla sicurezza.