RICERCA ITALIANA     

Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile

Abstract

Coordinatore Scientifico del Programma di Ricerca

Obiettivo del Programma di Ricerca

Obiettivi e approccio
Lo scopo del progetto è di far progredire lo stato dell'arte sulle tecniche proprie della teoria della concorrenza per l'analisi e la verifica del software, estendendole in modo da renderle efficaci sia nell'analisi di proprietà complesse, sia in presenza di ipotesi più deboli sulle componenti del sistema. Ad alto livello gli obiettivi del progetto hanno una doppia valenza ed includono:

. lo sviluppo di nuovi modelli astratti per descrivere computazioni distribuite in sistemi con mobilità. Questi modelli saranno basati su calcoli di processo e forniranno la base per condurre analisi formali sull'esecuzione e sulla mobilià del codice, sull'esplorazione del contesto di esecuzione, descritte in termini delle proprietà osservabili rilevanti in tali computazioni.
. lo sviluppo di tecniche formali, basate su sistemi di tipo e teorie logiche, per la specifica e verifica del comportamento di programmi concorrenti. Tali tecniche dovranno rendere possibile esprimere le politiche di autorizzazione per la migrazione del codice in ambienti computazionali remoti, e allo stesso tempo permettere il controllo dei meccanismi di accesso, protezione, negoziazione ed utilizzo delle risorse disponibili in tali ambienti.

Il nostro approccio sarà incentrato sullo sviluppo dei fondamenti teorici alla base delle tecniche di specifica ed analisi, con lo scopo di identificare nozioni unificanti e produrre strumenti formali flessibili e adattabili. Allo stesso tempo, svolgeremo una attività complementare di ricerca su casi di studio per valutare i risultati teorici, il loro progresso e la loro adeguatezza.

Sul piano delle tecniche, la nostra ricerca si fonderà su modelli operazionali e sistemi "proof theoretic". La ricerca nell'area della teoria della concorrenza ha da tempo prodotto strumenti potenti per ragionare sul comportamento "contestuale" di processi concorrenti, e per analizzare e specificare il loro comportamento tramite tipi e sistemi logici. Negli anni questi strumenti hanno trovato una sempre più ampia applicazione nei calcoli di processi del prim'ordine e, in una certa misura, anche nei calcoli con mobilità di nomi come il pi-calcolo. Nella presente proposta, intendiamo estendere le tecniche esistenti a processi e sistemi le cui componenti siano mobili, distribuite, possibilmente non fidate. Proponiamo l'uso di tipi e formule logiche come interfacce, o come contratti, che esprimano e regolino la negoziazione per l'acquisizione delle risorse tra i processi e gli ambienti circostanti. L'uso di caratterizzazioni logiche e coinduttive delle corrispondenti equivalenze comportamentali fornirà la base per l'analisi formale degli effetti osservabili dell'esecuzione dei processi. Saranno richieste tecniche innovative per fornire adeguate caratterizzazioni dell'uso e della gestione delle risorse - limiti, protezione, autorizzazione, confinamento. Analogamente, nuove tecniche saranno necessarie per formalizzare meccanismi che consentano al codice cliente di scoprire/acquisire le sue risorse, spostandosi in una rete distribuita con connettività e struttura dinamiche, e con diritti di accesso/autorizzazioni ugualmente dinamici.
L'analisi statica, basata sui tipi e su sistemi logici è la soluzione che proponiamo per rendere sicure ed efficienti computazioni che devono adattarsi sulla base delle informazioni relative al loro contesto. Questa analisi contribuirà a dotare il codice cliente di certificati verificabili che ne dimostrino la conformità alle politiche di controllo dell'ambiente ospite in merito a diversi aspetti, che vanno da garanzie di segretezza e integrità dei dati, a garanzie di uso limitato delle risorse di sistema.

Le tecniche e gli strumenti di verifica sviluppati nel progetto verranno valutati su un insieme di casi di studio. Se da un lato l'identificazione dei casi di studio costituisce di per sè oggetto di studio, abbiamo al momento già identificato due esempi significativi. Il primo riguarda la specifica ed analisi di protocolli per la comunicazione e l'instradamento in reti wireless "ad hoc". Se da un lato le reti "ad hoc" sono interessanti di per sè per la loro natura profondamente dinamica, dall'altro i protocolli di instradamento in tali reti sono rilevanti all'interno del progetto poiché, vista la loro natura tipicamente cooperativa, essi richiedono la capacità di stabilire adeguate forme di "trust" tra i partecipanti all'instradamento e, dualmente, di proteggersi da componenti verso le quali non è disponibile sufficiente informazione per stabilire adeguati livelli di trust. Il secondo scenario riguarda la pratica, sempre più comune tra gli utenti, di scaricare codice remoto per mandarlo in esecuzione sui propri dispositivi (portatili o palmari). Nell'ambito del progetto, studieremo tecniche per rilevare attacchi di vario tipo, da attacchi alla sicurezza ed integrità dei dati, ed attacchi di tipo "denial-of-service" da parte di agenti ostili che degradano le prestazioni del sistema ospite sovra-utilizzandone le risorse.

Lo scopo dei casi di studio è duplice. Da una parte, permetterà di stimolare il lavoro sulle techniche di specifica e di analisi fornendo problemi specifici. Dall'altro lato, fornirà un indicatore misurabile per valutare il progresso del progetto e la qualità dei suoi risultati.

Per una descrizione dettagliata delle attività di progetto è si rimanda alla sezione "workplan" della proposta. <<<

Durata

Base di partenza scientifica nazionale o internazionale

Sistemi di tipo


Negli ultimi anni le problematiche legate al controllo delle risorse e della mobilità , in forme diverse, sono state un tema cardine della ricerca di base nella teoria dei tipi. Gli argomenti considerati comprendono l'analisi di aspetti quali: l'abilità di leggere da / scrivere su un canale [PS96], il controllo della distribuzione dei nomi dei canali [YH99], la garanzia che gli agenti mobili utilizzeranno le risorse solo dopo essere stati autorizzati [HR02,DFPV00,BC01,HMR03], il controllo dell'interferenza [LS03], il controllo della mobilità degli agenti eventualmente basata su permessi specificati mediante tipi [DS00,MS02,CGG02,CDGS03], le garanzie di safety per gli scambi all'interno di ambienti di calcolo locali [CGG02], la segretezza di tali scambi [CGG00], il controllo della diffusione e condivisione di informazioni basato sul contenuto e sul contesto [Mye99,CDV03].
La maggior parte dei sistemi suddetti, con poche eccezioni, si fonda su tecniche di tipizzazione classiche nelle quali ad ogni componente del sistema è assegnato un tipo sulla base di assunzioni stabilite a livello globale. Questo approccio nonè certamente realistico in ambienti distribuiti e dinamici come quelli di interesse per il progetto. Una soluzione che consente di superare questa limitazione consiste nell'utilizzare primitive crittografiche per proteggere gli agenti mobili trusted (ovvero, tipati) dagli ambienti untrusted che tali agenti attraversano. Quindi il sistema di tipo separa il codice trusted da quello untrusted, permettendo interazioni, che vengano giudicate sicure, con siti non trusted [BCPS03]. Una soluzione alternativa si basa sul type checking dinamico, che consente di verificare, al momento dell'interazione, le assunzioni locali fatte sui componenti remoti [BC01,HR02,DFPV00]. In alcuni casi [BC01,CDGS03] le tecniche di type checking dinamiche sono formulate in termini di sistemi di inferenza di tipo, in grado di estrarre informazioni di tipo da un codice (non tipato) al fine di approssimarne il comportamento. Tali tecniche sono particolarmente rilevanti ed efficaci nel caso di sistemi che ammettono tipo principale, proprietà che risulta essenziale per un analisi composizionale dei tipi [W02]. Per estrarre informazioni sul comportamento di termini dei calcoli per la mobilità , tipati o meno, sono state utilizzate anche altre tecniche di analisi statica. Ricordiamo, tra queste, l'attività sulla flow analysis [DLB00,BDNN01], sull'interpretazione astratta [NHN99] e sulle logiche modali [CG00].

Una linea di ricerca complementare nell'ambito dei sistemi di tipo si concentra sulla certificazione di limiti sul consumo delle risorse. Tra i riferimenti rilevanti ricordiamo [Hof02,HJ03], dove si introduce una nozione di "tipo risorsa" in grado di rappresentare un'unità di spazio astratta e si utilizza un sistema di tipo lineare al fine di garantire che la computazione richieda uno spazio lineare; [CW00] dove l'uso di un linguaggio assembly tipato consente di stabilire dei limiti quantitativi sul tempo di esecuzione; e [IK02] che propone una formulazione generale di analisi dell'uso delle risorse. Nel contesto dei calcoli concorrenti e distribuiti ricordiamo [GHS02], che presenta un calcolo in cui le risorse possono essere trasportate da una locazione all'altra, a condizione che nella locazione di destinazione vi sia sufficiente spazio; [TZH02,BBDS03] che usa i sistemi di tipo per controllare l'uso ed il consumo delle risorse; e [CGT02] che adotta tecniche statiche per analizzare il comportamento di processi con controllo finito, ovvero processi con capacità limitata di allocazione di ambienti e di creazione di output.

Equivalenze comportamentali

Un'equivalenza comportamentale identifica due processi quando questi "si comportano allo stesso modo" in tutti i possibili contesti, ovvero in tutti gli ambienti nei quali possono essere utilizzati. Il comportamento dei processiè determinato da come questi interagiscono con l'ambiente e dagli effetti che producono su di esso. Nelle teorie classiche della concorrenza (dove sono assenti distribuzione e tipizzazione) il comportamento viene rappresentato dalle azioni che i processi possono eseguire ed è, in genere, formalizzato tramite la semantica operazionale strutturata. Quindi due processi sono considerati equivalenti quando possono "eseguire le stesse azioni".

La nozione di equivalenzaè particolarmente utile per giustificare formalmente le tecniche di trasformazione dei programmi ("è possibile rimpiazzare un programma P con un programma Q perché essi hanno lo stesso comportamento in tutti i contesti"), utilizzate sia dai programmatori durante lo sviluppo di software che dai compilatori nelle fasi di ottimizzazione. Tali trasformazioni richiedono però che le relazioni di equivalenza siano congruenze. e quindi che siano preservate da tutti gli operatori del calcolo, una proprietà che risulta fondamentale anche per poter ragionare in modo composizionale su sistemi complessi.

Sono state definite diverse nozioni di equivalenza comportamentale tra processi (una buona rassegnaè presentata da van Glabbeek in [Gla93]). In particolare l'equivalenza "testing" [DeHe84] e quella basata sulla bisimulazione [Pa81] si sono dimostrate tra le più utili e stabili. A partire dagli studi di Hennessy e Milner [HeMi85], queste equivalenze sono state messe in relazione con logiche modali, caratterizzando l'equivalenza tra processi in termini di equisoddisfacibilità di proprietà modali, e con teorie algebriche che permettono di trasformare processi a stati finiti in processi equivalenti utilizzando tecniche di riscrittura. Altre tecniche per verificare l'equivalenza tra processi sono quelle operazionali basate sulla coinduzione. Particolarmente importante è il caso della bisimulazione e delle "tecniche up-to" [Mil89,San98] basate sul rafforzamento del principio di coinduzione.

Tutti questi risultati sono in genere consolidati nel caso "classico" dei calcoli di processi à la CCS e, in qualche modo, anche per i calcoli puri per la mobilità come il pi-calcolo (con il termine "puro" si vuole intendere la presenza di mobilità , data dal fatto che i nomi possono essere comunicati, ma nè tipi nè primitive per la distribuzione sono considerate in questi calcoli). Nel pi-calcolo, tuttavia, lo sviluppo di strumenti per l'analisiè stato nettamente minore rispetto al caso dei calcoli classici.

Le equivalenze comportamentali per calcoli che supportano mobilità di codice e agenti, con locazioni distribuite e topologie di rete complesse, hanno ricevuto una crescente ma purtroppo ancora limitata attenzione in letteratura. I primi lavori in quest'area [LS03,BCMS04] mostrano che concetti come la mobilità e la distribuzione hanno un forte impatto sui problemi classici della teoria della concorrenza, ad es. sull'interferenza, con effetti non trascurabili sulle teorie algebriche e sugli algoritmi di verifica. Anche la mobilità stessa crea difficoltà sorprendenti nella modellazione di semplici equivalenze basate sulla bisimulazione e nell'individuazione di caratterizzazioni coinduttive di equivalenze contestuali [GHS02,CZ02,MZ03]. Difficoltà simili si riscontrano quando si utilizzano i tipi per disciplinare il comportamento dei processi con forme di controllo degli accessi [PiSa00] e della mobilità del codice [HMR03, HRY03].

Le equivalenze comportamentali per i calcoli di processi sono state studiate anche nell'approccio conosciuto come "semantica logica" nel quale gli elementi di un calcolo sono interpretati come l'insieme (filtro) delle proprietà che essi soddisfano. Queste proprietà sono di solito espresse come tipi, stabilendo così una dualità tra i termini del calcolo e i loro tipi (proprietà ), che spesso rappresentano in modo approssimato il comportamento dei processi. Quest'ideaè stata approfondita e studiata in diversi articoli sulla teoria dei calcoli dei processi. Sono stati costruiti modelli a filtro per il pi-calcolo [HH97, DDG99], il calcolo degli ambienti [CD02,MZ04] e alcune sue estensioni ad oggetti [BdL03]; le teorie equazionali di questi modelli sono state messe in relazione con equivalenze osservazionali tra processi. Esistono relazioni interessanti tra sistemi di tipo soggiacenti ai modelli a filtro e sistemi di transizione etichettati, come mostrato in [MZ04].

Logiche di Specifica

Il lavoro sulle logiche per sistemi distribuiti si è sviluppato nella letteratura recente in direzioni diverse. La logica per gli ambienti [CG00]è una logica modale, solidamente basata sul calcolo degli ambienti, che& egrave; in grado di trattare tanto lo spazio quanto il tempo. Questa logica è dotata di operatori che permettono di fare asserzioni sulle locazioni e sui loro nomi, e di esprimere loro proprietà . Un approccio collegato è quello seguito per Klaim, dove è stata adottata una logica temporale per specificare e verificare proprietà dinamiche di agenti mobili eseguiti su reti di larga scala. Inoltre, le logiche spaziali e temporali sono anche utili per analizzare sistemi aperti, dove le componenti possono essere dinamicamente connesse per interagire con i servizi di rete. Di particolare interesse in questo contesto è il nuovo approccio per la modellizzazione di sistgemi aperti basato sui "bigrafi", un formalismo che sta emergendo come una generalizzazione di molti calcoli di processo esistenti.

Le logiche modali e temporali si sono dimostrate efficaci come formalismi per la specifica e la verifica di proprietà di sistemi concorrenti, e diversi strumenti software sono stati sviluppati per supportare tali attività . La logica di Hennessy-Milner, il mu-calcolo, CTL, CTL*, ACTL si sono affermati come strumenti utili per descrivere e stabilire proprietà di sistemi concorrenti modellati per mezzo di calcoli di processi. Facendo seguito al lavoro di Hennessy e Milner [HeMi85], varie corrispondenze sono state fissate in [BCG88], dove due equivalenze sulle strutture di Kripke (sistemi di transizione con nodi etichettati) sono state messe in relazione con varianti di CTL*, e in [DV95] dove CTL e HML sono state messe in relazione con la bisimulazione branching.

Il crescente utilizzo delle reti su larga scala e la computazione pervasiva, insieme con l'introduzione di nuovi paradigmi e linguaggi che modellano l'interazione tra attori differenti (possibilmente mobili), ha suscitato un rinnovato interesse per lo studio di nuove logiche. Per queste nuove classi di programmi, come per i formalismi concorrenti, è cruciale avere strumenti per stabilire proprietà quali l'assenza di deadlock, la liveness e la correttezza rispetto a specifiche date. Comunque, per questa nuova classe di sistemi, è anche importante stabilire altre proprietà riguardanti l'allocazione e l'uso delle risorse e la diffusione delle informazioni. Per tale motivo, l'uso delle logiche modali per specificare e verificare proprietà di sistemi mobili ha trovato ampia diffusione. Le proprietà sono specificate per mezzo di operatori modali spaziali e temporali e quindi verificate tramite sistemi di prova o con il supporto di model checker. Nell'approccio basato sui sistemi di prova vengono fornite delle regole di inferenza che consentono di costruire dimostrazioni formali del fatto che le formule di interesse sono soddisfatte dai sistemi studiati. Nell'approccio basato su model checking viene introdotta, invece, una metodologia per verificare automaticamente se un sistemaè un modello formale di una formula data. Le logiche per calcoli di processi con mobilità sono state studiate in diversi articoli. A seguire riportiamo una breve panoramica dei riferimenti presenti in letteratura che sono rilevanti per gli scopi della presente proposta.

[MPW93] introduce una logica modale per il pi-calcolo. Questa logica, che mira a catturare le differenti equivalenze tra i processi e a stabilire le diversità tra la bisimulazione late e la early, è basata sulla logica di Hennessy e Milner ma non ha operatori per la ricorsione. In [D96]è presentata una logica, ispirata alla logica di Hennessy-Milner con ricorsione, per il pi-calcolo. Questa logica è dotata di un sistema di prova basato su tableau, ma non offre operatori per trattare proprietà spaziali e la mobilità degli agenti.

[CG00] presenta una logica modale per gli Ambienti Mobili. Tale logica, solidamente basata sul calcolo degli Ambienti, permette di descrivere sia proprietà spaziali che proprietà temporali. È dotata di operatori logici che possono essere usati per fare asserzioni sulle locazioni e sui loro nomi, e permette di esprimere proprietà di natura piuttosto intensionale [San01]. Il lavoro sulle logiche spaziali per i sistemi distribuiti è quindi proseguito in diverse direzioni.

[CC01] introduce una variante della logica per gli ambienti adattata al pi-calcolo asincrono. Questa interessante logica è dotata di operatori per la specifica di proprietà temporali e spaziali, e per la specifica composizionale di proprietà di sistemi. In [CG01] sono stati introdotti nuovi operatori per esprimere proprietà logiche dei nomi ristretti. Questa logica consente di specificare configurazioni spaziali e numerose proprietà di computazioni mobili, comprese le proprietà di sicurezza.

[DL04] sviluppa una logica temporale per la specifica di proprietà nel linguaggio Klaim [DPF98]. Questa logica, ispirata alla logica di Hennessy-Milner e al mu-calcolo, presenta nuove caratteristiche che permettono di catturare sia proprietà degli stati che l'impatto delle azioni e dei movimenti degli agenti sui diversi siti. La logica è dotata di un sistema di prova che consente la verifica di proprietà per sistemi mobili. Le logiche temporali sono state studiate anche nell'ambito dell'approccio ai sistemi concorrenti basato sulla teoria degli automi, con lo sviluppo di tecniche di verifica fondate sul model-checking. Gli automi History Dependent, che sono in grado di allocare e deallocare i nomi dinamicamente, sono stati introdotti e utilizzai per la verifica di (frammenti finiti di) calcoli con causalità , località e mobilità [FGMP04]. <<<