Riepilogo Tecnico: Veritas

Enunciato del Problema

Rilevare vulnerabilità di corruzione della memoria (MCV) in binari privi di simboli presenta una sfida fondamentale di ricostruzione semantica. A differenza dell'analisi del codice sorgente, l'analisi dei binari deve recuperare come gli oggetti di memoria vengono allocati, propagati, vincolati e accessi attraverso le funzioni partendo da artefatti che hanno perso la struttura di alto livello, i confini degli oggetti e il flusso di controllo esplicito a causa della compilazione e della rimozione dei simboli.

I recenti approcci basati su Large Language Model (LLM) hanno migliorato la comprensione del codice, ma faticano nel rilevamento delle MCV nei binari per tre motivi principali:

1. Tracciamento dello Stato Condiviso: Le vulnerabilità spesso derivano da ipotesi incoerenti su regioni di memoria condivise tra funzioni disgiunte che mancano di archi diretti nella catena di chiamate. L'espansione standard del grafo delle chiamate non riesce a catturare queste dipendenze.
2. Perdita Semantica: Le rappresentazioni recuperate sono frammentate. L'IR LLVM sollevato preserva i pattern di accesso alla memoria a basso livello, ma è oscurato da artefatti del compilatore (variabili SSA, cast), mentre il C decompilato fornisce una struttura di alto livello ma collassa le operazioni di memoria in espressioni di offset generiche, cancellando l'identità degli oggetti.
3. Verifica dei Vincoli: L'analisi statica spesso non può determinare se un accesso sospetto sia raggiungibile sotto condizioni di percorso fattibili. Senza prove eseguibili, gli LLM si affidano a proxy sintattici piuttosto che alla prova di come i dati controllati dall'attaccante si propaghino verso operazioni sensibili alla memoria, portando a ragionamenti fragili e alti tassi di falsi positivi.

I framework agentici esistenti progettati per il codice sorgente (che fanno affidamento sulla sintesi o sull'espansione del grafo delle chiamate) non risolvono il problema del recupero semantico posto dai binari privi di simboli, dove la struttura semantica richiesta è parzialmente assente per costruzione.

Metodologia

Veritas è un framework agentico ibrido e semanticamente fondato progettato per vincolare il ragionamento degli LLM a semantica del programma verificabile e comportamento eseguibile. Organizza l'analisi in tre fasi allineate a due livelli di fondamento: Fondamento Statico (fatti del programma recuperati) e Fondamento Runtime (prove di esecuzione concreta).

1. Tagliatore di Contesto Guidato dalla Semantica (Fondamento Statico)

Il Tagliatore opera senza LLM per estrarre flussi sorgente-sink compatti e supportati da prove dall'IR LLVM sollevato.

• Grafo di Propagazione Interprocedurale: Solleva il binario in IR LLVM utilizzando RetDec e costruisce un grafo di propagazione interprocedurale tipizzato ($G_P$) che codifica dipendenze di chiamata, ritorno e globali. Questo grafo traccia come i valori rilevanti per la contaminazione (puntatori, offset, lunghezze) si propagano attraverso le funzioni.
• Estrazione di Flussi Basata su Prove: Invece di trattare tutte le coppie sorgente-sink raggiungibili come significative, il Tagliatore verifica testimoni interprocedurali limitati. Traccia i token contaminati dalle fonti di input (ad esempio fread) fino agli sink a rischio di memoria (ad esempio argomenti di API pericolose), validando la propagazione a ogni confine di funzione utilizzando catene def-use e metadati.
• Costruzione di Oggetti di Flusso: I testimoni accettati vengono convertiti in oggetti di flusso compatti contenenti funzioni ordinate, token rilevanti per la contaminazione e "indici di ancoraggio" (classi di provenienza e annotazioni degli endpoint). Questo sostituisce l'intero binario con un contesto piccolo e semanticamente completo per l'analisi a valle.

2. Rilevatore di Vulnerabilità a Doppia Vista (Ragionamento LLM Controllato)

Il Rilevatore esegue un ragionamento passo-passo sui flussi supportati da prove, utilizzando una rappresentazione di input a doppia vista per superare la perdita semantica.

• Rappresentazione a Doppia Vista: Per le funzioni sorgente e sink, l'LLM riceve sia il codice C decompilato (per il ragionamento sul flusso di controllo) sia l'IR LLVM sollevato (per disambiguare le operazioni di memoria e la semantica degli sink). Per le funzioni intermedie, utilizza principalmente il codice decompilato, guidato dagli indici di ancoraggio.
• Ragionamento Passo-Passo: L'LLM analizza il flusso una funzione alla volta, mantenendo uno stato di ragionamento accumulato (inventario di valori propagati, alias e limiti). Aggiorna questo stato in base alle assegnazioni e alle decisioni del flusso di controllo, evitando i limiti di contesto del trattamento dell'intero flusso in una sola volta.
• Memorizzazione a Trie: Per ridurre la ridondanza, il sistema memorizza gli stati di ragionamento per i prefissi di flusso condivisi, invocando l'LLM solo sul suffisso unico di un flusso.
• Controllo di Coerenza: Prima di segnalare un candidato, il Rilevatore esegue una verifica finale sensibile al percorso per garantire che il valore contaminato rimanga rilevante per la vulnerabilità e che l'accesso allo sink violi la sicurezza della memoria in condizioni fattibili.

3. Validatore Automatico delle Vulnerabilità (Fondamento Runtime)

Il Validatore traduce le ipotesi del rilevatore in controlli eseguibili per confermare o smentire i candidati.

• Preparazione degli Artefatti: Mappa le ipotesi del rilevatore su coordinate eseguibili (RVAs, simboli) utilizzando Radare2, colmando il divario tra le visualizzazioni del decompilatore e il debug runtime.
• Collaborazione Multi-Agente: Tre agenti orchestrano la validazione:
  • Stratega: Pianifica la validazione, selezionando obiettivi di strumentazione, punti di interruzione e modalità di attivazione (file, rete, CLI).
  • Verificatore: Esegue il piano, generando Proof-of-Concept (PoC) ed eseguendo il binario sotto debugger (Radare2) o controllori di memoria (Valgrind) per osservare crash o accessi non validi.
  • Esploratore: Se le prove iniziali sono insufficienti, sonda stati alternativi o funzioni correlate per trovare prove di supporto.
• Conferma: Una vulnerabilità è confermata solo quando prove concrete di runtime (ad esempio, un segmentation fault, un errore Valgrind o uno stato di memoria specifico) corroborano lo sink segnalato, il pattern di accesso e la causa radice.

Contributi Chiave

1. Framework Veritas: Un framework agentico semanticamente fondato che unifica l'analisi statica del programma e la validazione runtime per rilevare la corruzione della memoria nei binari privi di simboli.
2. Architettura a Tre Fasi:
   • Un Tagliatore che estrae flussi supportati da prove dall'IR sollevato senza LLM.
   • Un Rilevatore a Doppia Vista che ragiona sui flussi utilizzando supporto IR selettivo per risolvere l'ambiguità semantica.
   • Un Validatore che conferma le ipotesi utilizzando artefatti visibili al debugger ed esecuzione concreta.
3. Benchmark Granulare: Un dataset curato di 20 casi reali di corruzione della memoria in binari con verità fondamentale a livello di traccia, costruito per valutare il rilevamento di binari fondati.
4. Prestazioni: La valutazione mostra che Veritas raggiunge un recall del 90% sul benchmark, superando significativamente gli analizzatori statici (0% recall), il fuzzing (10% recall) e le baseline agentiche (25–35% recall). Ha prodotto zero falsi positivi in una validazione esaustiva di 623 candidati e solo 2 falsi positivi in un audit campionario più ampio.
5. Scoperta nel Mondo Reale: Veritas ha scoperto una lettura fuori dai limiti zero-day precedentemente sconosciuta nella libreria Universal Scene Description di Apple (libusd_ms.dylib), che è stata confermata e assegnata un CVE.

Risultati e Significato

Il documento sostiene che l'efficacia della scoperta di vulnerabilità basata su LLM non dipende solo dalla capacità intrinseca del modello, ma dalla capacità dell'infrastruttura circostante di recuperare la struttura semantica necessaria per il ragionamento.

• Fondamento Semantico come Principio di Progettazione: I risultati supportano il fondamento semantico come principio di progettazione operativo. Vincolando il ragionamento degli LLM a fatti espliciti rilevanti per la memoria (fondamento statico) e validando le conclusioni contro il comportamento eseguibile (fondamento runtime), Veritas evita la fragilità della speculazione del modello non vincolata.
• Superiorità rispetto alle Baseline: Gli strumenti tradizionali falliscono a causa della mancanza di fondamento semantico attraverso le funzioni. Le baseline agentiche falliscono perché mancano di modelli espliciti dei cicli di vita degli oggetti di memoria e si affidano a esplorazioni non guidate o pattern sintattici. Veritas colma questo divario utilizzando analisi deterministiche per pre-calcolare la propagazione e LLM per interpretare semantica complessa, seguiti da una rigorosa conferma runtime.
• Compromesso Costo-Precisione: Sebbene la validazione runtime sia il principale collo di bottiglia dei costi (richiedendo la generazione di PoC e il debug), il framework dimostra che un'alta precisione nell'analisi di binari privi di simboli è raggiungibile solo attraverso prove eseguibili. Il sistema dà priorità all'affidabilità del rilevamento rispetto alla produttività, un compromesso necessario per l'analisi di binari critici per la sicurezza.

Il documento conclude che per il rilevamento pratico di vulnerabilità nei binari, il ragionamento deve essere ancorato sia alla semantica del programma recuperata sia alle prove eseguibili, un principio che Veritas implementa attraverso la sua architettura modulare e ibrida.