Riepilogo Tecnico: Potenziamento dell'Esecuzione Simbolica per l'Analisi della Fattibilità dei Percorsi di Controllo Interprocedurale

Definizione del Probleamento

L'analisi statica è una tecnica scalabile per la sicurezza e l'affidabilità del software, tuttavia soffre frequentemente di alti tassi di falsi positivi. Questi falsi positivi derivano spesso dal fatto che gli analizzatori statici riportano percorsi di flusso di controllo in un Grafo di Flusso di Controllo Interprocedurale (ICFG) che sono teoricamente possibili ma in realtà irrealizzabili a runtime a causa di vincoli semantici (ad esempio, valori contraddittori delle variabili). Determinare se un percorso specifico in un ICFG di un programma sia eseguibile è noto come analisi della fattibilità del percorso.

Sebbene l'esecuzione simbolica sia una tecnica potente per verificare la fattibilità dei percorsi esplorando i percorsi utilizzando valori simbolici e solver SMT, essa affronta due sfide primarie quando applicata a questo problema specifico:

1. Domanda di Risorse e Esplosione dei Percorsi: L'esecuzione simbolica standard tenta di esplorare tutti i percorsi raggiungibili, portando a una crescita esponenziale degli stati, in particolare in presenza di cicli e ramificazioni complesse.
2. Lacune di Automazione: I motori esistenti richiedono spesso configurazioni manuali per gestire variabili con valori sconosciuti (ad esempio, memoria non inizializzata, ritorni di funzioni esterne o argomenti di puntatori), il che ostacola l'integrazione completamente automatizzata con gli strumenti di analisi statica.

Metodologia

Gli autori propongono un metodo di esecuzione simbolica diretta progettato specificamente per verificare la fattibilità di un insieme predefinito di percorsi ICFG. A differenza dell'esecuzione simbolica tradizionale che esplora l'intero spazio degli stati, questo approccio dirige l'esecuzione strettamente verso un percorso target, eliminando l'esplorazione di rami non correlati.

La metodologia si basa su quattro componenti tecniche fondamentali:

1. Esecuzione Diretta e Pruning (Potatura)

L'algoritmo prende in input un insieme di blocchi di base consentiti ($S_{allowed}$) e un insieme di milestone richieste ($S_{req}$). Durante l'esecuzione:

• Pruning: In ogni punto di ramificazione, qualsiasi blocco di base successore che non appartenga a $S_{allowed}$ viene potato, impedendo al motore di esplorare regioni di codice irrilevanti.
• Verifica: Un percorso è considerato fattibile solo se l'esecuzione raggiunge il blocco target ($B_{target}$) avendo visitato tutti i blocchi in $S_{req}$ e rimanendo all'interno di $S_{allowed}$.

2. Strategie di Simbolizzazione Automatica

Per abilitare un'analisi completamente automatica senza intervento dell'utente, gli autori introducono strategie per simbolizzare valori che sono tipicamente sconosciuti o concreti nell'esecuzione standard:

• Parametri del Punto di Ingresso: Tutti i parametri della funzione in cui inizia l'analisi del percorso sono simbolizzati.
• Variabili e Memoria Non Inizializzate: Le variabili locali non inizializzate e la memoria allocata dinamicamente (ad esempio, tramite malloc) sono trattate come oggetti simbolici con valori non vincolati, anziché causare comportamenti indefiniti o inizializzazioni concrete.
• Funzioni Esterne:
  • Valori di Ritorno: I valori di ritorno dalle funzioni esterne (i cui corpi non sono disponibili) sono simbolizzati.
  • Argomenti di Puntatore: Le locazioni di memoria riferite da argomenti di puntatori non costanti di chiamate esterne vengono riesimbolizzate per tenere conto degli effetti collaterali.
  • Globali Speciali: Viene applicata una gestione specifica per errno (reso simbolico dopo le chiamate esterne) e environ (modellato come un insieme fisso di variabili simboliche con lunghezze fisse per prevenire la non-terminazione durante i confronti di stringhe).
• Puntatori a Funzione e Funzioni Virtuali: Il sistema risolve i potenziali target per i puntatori a funzione e le chiamate virtuali analizzando le tabelle virtuali e le firme delle funzioni, creando fork degli stati simbolici per tutti i candidati validi.

3. Modello di Memoria Flessibile

Il documento introduce un modello di memoria che supporta puntatori simbolici senza fare affidamento su allocazioni di array a dimensione fissa.

• Allocazione Pigra (Lazy Allocation): Gli oggetti di memoria non vengono creati finché il puntatore simbolico non viene dereferenziato.
• Gestione dell'Aliasing: Quando un puntatore simbolico viene dereferenziato, il motore considera gli scenari di aliasing. Esso crea un fork dello stato simbolico per esplorare i casi in cui il puntatore riferisce un oggetto di memoria esistente (con offset corrispondenti o differenti) rispetto a una locazione di memoria completamente nuova. Ciò consente l'analisi di strutture dati complesse come liste collegate e alberi senza predefinire la loro dimensione.

4. Strategia di Bounding dei Cicli

Per mitigare l'esplosione dei percorsi nei cicli, il metodo impiega una strategia di bounding dei cicli:

• Viene definito un numero massimo di iterazioni ($C_{max}$).
• Se uno stato simbolico entra in un ciclo più di $C_{max}$ volte, il motore forza lo stato a uscire dal ciclo attraverso gli archi di uscita disponibili.
• Fondamentalmente, le locazioni di memoria scritte durante l'esecuzione del ciclo vengono simbolizzate prima dell'uscita forzata. Ciò assicura che il motore possa ancora esplorare i percorsi che dipendono dagli effetti collaterali del ciclo, anche se l'esatto numero di iterazioni è troncato. Questo introduce un compromesso tra completezza e scalabilità, dando priorità alla raggiungibilità della locazione del difetto target.

Contributi Chiave

Il documento dichiara i seguenti contributi:

1. Un algoritmo di esecuzione simbolica diretta per determinare la fattibilità di qualsiasi percorso ICFG in un set specificato.
2. Strategie di simbolizzazione completamente automatiche per variabili con valori sconosciuti, ritorni di funzioni esterne e argomenti di puntatori.
3. Un modello di memoria che supporta il ragionamento sui puntatori simbolici e l'aliasing senza vincoli di dimensione fissa.
4. Un algoritmo di bounding dei cicli che limita le iterazioni senza terminare l'esecuzione simbolica del percorso.
5. Una valutazione empirica su software reali e sul Juliet test suite.

Risultati Sperimentali

Il metodo è stato implementato come estensione del motore di esecuzione simbolica KLEE (v3.1) ed è stato valutato utilizzando i seguenti dataset:

1. Verifica dei Percorsi nel Mondo Reale (GNU Coreutils)

• Dataset: 234 percorsi ICFG unici estratti da GNU Coreutils, che variano da 22 a 1.218 blocchi di base.
• Risultato: Lo strumento ha raggiunto un richiamo (recall) del 95,3%, verificando con successo 223 percorsi su 234.
• Osservazione: 49 percorsi hanno richiesto la strategia di bounding dei cicli. Lo studio ha notato che una strategia di ricerca in ampiezza (BFS) è stata occasionalmente necessaria per trovare gli stati target in scenari di cicli complessi dove la ricerca in profondità (DFS) non riusciva a raggiungere lo stato entro i limiti di tempo.

2. Integrazione con l'Analizzatore Statico MLH

• Configurazione: Il metodo è stato integrato nello strumento di analisi statica MLH ed è stato testato sul Juliet Test Suite (CWE-401: Memory Leak).
• Risultato: L'integrazione ha aumentato la precisione dello strumento dal 56% al 100% mantenendo un richiamo del 100%. Il metodo ha eliminato con successo tutti i falsi positivi senza scartare alcun vero positivo.

3. Confronto con KLEEF

• Configurazione: Il metodo proposto è stato confrontato con KLEEF (un derivato specializzato di KLEE) utilizzando i report di Infer e Clang Static Analyzer (CSA) sul Juliet Test Suite (CWE-415 e CWE-416).
• Risultato:
  • Infer: KLEEF ha ridotto l'F1-score da 1.0 a 0.0 (andando in crash su 60 report e classificando tutti i veri positivi come infattibili). Il metodo proposto ha mantenuto l'F1-score a 1.0.
  • CSA: KLEEF ha ridotto l'F1-score da 0.766 a 0.058. Il metodo proposto ha mantenuto l'F1-score a 0.767 (migliorando leggermente la precisione filtrando alcuni falsi positivi pur mantenendo il richiamo al 100%).
• Analisi: Gli autori attribuiscono il fallimento di KLEEF alla sua incapacità di gestire specifiche chiamate a funzioni esterne e l'aritmetica dei puntatori simbolici, portando a una terminazione anticipata.

Significato e Dichiarazioni

Il documento posiziona questo lavoro come una soluzione pratica per colmare il divario tra la scalabilità dell'analisi statica e la precisione dell'esecuzione simbolica. Gli autori affermano che, dirigendo l'esecuzione simbolica e automatizzando la simbolizzazione, il metodo filtra efficacemente i percorsi infattibili riportati dagli analizzatori statici.

La significatività risiede nella capacità di:

• Automatizzare il processo di verifica senza la configurazione manuale delle variabili simboliche.
• Gestire modelli di memoria complessi (puntatori, allocazione dinamica) che spesso causano il fallimento di altri strumenti o richiedono approssimazioni di dimensione fissa.
• Migliorare le metriche dell'analisi statica: Nello specifico, il metodo dimostra la capacità di eliminare i falsi positivi (aumentando la precisione) senza sacrificare il rilevamento di vulnerabilità reali (preservando il richiamo).

Gli autori riconoscono un compromesso tra completezza e scalabilità dovuto alla strategia di bounding dei cicli, ma sostengono che, per l'obiettivo specifico di validare i report dell'analisi statica, dare priorità alla raggiungibilità della locazione del target sia un compromesso accettabile. Il lavoro futuro proposto consiste nel parallelizzare l'analisi e sviluppare strategie specializzate di selezione dello stato per migliorare ulteriormente l'efficienza.