Riepilogo Tecnico: Heimdall

Enunciato del Problema

I programmi Extended Berkeley Packet Filter (eBPF) sono fondamentali per le estensioni del kernel Linux nel networking, nell'osservabilità e nella sicurezza. Sebbene il verificatore eBPF integrato nel kernel imponga la sicurezza della memoria a basso livello e la terminazione, non riesce a imporre proprietà di livello superiore a livello di sorgente, come la disciplina di inizializzazione, la coerenza dello schema e la gestione degli errori. Gli autori documentano sei classi di bug a livello di sorgente che vengono compilati e superano il verificatore del kernel, ma possono corrompere silenziosamente i dati, perdere informazioni sensibili o produrre risultati di applicazione delle regole errati.

Le vulnerabilità chiave identificate includono:

• Stato non inizializzato: Programmi che emettono strutture residenti nello stack senza inizializzazione a zero perdono residui dello stack per CPU, inclusi puntatori al kernel e indirizzi di ritorno sufficienti a recuperare gli offset di randomizzazione dello spazio degli indirizzi del kernel (KASLR).
• Valori di ritorno delle helper non controllati: Le funzioni helper (ad esempio bpf_probe_read_user_str) che falliscono vengono spesso ignorate, causando l'emissione di dati dello stack obsoleti invece di stringhe troncate.
• Disallineamenti Buffer/Dimensione: Gli sviluppatori che passano dimensioni errate alle helper di output possono perdere campi privati adiacenti contenenti puntatori al kernel.
• Disallineamenti Hook/Contesto: L'uso di strutture di contesto errate (ad esempio __sk_buff in un hook XDP) porta a dati interpretati erroneamente.
• Confusione Tipo/Schema Mappa: Disallineamenti tra le dimensioni dei valori delle mappe dichiarate e i dati effettivi, o la reinterpretazione dei risultati della ricerca nella mappa come tipi non correlati.
• Confusione Segnato/Non Segnato: L'archiviazione di valori di ritorno di helper con segno (che indicano errori) in campi senza segno crea grandi valori positivi spurii utilizzati come chiavi di mappa.

Inoltre, lo stesso verificatore eBPF presenta vulnerabilità note (ad esempio, potatura non fondata, mancata convalida dei contratti) che possono essere sfruttate. La migrazione a un linguaggio sicuro per la memoria come Rust potrebbe colmare queste lacune, ma la riscrittura manuale è impraticabile su larga scala e gli strumenti esistenti di traduzione automatizzata mancano del rigore necessario per garantire l'equivalenza semantica o la sicurezza nel contesto eBPF.

Metodologia: La Pipeline Heimdall

Heimdall è una pipeline automatizzata che traduce programmi C libbpf legacy in Rust idiomatico e sicuro Aya. Impiega un processo iterativo a cinque stadi che combina Modelli Linguistici su Grande Scala (LLM), analisi statica e verifica formale:

1. Traduzione LLM: Un LLM traduce il sorgente C in Rust utilizzando mappature API Aya, macro hook ed esempi funzionanti.
2. Compilazione e Verifica Kernel: Il codice Rust generato viene compilato in bytecode eBPF. I controlli di lint del compilatore (ad esempio, il rifiuto di blocchi unsafe non utilizzati) e il verificatore del kernel controllano la sicurezza e la correttezza di base. Gli errori vengono inviati all'LLM per la riparazione.
3. Controllo di Sicurezza (Analisi Statica): Un motore di analisi statica personalizzato scansiona il sorgente Rust alla ricerca di vie di fuga unsafe che il compilatore e il verificatore potrebbero non rilevare. Ciò include il divieto di prenotazioni di ring buffer non tipizzate, l'imposizione dell'inizializzazione a zero e l'esigenza di una gestione esplicita dei tipi Result per i valori di ritorno delle helper.
4. Esecuzione Simbolica: Sia il binario C originale che il binario Rust compilato vengono caricati in un backend eBPF personalizzato per angr. Questo backend modella le helper eBPF, le mappe, le rilocazioni e le operazioni atomiche. Esegue l'esecuzione simbolica per esplorare tutti i percorsi fattibili, generando formule strutturate per i valori di ritorno e gli effetti collaterali delle mappe.
5. Controllo di Equivalenza: Un solver basato su Z3 verifica se i programmi C e Rust sono semanticamente equivalenti. Gli autori introducono l'Equivalenza Semantica Condizionale, che richiede equivalenza solo sugli input che soddisfano le condizioni di sicurezza dichiarate (ad esempio, il successo delle chiamate helper). Ciò consente alla traduzione Rust più sicura (che gestisce gli errori o riempie di zero la memoria) di essere considerata equivalente alla sorgente C errata sui percorsi in cui viene attivato il bug, verificando comunque che la logica sia preservata sui percorsi validi. Se viene trovato un controesempio, viene inviato all'LLM per una riparazione mirata.

Per supportare ciò, gli autori hanno costruito un backend eBPF completo per angr, inclusi un loader ELF, una definizione di architettura, un lifter IR VEX e stub per le helper. Hanno inoltre sviluppato una codifica ITE-chain personalizzata per modellare gli effetti collaterali delle mappe sotto chiavi simboliche, catturando la semantica "last-write-wins".

Contributi Chiave

• Pipeline Heimdall: Il primo sistema automatizzato per tradurre programmi eBPF di produzione da C a Rust con garanzie formali per programma della preservazione del comportamento osservabile.
• Equivalenza Condizionale: Un approccio di verifica innovativo che convalida traduzioni che migliorano la sicurezza (che si comportano diversamente sui percorsi che attivano il bug) limitando i controlli di equivalenza ai percorsi di esecuzione sicuri.
• Backend di Esecuzione Simbolica eBPF: Un backend eBPF completo per angr che modella helper del kernel, mappe e chiamate BPF-to-BPF, abilitando il ragionamento formale a livello di bytecode.
• Analizzatore Statico Safe-Aya: Un motore di policy che rifiuta pattern Rust unsafe (ad esempio, ring buffer non tipizzati, errori helper ignorati) che superano il verificatore del kernel.
• Risultati di Sicurezza: Scoperta di perdite di informazioni precedentemente non segnalate in dieci programmi eBPF open-source, inclusa il recupero di KASLR tramite residui dello stack e perdite di contenuto tra eventi diversi nei ring buffer.
• Benchmark e Valutazione: Un benchmark pubblico di 102 programmi eBPF e una valutazione completa della pipeline di traduzione.

Risultati

Il sistema è stato valutato su 102 programmi eBPF reali provenienti da varie fonti (libbpf-tools, libbpf-bootstrap, KEN, Suricata, ecc.).

• Tasso di Successo: Heimdall ha prodotto 96 traduzioni formalmente verificate come equivalenti (94,1%). Le restanti sei erano parzialmente verificate (a causa dei limiti dell'esecuzione simbolica) o hanno superato i limiti di scalabilità del solver.
• Chiusura Bug: Nelle 96 traduzioni verificate, Heimdall ha chiuso il 100% delle istanze osservate di stato non inizializzato, valori di ritorno helper non controllati e confusione segnato/non segnato.
• Confronto con le Baseline: Rispetto agli agenti LLM di base senza la pipeline Heimdall, Heimdall (Agentic) ha raggiunto un tasso di triple-pass del 98% (Compilazione, Verifica Kernel, Sicurezza, Equivalenza) contro il 4-12% delle baseline.
• Sovraccarico di Runtime: La convalida del runtime su 10 programmi ha mostrato che le traduzioni Rust hanno generalmente comportato un sovraccarico modesto (media geometrica che varia da 0,44× a 3,60× rispetto a C), con la maggior parte compresa tra 1,14× e 1,89×.
• Sicurezza: Le traduzioni hanno eliminato i pattern specifici non sicuri (memoria non inizializzata, errori non controllati) che hanno causato le vulnerabilità identificate.

Significato

Il documento afferma che Heimdall è il primo sistema ad automatizzare la migrazione sicura per la memoria di programmi eBPF di produzione con garanzie formali per programma che la migrazione preservi il comportamento osservabile. Colma il divario tra le garanzie a basso livello del verificatore del kernel e i requisiti di sicurezza di alto livello delle moderne applicazioni eBPF. Combinando LLM con verifica formale e analisi statica, Heimdall dimostra che la traduzione automatizzata può produrre codice non solo sintatticamente corretto, ma anche semanticamente equivalente e privo di classi specifiche di bug di sicurezza a livello di sorgente che il verificatore del kernel non può rilevare. Il lavoro stabilisce un nuovo benchmark per la migrazione eBPF e fornisce una base per costruire estensioni del kernel più robuste e sicure per la memoria.