RICERCA ITALIANA     

Programma di ricerca

AIDA - Interpretazione Astratta: Progettazione e Applicazioni

Università di riferimento

Università di PISA - INFORMATICA - PISA(PI)

Responsabile dell'Unità di ricerca

Roberto BARBUTI

Descrizione

L'attivita di ricerca dell'unita' di Pisa si svolgera' all'interno dei seguenti Workpackage: Workpackage WP1. Analisi statica Task PI1.1 Analisi statica del calcolo degli ambienti In questo ambito intendiamo utilizzare l'interpretazione astratta per studiare le relazioni tra le analisi di controllo del flusso ed i sistemi di tipo sviluppate per il calcolo degli ambienti. Ci interessa confontare i due approcci in termini di precisione, di potere espressivo, ed anche di confrontare i corrispondenti algoritmi. In particolare siamo interessati alla loro applicazione per la verifica di sistemi aperti, e quindi terremo conto in questa valutazione della classe di contesti esterni rispetto ai quali e' stata provata la proprieta'. Inoltre intendiamo prendere in considerazione un approccio molto diffuso nell'ambito della CFA, che consiste nell'analizzare il sistema non in isolamento ma mettendolo in parallelo con un processo, detto hardest attacker, che simula una certa classe di contesti esterni,. Determinare l'hardest attacker che rappresenta l'insieme dei contesti ben-tipati, puo' essere utile per integrare le due tecniche, ombinando la composizionalita' del sistema di tipo, utile per trattare i contesti, con la precisione della CFA. Infine prevediamo, durante il secondo anno del progetto, di estendere l'approccio ad altre proprieta', ovvero ad altri sistemi di tipo, o ad altri linguaggi per la mobilita'. Task PI1.2 Analisi statica di un calcolo concorrente orientato ad oggetti. Intendiamo applicare l'interpretazione astratta per individuare proprieta' di programmi scritti in un calcolo concorrente orientato ad oggetti. Le proprieta' dimostrate possono essere utilizzate come guida alla costruzione di strumenti di analisi per linguaggi reali orientati agli oggetti con caratteristiche di concorrenza (come Java). Lo studio iniziera' con lo stabilire le caratteristiche che il calcolo deve avere per catturare gli aspetti di interesse del linguaggio reale. Dovra' poi essere individuata la semantica concreta e astratta del calcolo e infine dovranno essere definiti strumenti di analisi sulla base dell'interpretazione astratta. Quello che vogliamo studiare sono le relazioni tra tali strumenti e quelli analoghi sviluppati sulla base di sistemi di tipi. Task PI1.3 Analisi statica di linguaggi dichiarativi. Il primo passo per qualunqe analisi di linguaggi logici basata sull'interpretazione astratta e' la scelta di una semantica collecting appropriata, partendo da una semantica standard non-collecting. Nel campo della interpretazione astratta di linguaggi logici, ci sono essenzialmente due maniere differenti di costruire una semantica collecting: in modo goal-dependent e goal-independent. Poiche' la semantica goal-dependent soffre di perdita di precisione, molte analisi sono svolte sulla base di una semantica collecting goal-independet. Comunque, mentre alcuni domini astratti traggono effettivamente beneficio da una semantica goal-independent( quelli per le proprieta' chiuse per anti-istanza), esattamente l'opposto vale per domini chiusi per istanza, e nulla puo' essere detto per il caso generale. Alcune ricerche sono state condotte nel tentativo di unificare entrambe gli stili semantici, e si e' ottenuta una nuova semantica che calcolo contemporaneamente in maniera goal-dependent e goal-independent, migliorando ognuna delle due analisi con il risultato dell'altra. Sebbene questo possa anche essere efficace dal punto di vista della precisione dell'analisi, la soluzione non e' adeguata dal punto di vista computazionale. Pertanto, stiamo cercando una nuova semantica che sia costruita da zero per essere piu' precisa sia di quella goal-dependent che di quella goal-independent, per tutti i domini astratti. Il vantaggio di questa ricerca sarebbe la disponibilita' di una semantica unica adatta a tutti i tipi di analisi di linguaggi lgici. Pensiamo inoltre che essa porterebbe a una comprensione piu' profonda della maniera in cui i domini astratti sono costruiti, specialmente della maniera in cui essi posso essere decomposti in due componenti, chiusi per istanze ed anti-istanze rispettivamente. Una volta fissata la semantica collecting, abbiamo in programma lo studio di algoritmi per l'unificazione astratta di sostituzioni e vincoli. In effetti, a dispetto della grande quantita' di lavori recentemente prodotti su questo argomento, la maggior parte degli algoritmi di unificazione astratta non sono ottimali. Questo conduce a una significativa perdita di precisione nei risultati finali dell'analisi. Vogliamo sviluppare uno schema generale con il quale derivare algoritmi di unificazione astratta che siano ottimali, ovvero piu' precisi possibile, rispetto al dominio astratto di interesse. In questo contesto, siamo particolarmente interessati ai domini astratti per proprietà di analisi e sharing, utili per la parallelizzazione automatica di programmi logici (con vincoli). Pensiamo inoltre che il matching astratto possa essere applicato in altri campi, come la riscrittura di termini (astratta) e la semantica dei linguaggi funzionali, e che molti risultati concernenti l'ottimalità della unificazione astratta possano essere riutilizzati su questi domini. Piu' in particolare, pensiamo di studiare la relazione tra vari domini per l'analisi di intervalli, dal punto di vista della precisione. Pensiamo che le tecniche sviluppate per i lingaggi dichiarativi riguardanti ottimalita' e completezza degli operatori astratti possano essere applicati pure alla analisi degli intervalli. Questo potrebbe portare a nuovi domini con un migliore rapporto costi/benefìci. Questa ricerca verra' svolta in collaborazione con l'unita' di Bologna. Task PI1.4 Interpretazione astratta e sistemi di tipi. Algoritmi per l'inferenza di tipo possono essere sviluppati in modo sistematico come interpretazioni astratte di una. Intendiamo affrontare il problema della derivazione sistematica di un dominio astratto per l'inferenza di tipi monomorfa in lambda-calcolo L'obiettivo principale che si intende perseguire e' quello di sviluppare tecniche per la trasformazione sistematica di un dominio di tipi pensato per il type checking in un dominio adatto all'inferenza. Il dominio utilizzato nel type checking e' di solito esattamente la proprieta' che si vuole osservare, mentre una inferenza precisa richiede un dominio piu' complesso. L'idea e' quella di provare ad utilizzare alcuni degli operatori di raffinamento noti, che hanno proprio la caratteristica di derivare domini piu' concreti e di migliorare la precisione. In particolare, tenteremo di ricostruire la trasformazione del semplice dominio di monotipi con variabili (rappresentati con termini di Herbrand) nel dominio astratto utilizzato nell'algoritmo di inferenza di tipi di ML, in cui compaiono oltre ai termini anche i vincoli. La ricostruzione avverra' utilizzando una opportuna combinazione di operatori di raffinamento noti. La possibilita' di disporre di tecniche che permettano di passare con facilita' dalle regole di type checking a quelle di type inference e' importante per l'analisi di proprieta' (tra le quali quelle legate alla sicurezza) di calcoli orientati alla concorrenza ed alla mobilit‡, dove le proprieta' interessanti sono spesso espresse mediante regole di type checking. Nel primo anno, verra' sviluppata la trasformazione, derivando il dominio astratto e le corrispondenti operazioni astratte ottime. Nel secondo anno, si definira' l'analizzatore come interprete astratto, fornendone anche una implementazione e confrontandolo con l'algoritmo di ML. Si valutera' infine la possibilita' di applicare trasformazioni simili a sistemi di tipi definiti per calcoli mobili. Task PI1.5 Interpretazione astratta probabilistica. Le tecniche basate sull'interpretazione astratta probabilistica risultano particolarmente appropriate per la costruzione di analisi statiche di proprieta' "approssimate". La considerazione di proprieta' approssimate piuttosto che assolute corrisponde a stabilirne la validita' con un certo margine di errore piuttosto che in termini di una relazione booleana. Questo approccio e' significativo in quanto permette in generale di ottenere delle analisi piu' realistiche. Ad esempio una proprieta' di sicurezza come la non interferenza non e' soddisfatta da nessun sistema reale nella sua formulazione assoluta. Ci proponiamo di stabilire la corrispondenza (o piu' precisamente la dualita') tra le tecniche di analisi per queste proprieta' approssimate finora sviluppate e analisi basate su sistemi di tipo non-standard. A questo scopo sara' utile considerare tale relazione come un caso particolare della relazione tra semantica denotazionale e assiomatica. Workpackage WP2. Sicurezza Task PI2.1 Proprieta' di sicurezza in linguaggi orientati ad oggetti. La nostra intenzione e' di definire una interpretazione astratta capace di verificare il flusso di informazione sicuro nei lingaggi con oggetti. Si rende necessaria una definizione formale del flusso di informazione sicuro, nel caso in cui gli oggetti possano essere creati e distrutti dinamicamente. Normalmente, la proprieta' del flusso di informazione sicuro viene definita sfruttando la nozione di "non interferenza". La non interferenza classica, nel contesto della teoria del flusso di informazione, richiede la definizione di una relazione tra gli stati iniziali e finali di due esecuzioni dello stesso programma. In questo caso, la definizione della relazione risulta complicata dal fatto che gli stati iniziali possono differire nel numero e nel tipo degli oggetti che li compongono. L'interpretazione astratta dovrebbe essere in grado di cogliere il flusso di informazione, sia esplicito che implicito, tra gli oggetti manipolati dal programma analizzato. Poiche' gli oggetti sono creati dinamicamente, sono potenzialmente infiniti. Ogni interpretazione astratta finita dovra' far coincidere piu' oggetti concreti in una stessa astrazione. Quindi, l'astrazione potrebbe introdurre dei falsi flussi di informazione tra oggetti concreti che, altrimenti, sarebbero scorrelati. La nostra intenzione e' di studiare delle intrepretazioni astratte che cerchino di ridurre il numero di falsi allarmi nell'analisi dei programmi. Poiche' gli oggetti vengono normalmente allocati a tempo di esecuzione in uno heap dovranno essere definiti dei domini astratti per la struttura dati dinamica rappresentata dallo heap. La nostra intenzione e' di studiare e, eventualmente, di estendere, gli approcci basati sui token. La segretezza dei dati memorizzati negli oggetti e i flussi di informazione permessi tra gli oggetti stessi sara' modellata usando il classico modello a "reticolo di livelli di sicurezza". La nostra intenzione e' di usare una collecting semantics per tracciare le dipendenze tra gli oggetti. Verranno studiate tecninche di "widening" per garantire la finitezza del calcolo dei punti fissi, anche in presenza di invocazioni di metodi ricorsive. Abbiamo intenzione di scegliere il bytecode di Java come un caso di studio per le tecniche svilupptate nella ricerca teorica. Quindi, abbiamo intenzione di sviluppare uno strumento automantico che controlli la sicurezza del flusso delle informazioni nelle applet Java. Infine, sempre all'interno del linguaggio Java bytecode, vogliamo riformulare il verificatore come interpretazione astratta e vogliamo mostrare come l'interpretazione astratta consenta di rilevare una classe di programmi sicuri piu' grande rispetto a quella individuata dalle attuali implementazioni. Questa ricerca verra' svolta in collaborazione con l'unita' di Bologna. Task PI2.2 Confinamento probabilistico. Un'area dove la probabilita' ha un ruolo particolarmente importante per l'analisi e' quella della sicurezza dei sistemi informatici. Molto spesso e' poco realistico richiedere la sicurezza assoluta di un sistema, mentre sembra piu' ragionevole porsi domande del tipo: quale livello di sicurezza si puo' ottenere dato un certo investimento per la protezione del sistema? L'analisi in questo caso e' piu' un'analisi di rischio che una validazione della sicurezza assoluta del sistema. Abbiamo studiato il problema di quantificare il livello di confinamento di sistemi concorrenti sulla base di un'analisi probabilistica del loro comportamento. L'obiettivo che ci poniamo e' di estendere questo approccio ai sistemi distribuiti. Ad esempio considereremo il problema di come l'informazione si propaga in un sistema distribuito concentrandoci soprattutto sull'aspetto quantitativo di stabilire il numero di passi necessari perche' un dato sia trasmesso da un nodo ad un altro. Se pensiamo all'informazione trasmessa come ad un virus, allora questo tipo di analisi permette di stabilire con quale rapidita' il virus si propaga sulla rete. Per sviluppare questo tipo di analisi intendiamo utilizzare le tecniche di interpretazione astratta probabilistica. Sara' pertanto necessario sviluppare una semantica distribuita basata su operatori lineari su opportuni domini probabilistici (spazi lineari o algebre di operatori). L'utilizzo del prodotto tensore nella definizione di tale semantica sembra particolarmente promettente sia per le proprieta' dell'operazione stessa che per l'interazione con le tecniche di interpretazione astratta probabilistica permettendo un'approccio composizionale all'analisi di reti distribuite. Task PI2.3 Non interferenza temporizzata. Una classe di attacchi a componenti in una rete di calcolatori e' basata sull'uso del tempo. Ad esempio il tempo di esecuzione puo' essere utilizzato per scoprire una chiave segreta. In altri casi il tempo puo' essere usato in attacchi diretti: se la frequenza delle intrusioni e' abbastanza alta, il funzionamento del sistema attaccato puo' essere compromesso. Allo scopo di studiare la robustezza di un sistema rispetto alla frequenza degli attacchi, lo abbiamo modellato mediante automi temporizzati e abbiamo definito il concetto di non interferenza temporizzata. La non interferenza temporizzata include il concetto di tempo e puo' essere utilizzata per scoprire l'interferenza dovuta alla frequenza di alcune azioni. Sfortunatamente la proprieta' di non interferenza temporizzata, in molti casi, e' indecidibile. Vogliamo sfruttare l'interpretazione astratta per approssimare le proprieta' e per costruire strumenti di analisi. Questa ricerca verra' svolta in collaborazione con l'unita' di Bologna. Workpackage WP3. Testing e debugging. Task PI3.1 Il testing e' una tecnica indispensabile per la certificazione di sistemi reattivi, malgrado non assicuri in generale la correttezza dell'analisi. L'interpretazione astratta e' stata utilizzata per superare alcuni dei problemi che si presentano con il testing, come per esempio la terminazione dell'esecuzione di un programma entro un dato intervallo di tempo. Ci proponiamo di usare l'interpretazione astratta probabilistica per misurare l'errore commesso nella valutazione dell'affidabilita' dei sistemi mediante il testing Monte-Carlo. Il problema che affrontiamo e' quello di determinare la probabilita' che la risposta di un sistema reattivo cada all'interno di un certo insieme di possibili output, cioe' che superi un certo test. Poiche' il testing Monte-Carlo di un sistema reale non e' sempre fattibile, I test possono essere effettuati su un sistema astratto. Questo introduce un'ulteriore approssimazione di cui si deve tener conto nella stima dell'errore del testing. Il problema e' di stabilire la "distanza" tra il sistema astratto e quello concreto.