RICERCA ITALIANA     

Programma di ricerca

AIDA2007 - Interpretazione Astratta: Progettazione e Applicazioni

Università di riferimento

Università degli Studi di VERONA - INFORMATICA - ()

Responsabile dell'Unità di ricerca

Roberto Giacobazzi

Descrizione

L'unità di ricerca di Verona contribuirà ai seguenti work-packages: WP1: Sviluppo dell'interpretazione astratta (AI), WP2: Analisi statica mediante interpretazione astratta e WP 3: Protezione del codice mediante interpretazione astratta; nei tempi stabiliti dal seguente GANTT:




WP1 concerne lo studio di metodologie sistematiche per rendere completi domini e semantiche, e per misurare precisione e costi di un'AI tramite un'opportuna misura sui domini.

Task VR-1.1 Trasformazioni semantiche orientate alla completezza. Siamo interessati alla progettazione di trasformazioni che rendano complete le semantiche rispetto ad una data astrazione. La completezza è raggiunta calcolando la semantica più simile alla semantica di partenza che sia al contempo completa per l'astrazione data. Crediamo che il problema si risolva sotto condizioni non restrittive per completezza sia backward che forward [GQ01] e che l'esistenza e l'unicità della semantica da noi ricercata sia garantita in caso tanto di sovra- quanto di sotto-approssimazioni. La soluzione di questo problema teorico risponde ad un triplice interesse: (1) scioglie il problema centrale della completezza in AI, affiancando i trasformatori di semantiche ai ben noti trasformatori di domini astratti [GRS00]; (2) poiché trasformare semantiche significa trasformare programmi [CC02], l'aver reso completa una semantica implica che il corrispondente programma è stato sottoposto ad una deformazione (una trasformazione che non ne preserva per forza la semantica) la cui AI è completa. Un programma trasformato in tal modo non rilascia, in prospettiva della non-interferenza astratta, informazioni in modo inatteso, e dualmente non presenta incompletezze semantiche in cui nascondere informazione (ad esempio, software watermark); (3) il problema duale a rendere la semantica il più possibile incompleta corrisponde a massimizzare l'attitudine del programma deformato ad ospitare watermark. Questi aspetti verranno entrambi sviluppati e applicati nei Task: VR-3.1, VR-3.2 e VR-3.4.

Task VR-1.2: Misura di precisione basata su domini numerici. Spesso, per analizzare i possibili valori (numerici) delle variabili di un programma, si usano domini astratti (e.g. dominio degli intervalli) che danno risultati imprecisi. L'imprecisione degli intervalli è dovuta alla perdita delle relazioni tra variabili e alla rappresentazione dei valori assunti da una variabile tramite i soli minimo e massimo, che non permettono ad esempio l'individuazione di segmenti "proibiti" all'interno degli intervalli. Una delle analisi più precise si basa sul dominio dei poliedri [CH78], in cui un insieme di valori è rappresentato da un insieme di vincoli lineari. Riducendo l'espressività dei vincoli, si ottengono domini relazionali più deboli, come il dominio degli ottagoni. Chiaramente, una volta quantificata la precisione di un dominio, si può scegliere il dominio più appropriato per l'analisi di un'applicazione in base ad un trade-off con fattori di costo (come il tempo d'esecuzione), e non solo alla correttezza dell'analisi. Nell'analisi statica classica, l'imprecisione di un'analisi rispetto ad un programma è di solito valutata mediante l'estremo inferiore e superiore dell'insieme dei falsi positivi. Questa stima è tuttavia piuttosto approssimativa. Per introdurre una maggiore sistematicità nella scelta dei domini astratti, useremo PAI. A questo scopo investigheremo la struttura del reticolo delle PAI ereditata dal reticolo delle proiezioni di Birkhoff-von Neumann, una misura della precisione relativa calcolata mediante un operatore di norma associato, e un'interpretazione statistica del numero che esprime la precisione relativa. Studieremo poi la rappresentazione della semantica di un programma come prodotto tensore degli spazi vettoriali associati al dominio di ogni sua variabile; con ciò collegheremo la nozione di dipendenza relazionale nell'ambito dell'analisi di programmi con quelle statistiche di correlazione e indipendenza: due proprietà possono essere analizzate isolatamente, ossia non considerando l'interazione reciproca, se sono statisticamente indipendenti; maggiore è la correlazione fra le due, maggiori saranno l'imprecisione dell'analisi e il numero degli elementi (debolmente) relazionali necessari per ottenere risultati sufficientemente precisi.

Nel WP2 investigheremo alcune fondamentali questioni di analisi di terminazione, di analisi di complessità e di PAI legate all'uso di informazione statistica per migliorare il rendimento dell'analisi statica.

Task VR-2.1: Analisi statica di terminazione e complessità. La nostra analisi di terminazione basata su Julia e BinTerm è in grado di provare la terminazione di piccoli programmi in Java bytecode, anche con strutture dati. L’idea è di estendere l’analisi a programmi reali (grandi). Per questo intendiamo migliorare le analisi preliminari in modo da renderle più veloci e precise. In particolare, approfondiremo la relazione tra pair-sharing e set-sharing, definiremo elementi di domini astratti più precisi per sharing e mostreremo la loro ottimalità. L’analisi di lunghezza dei cammini richiede un impegno maggiore, poiché i poliedri sono strutture dati più complesse dei BDD. L’efficienza della Parma Polyhedra Library può essere migliorata considerando, nel nostro caso, la forma speciale dei poliedri, dove molte variabili di input e output mantengono lo stesso valore. Studieremo il comportamento di sharing, ciclicità e lunghezza di cammino nel caso di programmi concorrenti, in modo da garantire la correttezza dei risultati anche in questo caso. Integreremo l’esistente analisi di terminazione con dimostrazioni automatiche di assenza di deadlock, poiché possono creare problemi di terminazione nel caso della concorrenza. Questo punto sarà sviluppato in coordinazione con Padova rispetto all’analisi e verifica di sistemi concorrenti. BinTerm ritorna le funzioni di ranking e prende in ingresso un programma CLP su vincoli di lunghezza di cammino, la cui terminazione richiede quella dell’analisi del programma Java bytecode. L’efficienza di BinTerm non è ancora soddisfacente. Troveremo tecniche migliori per l’identificazione delle funzioni di ranking che integreremo in Parma Polyherdra Library. L’analisi automatica di complessità per programmi Java (bytecode) sarà basata sulle stesse analisi preliminari e di lunghezza di cammino implementate in Julia e userà tecniche simili a quelle in [AAGPZ07], che hanno ancora bisogno di implementazione e valutazione. Probabilmente, durante il miglioramento e lo sviluppo delle analisi di terminazione e complessità, avremo bisogno di maggiori informazioni sui programmi per ottenere risultati più precisi. Ovvero, siamo coscienti che il dominio di lunghezza di cammino beneficerà dell’informazione preliminare sul valore costante delle variabili legate agli oggetti, sul segno delle variabili numeriche, sulle variabili numeriche definite fuori dall’intervallo [-1,1] e così via. Svilupperemo nuovi domini astratti per queste proprietà per migliorare l’analisi di lunghezza di cammino e, indirettamente, quella di terminazione e complessità. Manterremo l’interfaccia web di Julia+BinTerm e la estenderemo con nuove funzionalità per fornire un servizio web di dimostrazione automatica di terminazione e complessità, possibilmente correlato da certificazioni stile proof-carring code.

Task VR-2.2: Ottimizzazione speculativa. L’idea è (i) di eseguire il codice in modo “speculativo” rispetto a un certo “guess”; (ii) verificare successivamente la correttezza del “guess”; (iii) se è corretto la computazione continua, altrimenti viene eseguito del codice riparatore. Questo garantisce che la computazione sia sempre eseguita correttamente. Il problema principale è il costo (medio) della “riparazione”. Se il “guess” è spesso corretto allora il costo di esecuzione del codice riparatore è ammortizzato. Nell’approccio speculativo il compilatore può sfruttare informazione statistica (piuttosto che definita) per scegliere se fare l’ottimizzazione. PAI permette di sfruttare meglio il caso del “forse” rispetto alla classica analisi conservativa di ottimizzazione dei compilatori, sostituendo un’analisi di possibilità con una di probabilità. Consideriamo per esempio l’importante problema della parallelizzazione del codice. Quando un compilatore deve parallelizzare due pezzi di codice deve considerare tutte le possibili dipendenze. Le tecniche esistenti sono over-conservative: se una dipendenza non può essere provata, il compilatore assume che ci sia. Quindi molte opportunità di parallelizzazione vengono scartate. Contrariamente a questo approccio conservativo di “caso pessimo”, il threading speculativo è una tecnica emergente che permette alcune parallelizzazioni incorrette di thread ritardando la verifica ad un momento successivo. Questo approccio ottimistico è supportato da PAI. Questo può essere utilizzato per affrontare il problema dell’esplosione degli stati nella valutazione delle prestazioni si sistemi paralleli.

Nel WP3 applichiamo metodi di AI alla generalizzazione di firme per l’identificazione dei malware, al software watermarking sfruttando i buchi di incompletezza e all’offuscamento di codice per rafforzare l’inserimento di predicati opachi.

Task VR-3.1: Generalizzazione di firme. Il problema principale degli algoritmi di identificazione di malware basati su firme è che non sono in grado di riconoscere malware offuscati. Per affrontare questo problema forniremo un metodo di generalizzazione della firma in modo da poter riconoscere anche le varianti metamorfiche. L’idea è di partire da una descrizione iniziale di un malware e poi di generalizzarla in modo da identificare anche le sue varianti offuscate. L’intento malizioso di un malware può essere espresso tramite particolari sequenze di system call che possono essere modellate come un linguaggio riconosciuto da un automa. Partiremo considerando EFSA (Extended Finite State Automata) poiché è un modello di specifica spesso usato in sicurezza. Consideriamo un EFSA S che modella la firma e un possibile offuscamento O utilizzato dagli hackers per evitare l’identificazione. Se il modello dell’EFSA è chiuso rispetto ad O, allora la generalizzazione restituisce
Closure(S,O) che può essere utilizzata per identificare tutte le varianti di S ottenibili con O. Dato un modello di specifica, come EFSA, vogliamo identificare l’insieme di trasformazioni per cui è chiuso per poter caratterizzare la classe di offuscamenti che è possibile gestire con la generalizzazione.

Task VR-3.2: Predicate obfuscation. Vogliamo studiare quali sono i reali limiti implicati dal noto risultato di Barak et al. [B01] sull’impossibilità dell’offuscamento. Tale risultato si basa sul fatto che l’offuscamento debba nascondere ogni proprietà di programmi che non è derivabile dall’osservazione del loro comportamento input-output. Questa è chiaramente una richiesta molto forte mentre, in pratica, si è interessati a proteggere proprietà particolari (sensibili) di particolari programmi. Sarebbe quindi interessante studiare la possibilità di nascondere una specifica proprietà di un particolare programma (o classe di programmi). Vogliamo studiare l’esistenza di trasformazioni di codice, dette predicate-obfuscator, che cercano di proteggere un particolare tipo di informazione di un certo programma (o classe di programmi). Vorremo poi caratterizzare la classe di predicati che è possibile nascondere in modo da fornire una descrizione più precisa delle potenzialità e limiti dell’offuscamento.

Task VR-3.3: Inserimento di software watermark in strutture cicliche. Un ciclo è un costrutto di programmazione eseguito iterativamente. Dispiegando le sue iterazioni come codice sequenziale, rendiamo il comportamento del ciclo ad ogni iterazione sintatticamente analizzabile. Così la trasformazione inversa diviene un modo per ridurre la comprensione del comportamento di ciascuna iterazione. L'idea è di sfruttare questo fatto per l'inserimento, all'interno di un ciclo, di watermark calcolati iterativamente. Ciò si attua dispiegando interamente il ciclo e cercando l'iterazione più adeguata a promuovere la costruzione del watermark. Collegando poi l'inizializzazione del watermark a tale iterazione e inserendo il watermark così modificato nel ciclo originale, renderemo difficile l'individuazione dell'iterazione promotrice. L'estrazione sarà guidata da una chiave che useremo per dipanare soltanto l'iterazione promotrice e quelle ulteriori richieste per la computazione del watermark. Ipotizziamo che sia difficile manomettere il ciclo marcato con trasformazioni di ciclo che preservano la semantica, poiché tali modifiche sono possibili solo se il numero di iterazioni è staticamente noto. Questo task richiederà tecniche di program slicing generalizzate (astratte) in grado di gestire anche dipendenze approssimate. Su tali tecniche infatti si basa, almeno parzialmente, l'estrazione del watermark.

Task VR-3.4: Nascondere il Watermarks nei buchi di completezza. Le astrazioni complete modellano la precisa comprensione della semantica di programmi da parte di un osservatore approssimato, e corrispondono alla possibilità di sostituire, senza perdita di precisione, le computazioni concrete con quelle astratte. La mancanza di completezza dell’osservatore corrisponde quindi ad una imprecisa comprensione della semantica. Questo fornisce la base per lo sviluppo di una nuova famiglia di metodi per la steganografia che sono ben definiti e dimostrabilmente sicuri, e più in generale per l’offuscamento. Consideriamo il seguente comando: C: x = a*b che memorizza in x il prodotto di a e b. Un osservatore (passivo) analizzando il segno delle variabili del programma e conoscendo il segno di a e b ha una comprensione completa del segno del risultato. Un’analisi automatica dei segni che sostituisce il calcolo concreto con quello approssimato (i.e. la regola dei segni) è quindi capace di conoscere, senza perdita di precisione, il valore del segno voluto da C. Infatti l’astrazione dei segni A = {+, 0, -, ?}, dove ? rappresenta ogni possibile valore intero, è completa per la moltiplicazione intera. Una trasformazione t che sostituisce C con t(C): x=b; se b !=0 {x = a + x; b = b - 1} offusca l’informazione di segno all’osservatore A. Questo perché la regola dei segni è incompleta per l’addizione intera, infatti i segni in A perdono la grandezza dell’intero. Per capire in modo automatico il segno calcolato da t(C) sono necessari gli intervalli, i.e., un osservatore molto più concreto. In questo senso offuscamento e incompletezza sonno concetti profondamente legati: mentre la steganografia può essere vista come nascondere informazione in buchi di incompletezza, l’offuscamento può essere visto come trasformare programmi in modo che le uniche astrazioni complete che gli osservatori possono usare siano molto costose, e.g. analisi relazionali o esponenziali sul numero di variabili. Siamo interessati allo studio di attacchi passivi e attivi e all’utilizzo del Task VR1.1 per fornire un modello per questi comportamenti. Gli attacchi passivi corrispondono ad analisi statiche e dinamiche, i.e. astrazioni della semantica, che non interferiscono con la struttura del codice e il comportamento del programma. Gli attacchi attivi invece corrispondono a deformare i programmi. Crediamo che molte tecniche di software watermarking siano casi speciali dell’inserimento di watermark basato sull’incompletezza dell’osservatore. Inizieremo considerando i programmi modellati da strutture di Kripke (finite) e poi estenderemo questo metodo ad arbiotrari linguaggi di programmazione in modo da sfruttare l’incompletezza come un metodo generale per l’inserimento di watermark.