Natural Language based Specification and Verification

Sintesi Tecnica: Specifica e Verifica basate sul Linguaggio Naturale (NLForge)

Enunciato del Problema
Le violazioni della sicurezza della memoria nei programmi C e C++ — come dereferimenti non validi, utilizzo dopo rilascio (use-after-free) e accessi fuori dai limiti — rimangono una fonte primaria di vulnerabilità software. Questi errori derivano spesso da interazioni interprocedurali complesse che coinvolgono allocazione, deallocazione, inizializzazione e aliasing, che gli strumenti tradizionali di analisi statica faticano a verificare su larga scala. Sebbene i Modelli Linguistici su Grande Scala (LLM) abbiano dimostrato capacità solide nell'identificare bug, affrontano sfide significative nel prevenire l'introduzione di nuove vulnerabilità attraverso la verifica formale. Le pipeline di verifica esistenti richiedono tipicamente specifiche in linguaggi formali rigidi (ad esempio, invarianti di ciclo, pre/post-condizioni), creando un elevato onere di annotazione. I tentativi precedenti di utilizzare gli LLM per sintetizzare queste specifiche formali hanno mostrato risultati limitati. Inoltre, recenti benchmark indicano che le prestazioni degli LLM crollano precipitosamente quando si passa dalla verifica di una singola funzione al ragionamento compositivo su più funzioni, principalmente a causa delle limitazioni della finestra contestuale e della difficoltà nel mantenere una coerenza semantica globale.

Metodologia: NLForge
Gli autori propongono NLForge, un framework di verifica compositivo che sfrutta gli LLM per generare e ragionare su specifiche in linguaggio naturale anziché su artefatti formali rigidi. Il sistema opera su un'analisi dal basso verso l'alto, dai callee ai chiamanti, del grafo delle chiamate del programma.

1. Architettura della Pipeline:

   • Preprocessing: Il sistema estrae definizioni di funzione, firme e siti di chiamata dal codice C/C++ per costruire un grafo delle chiamate. Le chiamate non risolte sono gestite tramite stub esterni.
   • Analisi dal Basso verso l'Alto: Il framework esegue una sequenza di passaggi di analisi sul grafo delle chiamate in ordine topologico (elaborando i callee prima dei chiamanti).
   • Sintesi in Linguaggio Naturale: Invece di generare logica formale, l'LLM produce sintesi strutturate in linguaggio naturale (codificate come JSON tipizzato con descrizioni in linguaggio naturale) per proprietà specifiche:
     • Allocazione/Rilascio/Inizializzazione: Riassunto della creazione di oggetti heap, degli effetti della deallocazione e dell'inizializzazione dei parametri di output.
     • Contratti di Sicurezza della Memoria: Inferenza di precondizioni (ad esempio, non nullo, non rilasciato, dimensione del buffer) e postcondizioni.
     • Sintesi su Perdite e Interi: Tracciamento degli obblighi irrisolti e dei rischi di overflow intero.
   • Controllo Compositivo: Nel passaggio finale di verifica, l'LLM analizza una funzione utilizzando le proprie precondizioni inferite e le sintesi in linguaggio naturale dei suoi callee. Il modello agisce come un agente di ragionamento che mantiene uno stato di esecuzione latente, verificando i requisiti di sicurezza rispetto ai contratti dei callee senza inlining dell'intera implementazione del callee.

2. Razionale di Progettazione:
   L'approccio è motivato dall'osservazione che gli LLM, addestrati su codice e documentazione, possono generare, interpretare e rifinire sintesi in linguaggio naturale in modo più coerente rispetto a notazioni formali rigide. Questa progettazione mira a decomporre il problema della verifica in sintesi semantiche riutilizzabili, permettendo al modello di ragionare su una funzione sotto assunzioni esplicitamente dichiarate riguardo ai suoi callee, anziché riesaminare il codice sorgente grezzo per ogni chiamante.

Contributi Chiave

• Framework Compositivo: Un framework di verifica interprocedurale dal basso verso l'alto per C/C++ che utilizza gli LLM per inferire e verificare proprietà di sicurezza della memoria.
• Rappresentazione Intermedia in Linguaggio Naturale: L'introduzione di sintesi semantiche in linguaggio naturale come rappresentazione intermedia per la verifica, in contrasto con lavori precedenti focalizzati sulla generazione di specifiche formali per verificatori simbolici esterni.
• Pipeline di Analisi a Fasi: Una decomposizione del ragionamento sulla sicurezza della memoria in sintesi riutilizzabili (allocazione, deallocazione, inizializzazione e obblighi lato chiamante) che vengono reimmesse all'LLM nelle fasi successive.
• Valutazione Empirica: Uno studio comparativo del ragionamento compositivo rispetto a una baseline di prompting su intero programma non compositivo sui benchmark SV-COMP 2026.

Risultati
Gli autori hanno valutato NLForge su un sottoinsieme dei benchmark di sicurezza della memoria SV-COMP 2026 utilizzando quattro backbones LLM (Claude Sonnet-4.6, GPT-5.4, Gemini-3.1-flash-lite e Qwen3.5-27B-UD-Q4), confrontandoli con verificatori tradizionali (CPAchecker, Symbiotic, Ultimate Automizer).

• RQ1 (LLM come Verificatori): L'analisi basata su LLM dimostra un'elevata sensibilità (recall) e copertura, identificando la maggior parte dei veri positivi (ad esempio, Sonnet-4.6 ha raggiunto una recall del 99,8% su valid-memsafety). Tuttavia, producono significativamente più falsi positivi rispetto agli strumenti tradizionali e non possono ancora fungere da verificatori autonomi e sound. Gli strumenti tradizionali spesso restituiscono "Sconosciuto" (UNK) per casi difficili per evitare falsi positivi, mentre gli LLM forniscono risposte definitive con tassi di errore più elevati.
• RQ2 (Verifica Compositiva): L'approccio compositivo supera significativamente la baseline non compositiva, in particolare su benchmark complessi del mondo reale relativi al flusso di controllo e alle strutture dati.
  • Le esecuzioni compositive hanno aumentato i Veri Positivi da 3.390 a 3.476 e ridotto i Falsi Negativi da 301 a 216 su tutti i modelli.
  • Il miglioramento è stato più pronunciato per i modelli più piccoli (ad esempio, Qwen3.5-27B-Q4 ha visto i Falsi Negativi scendere da 218 a 97) e sui benchmark che richiedono un forte ragionamento interprocedurale.
  • I guadagni sono stati meno consistenti sui test sintetici e localizzati di Juliet, dove i modelli non compositivi potevano sfruttare direttamente pattern locali.

Significato e Affermazioni
Il documento sostiene un cambiamento nel modo in cui gli LLM sono utilizzati nella verifica: passando dal considerarli esclusivamente come generatori di artefatti formali per motori esterni all'impiegarli come agenti di ragionamento su sintesi strutturate e riutilizzabili in linguaggio naturale.

• Praticità: Il linguaggio naturale funge da livello di specifica intermedia pratico che abilita la verifica compositiva, in particolare per attività in cui il prompting su intero programma supera il budget di ragionamento del modello o la finestra contestuale.
• Limitazioni: Gli autori riconoscono che l'informalità del linguaggio naturale porta a problemi di calibrazione (più falsi positivi) e che l'approccio è sensibile alla qualità delle sintesi generate; errori nelle sintesi possono propagarsi e amplificarsi.
• Prospettive Future: Il lavoro suggerisce che, sebbene gli LLM non siano ancora un sostituto per la verifica formale sound, offrono una direzione promettente per la verifica di individuazione di bug scalabile. Il lavoro futuro dovrebbe concentrarsi sul miglioramento della calibrazione, sulla combinazione delle sintesi con controlli simbolici e sulla gestione più robusta di funzionalità complesse come chiamate indirette e invarianti heap.

Lo studio conclude che la questione non è semplicemente se gli LLM possano verificare la sicurezza della memoria, ma sotto quali rappresentazioni e decomposizioni diventano più affidabili, evidenziando che il linguaggio naturale può efficacemente colmare il divario tra la struttura modulare del programma e le capacità di ragionamento degli LLM.