Ricerca Scientifica 1999

Ministero dell'Universita' e della Ricerca Scientifica e Tecnologica Dipartimento Affari Economici


Coordinatore		ROBERTO GIACOBAZZI

Titolo della Ricerca		CERTIFICAZIONE AUTOMATICA DI PROGRAMMI MEDIANTE INTERPRETAZIONE ASTRATTA

Finanziamento assegnato		M£ 271 , Euro 139959,820

Rd+Ra		M£ 140 , Euro 72303,966 (dichiarata)

Durata		24 mesi

Obiettivo della Ricerca

L'obiettivo principale del progetto e' l'utilizzo dell'interpretazione astratta come strumento unificante per lo studio e lo sviluppo di tecniche per l'analisi sul flusso dei dati e del controllo nei programmi, dei metodi di prova, e dei metodi per l'analisi di programmi basati su tipi e su vincoli. La certificazione dei programmi rappresenta la perfetta base dalla quale partire per studiare sia gli aspetti piu' fondamentali dell'analisi e verifica dei programmi, come l'analisi di programmi parzialmente definiti, i fondamenti teorici dei domini, e gli aspetti riguardanti la precisione e la complessita' dell'analisi, che per progettare strumenti utili per la certificazione dei programmi basata sulla semantica, strumenti che possono essere direttamente utilizzati nei moderni sistemi software per la certificazione del codice.

Dal punto di vista degli aspetti fondazionali conivolti nel progetto, siamo interessati a:

- un ambiente comune per l'integrazione di diverse tecniche per la certificazione, quali analisi basata sui tipi, debugging dichiarativo, analisi data-flow e verifica;
- nuovi modelli semantici per l'analisi di programmi mobili nel contesto di linguaggi di programmazione dichiarativi e imperativi;
- tecnologie per la progettazione di domini per la certificazione automatica di programmi;
- tecniche efficienti di risoluzione di vincoli e calcolo di punto fisso;
- metodologie per la valutazione delle prestazioni dei metodi di certificazione di programmi, quali complessita', precisione, ed errori di approssimazione.

Per quanto riguarda gli aspetti piu' applicativi dell'interpetazione astratta, il progetto si interessara' dell'integrazione di diverse tecnologie per la certificazione di programmi e dello sfruttamento di queste per progettare strumenti adatti alla certificazione automatica di programmi inseribili direttamente in ambienti di programmazione. Sebbene l'interesse sara' in primo luogo concentrato su metodi indipendenti dai linguaggi, come "case study" per la certificazione dei programmi si porra' particolare attenzione alla realizzazione di analizzatori di codice mobile in linguaggi dichiarativi.

Innovazione rispetto allo stato dell'arte nel campo

Il progetto si concentrera' sullo studio e la progettazione di strumenti automatici per l'analisi e la certificazione di programmi per mezzo dell'interpretazione astratta. I proponenti sono convinti che questa alternativa, rispetto ad altre metodologie, sia ormai scientificamente matura, sebbene le sue applicazioni nel campo dell'analisi di sicurezza e della certificazione automatica di programmi non siano ancora state studiate in dettaglio, ne' in campo accademico ne' industriale. Gli strumenti ed i metodi esistenti allo stato dell'arte sono classificabili essenzialmente in due classi: metodi e strumenti basati sull'analisi statica e metodi e strumenti basati su sistemi logico-formali di prova. Questa distinzione risulta particolarmente debole sotto una piu' attenta analisi. L'interpretazione astratta fornisce infatti un paradigma unificante per poter trattare nel medesimo contesto sia l'analisi statica sul flusso dei dati e sul controllo che i metodi per generare automaticamente invarianti di programma. In questo senso risulta possibile integrare in un medesimo paradigma metodi e strumenti differenti per la certificazione di programmi e al tempo stesso avere una vasta gamma di metodi formali per costruire nuovi strumenti di certificazione automatica.

Criteri di verificabilità

1) Possibilita' di integrazione di tecnologie differenti per la certificazione di programmi.

2) Sviluppo di metodologie per la costruzione sistematica di strumenti di analisi indipendenti dal linguaggio di programmazione considerato.

3) Possibilita' di controllare la fase di progetto dell'interpretazione astratta nei termini della precisione richiesta e dei costi.

4) Migliori risultati in termini di precisione, modularita' e astrazione rispetto ad altre metodologie.

Unità di Ricerca

1]  Unità di       Universita' degli Studi di VERONA

     Responsabile Roberto GIACOBAZZI
     Rd+Ra      M£ 33 , Euro 17043,078 (dichiarata)

     Finanziamento   M£ 71 , Euro 36668,440

     Compito


In questo progetto prevediamo di contribuire nei seguenti campi principali:
- Tecnologie per il progetto sistematico di domini per la caratterizzazione di proprieta' sul flusso dei dati e del controllo nei programmi.
- Nuovi metodi per la valutazione degli errori, come interpretazione astratta basata su metriche.
- Domini per la approssimazione probabilistica.
- Relazione tra certificazione basata su tipi e interpretazione astratta.
- Tecniche efficienti per la soluzione di problemi con vincoli nella certificazione di programmi.
- Domini specifici per analisi di sicurezza, come integrita' dei dati, stima dell'utilizzo delle risorse (e.g.CPU, memoria, ecc.), flussi di controllo e di dati in sistemi multiagente.
- Metodi basati sull'interpretazione astratta per la verifica efficiente e la certificazione automatica di sistemi reattivi mediante model checking.

2]  Unità di       Universita' degli Studi di PARMA

     Responsabile Gianfranco ROSSI
     Rd+Ra      M£ 18 , Euro 9296,224 (dichiarata)

     Finanziamento   M£ 38 , Euro 19625,362

     Compito


L'Unita' di Parma si propone di continuare ed approfondire le ricerche inerenti l'analisi di aliasing, la definizione di linguaggi con vincoli insiemistici ed il loro utilizzo nell'analisi di programmi basata su insiemi. Per quanto riguarda l'analisi di aliasing ci si propone di portarla a livelli di precisione ed efficienza superiori a quelli odierni. E` chiaro che l'aspetto della precisione e` molto importante nel campo della certificazione di programmi. Piu` importante di quanto non lo sia, ad esempio, nel campo della compilazione ottimizzata: un fatto e` un'opportunita` di ottimizzazione mancata; altra cosa e` il non riuscire a produrre certificati per i programmi analizzati, richiedendo cosi` l'intervento diretto dell'utente. In questo progetto studieremo l'applicazione dell'analisi di aliasing, mirata alla certificazione di programmi per "agenti mobili" scritti in linguaggi logici (con vincoli). Per quanto riguarda i vincoli insiemistici ci si pone come primo obiettivo lo studio e la definizione di domini astratti di tipo insiemistico e lo sviluppo di techniche di analisi di programmi basate sull'utilizzo di tali domini che permettano di ottenere forme di "set-based analysis" piu' generali e flessibili di quelle attualmente descritte in letteratura. Un ulteriore obiettivo che ci si pone in questo contesto e' lo sviluppo di un linguaggio logico con insiemi che permetta la definizione e manipolazione delle astrazioni insiemistiche previste dalle tecniche di analisi sviluppate al punto precedente, con particolare riferimento alle possibilita' di analisi di soddisfacibilita' dei vincoli insiemistici derivanti dall'applicazione delle tecniche stesse. Infine, utilizzando il linguaggio logico sviluppato, si intende realizzare semplici strumenti di analisi di programmi basati sulle tecniche di "set-based analysis" definite.

3]  Unità di       Universita' "Ca' Foscari" di VENEZIA

     Responsabile Agostino CORTESI
     Rd+Ra      M£ 23 , Euro 11878,509 (dichiarata)

     Finanziamento   M£ 44 , Euro 22724,104

     Compito


Il programma di ricerca di questa unita' si concentrera' sul conseguimento dei seguenti obiettivi. (1) La caratterizzazione delle proprieta' comportamentali di programmi che sono particolarmente significative rispetto alle problematiche di sicurezza, come segretezza, integrita', e autenticita' dei dati, e di certificazione, come l'uso di risorse e consistenza rispetto ai tipi, con particolare enfasi su quelle che possono trarre beneficio da tecniche di analisi statica. (2) La definizione formale delle relazioni tra le diverse tecniche di analisi statica al fine di definire un framework unificante, all'interno del quale tali diverse tecniche possano essere combinate e integrate. (3) Lo studio di opportune semantiche che permettano di catturare diversi modelli di computazione e le loro proprieta'. Questo studio sara' il piu' possibile indipendente da particolari linguaggi. (4) Lo sviluppo di domini che possano approssimare queste proprieta' (per lo piu' indecidibili). La progettazione di domini astratti per l'analisi e la verifica di programmi sara' basata su opportune strutture dati che possano garantire l'efficienza dell'implementazione, ad esempio mediante strutture dati basate su grafi. Come passo successivo, applicheremo a tali domini gli operatori di composizione e scomposizione e gli operatori di confronto, cosi' da fornire gli strumenti per modulare l'accuratezza e l'efficienza dell'analisi a seconda dei diversi contesti di applicazione. (5) Lo sviluppo del prototipo di analizzatori astratti per la certificazione di protocolli e di codice intermedio (bytecode) generato da programmi Java.

4]  Unità di       Universita' di PISA

     Responsabile Roberto BARBUTI
     Rd+Ra      M£ 42 , Euro 21691,190 (dichiarata)

     Finanziamento   M£ 71 , Euro 36668,440

     Compito


L'unita' di Pisa intende partecipare al progetto in particolare nei segienti ambiti di ricerca:
- Studio di nuove classi di proprieta' osservabili utili per la certificazione automatica di programmi dichiarativi, in particolare logici. Si vuole considerare la verifica rispetto al fallimento finito e la verifica di linguaggi concorrenti con vincoli, che possono essere visti come modelli dei linguaggi usati per realizzare processi mobili;
- Studio di metodi di verifica e debugging basati sull'interpretazione astratta per linguaggi funzionali;
- Derivazione sistematica della semantica astratta a partire da una semantica concreta ed un dato linguaggio di asserzioni.
Inoltre Pisa intende studiare il problema di rendere efficiente l'analisi di flusso dei dati. L'analisi del flusso dei dati e' un metodo per verificare proprieta' della computazione di un programma. Queste proprieta' possono essere espresse mediante formule di logica temporale (ad esempio mu-calcolo) che possono essere verificate su un sistema di transizioni che esprime le transizioni di stato corrispondenti alla computazione del programma. Poiche' questo sistema di transizioni puo' essere infinito o estremamente complesso, le proprieta' sono verificate rispetto ad una sua astrazione. L'unita' di Pisa intende sviluppare tecniche di interpretazione astratta al fine di ridurre la struttura del sistema di transizione e al tempo stesso mantenere corretta l'interpretazione delle formule: se una proprieta' e' verificata da un sistema astratto allora e' verificata da quello originale. Verranno anche studiati modelli probabilistici per caratterizare proprieta' di programmi. In questo senso Pisa prevede di estendere l'interpretazione astratta a semantiche con probabilita'.

5]  Unità di       Universita' degli Studi di UDINE

     Responsabile Moreno FALASCHI
     Rd+Ra      M£ 24 , Euro 12394,966 (dichiarata)

     Finanziamento   M£ 47 , Euro 24273,474

     Compito


Intendiamo studiare un framework generale per il debugging dichiarativo di programmi logico funzionali, che sia valido sia per programmi 'eager' che per programmi 'lazy'. Partiremo dai risultati generali sviluppati in letteratura ed all'interno di questo progetto riguardo alla certificazione di sicurezza ed applicheremo tecniche di interpretazione astratta per definire dei metodi per il debugging composizionale di programmi mediante un'approssimazione della loro semantica. Altre due aree in cui il gruppo di Udine sarà attivo sono quelle relative alla soluzione di vincoli ed alla definizione, lo studio, e l'analisi di linguaggi per la specifica e la verifica di sistemi in tempo reale. Per quanto riguarda i linguaggi temporali, Udine prevede lo studio della connessione tra queste idee e la nozione di granularità temporale. Questa nozione, che risulta specialmente adeguata in situazioni in cui si devono prendere in considerazione contemporaneamente scale temporali diverse, sara' studiata dal punto di vista dello sviluppo di adeguati strumenti per l'analisi statica e la verifica automatica di sistemi reattivi. Intendiamo quindi applicare le tecniche di verifica così determinate alla verifica di agenti mobili in sistemi reattivi. Inoltre Udine sviluppera' le possibilità offerte dalla programmazione in un linguaggio logico funzionale per definire codice mobile e contemporaneamente fornire le basi al linguaggio per la specifica delle proprietà da testare, come avviene nel caso dei sistemi proof carrying code (PCC). I vantaggi dovrebbero derivare dal fatto che la componente funzionale permetterebbe la specifica di proprietà in modo simile ai PCC, mentre la componente logica dovrebbe fornire la base per la definizione di appropriati dimostratori di proprietà.