Riassunto Tecnico: CNnotator: Sintesi di Annotazioni per la Sicurezza della Memoria Guidata da LLM

Definizione del Problema

Gli errori di sicurezza della memoria costituiscono una parte significativa delle vulnerabilità di sicurezza nei sistemi C e C++. A differenza dei moderni linguaggi sicuri per la memoria (ad esempio, Rust, Java) che prevengono questi bug per progettazione, il C si affida a modelli di utilizzo della memoria impliciti che sono difficili da estrarre e verificare per l'essere umano. Sebbene i metodi formali e l'IA offrano punti di forza complementari — le reti neurali eccellono nel "indovinare" schemi mentre gli strumenti formali eccellono nel "verificare" — esiste un divario nell'automatizzare la traduzione di codice C legacy in specifiche verificabili. Nello specifico, determinare come un programma C manipoli la memoria (proprietà, allocazione e deallocazione) è un compito laborioso per gli umani ma potenzialmente inferibile dai Large Language Models (LLM). La sfida consiste nel generare specifiche formali che rappresentino accuratamente questi schemi impliciti per consentire la verifica o la transpilazione sicura.

Metodologia

Gli autori presentano CNnotator, uno strumento che sintetizza annotazioni di sicurezza della memoria per codice C utilizzando un ciclo "indovina e controlla" guidato da LLM. Il sistema prende come bersaglio CN, un linguaggio di contratto basato sulla logica di separazione (simile a Frama-C ma con una rappresentazione esplicita della memoria simile al borrow checker di Rust).

Il Flusso di Lavoro di CNnotator

Lo strumento opera come un ciclo iterativo:

1. Pre-elaborazione: Lo strumento unisce i file del progetto C in un singolo contesto e inietta le librerie e le macro CN necessarie per gestire correttamente allocazione e deallocazione. Analizza il codice in un Albero di Sintassi Astratta (AST) utilizzando Tree-sitter.
2. Selezione della Funzione: Itera attraverso le funzioni, partendo dal fondo del file per preservare le posizioni dell'AST.
3. "Indovino" dell'LLM (Generazione delle Annotazioni):
   • L'LLM viene istruito con una guida sulla sintassi di CN (estratta dal Tutorial di CN), l'intero codice del progetto e la specifica funzione target.
   • Prima di generare un'annotazione, all'LLM viene chiesto di identificare se la funzione è intrinsecamente insicura (ad esempio, use-after-free). Se ritenuta insicura, il processo si interrompe per quella funzione e viene inserito un commento che spiega il bug.
   • Se la funzione appare sicura, l'LLM genera un'annotazione CN che specifica i prerequisiti (requisiti di proprietà) e i post-requisiti.
4. "Controllo" Formale (Test):
   • L'annotazione generata viene iniettata nel codice C.
   • Il backend Fulminate compila la specifica in controlli a runtime.
   • Il framework Bennet deriva generatori di input casuali dalle precondizioni per creare stati concreti dell'heap.
   • Il sistema esegue 100 test basati sulle proprietà per verificare se il codice viene eseguito senza violazioni della sicurezza della memoria sotto la specifica generata.
5. Raffinamento:
   • Successo: Se tutti i 100 test passano, l'annotazione viene accettata.
   • Fallimento: Se i test falliscono, i messaggi di errore vengono forniti all'LLM per raffinare l'annotazione. Questo ciclo può essere eseguito fino a sei volte.
   • Errori di Sintassi: Se la generazione iniziale fallisce a causa di errori di sintassi (che spesso producono messaggi del compilatore poco utili), il sistema riprova il prompt originale fino a due volte aggiuntive invece di utilizzare il feedback dell'errore, sfruttando la nondeterminazione dell'LLM.

Contributi Chiave

• Sviluppo dello Strumento: La creazione di CNnotator, uno strumento basato su Python che integra LangChain/LangGraph per il controllo degli agenti, Tree-sitter per il parsing e i framework Fulminate/Bennet per il testing automatizzato.
• Approccio di Verifica Ibrido: Dimostrazione di una pipeline pratica in cui gli LLM generano specifiche di logica di separazione (CN) e i backend di testing formale ne validano l'esistenza, aggirando efficacemente la necessità di fidarsi del ragionamento dell'LLM.
• Benchmark Suite: La costruzione di una suite di test composta da 31 funzioni C annotabili (che spaziano dalla semplice proprietà a loop complessi con variabili globali e macro) e 3 funzioni intrinsecamente insicure progettate per testare la capacità dello strumento di rilevare bug.

Risultati Sperimentali

Gli autori hanno valutato CNnotator attraverso cinque backend di LLM di OpenAI (o3, o4-mini, o3-mini, GPT-4.1 e GPT-4o) sulle 31 funzioni annotabili.

• Performance: Il modello di ragionamento o3 ha ottenuto le prestazioni più elevate, annotando con successo il 96,8% delle funzioni (30/31). Ha raggiunto un tasso di successo del 90,3% al primo tentativo, richiedendo in media solo 1,10 tentativi per ogni annotazione riuscita.
• Modelli Chat: Anche il modello chat GPT-4o ha ottenuto un tasso di successo al primo tentativo del 64,5% e un tasso di successo complessivo del 71,0%, superando o3-mini nelle metriche del primo tentativo.
• Modalità di Fallimento:
  • Lo strumento ha identificato con successo tutte e tre le funzioni intrinsecamente insicure inserite manualmente (use-after-free, double-free) e ha rifiutato di annotarle.
  • Non sono stati osservati falsi positivi (annotazioni che passano i test ma sono errate) durante le ispezioni manuali dei risultati di o3.
  • Sono state notate come potenziale problema le annotazioni troppo permissive (che richiedono più proprietà del necessario), ma sono state considerate accettabili in quanto forniscono comunque specifiche valide.
• Efficienza: Il sistema dimostra che per programmi di piccole e medie dimensioni, l'annotazione assistita dall'IA sta diventando pratica, con un numero minimo di iterazioni richieste per i modelli ad alto successo.

Significato e Rivendicazioni

Il documento sostiene che CNnotator dimostri la fattibilità dell'annotazione assistita dall'IA per codebase C reali. Combinando le capacità di riconoscimento dei pattern degli LLM con il rigoroso controllo degli strumenti di testing formale, l'approccio affronta la natura "indovina e controlla" della verifica formale.

Gli autori posizionano questo lavoro come un passo verso:

1. Modernizzazione del Codice: Facilitare la migrazione di codice C legacy verso linguaggi più sicuri (come Rust) stabilendo prima i contratti di sicurezza della memoria.
2. Automazione della Verifica: Automatizzare la generazione di specifiche di sicurezza della memoria, un compito tradizionalmente manuale e soggetto a errori.
3. Praticità: Dimostrare che gli attuali modelli possono gestire la complessità della proprietà della memoria in C, raggiungendo alti tassi di successo con un intervento umano minimo.

Il documento rimane modesto riguardo al proprio ambito, osservando che i benchmark consistono in funzioni inferiori alle 50 righe con un flusso di controllo semplice e non coprono ancora schemi di codice di produzione complessi come il casting di tipi o l'aritmetica avanzata dei puntatori. Tuttavia, i risultati suggeriscono che, con il miglioramento delle capacità degli LLM, la tecnica potrebbe scalare su sistemi più grandi e complessi.