Buffer Overrun Detection using Linear Programming and Static Analysis

34
Analisi e Verifica di Programmi Analisi e Verifica di Programmi Alberto De Lazzari - Alberto De Lazzari - Fabio Pustetto Fabio Pustetto Buffer Overrun Buffer Overrun Detection Detection using Linear using Linear Programming Programming and Static Analysis and Static Analysis Prevedere il Buffer Overrun Prevedere il Buffer Overrun usando Programmazione Lineare usando Programmazione Lineare e Analisi Statica e Analisi Statica

description

Buffer Overrun Detection using Linear Programming and Static Analysis. Prevedere il Buffer Overrun usando Programmazione Lineare e Analisi Statica. Introduzione. Scrivere oltre i limiti di un buffer in memoria - PowerPoint PPT Presentation

Transcript of Buffer Overrun Detection using Linear Programming and Static Analysis

Page 1: Buffer Overrun Detection using Linear Programming and Static Analysis

Analisi e Verifica di Programmi Analisi e Verifica di Programmi Alberto De Lazzari - Fabio PustettoAlberto De Lazzari - Fabio Pustetto

Buffer Overrun Buffer Overrun DetectionDetection

using Linear using Linear ProgrammingProgramming

and Static Analysisand Static Analysis

Prevedere il Buffer OverrunPrevedere il Buffer Overrunusando Programmazione Lineareusando Programmazione Lineare

e Analisi Staticae Analisi Statica

Page 2: Buffer Overrun Detection using Linear Programming and Static Analysis

IntroduzioneIntroduzione

Scrivere oltre i limiti di un buffer in memoriaScrivere oltre i limiti di un buffer in memoria– C permette la manipolazione diretta dei puntatori senza alcun tipo di C permette la manipolazione diretta dei puntatori senza alcun tipo di

controllo sui limiticontrollo sui limiti– Dati validi possono essere sovrascrittiDati validi possono essere sovrascritti– Hacker sfruttano per eseguire codice malvagioHacker sfruttano per eseguire codice malvagio

Caricato in memoria come validoCaricato in memoria come valido acquisizione dei privilegi di rootacquisizione dei privilegi di root

Gli approcci per rilevare il buffer overrun possono essere di tipoGli approcci per rilevare il buffer overrun possono essere di tipo – StaticoStatico

esamina il codice sorgente per eliminare questo tipo di bug prima che il codice sia distribuitoesamina il codice sorgente per eliminare questo tipo di bug prima che il codice sia distribuito

– DinamicoDinamico previene gli “attacchi” basati sul bugpreviene gli “attacchi” basati sul bug perciò non sono eliminati come nell’analisi staticaperciò non sono eliminati come nell’analisi statica generalmente causano il crash dell’applicazione quando è rilevato un attaccogeneralmente causano il crash dell’applicazione quando è rilevato un attacco Controlli ridondanti portano ad overheadControlli ridondanti portano ad overhead

Page 3: Buffer Overrun Detection using Linear Programming and Static Analysis

Linee Guida:Linee Guida:

Uso di analisi statica per modellare stringhe di codice C Uso di analisi statica per modellare stringhe di codice C sorgente come programma linearesorgente come programma lineare

Definizione e implementazione di risolutori veloci e scalabili Definizione e implementazione di risolutori veloci e scalabili basati su tecniche innovative della programmazione lineare. basati su tecniche innovative della programmazione lineare. La soluzione al programma lineare determina i limiti del bufferLa soluzione al programma lineare determina i limiti del buffer

Tecniche per rendere l’analisi del programma sensibile al Tecniche per rendere l’analisi del programma sensibile al contestocontesto

Efficacia di altre tecniche di analisi come il partizionamento Efficacia di altre tecniche di analisi come il partizionamento statico per eliminare bug dal codice sorgentestatico per eliminare bug dal codice sorgente

La definizione e l’implementazione del tool che permette l’analisi statica del codice, si divide nei seguenti punti:

-> tool deve essere scalabile-> tool deve essere scalabile

Page 4: Buffer Overrun Detection using Linear Programming and Static Analysis

Tecniche dinamiche: Tecniche dinamiche: approfondimento approfondimento

Proteggere l’indirizzo di ritorno sullo stackProteggere l’indirizzo di ritorno sullo stack– controllo d’integrità sui record evitando la modifica controllo d’integrità sui record evitando la modifica

dell’indirizzo di ritornodell’indirizzo di ritorno– si può rilevare e prevenire un attacco di tipo stack smashingsi può rilevare e prevenire un attacco di tipo stack smashing

Corrompere lo stack scrivendo oltre la sua fine, permettendo di Corrompere lo stack scrivendo oltre la sua fine, permettendo di cambiare l’indirizzo di ritorno di una funzionecambiare l’indirizzo di ritorno di una funzione

– Altre tecniche generalizzano il concetto precedente estendendolo a Altre tecniche generalizzano il concetto precedente estendendolo a puntatori, variabili locali e argomenti di funzionipuntatori, variabili locali e argomenti di funzioni

Proteggere tutti gli accessi ai puntatoriProteggere tutti gli accessi ai puntatori– cifrandoli quando sono memorizzaticifrandoli quando sono memorizzati– decifrandoli quando sono caricati nei registri della CPUdecifrandoli quando sono caricati nei registri della CPU– non evita la possibilità di distruggere il puntatorenon evita la possibilità di distruggere il puntatore– impedisce di ottenere un valore di puntatore prevedibile in memoriaimpedisce di ottenere un valore di puntatore prevedibile in memoria

non si conosce la chiave di decifraturanon si conosce la chiave di decifratura

Page 5: Buffer Overrun Detection using Linear Programming and Static Analysis

Tecniche statiche: Tecniche statiche: approfondimentoapprofondimento suddivise in tre classisuddivise in tre classi

1.1. tool guidati da annotazionitool guidati da annotazioni utilizza annotazioni date dall’utenteutilizza annotazioni date dall’utente

– Es: pre/post-condizioni di una funzione Es: pre/post-condizioni di una funzione

2.2. tool che usano l’analisi simbolicatool che usano l’analisi simbolica

3.3. tool che estraggono un modello dal tool che estraggono un modello dal codice sorgente e lo utilizzano per codice sorgente e lo utilizzano per rilevare la presenza di bug rilevare la presenza di bug

Page 6: Buffer Overrun Detection using Linear Programming and Static Analysis

1.1. tool guidati da tool guidati da annotazioniannotazioni

CSSV converte un programma in C in un CSSV converte un programma in C in un programma intero, con asserzioni di programma intero, con asserzioni di correttezza incluse e usa un algoritmo di correttezza incluse e usa un algoritmo di analisi statica conservativa per trovare analisi statica conservativa per trovare manipolazioni erronee sugli interi che manipolazioni erronee sugli interi che direttamente si traducono in bug sul codice C.direttamente si traducono in bug sul codice C.

L’analisi è fatta sulla base di annotazioni L’analisi è fatta sulla base di annotazioni (chiamate contract) che sono usate per (chiamate contract) che sono usate per rendere l’analisi interproceduralerendere l’analisi interprocedurale

Split è simile a CSSV anche se usa un’analisi Split è simile a CSSV anche se usa un’analisi flow-sensitive e pre/post-condizioni fornite flow-sensitive e pre/post-condizioni fornite dall’utente. dall’utente.

Page 7: Buffer Overrun Detection using Linear Programming and Static Analysis

2.2. tool che usano tool che usano l’analisi simbolical’analisi simbolica

Alcuni tool (Alcuni tool (Archer, ARray CHeckERArcher, ARray CHeckER) eseguono il ) eseguono il codice in manieracodice in maniera– SimbolicaSimbolica

permette di analizzare il codice senza conoscere l’esatto permette di analizzare il codice senza conoscere l’esatto valore delle variabili che si stanno manipolandovalore delle variabili che si stanno manipolando

– InterproceduraleInterprocedurale permette di trattare una stessa variabile che si trova in permette di trattare una stessa variabile che si trova in

metodi diversimetodi diversi– mantenendo l’informazione riguardo alle variabili in un mantenendo l’informazione riguardo alle variabili in un

database man mano che l’esecuzione procededatabase man mano che l’esecuzione procede l’esecuzione di statement può portare alla modifica dello l’esecuzione di statement può portare alla modifica dello

stato del programmastato del programma quando in uno statement si accede ad un buffer, Archer quando in uno statement si accede ad un buffer, Archer

controlla, attraverso il database, se l’accesso avviene nel controlla, attraverso il database, se l’accesso avviene nel rispetto dei limiti del buffer rispetto dei limiti del buffer

Page 8: Buffer Overrun Detection using Linear Programming and Static Analysis

3.3. tool che estraggono un tool che estraggono un modello dal codice sorgente e modello dal codice sorgente e lo utilizzano per rilevare la lo utilizzano per rilevare la presenza di bugpresenza di bug

Si estrae un modello dal codice sorgenteSi estrae un modello dal codice sorgente Si modellano le stringhe come tipi di dato Si modellano le stringhe come tipi di dato

astratto e si trasforma il rilevamento del astratto e si trasforma il rilevamento del buffer overrun in un problema di analisi sul buffer overrun in un problema di analisi sul range di valori interirange di valori interi

Il tool presentato in questo paper rientra in Il tool presentato in questo paper rientra in questa classe di tecniche introducendo questa classe di tecniche introducendo un’analisi dei puntatori più precisa un’analisi dei puntatori più precisa

Page 9: Buffer Overrun Detection using Linear Programming and Static Analysis

Architettura Architettura complessiva complessiva plug-in per CodeSurferplug-in per CodeSurfer

– tool utilizzato per la comprensione del codicetool utilizzato per la comprensione del codice– costruisce una rappresentazione totale del programma costruisce una rappresentazione totale del programma

attraversoattraverso grafo delle dipendenze di sistema composto dai grafi di grafo delle dipendenze di sistema composto dai grafi di

dipendenza di ciascuna proceduradipendenza di ciascuna procedura grafo del controllo del flusso interproceduralegrafo del controllo del flusso interprocedurale alberi di sintassi astratta per le espressioni del programmaalberi di sintassi astratta per le espressioni del programma informazioni sui puntatoriinformazioni sui puntatori

SlicingSlicing– partizionamento di un programmapartizionamento di un programma – Tecnica per visualizzare le dipendenzeTecnica per visualizzare le dipendenze– restringe l’attenzione alle componenti di un programma restringe l’attenzione alle componenti di un programma

rilevanti per la valutazione di espressionirilevanti per la valutazione di espressioni– backward slicing / forward slicingbackward slicing / forward slicing

Page 10: Buffer Overrun Detection using Linear Programming and Static Analysis

Generazione dei Generazione dei vincoli …vincoli …

buf: puntatore a buffer modellato da 4 variabili di vincolo:buf: puntatore a buffer modellato da 4 variabili di vincolo:– buf!alloc!maxbuf!alloc!max– buf!alloc!minbuf!alloc!min

numero massimo e minimo di byte allocati per il buffer numero massimo e minimo di byte allocati per il buffer bufbuf– buf!used!maxbuf!used!max – buf!used!minbuf!used!min

numero massimo e minimo di byte usati da numero massimo e minimo di byte usati da bufbuf

i: variabile intera, modellata da 2 variabili di vincoloi: variabile intera, modellata da 2 variabili di vincolo– i!maxi!max

indica il massimo valore di indica il massimo valore di ii – i!mini!min

denota il minimo valore di denota il minimo valore di ii

I vincoli modellano il programma in manieraI vincoli modellano il programma in maniera– non sensibile al flussonon sensibile al flusso

ignora l’ordine degli statementignora l’ordine degli statement– non sensibile al contestonon sensibile al contesto

non fa differenze per molteplici punti di chiamata, alla stessa non fa differenze per molteplici punti di chiamata, alla stessa funzionefunzione

Page 11: Buffer Overrun Detection using Linear Programming and Static Analysis

…… 4 statement generano 4 statement generano

vincolivincoli– dichiarazioni di bufferdichiarazioni di buffer– assegnamentiassegnamenti– chiamate a funzionechiamate a funzione– statement di ritornostatement di ritorno

Es: alla riga 17 del Es: alla riga 17 del codicecodice– strcpy(copy,buffer)strcpy(copy,buffer)

Risultano i vincoli Risultano i vincoli ((associati ai puntatori dei associati ai puntatori dei bufferbuffer):):

copy!used!max ≥ copy!used!max ≥ buffer!used!maxbuffer!used!max

copy!used!min ≤ copy!used!min ≤ buffer!used!minbuffer!used!min

Page 12: Buffer Overrun Detection using Linear Programming and Static Analysis

… … alcuni chiarimenti alcuni chiarimenti Poiché è ignorata l’analisi di flusso, i predicati come Poiché è ignorata l’analisi di flusso, i predicati come counter counter

< 10< 10 sono ignorati sono ignorati Se generiamo un vincolo del tipo Se generiamo un vincolo del tipo counter!max ≥ counter!counter!max ≥ counter!

max + 1max + 1 (generato da (generato da counter++counter++), questo non può essere ), questo non può essere interpretato da un risolutore di programmi lineariinterpretato da un risolutore di programmi lineari– dunque questo statement è modellato trattandolo come due dunque questo statement è modellato trattandolo come due

statement: statement: counter’ = counter + 1counter’ = counter + 1 e e counter = counter’counter = counter’. I due . I due vincoli catturano il fatto che il puntatore è incrementato di uno vincoli catturano il fatto che il puntatore è incrementato di uno e sono accettabili dal risolutore, anche se il programma lineare e sono accettabili dal risolutore, anche se il programma lineare risultante sarà non ammissibilerisultante sarà non ammissibile

Una variabile di programma che ottiene il suo valore Una variabile di programma che ottiene il suo valore dall’ambiente o dall’input dell’utente in un modo non dall’ambiente o dall’input dell’utente in un modo non controllato, è considerata insicuracontrollato, è considerata insicura– Se consideriamo, ad esempio, lo statement Se consideriamo, ad esempio, lo statement getenv(“PATH”)getenv(“PATH”), ,

che ritorna il percorso di ricerca, può ritornare una stringa che ritorna il percorso di ricerca, può ritornare una stringa arbitrariamente lunga. Per riflettere il fatto che la stringa può arbitrariamente lunga. Per riflettere il fatto che la stringa può essere arbitrariamente lunga, sono generati dei vincoli del tipo essere arbitrariamente lunga, sono generati dei vincoli del tipo getenv$return!used!max ≥ +∞getenv$return!used!max ≥ +∞ e e getenv$return!used!min ≤ 0getenv$return!used!min ≤ 0. . Allo stesso modo, una variabile intera Allo stesso modo, una variabile intera ii inserita dall’utente inserita dall’utente genera i vincoli: genera i vincoli: i!max ≥ +∞i!max ≥ +∞ e e i!min ≤ -∞i!min ≤ -∞

Page 13: Buffer Overrun Detection using Linear Programming and Static Analysis

Analisi di alterazione Analisi di alterazione

Vincoli generati, passati al modulo di Vincoli generati, passati al modulo di analisi di analisi di alterazionealterazione– Scopo: ottenere dei vincoli che siano successivamente Scopo: ottenere dei vincoli che siano successivamente

utilizzabili dal risolutore utilizzabili dal risolutore – Solo valori finitiSolo valori finiti

2 passi2 passi– Identificare e rimuovere variabili che danno valore infinito Identificare e rimuovere variabili che danno valore infinito – Identifica e rimuove variabili di vincolo non inizializzataIdentifica e rimuove variabili di vincolo non inizializzata

il sistema di vincoli è esaminato per vedere seil sistema di vincoli è esaminato per vedere se– vincoli di tipo vincoli di tipo maxmax hanno un estremo inferiore finito hanno un estremo inferiore finito– vincoli di tipo vincoli di tipo minmin hanno un estremo superiore finito hanno un estremo superiore finito

Requisito non soddisfatto seRequisito non soddisfatto se– non sono state inizializzate nel codice sorgentenon sono state inizializzate nel codice sorgente– gli statement che influiscono sulle variabili di programma non sono gli statement che influiscono sulle variabili di programma non sono

state catturate dal generatore di vincolistate catturate dal generatore di vincoli => non esiste modello per funzioni di librerie=> non esiste modello per funzioni di librerie

Page 14: Buffer Overrun Detection using Linear Programming and Static Analysis

Risoluzione dei Risoluzione dei vincoli…vincoli… si utilizza la programmazione linearesi utilizza la programmazione lineare

– modella e manipola nuovi tipi di vincolimodella e manipola nuovi tipi di vincoli– garantisce correttezza dei risultatigarantisce correttezza dei risultati

Un programma lineare e' un problema di Un programma lineare e' un problema di ottimizzazione:ottimizzazione:

minimizza cminimizza cTTxxriferito a Ax ≥ briferito a Ax ≥ b

– A matrice A matrice m x nm x n di costanti di costanti– bb e e cc vettori di costanti vettori di costanti– xx è vettore di variabili è vettore di variabili

sistema di sistema di mm disequazioni in disequazioni in nn variabili, necessarie variabili, necessarie per trovare i valori delle variabili che soddisfano i per trovare i valori delle variabili che soddisfano i vincoli e minimizzano la vincoli e minimizzano la funzione obiettivo cfunzione obiettivo cTTxx, nel , nel campo dei numeri reali finiti.campo dei numeri reali finiti.

Page 15: Buffer Overrun Detection using Linear Programming and Static Analysis

……

Insieme di vincoli ottenuti dopo l'analisi è insieme Insieme di vincoli ottenuti dopo l'analisi è insieme di vincoli linearidi vincoli lineari– si può allora formulare come problema di si può allora formulare come problema di

programmazione lineareprogrammazione lineare– Obiettivo: ottenere i valoriObiettivo: ottenere i valori

buf!alloc!maxbuf!alloc!max buf!alloc!minbuf!alloc!min buf!used!maxbuf!used!max buf!used!minbuf!used!min

– che rendono la differenza tra byte allocati e byte usati dal che rendono la differenza tra byte allocati e byte usati dal puntatore al buffer puntatore al buffer bufbuf più piccola possibile, rispettando i vincoli più piccola possibile, rispettando i vincoli

– se tutte le variabili se tutte le variabili maxmax hanno minimo finito e hanno minimo finito e tutte le variabili tutte le variabili minmin hanno massimo finito, vale hanno massimo finito, vale che:che:

min min ΣΣbufbuf (buf!alloc!max - buf!alloc!min + buf!used!max - buf!used! (buf!alloc!max - buf!alloc!min + buf!used!max - buf!used!min)min)

Page 16: Buffer Overrun Detection using Linear Programming and Static Analysis

……

Trovare soluzioni intere è Programmazione Trovare soluzioni intere è Programmazione Lineare Intera: problema NP-completo ben Lineare Intera: problema NP-completo ben conosciutoconosciuto– NP = è noto un algoritmo che termina in tempo polinomiale rispetto alla NP = è noto un algoritmo che termina in tempo polinomiale rispetto alla

dimensione dei dati dimensione dei dati – NP-hard = un algoritmo per risolvere uno di questi problemi può essere NP-hard = un algoritmo per risolvere uno di questi problemi può essere

convertito in un algoritmo per risolvere un qualunque problema NPconvertito in un algoritmo per risolvere un qualunque problema NP– NP-completi = sia NP che NP-hardNP-completi = sia NP che NP-hard

programma lineare programma lineare ammissibileammissibile– si trovano valori finiti per tutte le variabili si trovano valori finiti per tutte le variabili

(rispettando i vincoli)(rispettando i vincoli) soluzione soluzione ammissibile è ottimaammissibile è ottima

– se massimizza (o minimizza) il valore della se massimizza (o minimizza) il valore della funzionefunzione

programma lineare programma lineare inammissibileinammissibile– se non ha soluzioni ammissibili se non ha soluzioni ammissibili

Page 17: Buffer Overrun Detection using Linear Programming and Static Analysis

……

soluzione ottima per determinare i limiti del buffersoluzione ottima per determinare i limiti del buffer nessun programma può essere illimitatonessun programma può essere illimitato

– vincoli esaminati dall'analizzatore di alterazionevincoli esaminati dall'analizzatore di alterazione tutte le variabili tutte le variabili max max della funzione obiettivo hanno limite inferiore della funzione obiettivo hanno limite inferiore

finitofinito Minimizzando le variabili Minimizzando le variabili maxmax otterremo ancora valori finiti otterremo ancora valori finiti Similmente per Similmente per minmin

se programma lineare non ha soluzioni ammissibilise programma lineare non ha soluzioni ammissibili– non si può assegnare arbitrariamente dei valori finiti alle non si può assegnare arbitrariamente dei valori finiti alle

variabili per ottenere soluzioni ammissibilivariabili per ottenere soluzioni ammissibili– Es: settare tutte le variabili di max a +∞ e quelle di min a -∞ Es: settare tutte le variabili di max a +∞ e quelle di min a -∞

=> ci sarebbero troppi falsi allarmi!=> ci sarebbero troppi falsi allarmi!

approccio in cui si rimuovere un piccolo insieme di vincoli approccio in cui si rimuovere un piccolo insieme di vincoli per rendere il sistema ammissibileper rendere il sistema ammissibile– noto come noto come Irreducibly Inconsistent SetIrreducibly Inconsistent Set ( (IISIIS))

insieme minimale di vincoli: l'intero insieme dei vincoli di un IIS è insieme minimale di vincoli: l'intero insieme dei vincoli di un IIS è inammissibile ma ogni sottoinsieme è ammissibile inammissibile ma ogni sottoinsieme è ammissibile

Page 18: Buffer Overrun Detection using Linear Programming and Static Analysis

Elastic Filtering Elastic Filtering algorithmalgorithm

Dato un insieme di vincoli determina un IIS (se esiste) e garantisce Dato un insieme di vincoli determina un IIS (se esiste) e garantisce che nel caso ce ne siano più di uno almeno uno venga rilevatoche nel caso ce ne siano più di uno almeno uno venga rilevato

si può iterare l'algoritmo più volte sul risultato dell'iterazione si può iterare l'algoritmo più volte sul risultato dell'iterazione precedente per creare il più piccolo programma lineare precedente per creare il più piccolo programma lineare ammissibile da uno non ammissibile ammissibile da uno non ammissibile

1.1. esamina l'insieme dei vincoli C per esamina l'insieme dei vincoli C per determinare ammissibilitàdeterminare ammissibilità

Se è ammissibile STOPSe è ammissibile STOP

Altrimenti -> 2Altrimenti -> 2

2.2. allora esiste almeno un C’ allora esiste almeno un C’ C che C che è IISè IIS

3.3. genera dopo un certo numero di genera dopo un certo numero di iterazioni, C-C’ ammissibileiterazioni, C-C’ ammissibile

4.4. settare i valori delle variabili settare i valori delle variabili maxmax e e minmin in C' rispettivamente a in C' rispettivamente a ∞∞ e e -∞-∞

5.5. ci sono variabili a ci sono variabili a ∞∞rimuovere i vincoli alterati da rimuovere i vincoli alterati da queste variabili: C’’ queste variabili: C’’ C-C‘ C-C‘

D=C-C’-C”D=C-C’-C”

Page 19: Buffer Overrun Detection using Linear Programming and Static Analysis

Risolvere i vincoli Risolvere i vincoli gerarchicamente gerarchicamente Elastic Filtering algorithmElastic Filtering algorithm veloce ma veloce ma

anche un’approssimazioneanche un’approssimazione– può rimuovere più vincoli di quelli può rimuovere più vincoli di quelli

necessari per avere una soluzione necessari per avere una soluzione ammissibile ammissibile

risolutore gerarchicorisolutore gerarchico scomporre l’insieme dei vincoli in insiemi più scomporre l’insieme dei vincoli in insiemi più

piccoli e risolverli separatamentepiccoli e risolverli separatamente– grafo diretto aciclico grafo diretto aciclico (DAG)(DAG)

ogni insieme di vincoli è associato a un vertice ogni insieme di vincoli è associato a un vertice del DAG e gli archi rappresentano le dipendenze del DAG e gli archi rappresentano le dipendenze tra essitra essi

modifica a ∞ un numero inferiore di variabili, modifica a ∞ un numero inferiore di variabili, risulta più preciso e determina dei valori precisi risulta più preciso e determina dei valori precisi

Page 20: Buffer Overrun Detection using Linear Programming and Static Analysis

Individuare overrunIndividuare overrun basata sui valori restituiti dal risolutore e dai basata sui valori restituiti dal risolutore e dai

valori dell’analisi di alterazionevalori dell’analisi di alterazione– buffer puntato da buffer puntato da header header ha 2048 byte allocati e la ha 2048 byte allocati e la

sua lunghezza può variare tra 1 e 2048 byte => sua lunghezza può variare tra 1 e 2048 byte => non si può verificare un buffer overrun => non si può verificare un buffer overrun => headerheader è segnato come “sicuro”. La stessa cosa vale per è segnato come “sicuro”. La stessa cosa vale per bufbuf..

– buffer puntato da buffer puntato da ptrptr ha un numero di byte allocati ha un numero di byte allocati [1024..2048] mentre la lunghezza può variare [1024..2048] mentre la lunghezza può variare [1..2048]. [1..2048]. ptrptr fa parte di due statement. Alla riga fa parte di due statement. Alla riga (6) (6) ptrptr punta ad un buffer lungo 2048 byte mentre punta ad un buffer lungo 2048 byte mentre alla riga (9) punta ad un buffer lungo 1024 byte. La alla riga (9) punta ad un buffer lungo 1024 byte. La non sensibilità al contesto dell’analisi significa che non sensibilità al contesto dell’analisi significa che non possiamo fare differenze tra i due punti del non possiamo fare differenze tra i due punti del programma e dunque possiamo derivare che al programma e dunque possiamo derivare che al massimo massimo ptrptr è di 2048 byte. In questo tipo di è di 2048 byte. In questo tipo di situazione in cui si verifica chesituazione in cui si verifica che

ptr!alloc!min < ptr!used!maxptr!alloc!min < ptr!used!max ≤≤ ptr!alloc!maxptr!alloc!max possiamo avere un overrun. Questo però è un falso possiamo avere un overrun. Questo però è un falso

positivo dovuto alla non sensibilità del contesto positivo dovuto alla non sensibilità del contesto dell’analisidell’analisi

– variabile variabile copy:copy: copy!alloc!max < copy!used!max e copy!alloc!max < copy!used!max e c’è un’esecuzione del programma in cui saranno c’è un’esecuzione del programma in cui saranno scritti più byte di quelli che possono essere ottenutiscritti più byte di quelli che possono essere ottenuti

Concludiamo dunque che in questa situazione si Concludiamo dunque che in questa situazione si verifica un overrunverifica un overrun

Page 21: Buffer Overrun Detection using Linear Programming and Static Analysis

Aggiungere la Aggiungere la sensibilità al contestosensibilità al contesto generazione dei vincoligenerazione dei vincoli

– non è sensibile al contestonon è sensibile al contesto– si considera ogni punto di chiamata come si considera ogni punto di chiamata come

un assegnamento delle variabili in input un assegnamento delle variabili in input reali alle variabili in input formali e il reali alle variabili in input formali e il ritorno dalla funzione come un ritorno dalla funzione come un assegnamento delle variabili in output assegnamento delle variabili in output formali alle variabili in output realiformali alle variabili in output reali

si fondono le informazioni attraverso i punti di si fondono le informazioni attraverso i punti di chiamata, ottenendo un’analisi imprecisachiamata, ottenendo un’analisi imprecisa

2 tecniche2 tecniche constraint inlining constraint inlining summary information summary information

Page 22: Buffer Overrun Detection using Linear Programming and Static Analysis

constraint inlining…constraint inlining…

Inlining nelle funzioniInlining nelle funzioni– rimpiazza una chiamata di rimpiazza una chiamata di

funzione con un’istanza del funzione con un’istanza del corpo della funzionecorpo della funzione

– gli argomenti reali sono gli argomenti reali sono sostituiti a quelli formalisostituiti a quelli formali

– eseguita a tempo di eseguita a tempo di compilazionecompilazione

– crea una nuova istanza dei crea una nuova istanza dei vincoli della funzione vincoli della funzione chiamata ad ogni punto di chiamata ad ogni punto di chiamata chiamata

Se non sensibile al contestoSe non sensibile al contesto– si trattano differenti punti di si trattano differenti punti di

chiamata ad una funzione, in chiamata ad una funzione, in modo identico modo identico

Ad ogni punto di chiamata di una funzione, produciamo i vincoli per la funzione con le variabili locali e i parametri formali, rinominati unicamente per quel punto di chiamata

Page 23: Buffer Overrun Detection using Linear Programming and Static Analysis

…… La sensibilità al contesto si può ottenere modellando La sensibilità al contesto si può ottenere modellando

ciascun punto di chiamata alla funzione come un insieme di ciascun punto di chiamata alla funzione come un insieme di assegnamenti di istanze rinominate delle variabili formaliassegnamenti di istanze rinominate delle variabili formali

un assegnamento per ciascun parametro in input formale un assegnamento per ciascun parametro in input formale rinominato della funzionerinominato della funzione– allevia il problema di unire le informazioni attraverso differenti allevia il problema di unire le informazioni attraverso differenti

chiamate alla stessa funzionechiamate alla stessa funzione– per il puntatore per il puntatore cc1cc1 otteniamo il range [0…2047] per otteniamo il range [0…2047] per cc1!alloc cc1!alloc

e e [1…2048] per [1…2048] per cc1!usedcc1!used– per il puntatore per il puntatore cc2cc2 otteniamo il range [0…1023] per otteniamo il range [0…1023] per cc2!alloccc2!alloc

e [1…1024] per e [1…1024] per cc2!usedcc2!used

miglioramento rispetto a non sensibile al contesto, ma…miglioramento rispetto a non sensibile al contesto, ma…– Se numero esponenziale di contesti di chiamataSe numero esponenziale di contesti di chiamata

il sistema di vincoli avrà un numero molto grande di variabiliil sistema di vincoli avrà un numero molto grande di variabili ci sarà anche un grande numero di vincolici sarà anche un grande numero di vincoli

non può funzionare con le chiamate di funzioni ricorsive non può funzionare con le chiamate di funzioni ricorsive

Page 24: Buffer Overrun Detection using Linear Programming and Static Analysis

summary information… summary information…

supera i difetti del constraint inliningsupera i difetti del constraint inlining si ottiene un “riassunto” per ciascuna si ottiene un “riassunto” per ciascuna

funzione funzione ff per “simulare” l’effetto della per “simulare” l’effetto della chiamatachiamata– Vincoli riassuntiviVincoli riassuntivi

riassumono l’effetto della funzione in termini di variabili riassumono l’effetto della funzione in termini di variabili di vincolo rappresentanti variabili globali e parametri di vincolo rappresentanti variabili globali e parametri formali della funzione stessaformali della funzione stessa

Es: i vincoli generati dalla funzione Es: i vincoli generati dalla funzione copy_buffercopy_buffer

Rimpiazzare parametri formali dei vincoli riassuntivi con Rimpiazzare parametri formali dei vincoli riassuntivi con quelli reali corrispondenti a ciascun punto di chiamataquelli reali corrispondenti a ciascun punto di chiamata

Page 25: Buffer Overrun Detection using Linear Programming and Static Analysis

…… Questo approccio non causa un accrescimento del Questo approccio non causa un accrescimento del

numero di variabili di vincolo numero di variabili di vincolo – è più efficiente ma meno preciso del constraint inliningè più efficiente ma meno preciso del constraint inlining– può manipolare anche le funzioni ricorsive può manipolare anche le funzioni ricorsive

Es:Es:– i valori per i valori per cc1!usedcc1!used, , cc1!alloccc1!alloc, , cc2!usedcc2!used e e cc2!alloccc2!alloc

sono gli stessi che si ottengono usando il constraint sono gli stessi che si ottengono usando il constraint inlininginlining

– i valori di i valori di copy!alloccopy!alloc e e copy!usedcopy!used sono [0…2047] e sono [0…2047] e [1...2048] rispettivamente[1...2048] rispettivamente

Questo perché i valori di queste variabili ottenute dalla Questo perché i valori di queste variabili ottenute dalla chiamata alla riga (7) e alla riga (10) sono “unite”chiamata alla riga (7) e alla riga (10) sono “unite”

– Il constraint inlining ritorna i valori [0...2047] e [1…2048] Il constraint inlining ritorna i valori [0...2047] e [1…2048] per per copy!alloccopy!alloc e copy!used, rispettivamente per la e copy!used, rispettivamente per la chiamata alla riga (7)chiamata alla riga (7)

– ritorna [0…1023] e [1…1024] per la chiamata alla riga ritorna [0…1023] e [1…1024] per la chiamata alla riga (10) (10)

Page 26: Buffer Overrun Detection using Linear Programming and Static Analysis

Sperimentazione su Sperimentazione su casi realicasi reali

Testato suTestato su– wu-ftpd (2.5.0 e 2.6.2) e sendmail (8.7.6 e wu-ftpd (2.5.0 e 2.6.2) e sendmail (8.7.6 e

8.11.6)8.11.6)– Pentium 4 Xeon 3GHz, 4 GB RAMPentium 4 Xeon 3GHz, 4 GB RAM– sistema operativo Debian Linux 3.0sistema operativo Debian Linux 3.0– CodeSurfer 1.8 e compilatore gcc-3.2.1CodeSurfer 1.8 e compilatore gcc-3.2.1– risolutore gerarchicorisolutore gerarchico– Context insensitiveContext insensitive

CodeSurfer per filtrare i warningCodeSurfer per filtrare i warning Testato per provare se riusciva a scoprire Testato per provare se riusciva a scoprire

bug già conosciuti e se riusciva a scoprirne bug già conosciuti e se riusciva a scoprirne altri non conosciuti altri non conosciuti

Page 27: Buffer Overrun Detection using Linear Programming and Static Analysis

Testing wu-ftpd 2.6.2Testing wu-ftpd 2.6.2 18mila righe di codice18mila righe di codice tool ha segnalato 178 warningtool ha segnalato 178 warning

– 14 overrun mai segnalati. Eccone 14 overrun mai segnalati. Eccone uno:uno:

potenziale overrun su buffer puntato potenziale overrun su buffer puntato da da accesspathaccesspath in in read_servers_lineread_servers_line nel file rdservers.c:nel file rdservers.c:

8192 byte possono essere copiati in 8192 byte possono essere copiati in un buffer in cui sono allocati al un buffer in cui sono allocati al massimo 4095 byte massimo 4095 byte

• La funzione fgets può copiare fino a 8192 (dimensione di BUFSIZ) byte in buffer• hcp e acp, puntano all’interno di buffer => qualcuno può far puntare hcp o acp ad un buffer

lungo fino a 8192 byte => overflow sul buffer puntato sia da accesspath sia da hostname• La procedura read_server_line è chiamata, ad es, nel main di ftprestart.c con due buffer

locali, hostaddress e configdir, per i quali sono allocati 32 byte e 4095 byte, rispettivamente• La chiamata legge il contenuto del file _PATH_FTPSERVERS, che tipicamente ha accesso

privilegiato• In alcune configurazioni questo file può essere scritto da un utente locale• Scegliendo dunque delle stringhe di input in maniera attenta, si può sfruttare l’overflow per ottenere

accessi privilegiati

Page 28: Buffer Overrun Detection using Linear Programming and Static Analysis

Testing wu-ftpd 2.5.0Testing wu-ftpd 2.5.0 16mila righe di codice16mila righe di codice tool ha segnalato 139 warningtool ha segnalato 139 warning

– overflow su una variabile globale, overflow su una variabile globale, mapped_pathmapped_path, che , che punta ad un buffer nella procedura punta ad un buffer nella procedura do_elemdo_elem nel file nel file ftpd.cftpd.c

Uso improprio di Uso improprio di strcat(mapped_path,dir)strcat(mapped_path,dir) – dirdir può derivata (indirettamente) dall’input dell’utente può derivata (indirettamente) dall’input dell’utente – range per range per mapped_path!usedmapped_path!used è [0…+∞] mentre per è [0…+∞] mentre per

mapped_path!allocmapped_path!alloc è [4095…4095] è [4095…4095]

La chiamata a La chiamata a strcatstrcat è modellata è modellata secondo quattro vincoli linearisecondo quattro vincoli lineari– I primi due vincoli rendono il I primi due vincoli rendono il

programma lineare non programma lineare non ammissibileammissibile

– risultato in risultato in dst!used!maxdst!used!max settato a settato a +∞+∞

– mapped_path!used!maxmapped_path!used!max settato settato +∞+∞

Page 29: Buffer Overrun Detection using Linear Programming and Static Analysis

Testing sendmailTesting sendmail 8.7.6 8.7.6

– 38mila righe di codice38mila righe di codice– tool ha segnalato 295 warningtool ha segnalato 295 warning

alcuni overflow di tipo off-by-onealcuni overflow di tipo off-by-one– si potrebbe verificare la scrittura di n+1 byte in un buffer che si potrebbe verificare la scrittura di n+1 byte in un buffer che

ha n byte allocatiha n byte allocati 8.11.68.11.6

– 68mila righe di codice68mila righe di codice– Tool ha segnalato 453 warningTool ha segnalato 453 warning

Uno coinvolge la funzione Uno coinvolge la funzione crackaddrcrackaddr nel file nel file headers.cheaders.c, che , che fa il parsing della stringa di un indirizzo e-mailfa il parsing della stringa di un indirizzo e-mail

– memorizza la stringa dell’indirizzo in un buffer statico locale, memorizza la stringa dell’indirizzo in un buffer statico locale, bufbuf lungo MAXNAME + 1 byte. lungo MAXNAME + 1 byte.

– molti controlli di limite per evitare l’overflow ma la condizione molti controlli di limite per evitare l’overflow ma la condizione di <> nella stringa di <> nella stringa FromFrom è imprecisa e porta all’overflow è imprecisa e porta all’overflow

– eseguite molte operazioni matematiche sui puntatori => eseguite molte operazioni matematiche sui puntatori => bp!bp!alloc!max alloc!max = +∞ e = +∞ e bp!used!maxbp!used!max = +∞ (bp puntatore a buf) = +∞ (bp puntatore a buf)

– warning esiste anche se le condizioni di controllo sui limiti sono warning esiste anche se le condizioni di controllo sui limiti sono corrette corrette

Page 30: Buffer Overrun Detection using Linear Programming and Static Analysis

PerformancePerformance tempi di esecuzione impiegati per il controllo del tempi di esecuzione impiegati per il controllo del

codicecodice– CODESURFER: tempo impiegato dall’applicazione per CODESURFER: tempo impiegato dall’applicazione per

l’analisi del codicel’analisi del codice– GENERATOR: tempo per la generazione dei vincoliGENERATOR: tempo per la generazione dei vincoli– TAINT: analisi di alterazioneTAINT: analisi di alterazione– LPSOLVE: tempi per il metodo IISLPSOLVE: tempi per il metodo IIS– HIERSOLVE: tempi per il metodo gerarchicoHIERSOLVE: tempi per il metodo gerarchico

– PRE-TAINT: vincoli generati prima dell’analisi di alterazionePRE-TAINT: vincoli generati prima dell’analisi di alterazione– POST-TAINT: vincoli generati dopo l’analisi di alterazionePOST-TAINT: vincoli generati dopo l’analisi di alterazione

Page 31: Buffer Overrun Detection using Linear Programming and Static Analysis

sensibilità al contesto sensibilità al contesto su casi realisu casi reali

Testata su wuftpd-2.6.2 usando sia l’approccio con constraint Testata su wuftpd-2.6.2 usando sia l’approccio con constraint inlining sia l’approccio summary constraintinlining sia l’approccio summary constraint

Aggiungere la sensibilità al contesto non trova nuovi overrun ma Aggiungere la sensibilità al contesto non trova nuovi overrun ma fornisce migliori valori dati dal risolutore dei vincolifornisce migliori valori dati dal risolutore dei vincoli

Test: controllo delle variabili “affinate”Test: controllo delle variabili “affinate” senza sensibilità al contesto: valori per 7310 variabilisenza sensibilità al contesto: valori per 7310 variabili summary constraint: raffinamento di 72 variabilisummary constraint: raffinamento di 72 variabili

– Il numero di variabili di vincolo è lo stesso dell’analisi senza sensibilità Il numero di variabili di vincolo è lo stesso dell’analisi senza sensibilità al contestoal contesto

– il numero di vincoli può cambiare e cresce dell’ 1%il numero di vincoli può cambiare e cresce dell’ 1% l’approccio introduce alcuni vincoli (i “riassunti”) e rimuove altri vincoli (i l’approccio introduce alcuni vincoli (i “riassunti”) e rimuove altri vincoli (i

vincoli degli assegnamenti dei vecchi punti di chiamata)vincoli degli assegnamenti dei vecchi punti di chiamata) Constraint inliningConstraint inlining

– specializza l’insieme di vincoli per ciascun punto di chiamata specializza l’insieme di vincoli per ciascun punto di chiamata aumento di 5,8 volte nel numero di vincoliaumento di 5,8 volte nel numero di vincoli aumento di 8,7 volte nel numero di variabili di vincoloaumento di 8,7 volte nel numero di variabili di vincolo

– 7310 variabili dell’analisi senza sensibilità al contesto sono 7310 variabili dell’analisi senza sensibilità al contesto sono specializzate in 63704 variabili basate sul contesto di chiamataspecializzate in 63704 variabili basate sul contesto di chiamata

– Su 63704 variabili specializzate, 7497 variabili sono molto più preciseSu 63704 variabili specializzate, 7497 variabili sono molto più precise– Su 7310 variabili non specializzate, 406 sono più precise in almeno un Su 7310 variabili non specializzate, 406 sono più precise in almeno un

contesto di chiamata contesto di chiamata

Page 32: Buffer Overrun Detection using Linear Programming and Static Analysis

Effetto dell’analisi dei Effetto dell’analisi dei puntatori puntatori

ridurre i falsi negativi con l’uso dell’analisi ridurre i falsi negativi con l’uso dell’analisi dei puntatoridei puntatori– tool ha la capacità di gestire, in maniera tool ha la capacità di gestire, in maniera

arbitraria, i livelli di dereferenziamento arbitraria, i livelli di dereferenziamento confronto risultati restituiti utilizzando i confronto risultati restituiti utilizzando i

puntatori e i risultati ottenuti senza analisi puntatori e i risultati ottenuti senza analisi dei puntatori:dei puntatori:– su sendmail sono generati 251 warning a su sendmail sono generati 251 warning a

differenza dei 295 generati con l’analisi dei differenza dei 295 generati con l’analisi dei puntatoripuntatori

tool fallisce nel generare i vincoli per alcuni tool fallisce nel generare i vincoli per alcuni statement statement

Page 33: Buffer Overrun Detection using Linear Programming and Static Analysis

ImperfezioniImperfezioni

flow insensitivity produce molti falsi allarmi flow insensitivity produce molti falsi allarmi – Con partizionamento è possibile affrontare questo tipo Con partizionamento è possibile affrontare questo tipo

di problemadi problema operazione manuale e dispendiosaoperazione manuale e dispendiosa

benefici della context sensitivity sono limitati benefici della context sensitivity sono limitati dalla flow insensitivity dell’analisidalla flow insensitivity dell’analisi

modellando i vincoli in termini di puntatori ai modellando i vincoli in termini di puntatori ai buffer piuttosto che buffer stessi, possiamo buffer piuttosto che buffer stessi, possiamo perdere gli overrun, portando a falsi negativi.perdere gli overrun, portando a falsi negativi.

algoritmi di analisi dei puntatori sono flow algoritmi di analisi dei puntatori sono flow insensitive e context insensitiveinsensitive e context insensitive– generare vincoli in termini di buffer avrebbe portato generare vincoli in termini di buffer avrebbe portato

come risultato ad un maggiore numero di vincoli e come risultato ad un maggiore numero di vincoli e conseguentemente ad un maggiore numero di falsi conseguentemente ad un maggiore numero di falsi allarmi allarmi

Page 34: Buffer Overrun Detection using Linear Programming and Static Analysis

BibliografiaBibliografia http://en.wikipedia.org/wiki/Buffer_overrun Analysis and verification: Buffer overrun detection using linear programming

and static analysis Vinod Ganapathy, Somesh Jha, David Chandler, David Melski, David Vitek, 10th ACM conference on Computer and communications security, 2003

The twenty most critical internet security vulnerabilities www.sans.org/top20 L. O. Andersen. Program Analysis and Specialization for the C Programming

Language. PhD thesis, DIKU, Univ. Of Copenhagen, 1994 C. Cowan, S. Beattie, J. Johansen, and P.Wagle PointGuardTM: Protecting

pointers from buffer overflow vulnerabilities. In 12th USENIX Sec. Symp., 2003

V. Ganapathy, S. Jha, D. Chandler, D. Melski, and D. Vitek. Buffer overrun detection using linear programming and static analysis.

2003. UW-Madison Comp. Sci. Tech. Report 1488 ftp://ftp.cs.wisc.edu/pub/tech-reports/reports/2003/tr1488.ps.Z

CPLEX Optimizer. www.cplex.com D. Wagner, J. S. Foster, E. A. Brewer, and A. Aiken. A first step towards

automated detection of buffer overrun vulnerabilities. In Network and Distributed System Security (NDSS), 2000.

Y. Xie, A. Chou, and D. Engler. ARCHER: Using symbolic, path-sensitive analysis to detect memory access errors. In 9° European Soft. Engg. Conf. and 11th ACM Symp. on Foundation of Soft. Engg. (ESEC/FSE), 2003.

CodeSurfer http://www.grammatech.com/products/codesurfer