Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

1. Il Problema

L'esecuzione simbolica è una tecnica potente per l'analisi del programma, ma la sua efficacia è limitata da tre ostacoli fondamentali:

1. Frammenti ostili ai solver: Istruzioni che generano vincoli complessi (es. aritmetica non lineare, funzioni trigonometriche, operazioni su floating-point) che i solver SMT (Satisfiability Modulo Theories) faticano a risolvere o che portano a tempi di calcolo proibitivi.
2. Modellazione imprecisa: La difficoltà di modellare accuratamente comportamenti complessi come le chiamate di sistema o le comunicazioni di rete.
3. Esplosione dei percorsi: L'infinità dei possibili percorsi di esecuzione, aggravata dall'uso di strutture dati dinamiche (heap) e aliasing, che rende l'esplorazione completa impossibile.

Approcci recenti hanno tentato di sostituire i solver SMT con Large Language Models (LLM) per bypassare questi limiti. Tuttavia, questi metodi falliscono spesso su codici reali complessi perché gli LLM faticano a mantenere una coerenza globale su percorsi di esecuzione profondi che richiedono vincoli interprocedurali precisi, a differenza dei solver SMT che sono progettati per questo scopo.

2. Metodologia: Gordian

Gli autori presentano Gordian, un framework ibrido di esecuzione simbolica che integra selettivamente gli LLM per generare "ghost code" (codice fantasma) leggero. L'obiettivo non è sostituire il solver SMT, ma potenziarlo intervenendo solo sui frammenti di codice dove il solver tradizionale fallisce.

Il sistema opera in tre fasi principali, generando tre tipi specifici di ghost code:

A. Inversione di Frammenti Difficili (Fragment Inversion)

• Concetto: Quando un frammento di codice (es. calcolo trigonometrico) è difficile da risolvere in avanti, l'LLM genera una funzione fantasma che inverte il calcolo.
• Meccanismo: Gordian esegue l'esecuzione simbolica sostituendo il frammento difficile con variabili simboliche fresche. Successivamente, utilizza un algoritmo di propagazione bidirezionale dei vincoli:
  1. Il solver SMT risolve i vincoli "suffisso" (dopo il frammento) per ottenere valori target.
  2. L'LLM esegue la funzione inversa (generata) per propagare questi valori all'indietro verso l'input.
  3. Un ottimizzatore trova l'input più vicino che soddisfa sia i vincoli "prefisso" (prima del frammento) che quelli inversi.
• Vantaggio: Permette di attraversare ostacoli matematici complessi mantenendo la precisione del solver SMT sui vincoli globali.

B. Modelli Surrogati (Surrogate Modeling)

• Concetto: Per frammenti che non possono essere invertiti (es. perdita di informazioni, dipendenze da stato esterno), l'LLM genera un modello surrogato.
• Meccanismo: L'LLM riscrive il frammento difficile con una versione semplificata che preserva il comportamento rilevante (ramificazioni, output) ma utilizza teorie "amichevoli" per il solver (es. sostituendo funzioni crittografiche o complesse con stub o approssimazioni lineari).
• Sicurezza: Poiché il surrogato è un'approssimazione, qualsiasi input generato viene validato eseguendo il programma originale per garantire la correttezza (soundness).

C. Partizionamento Semantico dell'Heap (Semantic Heap Partitioning)

• Concetto: Per gestire l'esplosione dei percorsi causata da strutture dati dinamiche (es. liste, alberi), l'LLM genera codice che impone topologie semantiche specifiche.
• Meccanismo: Invece di esplorare tutte le possibili configurazioni dell'heap, l'LLM identifica forme significative (es. "una lista di lunghezza >= 3", "un anello valido") e genera un codice fantasma che vincola l'heap a queste forme specifiche, lasciando i valori interni ancora simbolici.
• Vantaggio: Riduce drasticamente lo spazio di ricerca mantenendo la capacità di esplorare le condizioni di controllo dipendenti dalla struttura.

3. Contributi Chiave

1. Approccio Ibrido Innovativo: Un metodo che combina la forza di ragionamento globale dei solver SMT con la capacità generativa e di comprensione del dominio degli LLM, senza sacrificare la correttezza formale.
2. Tre Varianti di Ghost Code: Definizione e implementazione pratica di inversione, surrogati e partizionamento dell'heap, con prompt e algoritmi di integrazione specifici.
3. Validazione Completa: Dimostrazione che il ghost code generato dall'LLM non compromette la soundness, poiché tutti gli input finali sono verificati contro il programma originale.

4. Risultati Sperimentali

Il framework è stato implementato su KLEE e valutato su tre benchmark:

• LogicBombs: 53 programmi sintetici con "bombe logiche" (condizioni difficili da soddisfare).
• FDLibM: Una libreria matematica complessa con 78 punti di ingresso e aritmetica floating-point.
• Programmi a Input Strutturato: libexpat (XML), jq (JSON) e bc (linguaggio espressioni).

Risultati Principali:

• Copertura: Gordian ha migliorato la copertura del codice del 52–84% rispetto all'esecuzione simbolica tradizionale (KLEE) e dell'86–419% rispetto alle tecniche basate solo su LLM (come ConcoLLMic).
• Efficienza dei Token: Rispetto alle tecniche puramente basate su LLM, Gordian ha ridotto l'uso dei token dell'LLM del 90–96%, poiché l'LLM viene chiamato solo per generare piccoli frammenti di codice e non per ragionare su interi percorsi di esecuzione.
• Performance Specifiche:
  • Su LogicBombs, ha attivato fino al 94.3% delle bombe logiche (vs 39.6% di KLEE).
  • Su FDLibM, ha raggiunto una copertura media del 91.7% (vs 40% di ConcoLLMic).
  • Su programmi strutturati, ha coperto 9.7 volte più righe di codice rispetto a ConcoLLMic.

5. Significato e Impatto

Il lavoro di Gordian è significativo perché risolve il compromesso storico tra la precisione dei solver formali e la flessibilità degli LLM.

• Praticità: Dimostra che l'uso degli LLM nell'analisi del software non deve essere "tutto o nulla". L'approccio ibrido rende l'analisi simbolica applicabile a codici reali complessi (librerie matematiche, parser) che erano precedentemente intrattabili.
• Efficienza dei Costi: Riducendo drasticamente il numero di token necessari, rende l'uso di LLM avanzati economicamente sostenibile per l'analisi automatizzata su larga scala.
• Futuro: Apre la strada a framework di analisi che possono adattarsi dinamicamente alle difficoltà del codice, utilizzando l'intelligenza artificiale come "assistente specializzato" per sbloccare percorsi di esecuzione altrimenti bloccati.

In sintesi, Gordian rappresenta un passo avanti fondamentale verso l'automazione robusta del testing e della verifica del software, superando i colli di bottiglia dei solver tradizionali senza perdere la rigore matematico necessario per garantire la correttezza.