RICERCA ITALIANA     

Programma di ricerca

AIDA - Interpretazione Astratta: Progettazione e Applicazioni

Università di riferimento

Università degli Studi di VERONA - INFORMATICA - VERONA(VR)

Responsabile dell'Unità di ricerca

Roberto GIACOBAZZI

Descrizione

Il team di Verona ha maturato una grande esperienza nella teoria e nella pratica dell'interpretazione astratta, in particolare nei campi del design sistematico di domini astratti, nell'analisi statica di programmi, nel model checking astratto e nella sicurezza basata sui linguaggi. Il tema di ricerca comune nel nostro gruppo e' la definizione e la sistematica derivazione di domini astratti che modellino proprieta' rilevanti del sistema da analizzare. Contiamo di contribuire al progetto AIDA in questa direzione nei campi dell'analisi statica di programmi, della sicurezza nei linguaggi, della verifica di sistemi ibridi per mezzo di interpretazione astratta, model checking astratto e testing astratto. WP1: "Analisi statica di programmi" Task VR1.1: "Design sistematico di trasformatori di domini astratti". Siamo interessati alla definizione di un quadro generale per il design sistematico di trasformatori di domini astratti. L'idea principale nell'approccio di questo problema e' usare l'interpretazione astratta in questo caso portata all'ordine superiore: l'oggetto del discorso sono i domini anziche' le descrizioni degli stati dei programmi. L'uso dell'interpretazione astratta all'ordine superiore mostrera' il potenziale dell'interpretazione astratta nel definire adeguatamente analizzatori di programmi che siano versatili, cioe' parametrici sulle proprieta' che essi vogliono indurre o preservare nell'approssimazione. Questa ricerca e' una prospettiva fondamentale per WP1, WP2 e WP6. Uno degli aspetti principali di questa algebra di trasformatori di domini e' la caratterizzazione della reversibilita' degli operatori. Questo gioca un ruolo fondamentale per associare ad ogni operazione di raffinamento di domini una corrispondente semplificazione o compressione di domini. Intendiamo generalizzare i risultati in [GR98unif] per studiare come rendere reversibile un raffinamento. Questo corrisponde a specificare nuove operazioni di ordine superiore che producano trasformatori reversibili. Task VR1.2: "Analisi statica di bytecode Java". Intendiamo continuare lo sviluppo di un analizzatore statico generico per il bytecode Java. Un analizzatore statico per bytecode Java basato sull'interpretazione astratta, chiamato Julia [Julia], e' stato implementato a Verona ed e' disponibile sotto licenza pubblica GNU. Ci sono alcuni aspetti che devono essere migliorati in Julia. Maggiore attenzione deve essere posta alla sua efficienza per rendere possibile l'analisi di applicazioni sempre piu' grandi. In particolare studieremo come la possibilita' di suddividere l'analisi in differenti flussi di esecuzione possa rendere l'esecuzione di Julia parallela o distribuita. Questo aspetto sara' studiato nel contesto di nuovi domini astratti per escape analysis, analisi di classi e non-interferenza (vedi Obiettivi VR1.4 e VR2.1). Un ulteriore aspetto da sviluppare e' l'interfaccia dell'analizzatore, che dovrebbe permettere all'utente di controllare facilmente l'analisi e specificare i punti del programma dove essa deve essere concentrata. Insieme ad una tecnica basata su una semantica watchpoint sviluppata nell'Obiettivo VR1.3, questo consentira' una risposta veloce e focalizzata alle interrogazioni dell'utente sul comportamento astratto del programma da analizzare. Task VR1.3: "Analisi Watchpoint". Le dimensioni e la complessita' del software odierno sono una sfida per l'applicabilita' dell'interpretazione astratta e dell'analisi statica in generale. Poiche' il costo dell'analisi cresce con la dimensione del programma, molte applicazioni non possono essere analizzate per la mancanza di risorse computazionali. Per ovviare a questo problema spesso si deve ridurre la precisione dell'analisi: tipicamente si sacrifica l'analisi del flusso o del controllo. L'obiettivo della ricerca sara' quindi 1) mostrare come la semantica watchpoint possa essere applicata ad un linguaggio complesso e non strutturato come il bytecode Java; 2) istanziare la metodologia per escape analysis e class analysis. Per risolvere il punto 1 ricostruiremo la struttura nascosta del bytecode Java come un grafo di frammenti di codice, simile al grafo dei dominatori nella tecnologia dei compilatori. Si noti che non abbiamo garanzie che il codice in analisi derivi effettivamente dalla compilazione di Java. Per risolvere il punto 2 useremo i domini astratti definiti in [SJ03,HS02,HS02b] e li adatteremo alla filosofia basata sull'uso degli stack della macchina virtuale Java. Considereremo gli elementi dello stack come variabili e descriveremo ogni bytecode attraverso una funzione di trasferimento sugli stati costituiti da variabili locali e variabili di stack. Task VR1.4: "Escape analysis con vincoli". Il concetto di vincolo e' stato usato diffusamente per l'analisi statica di codice a oggetti. Comunque i vincoli sono stati usati fino ad ora solo per compilare un programma in un vincolo la cui soluzione esprime informazioni astratte corrette per il programma. Questo porta ad analisi veloci ma poco informative, che non analizzano il flusso ne' il controllo. Il nostro obiettivo e' di usare i vincoli per esprimere le funzioni astratte di trasferimento di istruzioni (o framemnti di bytecode) per migliorare l'escape analysis. In particolare vogliamo un'implementazione dell'escape analysis definita in [HS02, HS02b] e di alcune delle class analysis definite in [SJ03] attraverso vincoli insiemistici [DPPR00]. Poiche' le funzioni di trasferimento astratte per queste analisi lavorano su insiemi di punti di creazione di oggetti, i vincoli insiemistici sembrano la soluzione naturale, rispetto ad una rappresentazione in termini di diagrammi binari di decisione. Per esempio un'istruzione come v:=w, che copia il valore di w in quello di v, puo' essre modellata in termini astratti da una funzione di trasferimento che copia i punti di creazione (e le classi) di w in quelli di v. I vincoli devono essere mantenuti piccoli e facili da manipolare. Una possibile scelta e' usare solo i vincoli ottenuti per unione e intersezione. Questa scelta potrebbe imporre restrizioni nella rappresentazione di funzioni astratte di trasferimento, per cui dovrebbero essere usate rappresentazioni sub-ottimali invece di quelle ottimali delineate in [HS02, HS02b, SJ03]. WP2: "Sicurezza" Task VR2.1: "Non-interferenza astratta" La nozione di non-interferenza astratta in [GM04] e' generale e in principio applicabile a qualunque problema di sicurezza su linguaggi. Uno degli aspetti piu' interessanti della non-interferenza astratta sta nel fatto che essa e' una nozione semantica, quindi raffinando la semantica possiamo raffinare la corrispondente nozione di segretezza. In particolare questo permetterebbe di rivelare anche covert channels [SM03] dovuti alla non-terminazione, timing channels dovuti a diversi tempi di terminazione delle computazioni e canali probabilistici dovuti a differenti probabilita' di computazione. Noi vorremmo estendere la non-interferenza astratta anche a linguaggi concorrenti e multi-threaded, dove l'interleaving di processi aggiunge nuove possibili interferenze. Questa estensione richiede la definizione di una semantica di bisimulazione parametrica sull'attaccante specificato come astrazione. Questo sarebbe particolarmente utile per applicare la non-interferenza astratta per verificare protocolli di comunicazione sicuri, o per derivare condizioni di sicurezza per l'esecuzione di protocolli. Al fine di verificare la non-interferenza astratta in programmi reali possiamo intraprendere differenti strade. Un primo approccio e' quello di definire un sistema di prova corretto per la non-interferenza astratta basato sulla sintassi, questo permetterebbe di definire anche una architettura proof-carrying code (PCC) per la non-interferenza astratta [N97]. In questo caso il produttore di codice potrebbe creare un certificato di non-interferenza astratta che attesta il fatto che la segretezza del codice non puo' essere violata dal corrispondente modello dell'attaccante. Quindi l'utilizzatore del codice puo' convalidare il certificato per verificare che il codice e' sicuro per il corrispondente modello dell'attaccante. L'implementazione di questa tecnologia richiede un'appropriata scelta di un logical framework [HHP93] per specificare le astrazioni. Questo permetterebbe ai programmi di trasportare le dimostrazioni della loro non-interferenza astratta e ai processi ospitanti di verificare efficientemente la dimostrazione trasportata. Un altro importante aspetto applicativo della non-interferenza astratta e' lo slicing di programmi [W84]. Solitamente i criteri di slicing usati per lo slicing di programmi devono considerare le relazioni di dipendenza tra le variabili. Possiamo notare che se una variabile dipende da un'altra variabile, allora esiste un'interferenza. Questo significa che possiamo studiare come usare gli algoritmi di slicing esistenti in modo da verificare la non-interferenza astratta, o inversamente possiamo usare la non-interferenza astratta per indebolire i criteri di slicing not. Task VR2.2: "Modelli per flussi di controllo/dati" Siamo interessati nell'uso di funzioni booleane per modellare flussi di controllo/dati nella sicurezza su linguaggi. In particolare siamo interessati nella costruzione sistematica di domini per i flussi di informazione ottenuti combinando funzioni booleane e analisi di dipendenze. Siamo interessati allo studio del legame tra analisi del flusso di informazione e analisi di groundness nei programmi logici. Dal punto di vista del flusso dell'informazione, possiamo considerare i termini ground come oggetti sui quali l'informazione non puo' fluire. Questo approccio puo' ulteriormente essere generalizzato per modellare la non-interferenza astratta generalizzando le tecniche in [GM04] per modellare dipendenze di flussi di informazioni astratti. Inoltre siamo interessati nell'estendere le tecniche presentate in [GGM04] ad un linguaggio di programmazione piu' ricco con procedure, classi, ricorsione, ecc. Un buon linguaggio candidato per applicare l'analisi dei flussi di informazione e' Java. Siamo interessati ad estendere Julia in modo da renderlo un verificatore di bytecode per proprieta' di non-interferenza astratta di Java bytecode. Questo richiede tecnologie avanzate di domini astratti in modo da combinare funzioni booleane con informazione type-like per modellare non-interferenza astratta. WP3: "Testing e debugging" Task VR3.1: "Testing astratto" Il nostro interesse nel program testing e' principalmente connesso con la non-interferenza (Task VR2.1). La specifica e' una prescrizione di cosa il sistema dovrebbe fare: l'obiettivo del testing e' quello di verificare se il sistema implementato di fatto soddisfa questa prescrizione. Questo tipo di testing e' chiamato "conformance testing". A partire dai concetti dell' ISO 9646, l'aggettivo conformance e' interpretato come la soddisfazione di un insieme di requisiti di "conformance", che derivano dalla specifica stessa del sistema. Data una specifica formale, l'insieme dei requisiti di conformance definiti dalla specifica possono essere ottenuti mediante una particolare relazione. Questi requisiti sono un insieme di proprieta' che tutte le implementazioni dovrebbero soddisfare. Molte tecniche di testing sono basate sull'iniezione di errori, ovvero esse eseguono delle perturbazioni dell'ambiente, considerate come errori, e osservano cosa succede nell'esecuzione dell'implementazione. Per noi esiste una relazione tra questi metodi di testing e alcune nozioni di non-interferenza. Studiare queste relazioni permetterebbe di modellare il testing nel framework della non-interferenza astratta, fornendo sia una relazione tra testing astratto [CC00test] e non-interferenza astratta [GM04], sia un framework formale basato sulla semantica per gestire la regressione di test nel testing di programmi. WP4: "Sistemi ibridi e real-time" Task VR4.1: "Verifica di sistemi ibridi" In questo ambito di lavoro siamo interessati principalmente nella verifica automatica di sistemi ibridi mediante model checking astratto. La discretizzazione di un automa ibrido puo' essere vista nel contesto dell'interpretazione astratta come una sua astrazione completa, e quindi puo' essere visto come una istanza dell'interpretazione astratta. Il model checking e' interessato ad astrazioni complete, esse sono molto costose dal punto di vista computazionale, e la teoria dell'interpretazione astratta potrebbe essere un buon punto di partenza per derivare nuovi tipi di astrazioni e tecniche di verifica (widening e narrowing) che sono computazionalmente efficienti anche se non necessariamente complete. Noi siamo interessati a studiare la classificazione dei sistemi ibridi ottenuta da Henzingher et al. [HM00], nel contesto dell'interpretazione astratta, dimostrando che le classi di Henzingher sono relazionate da astrazioni e che ogni classe puo' essere vista come un'astrazione completa del modello concreto di un automa ibrido. L'interesse in questo approccio sta nel fatto che esso rende i metodi sistematici per derivare astrazioni complete in [GRS00], applicabili alla derivazione di sistemi di transizione simbolici a partire dalle logiche che devono essere preservate. Infatti, l'interpretazione astratta fornisce le costruzioni piu' efficienti, mentre le costruzioni usate nel model checking standard risultano essere semplicemente le migliori costruzioni ottenibili in base all'esperienza. Noi vorremmo capire come il widening e il narrowing possono essere usati come basi per nuovi algoritmi approssimati di model checking. In particolare siamo interessati nell'uso dei frattali come una base per il widening nei sistemi ibridi rettangolari. Infine, ci piacerebbe capire come i risultati che deriviamo per i sistemi ibridi possono essere estesi a sistemi ibridi stocastici. WP6: "Verifica". In questa area di lavoro siamo interessati ad applicazioni di trasformatori di domini astratti sia per semplificare il model checking astratto sia per ottenerne la preservazione forte. L'attivita' in questa area di lavoro e' un'applicazione delle tecniche sviluppate nel Task VR1.1. Task VR6.1: "Compressione di model checking astratti" In [GM03] viene introdotto un algoritmo per la compressione dei domini astratti relativamente a raffinamenti di completezza. Questo potrebbe essere importante per nel model checking astratto dal momento che in [GQ01,RT04] il problema di rendere i modelli strong preserving e' stato caratterizzato come raffinamento di completezza. Questo implica che comprimere i modelli corrisponde ad aggiungere tutti i possibili controesempi, astraendo il piu' possibile il sistema di transizione in modo che esso abbia comunque lo stesso raffinamento di completezza originale. A questo punto il raffinamento guidato dai controesempi per una data formula in [CGJL00] raffinerebbe il sistema di transizione astratto solo per rendere il modello fortemente preservante per la stessa formula, ottenendo in questo modo il piu' astratto sistema che preserva fortemente la formula data. Task VR6.2: "Raffinamento di semantiche" Un aspetto simmetrico in relazione alle tecniche di raffinamento dei domini astratti e' il raffinamento delle semantiche. Con questo intendiamo il problema di trasformare semantiche, ovvero funzioni Scott-continue, in modo che la loro approssimazione rispetto ad un dato dominio fissato sia completa. Questo problema e' importante al fine di caratterizzare quali sono le operazioni per le quali un dato dominio e' completo. La piu' importante applicazione di questa tecnologia si trova nel model checking astratto, per derivare la piu' concreta (piu' forte) logica per la quale il model checking astratto, sotto una certa astrazione fissata, e' completo o fortemente preservante. Questo fornirebbe una caratterizzazione basata sulla logica di una tassonomia di astrazioni nel model checking astratto sotto il requisito della preservazione forte.