Riepilogo Tecnico: Verifica di Modelli Agente

Enunciato del Problema

La verifica del codice di sistema generato da Large Language Models (LLM) presenta sfide uniche che aggravano le difficoltà esistenti nella verifica formale. Sebbene gli LLM possano generare corpi di codice sostanziali per sistemi operativi, compilatori e driver in linguaggi come C e Rust, i codebase risultanti spesso mancano di specifiche formali esplicite. Inoltre, i contratti di sicurezza nel codice generato dagli LLM sono frequentemente codificati implicitamente nei punti di chiamata anziché essere enforced ai confini delle funzioni.

Questa codifica implicita porta a una specifica modalità di fallimento: le funzioni di supporto (ad esempio, lettori indicizzati per byte, scrittori con aritmetica di offset) spesso mancano di controlli sui limiti e di protezioni contro gli overflow, affidandosi alla logica del chiamante circostante per mantenere gli invarianti. Di conseguenza, il codice funziona correttamente su input ben formati ma fallisce su input avversari o costruiti appositamente. Gli strumenti di verifica tradizionali faticano in questo contesto perché o segnalano eccessivamente (marchiando le funzioni di supporto come rotte senza contesto) o segnalano insufficientemente (mancando bug perché i chiamanti attuali non li attivano). Inoltre, gli approcci di verifica basati sugli LLM esistenti spesso mancano di correttezza per quanto riguarda la sicurezza aritmetica e della memoria, mentre i verificatori deduttivi tradizionali faticano con la scala e la natura ricca di cicli del codice di sistema e mancano della capacità di generare controesempi concreti.

Metodologia: Verifica di Modelli Agente

Gli autori propongono la Verifica di Modelli Agente, un paradigma di verifica che accoppia agenti LLM con un backend di verifica di modelli limitati (BMC) secondo il principio: "Gli agenti propongono, i solver verificano."

Il sistema, istanziato come BMC-Agent, opera attraverso una pipeline in cui gli agenti LLM gestiscono compiti che richiedono giudizio semantico, mentre un backend BMC deterministico (CBMC per C, Kani per Rust) espleta tutte le decisioni rilevanti per la correttezza.

Impegni Architettonici Fondamentali

1. Inferenza di Specifiche Top-Down:

   • Gli agenti inferiscono precondizioni e postcondizioni per funzione in senso top-down dal contesto del chiamante.
   • Le specifiche sono generate in un Linguaggio Specifico di Dominio (DSL) ristretto che si traduce deterministicamente nelle primitive native assume/assert del backend.
   • Il sistema genera specifiche di correttezza funzionale (ad esempio, espressioni di equivalenza di riferimento, identità algebriche) oltre ai controlli difensivi di assenza di panico, elevando la verifica dalla semplice prevenzione dei crash alla fedeltà comportamentale.

2. Verifica Compositiva:

   • La verifica è scomposta per funzione. Ogni funzione è verificata in isolamento rispetto alla sua specifica inferita.
   • Le funzioni chiamate (callees) sono sostituite da stub vincolati dalle loro postcondizioni. Ciò implementa una disciplina assume-guarantee in cui la postcondizione di un callee diventa l'assunzione per il chiamante.
   • Questo approccio previene l'esplosione dello stato dell'intero programma, consentendo alla verifica di scalare con la dimensione dello spazio di stato di una singola funzione piuttosto che dell'intero programma.

3. Validazione dei Controesempi Multi-Stadio:

   • I controesempi BMC non sono trattati come rapporti di bug immediati. Passano attraverso una pipeline di validazione rigorosa per distinguere i crash attivi nell'albero di codice da fallimenti latenti o artefatti di modellazione:
     • Raggiungibilità dell'Input: Propagazione degli input testimone lungo il grafo delle chiamate per determinare se un chiamante può fornire i valori.
     • Fattibilità del Callee: Esecuzione di BMC con i corpi reali dei callee per garantire che il testimone sia raggiungibile attraverso implementazioni reali.
     • Riproduzione Dinamica: Compilazione di un harness per eseguire il testimone su un sistema host, catturando segnali (SIGSEGV, SIGABRT, ecc.) per confermare i crash dinamici.
     • Audit di Realismo: Un agente LLM esamina il contesto completo (specifica, harness, stato del testimone) per classificare la scoperta come realistica o irrealistica, filtrando gli artefatti invarianti del framework (ad esempio, globali non inizializzati, stati hardware impossibili).

4. Ciclo di Raffinamento Adattivo (CEGAR a Livello di Specifica):

   • Quando un controesempio è classificato come spurio (ad esempio, un artefatto di srotolamento dei cicli), il sistema non lo sopprime semplicemente. Invece, un LLM propone raffinamenti (restringendo le precondizioni, rafforzando i contratti dei callee o regolando i parametri del solver).
   • Una guardia di correttezza assicura che questi raffinamenti non mascherino bug reali.
   • I raffinamenti accettati sono persistiti in una base di conoscenza (archivio di specifiche e libreria di pattern) e propagati a tutti i chiamanti, estendendo efficacemente il CEGAR dall'astrazione dei predicati al livello di specifica con propagazione compositiva.

Contributi Chiave

Il documento delinea sei contributi principali:

1. Paradigma di Verifica di Modelli Agente: Un framework in cui gli agenti LLM gestiscono compiti semantici (inferenza di specifiche, selezione dei controlli, classificazione) mentre i backend BMC garantiscono la correttezza, abilitando la verifica senza specifiche del codice C e Rust generato dagli LLM.
2. Livello di Specifica Top-Down: Un meccanismo per inferire pre/postcondizioni per funzione e selezionare controlli aritmetici semanticamente giustificati (ad esempio, overflow, controlli sui puntatori) tramite un DSL che si traduce in CBMC/Kani.
3. Architettura di Verifica Compositiva: Un approccio scalabile che verifica le funzioni in isolamento sotto contratti assume-guarantee, parallelizzando attraverso i livelli del grafo delle chiamate.
4. Pipeline di Validazione: Un processo a quattro stadi (raggiungibilità, fattibilità, riproduzione dinamica, audit di realismo) che categorizza le scoperte in livelli di evidenza (ad esempio, "confermato dinamico", "confermato ingresso di sistema").
5. Ciclo di Raffinamento Multi-Livello: Un sistema che eleva il CEGAR al livello di specifica, utilizzando controesempi spurii per guidare raffinamenti compositivi che persistono tra le esecuzioni.
6. Implementazione e Valutazione di BMC-Agent: Uno strumento funzionante valutato su corpora diversificati, dimostrando la capacità di confermare difetti reali, produrre verifiche pulite limitate su librerie fuzzate e provare l'equivalenza funzionale.

Risultati della Valutazione

Gli autori hanno valutato BMC-Agent su quattro corpora che coprono C e Rust:

• VibeOS (C): Un kernel ARM64 generato da LLM di 15.000 righe. BMC-Agent ha confermato 34 bug realistici in 12 moduli. Di questi, 16 sono stati riprodotti dinamicamente (SIGSEGV/SIGABRT), 14 sono stati confermati come punti di ingresso di sistema e 4 sono violazioni di modelli formali.
• Librerie OSS Mature (C): Valutate su jq, OpenSSL, libcurl, libxml2 e protobuf upb. Lo strumento ha rivelato 2 difetti di comportamento indefinito in jq (presentati come GHSA) e ha prodotto verifiche pulite limitate su superfici di parser pesantemente fuzzate (ad esempio, 15/24 funzioni foglia in ASN.1 di OpenSSL verificate pulite).
• Driver Realtek r8125 (C): Ha trovato un bypass del controllo dei limiti MMIO protetto da CAP_NET_ADMIN nell'ioctl dello strumento rtl8125, attivato abilitando controlli di overflow specifici tramite il selettore di flag.
• claudes-c-compiler (Rust): Un compilatore C generato da LLM di 50.000 righe. BMC-Agent ha confermato 25 bug reali, principalmente difetti di classe panico su helper di byte delle API pubbliche (OOB di slice, overflow interi) e una violazione di correttezza funzionale. Ha anche stabilito equivalenza funzionale limitata per gli helper di hash ELF e scrittura di intestazioni.

Osservazioni Chiave dai Risultati:

• La precisione dello strumento è attribuita ai rilevatori di fase di realismo (filtraggio degli artefatti del framework), alla selezione di flag per funzione (abilitando controlli disattivati di default nelle configurazioni standard) e al ciclo di feedback (convertendo pattern ricorrenti in invarianti permanenti).
• Nel caso del compilatore Rust, i bug seguivano un anti-pattern specifico: l'LLM scriveva funzioni di supporto senza controlli sui limiti, affidandosi ai chiamanti per mantenere gli invarianti. Ciò ha portato a un codice che funzionava su input ben formati ma falliva su input avversari, un profilo distinto dagli errori di logica tipici dei compilatori scritti da umani.

Significato e Affermazioni

Il documento afferma che la Verifica di Modelli Agente affronta il "divario di specifica" nel codice di sistema generato dagli LLM automatizzando l'inferenza dei contratti e accoppiandoli con una verifica di modelli limitata e corretta.

• Correttezza vs Scalabilità: Delegando la correttezza al BMC e utilizzando agenti per il giudizio semantico, l'approccio evita l'insoundness del ragionamento puro degli LLM superando al contempo i limiti di scalabilità della verifica dell'intero programma.
• Verifica Azionabile: La pipeline di validazione multi-stadio garantisce che i bug segnalati non siano solo controesempi teorici, ma siano classificati in base alla loro raggiungibilità e impatto dinamico, distinguendo tra crash attivi e attività di hardening latenti.
• Propagazione Compositiva: La capacità del sistema di raffinare le specifiche e propagarle attraverso il grafo delle chiamate gli permette di imparare dai controesempi spurii, migliorando la qualità della verifica nel tempo senza intervento manuale.

Gli autori rimangono modesti riguardo al lavoro futuro, notando che una valutazione quantitativa ampia (precisione/recall su larga scala), un'analisi più approfondita delle ipotesi di correttezza delle specifiche e la riduzione dei costi tramite ottimizzazione dei token sono i prossimi passi necessari. Sottolineano che i risultati attuali dimostrano la capacità della pipeline di confermare difetti e verificare superfici pulite, ma non affermano di aver risolto il problema generale della verifica di tutto il codice generato dagli LLM senza limitazioni.