RICERCA ITALIANA     

AIDA2007 - Interpretazione Astratta: Progettazione e Applicazioni

Università degli Studi di Padova

Abstract

Le scienze e tecnologie informatiche devono affrontare la grande sfida di sviluppare metodologie, tecnologie e strumenti adatti alla specifica dei requisiti, alla progettazione di architetture, all’implementazione, alla verifica e al test, all’utilizzo, al mantenimento e alla protezione sia durante il funzionamento che nell’evoluzione di software che sia componibile, affidabile, flessibile, scalabile e robusto. Avanzamenti ed innovazioni scientifiche sono necessari per mantenere e per guadagnare porzioni di mercato. L’astrazione, come formalizzata dall’ interpretazione astratta, è indispensabile nei processi di sviluppo, integrazione, verifica, analisi, testing e protezione del codice. Lo scopo del progetto AIDA2007 –- che è la continuazione del progetto AIDA2004 che raggiunse pienamente gli obiettivi – è di rafforzare la ricerca italiana nell’ambito dell’interpretazione astratta, promuovendo l’interpretazione astratta come tecnologia per la costruzione di sistemi software affidabili. L’interpretazione astratta rappresenta la teoria di base per la progettazione di metodologie e per la costruzione di strumenti in grado si assicurare l’interoperabilità, la composizionalità, la scalabilità, l’affidabilità, la robustezza, la sicurezza e l’auto-adattamento del software. Si è dimostrato come l'interpretazione astratta sia una tecnologia fondamentale per software sequenziale, parallelo (sincrono e asincrono), a vincoli, distribuito e mobile che si trova in sistemi e servizi informatici, siano essi centralizzati, distribuiti o integrati. Recentemente, è stato inoltre dimostrato che l’interpretazione astratta può essere scalata ed applicata anche a complesse applicazioni industriali di grandi dimensioni. AIDA2007 si focalizzerà sullo sviluppo di metodologie fondazionali e su tre filoni di applicazioni: l'analisi statica dei programmi, la protezione del codice e la verifica dei sistemi. Nell’ambito delle metodologie fondazionali, considereremo la progettazione sistematica di domini ottimali per il model checking, la definizione di domini astratti per l’analisi di puntatori e di aliasing per programmi C e Java, la progettazione di domini astratti numerici che siano scalabili e precisi, lo sviluppo di metodi sistematici per misurare la precisione dell’analisi che integrano nei domini astratti dell'informazione probabilistica e statistica, e la definizione di trasformazioni semantiche che permettano di ottenere proprietà di completezza. Per quanto riguarda l’analisi statica di programmi, affronteremo i seguenti problemi: specifica ed analisi di proprietà causali in sistemi concorrenti e distribuiti, ottimizzazione speculativa, analisi di terminazione e complessità di programmi C e Java mediante interpretazione astratta, definizione di astrazioni numeriche modulari, estensione di linguaggi mediante annotazioni nelle fasi di sviluppo e analisi del codice, analisi precise di string cleanness. Nell’ambito della protezione del codice, studieremo il problema di nascondere informazione nei linguaggi di programmazione, con particolare attenzione al software watermarking, alla protezione del copyright, all’offuscamento di codice per impedire il reverse engineering e all’identificazione di malware in presenza di malware metamorfici (ovvero offuscati). Per quanto riguarda la verifica automatica di sistemi, studieremo algoritmi di raffinamento delle astrazioni per il model checking astratto, trasformazioni di linguaggi temporali per ottenere la preservazione forte rispetto ad una data astrazione, e algoritmi efficienti basati su interpretazione astratta per calcolare equivalenze comportamentali in algebre di processi. <<<

Coordinatore Scientifico del Programma di Ricerca

Francesco Ranzato Università degli Studi di PADOVA

Obiettivo del Programma di Ricerca

Lo straordinario sviluppo delle tecnologie hardware e software è all'origine della moderna società dell'informazione e della comunicazione. Promotrici della più grande rivoluzione economica e culturale del secolo scorso, tali tecnologie rappresentano tuttavia il tallone d'Achille della nostra società, perché sia in campo software che hardware requisiti quali affidabilità e sicurezza sono difficili da garantire. Ciò motiva la crescente importanza ed il costo assunti dalla validazione di software e hardware. Gli strumenti tradizionali di validazione hanno tuttavia una scalabilità ridotta e costi sempre maggiori, sono spesso inefficienti, vengono rilasciati lentamente e non garantiscono una qualità ottimale.

L' Interpretazione Astratta è un metodo generale, sia teorico che pratico, per approssimare la semantica del comportamento di un sistema di calcolo. Gli strumenti di validazione del software -- come analisi statica, model checking, type and effect system -- rivelano aspetti unificanti se riformulati in termini di interpretazione astratta. Tali strumenti descrivono in modo sicuro ma approssimato il comportamento di un sistema di calcolo astraendone sistematicamente la semantica, il modello o il programma. L'interpretazione astratta non solo formalizza queste astrazioni, ma ne permette pure il raffinamento e la combinazione, e si pone altresì come base per la modellazione di strumenti per la verifica di tali proprietà a vari livelli di astrazione. Nell'ultimo decennio essa è andata ben oltre i normali circoli accademici, mostrando un ingente potenziale come tecnologia d'avanguardia per le applicazioni industriali. Alcuni esempi: AbsInt (www.absint.com) commercializza aiT, un'applicazione basata su interpretazione astratta che fornisce precise approssimazioni del tempo d'esecuzione di programmi real-time eseguiti su processori di sistemi integrati impiegati nell'industria aeronautica e automobilistica; la componente Polyspace (www.polyspace.com) di MathWorks fornisce uno strumento semantico per l'analisi automatica di software integrato in Ada, C e C++ e il debugging di errori a run-time; l'analizzatore statico Astrée (www.astree.ens.fr) è in grado di verificare automaticamente l'assenza di errori run-time in programmi per il controllo di volo di alcuni aerei civili europei (come l'AIRBUS A380), programmi che sono tipicamente sincroni, real-time e safety-critical, e contano più di 500.000 linee di codice C. Un altro segno dei tempi è il GlobalGCC project (GGCC) nell'ambito dell'ITEA programme (Information Technology for European Advancement), il cui obiettivo è estendere la GNU Compiler Collection (GCC) con tecniche di analisi statica globale. Sebbene i tempi siano maturi, ci sono tuttavia ancora problemi rilevanti da risolvere prima che questa rivoluzione, legata allo sviluppo di software critico, possa estendersi su larga scala.

Lo scopo primario del progetto AIDA2007 è di sostenere la comunità italiana di ricerca sull'interpretazione astratta promuovendo tale metodologia come tecnologia fondamentale per lo sviluppo di software affidabile. Ci proponiamo di mobilizzare, unificare e galvanizzare i ricercatori italiani di interpretazione astratta, creando laboratori virtuali di ricerca pura e applicata guidati dai medesimi obiettivi scientifici. Questo si realizzerà integrando le competenze dei gruppi di ricerca sull'interpretazione astratta già esistenti in Italia, specialmente quelli di Padova, Parma e Verona, che ne sono espressione trainante. L'interpretazione astratta servirà da teoria fondazionale per la progettazione di metodi e strumenti che assicurino interoperabilità, composizionalità, scalabilità, affidabilità, robustezza, sicurezza e auto-adattività del software.

Per quanto riguarda la ricerca di base in interpretazione astratta, siamo interessati allo sviluppo di domini e semantiche astratte. È notorio che le proprietà di un'intepretazione astratta dipendono fortemente dalle proprietà della semantica sottostante e dal tipo di astrazione operata. Noi affronteremo questo problema fondamentale studiando le astrazioni e le semantiche in rapporto alle proprietà che l'interpretazione astratta risultante deve soddisfare. Ciò trova applicazione nella definizione sistematica di domini ottimali per il model checking, di domini astratti per l'analisi di puntatori e di aliasing in C e Java, e di domini astratti numerici precisi e scalabili, oltre che nello sviluppo di metodi sistematici per misurare la precisione di un'analisi mediante informazione probabilistica e statistica e di trasformazioni semantiche che inducano proprietà di completezza. L'aspetto trasversale a questi temi è che tutti si riducono a processi di raffinamento dei domini astratti. La teoria delle trasformazioni dei domini astratti offrirà un'infrastruttura comune tramite la quale arricchire lo stato dell'arte in questo campo con nuovi, efficienti e precisi domini astratti.

Per quanto riguarda le applicazioni, vogliamo esplorare nuove direzioni nell'analisi statica di programmi, nella protezione del codice e nella verifica di sistemi. Nell'analisi statica di programmi, perlustreremo nuove idee desunte dall'analisi di complessità e terminazione di codice C e Java, e dall'analisi di dipendenze causali. Studieremo tecniche per provare automaticamente la terminazione o per maggiorare la complessità di frammenti di programma sfruttando opportune informazioni di natura metrica nei domini astratti. Un tale approccio, basato sulla teoria dei domini, ci consentirà di modellare le dipendenze causali fra azioni di processi in sistemi concorrenti e distribuiti, soprattutto nel CCS e nel pi-calculus, in termini sia della loro architettura spaziale, sia delle loro capacità di comunicazione. Mentre l'analisi statica è un ambito ben definito in cui l'interpretazione astratta gioca un ruolo chiave da decenni, ciò non accade nella verifica di sistemi e nell'emergente settore della protezione del codice. Nella verifica di sistemi siamo interessati ad algoritmi per il raffinamento delle astrazioni, alla trasformazione di linguaggi temporali e ad algoritmi efficienti per calcolare equivalenze comportamentali. Intendiamo studiare come sia possibile applicare l'interpretazione astratta nel contesto dei raffinamenti di astrazione guidati da controesempi, e per progettare algoritmi più accurati per il raffinamento di astrazioni nel model checking astratto. Studieremo simmetricamente le trasformazioni di linguaggi temporali che permettano di eludere i controesempi spuri. Nell'ambito della protezione del codice, considereremo i rischi connessi agli attacchi perpetrati sia da host che da software maligni. Gli host maligni tipicamente ricercano nei programmi dati confidenziali, usano analisi statiche e dinamiche per estrarne informazioni, li decompongono per riutilizzarne il codice, ne corrompono l'integrità. I software maligni sfruttano le falle di altri programmi per inserirvi funzionalità maligne. Gli host maligni sono i maggiori responsabili della pirateria informatica. Contro di essa e contro la reverse engineering maligna, strumenti come software watermarking e offuscamento del codice si pongono come adeguate tecniche di difesa. Intendiamo delineare nuove e robuste tecniche di software watermarking e offuscamento del codice basate su interpretazione astratta. Queste tecniche, oltre ad ostacolare la reverse engineering e la violazione del copyright, offriranno una teoria fondazionale agli attacchi del software maligno. La minaccia rappresentata da questi software è una sfida attuale alla sicurezza dei sistemi informatici. Intendiamo pertanto introdurre, accanto all'attuale riconoscimento sintattico del software maligno, algoritmi di rilevazione basati sulla semantica e sulle sue proprietà. <<<

Risultati parziali attesi

L'intento della proposta di progetto AIDA2007 è l'avanzamento dello stato dell'arte sull'interpretazione astratta (IA), sia dal punto di vista fondazionale, che da quello applicativo. Ciò avverrà tramite lo studio di specifici "Task" all'interno dei quattro WP che costituiscono AIDA2007. Vengono descritti nel seguito i risultati attesi da ogni singolo Task.

WP1: Progettazione di Interpretazioni Astratte

- Task PD-1.1: Domini astratti per il model checking
I domini astratti disgiuntivi risultano molto utili nel model checking astratto, e.g. nella predicate abstraction [MFHRS06] e negli algoritmi per il calcolo di equivalenze comportamentali [RT07b]. Intendiamo studiare come questi domini possano essere usati negli algoritmi di abstraction refinement. Poiché i domini astratti disgiuntivi sono caratterizzabili in termini di domini astratti completi per l'unione di insiemi, ci attendiamo di caratterizzare anche classi di domini astratti completi che possano essere vantaggiose per l'abstract model checking, e.g. domini astratti completi per qualche operatore temporale.

- Task PR-1.1: Domini astratti per l'analisi dei puntatori e dell'aliasing in programmi C e Java
L'approccio di [EGH94] alla stack pointer analysis di programmi C permette di definire un'analisi dipendente dal contesto e/o dal flusso capace di catturare l'aliasing sia potenziale che effettivo. La specifica in [EGH94] è piuttosto informale e rende quindi difficile un ragionamento rigoroso sulla correttezza e precisione dell'approccio proposto. Intendiamo riprogettare, formalizzare e implementare una variante di quel dominio, considerando in particolare come semantica concreta di riferimento quella specificata dallo standard del linguaggio C.
Per l'analisi di aliasing di programmi Java, individueremo un framework concettuale comune che inquadri le proposte che si trovano in letteratura. Riformuleremo le varianti più note di analisi di aliasing e di shape come astrazioni di una stessa semantica denotazionle, sensibile al flusso di esecuzione a al contesto. Ci aspettiamo di riuscire a confrontare formalmente i vari approcci, e di distinguere la rappresentazione tramite domini astratti delle strutture dati dinamiche dagli algoritmi per il calcolo del comportamento astratto.

- Task PR-1.2: Domini astratti scalabili a precisi
Esiste un'ampia letteratura sui domini astratti numerici: da semplici proprietà non relazionali a domini che codificano proprietà relazionali complesse. La questione è come avvicinarsi all'efficienza e scalabilità dei domini più semplici ottenendo una precisione simile a quella dei domini più complessi. Gli studi attuali esplorano lo spazio esistente tra gli estremi sopra menzionati cercando dei compromessi. In questo Task intendiamo progettare (1) operatori approssimati sui domini esistenti e (2) nuove combinazioni di domini esistenti e dei corrispondenti operatori per integrarli efficacemente.

- Task VR-1.1: Trasformazioni semantiche orientate alla completezza.
Ci aspettiamo come risultati: (1) La chiusura del problema della completezza in IA, affiancando i trasformatori di semantiche ai ben noti trasformatori di domini astratti; (2) Poiché trasformare semantiche significa trasformare programmi, l'aver reso completa una semantica implica che il corrispondente programma è stato sottoposto ad una deformazione la cui IA è completa; (3) Il problema duale di rendere la semantica il più possibile incompleta corrisponderà a massimizzare la capacità del programma deformato ad includere watermark.

- Task VR-1.2: Misura di precisione basata su domini numerici.
Studieremo la struttura del reticolo delle IA probabilistiche 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 valore che esprime la precisione relativa. Un aspetto importante sarà 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.


WP2: Analisi Statica mediante Interpretazione Astratta

- Task PD-2.1: Semantiche causali di sistemi concorrenti e distribuiti
Abbiamo sviluppato in [CVY07] una semantica composizionale basata su strutture ad eventi per il pi-calculus interno che cattura le dipendenze causali generate dal "name passing" sia sincrono che asincrono. Estenderemo questo approccio al "free name passing" per ottenere una semantica denotazionale fully abstract per il full pi-calculus. Studieremo inoltre semantiche composizionali simili per linguaggi imperativi multithreaded che, rispetto alle algebre di processi, si focalizzano sullo stato piuttosto che sul controllo di un thread.

- Task PD-2.2: Analisi statica di proprietà causali
La letteratura propone diverse nozioni di equivalenza su strutture ad eventi. Ci aspettiamo di individuare caratterizzazioni logiche di alcune di queste equivalenze, indagando in particolare sulle relazioni tra l'osservazione di distribuzione esprimibile mediante logiche spaziali per il pi-calculus e quella esprimibile tramite strutture ad eventi.
Il problema del model checking su strutture ad eventi è intrinsecamente ostico, poiché in generale queste strutture sono modelli infiniti anche per processi con un numero finito di stati. Ci aspettiamo che l'approccio dell'IA al model checking possa essere applicato con successo all'abstract model checking di strutture ad eventi.

- Task PR-2.1: Definizione di uno schema di analisi modulare e generico
Studieremo i problemi collegati al progetto e all'implementazione di uno schema generico di analizzatori statici per i linguaggi imperativi di largo uso, che sarà istanziato su analisi dei puntatori e dei valori delle variabili numeriche e booleane. Le innovazioni principali di questo schema saranno la flessibilità e la generalità, sia in termini delle proprietà che in termini del linguaggio analizzato.

- Task PR-2.2: Annotazione di programmi
Studieremo la specifica di un linguaggio di asserzioni che consenta al programmatore di codificare nel programma le condizioni logiche che garantiscono che lo stesso sia immune da una certa classe di errori e/o rispetti i limiti imposti dalle politiche di allocazione delle risorse. La presenza di un linguaggio di asserzioni espressivo sarà sfruttata anche per abilitare la comunicazione dall'analizzatore al programmatore. Il risutato atteso è un ambiente di sviluppo fortemente integrato, dove il feedback derivante dal confronto delle proprietà attese e quelle calcolate permetterà un processo di raffinamento sinergico, con benefici sia per lo sviluppo che per il debugging delle applicazioni.

- Task PR-2.3: Analisi di correttezza della manipolazione di stringhe
Studieremo un approccio trasformazionale al problema di assicurare la correttezza delle operazioni sulle stringhe nei programmi C. L'approccio consiste nel trasformare un programma P che usa stringhe, in un'altro, P', dove gli array di caratteri e i puntatori sono sostituiti da strutture ad hoc e dove sono state inserite delle asserzioni. La trasformazione (1) sarà completamente automatica e (2) tale che, se P' non può violare nessuna delle sue asserzioni, allora ogni esecuzione di P sarà esente da errori nella manipolazione delle stringhe. Le stringhe saranno sostituite da strutture che astraggono la loro semantica per mezzo di variabili intere e booleane. L'idea nasce dai lavori di Dor, Ellenbogen, Rodeh e Sagiv [DRS01, DRS03].

- Task PR-2.4: Analisi di terminazione e complessità
Ci attendiamo di progettare un'analisi di terminazione e complessità per il codice C nel modo seguente:
1) Identificazione dei cicli nel controllo: Si identificano le sorgenti di possibile non terminazione: cicli espliciti, chiamate di funzione ricorsive e salti all'indietro.
2) Identificazione dei cicli nei dati: sfruttando l'analisi dei puntatori viene analizzata la ciclicità delle strutture dati. Questa informazione servirà nel passo 3.
3) Generazione di vincoli: a) sui valori delle variabili numeriche; b) sulla lunghezza massimale di un percorso di puntatori seguito a partire da ciascuna variabile (path-length analysis).
4) Sintesi di funzioni di ranking: i vincoli generati vengono elaborati con tecniche automatiche che cercano di identificare una funzione di terminazione (norma) per il programma.

- Task VR-2.1: Analisi statica di terminazione e complessità
Ci aspettiamo di migliorare ed estendere i nostri tool Julia e BinTerm. Attulamente, la nostra analisi di terminazione basata su Julia e BinTerm è in grado di provare la terminazione di piccoli programmi Java bytecode, anche con strutture dati. L'analisi sarà estesa a programmi realistici. Per questo intendiamo migliorare le analisi preliminari rendendole più veloci e precise. Ci aspettiamo di incrementare l'efficienza della Parma Polyhedra Library considerando la forma speciale dei nostri poliedri, dove molte variabili di input e output mantengono lo stesso valore. Ci aspettiamo di sviluppare un'analisi statica di sharing, ciclicità e path-length nel caso di programmi Java concorrenti, e di integrare l'esistente analisi di terminazione con dimostrazioni automatiche di assenza di deadlock.

- Task VR-2.2: Ottimizzazione speculativa
La parallelizzazione del codice rappresenta un problema difficile: 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, si 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. Ci aspettiamo di applicare l'IA probabilistica per supportare questo approccio "ottimistico".


WP3: Protezione del Codice mediante Interpretazione Astratta

- Task VR-3.1: Generalizzazione di firme
Ci aspettiamo di sviluppare un metodo di generalizzazione della firma che riconosca anche le varianti metamorfiche. Consideriamo un EFSA (Extended Finite State Automaton) S che modella la firma e un possibile offuscamento O utilizzato da un hacker. Se il modello dell'EFSA è chiuso rispetto ad O, allora la generalizzazione dovrebbe restituire l'insieme di tutti i possibili EFSA che possono essere ottenuti da S attraverso O, e questo può essere usato per identificare le varianti metamorfiche originate da O. La classe di trasformazioni per cui EFSA è chiuso corrisponde alla classe di offuscamenti che la generalizzazione può gestire.

- Task VR-3.2: Predicate obfuscation
Siamo interessati alla possibilità di nascondere una specifica proprietà di un particolare programma (o classe di programmi). Vogliamo studiare l'esistenza di trasformazioni di codice, dette predicate-obfuscation, che cercano di proteggere uno specifico tipo di informazione di un certo programma (o classe di programmi). Ci aspettiamo quindi di caratterizzare la classe di predicati che è possibile nascondere in modo da precisare le potenzialità e i limiti dell'offuscamento.

- Task VR-3.3: Inserimento di software watermark in cicli
Intendiamo inserire, all'interno di un ciclo, dei watermark calcolati iterativamente. Ciò si attua dispiegando interamente il ciclo e cercando l'iterazione più adeguata per l'inserimento del watermark, detta iterazione promotrice. 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.

- Task VR-3.4: Nascondere watermark in lacune di completezza
Offuscamento e incompletezza sono concetti profondamente legati: mentre la steganografia può essere vista come il nascondere informazione in lacune di completezza, l'offuscamento può essere visto come il trasformare programmi in modo che le uniche astrazioni complete utilizzabili dagli osservatori siano molto costose, ad esempio analisi relazionali o esponenziali sul numero di variabili. Basandoci su questa idea, ci attendiamo di sviluppare una nuova famiglia di metodi e strumenti perla stenografia che siano ben definiti e dimostrabilmente sicuri, e piu` in generale per l'offuscamento. Ci aspettiamo di mostrare che molte tecniche di software watermarking sono casi speciali di inserimento di watermark basato sull'incompletezza dell'osservatore. Siamo interessati allo studio di attacchi passivi e attivi e utilizzeremo i risultati del Task VR-1.1 per fornire un modello per questi comportamenti.


WP4: Verifica di Sistemi mediante Interpretazione Astratta

- Task PD-4.1: Algoritmi di raffinamento di astrazioni
I model checker basati sulla tecnica dei raffinamenti di astrazioni guidati da controesempi (CEGAR, dall'acronimo inglese) considerano come controesempi dei cammini di stati astratti. Recentemente, Cousot, Ganty e Raskin [CGR07] hanno introdotto un algoritmo di raffinamento di astrazioni CGR che è guidato da punti fissi astratti piuttosto che da controesempi astratti. Intendiamo studiare se e come l'approccio generale dell'IA possa essere applicato in questo contesto. Ci aspettiamo di generalizzare la metodologia CEGAR a generici modelli astratti specificati tramite IA ed a generici linguaggi di specifica. Intendiamo inoltre studiare il ruolo dei domini astratti completi negli algoritmi di raffinamento di astrazioni. Ci aspettiamo che i raffinamenti di completezza possano essere utili per progettare o migliorare gli algoritmi di raffinamento di astrazioni, in particolare nel caso degli algoritmi guidati da punti fissi come l'algoritmo CGR.

- Task PD-4.2: Trasformazioni di linguaggi
Dato un modello astratto A, intendiamo studiare il problema di modificare sistematicamente, attraverso raffinamenti o semplificazioni minimali, gli operatori che definiscono qualche linguaggio L (e.g. OR e AU) con lo scopo di ottenere un linguaggio trasformato L' che sia tale che l'abstract model checking su A sia strongly preserving per L'. A questo scopo useremo tipiche tecniche di IA, in particolare raffinamenti e semplificazioni di domini astratti. Intendiamo applicare tale metodo al problema "branching vs linear" nel potere espressivo dei linguaggi temporali. Generalizzando la caratterizzazione in [Mai00], ci aspettiamo di trasformare sistematicamente LTL in un sotto-linguaggio massimale L' che caratterizza il potere espressivo branching di ACTL.

- Task PD-4.3: Algoritmi di calcolo di equivalenze comportamentali
Abbiamo recentemente individuato un nuovo algoritmo di calcolo dell'equivalenza di simulazione [RT07b] che migliora la complessità di tempo sinora conosciuta. Questa procedura si appoggia su tipici strumenti dell'IA come i raffinamenti di domini astratti e i domini astratti disgiuntivi. Una valutazione sperimentale ha inoltre dimostrato l'effettività pratica di questo algoritmo. Ci aspettiamo: (1) una versione simbolica efficiente di questo algoritmo, basata su BDDs e (2) una generalizzazione delle tecniche usate per questo nuovo algoritmo che permetta l'adattamento ad altre equivalenze comportamentali come la branching bisimulation.
<<<

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

L' interpretazione astratta è una ben nota teoria generale ed unificante per l'approssimazione della semantica formale di sistemi computazionali. Inventata da Cousot e Cousot [CC77, CC79] alla fine degli anni '70 come framewok unificante per progettare e validare analisi statiche di programmi, l'interpretazione astratta ha guadagnato sempre maggiore popolarità come metodologia generale per la descrizione e la formalizazione di computazioni approssimate in aree molto diverse dell'informatica come l'analisi statica di programmi, la trasformazione di programmi, la verifica di sistemi e programmi via model checking, i sistemi di tipi, l'analisi di sistemi mobili e distribuiti, la sicurezza, il constraint solving, etc. Come notevole recente esempio di applicazione dell'interpretazione astratta, ASTRÉE (http://www.astree.ens.fr/) è un analizzatore statico di programmi strettamente basato sulla teoria dell'interpretazione astratta che è riuscito a verificare formalmente l'assenza di errori a run-time nel software di controllo volo primario del sistema fly-by-wire dell'Airbus A340 (132,000 linee di codice C piuttosto peculiare). Ci stiamo avvicinando al punto in cui verranno inseriti analizzatori statici basati su interpretazione astratta negli ambienti di sviluppo dei principali linguaggi imperativi.

Gli obiettivi del progetto AIDA2007 sono strutturati in quattro WorkPackage (WP) che si focalizzano su precisi aspetti della progettazione e delle applicazioni dell'interpretazione astratta.

WP1: Progettazione di Interpretazioni Astratte
WP2: Analisi Statica mediante Interpretazione Astratta
WP3: Protezione del Codice mediante Interpretazione Astratta
WP4: Verifica di Sistemi mediante Interpretazione Astratta

I membri di AIDA2007 sono ben noti nella comunità internazionale di interpretazione astratta e posseggono un notevole background ed esperienza di ricerca su progettazione e applicazioni dell'interpretazione astratta, in particolare sugli argomenti dei quattro WP di AIDA2007.

WP1: Progettazione di Interpretazioni Astratte

I primi lavori di Cousot e Cousot [CC77, CC79] hanno gettato le fondamenta per una teoria dei domini astratti e dei trasformatori di domini astratti. Dopo questi lavori fondazionali, sono stati definiti numerosi operatori aventi lo scopo di migliorare la precisione, ridurre la complessità e decomporre i domini astratti in modo sistematico [CFGPR97, FGR96, GR97, GR99]. La completezza gioca un ruolo chiave in interpretazione astratta, ed in particolare in molti problemi riguardanti i raffinamenti di domini astratti. Le astrazioni complete possono sempre essere ottenute costruttivamente come mimini raffinamenti completi e massime semplificazioni complete di un generico dominio astratto [GRS00]. I corrispondenti trasformatori semantici, ovvero trasformazioni della semantica osservazionale che la rendono completa rispetto ad una certa astrazione, sono sinora sconosciuti. Recentemente la completezza è stata usata per modellare la non-interferenza e la perdita di informazione: "What you lose in precision is what you leak in observation" [BGM07, GM05]. Questi risultati si basano sulla generalizzazione mediante interpretazione astratta della nozione di non-interferenza di Goguen e Meseguer [GM84] che ha portato alla nozione di non-interferenza astratta [GM04]. Il più potente attaccante innocuo e la massima informazione rilasciata da un programma sono stati caratterizzati come trasformatori di domini astratti. Uno sforzo sostanziale nell`ultima decennio è stato anche dedicato al problema di raffinare in modo sistematico i domini in abstract model checking e in predicate abstraction [BPR02, BCDR04]. I membri di AIDA2007 hanno studiato varie problematiche collegate al problema di ottenere strong preservation in abstract model checking attraverso raffinamenti di domini astratti [GQ01, RT04, RT05a, RT06, RT07a].

L'analisi dei puntatori e dell'aliasing per i linguaggi imperativi è un passo importante, a volte essenziale, per migliorare la precisione di numerose altre analisi. Nonostante la vasta letteratura sull'argomento, ad oggi è difficile ottenere risultati sufficientemente precisi utilizzando una quantità ragionevole di risorse di calcolo [Ber07, Hin01]. Le analisi dei puntatori attualmente in uso per la compilazione ottimizzata, essendo indipendenti dal contesto e dal controllo di flusso, non forniscono un livello di precisione sufficiente ai fini della verifica dei programmi. D'altra parte, le analisi dipendenti da contesto e/o dal flusso proposte in letteratura non catturano tutti i costrutti di linguaggi come il C [Ber07], oppure sembrano essere state abbandonate [Deu94, EGH94]. I risultati preliminari sull'analisi di proprietà numeriche per programmi C realistici hanno mostrato l'esistenza di problemi di precisione e scalabilità. Se l'uso indiscriminato del dominio dei poliedri convessi impedisce la scalabilità, d'altra parte il ricorso al dominio degli intervalli o anche degli ottagoni può a volte portare ad un numero inaccettabile di falsi allarmi (ad es., per l'analisi di "string cleanness"). Una soluzione a tali problemi è quindi di primaria importanza.

WP2: Analisi Statica mediante Interpretazione Astratta

I difetti del software contribuiscono in maniera significativa al suo costo totale di sviluppo [RTI02], in particolare se individuati dopo la fase di rilascio del prodotto. I difetti dalle conseguenze più costose sono quelli che introducono vulnerabilità di sistema. A tal proposito, l'analisi sistematica di migliaia di segnalazioni ha permesso al CERT, l'autorevole ente che opera nel campo della sicurezza informatica (http://www.cert.org/), di evidenziare come, alla base dei problemi di sicurezza più comuni, vi sia un numero limitato di cause. Il caso più frequente è quello di errori di programmazione quali overflow durante l'accesso ai buffer o nei calcoli sui tipi interi, errori nella formattazione di stringhe ed altri errori nella gestione della memoria. È quindi necessario studiare, da un lato, metodologie di progettazione del software che aiutino a prevenire tali problemi, dall'altro, strategie di validazione del software che, tenendone conto, siano di supporto ad una loro efficace individuazione e rimozione. Naturalmente, un prodotto software immune da errori come quelli precedentemente menzionati potrebbe comunque avere altri difetti che influiscono sulla sua funzionalità ad un più alto livello di astrazione. In ogni caso, l'assenza degli errori "di basso livello" è un prerequisito irrinunciabile, mancando il quale qualunque analisi svolta ai livelli superiori non fornirebbe alcuna reale garanzia. Per favorire le ricadute a livello pratico, AIDA2007 focalizzerà l'attenzione sui linguaggi imperativi più diffusi, come C (con possibili estensioni a C++) e Java.

La maggior parte delle vulnerabilità presenti nei programmi C ha origine da errori di manipolazione di stringhe; l'assenza di tali errori ("string cleanness") è un prerequisito per la scrittura di programmi che abbiano un comportamento prevedibile e robusto. I programmi C sono particolarmente soggetti a tali errori per via dell'assenza di un tipo di dato stringa predefinito. Sebbene vi siano alcune analisi statiche per il rilevamento dei buffer overflow, molto lavoro rimane da fare per renderle efficaci [DRS03, Ell04]. L'analisi di terminazione per programmi C è un argomento di ricerca di primaria importanza. Il linguaggio C è ampiamente usato per lo sviluppo di dispositivi embedded, spesso caratterizzati da elementi di criticità (ad es., nell'automazione industriale) e per i quali la terminazione di ogni componente funzionale è una proprietà essenziale. Un dispositivo che mantiene una data interazione con l'ambiente può essere modellato da un ciclo composto da alcune fasi (lettura sensori, calcolo della reazione appropriata, invio dei comandi agli attuatori), per le quali la mancata terminazione sarebbe causa di malfunzionamenti gravi quanto un fallimento di sistema. Un altro esempio è fornito dai driver dei dispositivi hardware, la cui mancata terminazione può causare lo stallo del sistema operativo. È anche per questa ragione che, al fine di semplificare la verifica automatica dei driver del proprio sistema operativo, Microsoft ha iniziato un progetto di ricerca sull'analisi di terminazione dei programmi C [CPR06]. Assicurata la terminazione, il passo logico successivo è costituito dall'analisi di complessità, che consente di garantire, ad esempio, il rispetto delle scadenze temporali da parte dei sistemi software. Terminazione e complessità sono state studiate per programmi imperativi, ristretti a valori primitivi [CPR06, GST06] o nel caso di programmi iterativi numerici attraverso l'espressione della semantica dei programmi in forma polinomiale [C05]. L'estensione di questi metodi a programmi che usano dati allocati sullo heap e aggiornamenti distruttivi complessi rappresenta una grande sfida. Sviluppi recenti forniscono un modello preciso dello heap, con pair-sharing [SS05] e cyclicity [RS06], che è ora implementato in Julia [Sp05] sfruttando PPL [BHZ06]. Analogamente, l'analisi di complessità di linguaggi Java-like determina le classi di complessità dei metodi basandosi sull'induzione [AAGPZ07].

Gli approcci quantitativi all'analisi dei programmi hanno lo scopo di sviluppare tecniche che forniscono risposte approssimate dotate di una stima numerica dell'approssimazione introdotta. L'interpretazione astratta probabilistica [DW01] ridefinisce l'interpretazione astratta classica in un contesto probabilistico, fornendo, oltre all'analisi del caso pessimo [M00], anche l'analisi del caso medio [DHP06]. In interpretazione astratta probabilistica i domini sono spazi lineari normalizzati, l'astrazione è definita attraverso operatori lineari e la concretizzazione attraverso la nozione di un'inversa lineare generalizzata. La vicinanza metrica fornisce una stima numerica quantitativa della precisione dell'astrazione.

AIDA2007 si interesserà anche allo sviluppo di tecniche di analisi statica basate su modelli causali di sistemi concorrenti e distribuiti. In particolare, nel contesto delle algebre di processi, i modelli non interleaving per CCS e il pi-calculus sono stati formalizzati come reti di Petri, sistemi di transizione etichettati generalizzati e strutture ad eventi [Win82, CVY07]. Inoltre, i lavori [BS98, DP99, Cas95] mostrano come sia possibile usare le equivalenze comportamentali per catturare le dipendenze tra le azioni dei processi, sia in termini della loro struttura spaziale che delle loro capacità di comunicazione.

WP3: Protezione del Codice mediante Interpretazione Astratta

L'offuscamento e la steganografia di software sono tecnologie emergenti per la protezione della proprietà intellettuale del codice [CTL98, CT02]. In base alla natura del processo di estrazione, le metodologie esistenti per la steganografia (watermarking, fingerprinting e birth-marking) sono classificate come statiche e dinamiche [NCT02]. La distinzione tra statico e dinamico è spesso troppo grossolana per modellare accuratamente gli attaccanti, che potrebbero combinare analisi statica e dinamica ed utilizzare altri metodi d'analisi come model checking e interpretazione astratta [CC04]. Un noto risultato negativo dimostra l'impossibilità dell'offuscamento [B01], assumendo che il programma originale e quello trasformato abbiano comportamenti identici e che ogni programma offuscato diventi incomprensibile rispetto ad ogni attaccante. Nella realtà questi vincoli sono spesso rilassati. Metodologie pratiche per rendere difficile il reverse engineering possono confondere la fase di disassembly [LD05] o quella di decompilazione [CT98, CTL98]. In [DPG04] si può trovare un primo tentativo di dare un fondamento semantico all'offuscamento del codice. L'idea è che un offuscamento nasconde tutte quelle proprietà che non sono preservate dalla trasformazione. Questo approccio è stato applicato all'inserimento dei predicati opachi [DPG05, DPG06] dove la capacità di un attaccante nel riconoscere i predicati opachi è ridotta ad un problema di completezza dell'astrazione che modella l'attaccante [DPG05, DPG06]. Tipicamente un programma è classificato come infetto da un malware se esso contiene la firma del malware, cioè la sequenza di istruzioni che lo caratterizzano [Szor05]. Gli algoritmi basati sulle firme sono in grado di identificare malware conosciuti ma non nuovi malware o l'offuscamento di malware metamorfici [N97], dove ogni offuscamento cambia la sintassi del malware in modo da cambiarne la firma [J02, SF01]. Allo scopo di resistere al metamorfismo sono stati recentemente proposti: un identificatore di malware che tiene conto della semantica [CJ2005], un identificatore di malware basato su model checking [K05] e un identificatore di malware con firme semantiche basato su interpretazione astratta [DCJD2007].

WP4: Verifica di Sistemi mediante Interpretazione Astratta

Uno degli obiettivi di AIDA2007 è l'applicazione dell'interpretazione astratta alla verifica automatica basata su model checking [CES86, CGP99]. In particolare, siamo interessati allo studio della relazione tra interpretazione astratta e abstract model checking. L'approccio dell'abstract model checking [CGL94, CGP99] fornisce una soluzione al problema fondamentale della scalabilità del model checking, il ben noto problema dell'esplosione esponenziale degli stati [CGP99]. La metodologia comune di qualunque tecnica di abstract model checking è di eseguire l'algoritmo di verifica su un modello astratto ridotto A che approssima alcune proprietà di interesse del sistema concreto M. Idealmente, il modello astratto ridotto A dovrebbe essere fortemente preservante: una formula di specifica f vale su M se e solo se f vale nel modello astratto A. D'altronde, molti modelli astratti non sono fortemente preservanti [CGP99]. Quindi, la presevazione forte viene ottenuta mediante operazioni di raffinamento di un modello astratto approssimato iniziale. La soluzione standard al problema della preservazione forte consiste in raffinamenti del modello astratto che sono guidati da una specifica formula. In questo contesto, il raffinamento di astrazioni guidato da controesempi (CEGAR, dall'acronimo inglese), proposto dal gruppo di ricerca di Clarke [CGJLV03], è divenuto la metodologia standard. Esempi ben noti di model checker basati sull'approccio CEGAR sono BLAST [HJMS03], MAGIC [CGJLV03] e SLAM [BR02]. La relazione tra interpretazione astratta e abstract model checking è già stata studiata sotto vari aspetti [CC99, CC00, CGL94, DGG97], ed in particolare i membri di AIDA2007 hanno studiato la relazione tra preservazione forte in abstract model checking e completezza in interpretazione astratta [GR06, RT04, RT05a, RT06, RT07a].

Nota: Le citazioni bibliografiche in ogni sezione del presente Modello A si riferiscono alla bibliografia inserita nei Modelli B delle tre unità di ricerca. <<<