RICERCA ITALIANA     

Programma di ricerca

Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile

Università di riferimento

Università degli Studi di FIRENZE - SISTEMI E INFORMATICA - FIRENZE(FI)

Responsabile dell'Unità di ricerca

Rocco DE NICOLA

Descrizione

La nostra unita' e' coinvolta in tutti e tre le tematiche del progetto. In particulare, contribuiremo lavorando su
- Tipi e membrane per il controllo della mobilita' dei processi e dei dati
- Logiche modali per la specifica di reti aperte
- Equivalenze indotte dalle logiche e loro relazioni con equivalenze comportamentali

Di seguito, riportiamo i contributi attesi per i tre argomenti sopra menzionati. Alcune ricerche saranno portate avanti congiuntamente ad altre unità del progetto. In particolare, prevediamo di collaborare con l'Unità C su Logiche per la specifica, l'Unità T su Sistemi di tipo e con l'Unità E su Equivalenze comportamentali.

Tipi e membrane per il controllo della mobilita' dei processi e dei dati
Il nostro obiettivo e' quello di sviluppare sistemi di tipo che supportino ragionamenti su aspetti di sicurezza dei programmi distribuiti, come il trust sul codice migrante e gli accessi sicuri/autorizzati alle risorse. Per questo scopo studieremo i sistemi di tipo e le logiche che permettono la verifica dei programmi. Il nostro obiettivo e' quello di affrontare la grande dinamicita' dei sistemi di Ubiquitus Computing dove l'approccio statico al type checking non basta. Infatti, per gestire sistemi aperti occorre effettuare verifica dinamica per gestire quei sistemi in cui le informazioni di tipo sono parziali, inaccurate o mancanti e per trattare applicazioni distribuite, come ad esempio quelle relative al commercio elettronico.
Abbiamo già progettato sistemi di tipo potenti e non standard per garantire proprieta' di sicurezza, ossia accessi alle risorse, e controllo della mobilita' di codice, per il linguaggio Klaim (e sue varianti). Questi sistemi consentono la modifica dinamica delle politiche di sicurezza e dei privilegi sui processi ed una verifica a tempo di esecuzione dei programmi o di parti di esse.
Intendiamo arricchire i sistemi di tipo per (varianti di) Klaim con meccanismi per il controllo e la restrizione della mobilita' dei processi all'interno di aree ben definite. Questo dovrebbe prevenire, ad esempio, la migrazione degli agenti su nodi maligni. Studieremo anche lo sviluppo di meccanismi simili per il controllo della propagazione di dati/risorse sensibili. Inoltre, intendiamo generalizzare questo metodo ad altri calcoli per Global Computing, come il Pi-Calcolo Distibuito di Hennessy e Riely e varianti di Mobile Ambients di Cardelli e Gordon. Puntiamo ad estendere i sistemi di tipo gia' noti per questi calcoli con pochi concetti nuovi finalizzati ad un controllo specifico del movimento di dati. Inoltre intendiamo confrontare i differenti sistemi di tipo che svilupperemo in termini di implementabilita', efficienza e potere espressivo.
Investigheremo anche la possibilita' di dotare i nodi o le entita' computazionali autonome di guardiani o membrane che potrebbero essere in grado di reagire o di gestire i tentativi di eseguire azioni vietate e di controllare la mobilita' dei processi. Confronteremo, quindi, il potere espressivo di (super)processi espliciti che giocano il ruolo di supervisori con i sistemi di tipo introdotti.

Logiche modali per la specifica di reti aperte
Per i sistemi di calcolo pervasivi, come per i sistemi concorrenti, e' cruciale avere strumenti per la verifica di proprieta' come l'assenza di deadlock, la liveness e la correttezza rispetto a delle specifiche fissate. Ma, per programmi che coinvolgono attori e autorita' differenti e' anche importante stabilire altre proprieta' riguardanti l'allocazione e l'uso delle risorse, il movimento di agenti, e la diffusione di informazione. Per questo motivo, in diversi articoli e' stato sostenuto l'uso delle logiche temporali per la specifica e verifica di proprieta' dinamiche di agenti mobili in esecuzione su reti di larga scala. Comunque, per utilizzare questi strumenti formali per verificare le proprieta' dei sistemi occorre conoscere tutti i dettagli implementativi degli stessi. Ovviamente, questa e' un'assunzione troppo forte per la classe di sistemi che vogliamo considerare, visto che, molto spesso, solo alcune componenti del sistema sono note; inoltre c'e' una limitata conoscenza del contesto nel quale le componenti operano.
Il nostro scopo e' quello di studiare uno strumento formale che consenta di astrarre dalla reale implementazione dei sistemi. Utilizzando questo strumento sara' possibile specificare contesti computazionali per sistemi mobili e distribuiti. Inoltre, utilizzando una nozione di "accordo" tra un sistema concreto con una specifica di contesto, garantiremo che se una specifica di contesto e' parzialmente istanziata (implementata) mediante un sistema concreto, allora tutte le formule soddisfatte dal sistema piu' astratto sono soddisfatte anche da quello piu' raffinato.
Il framework proposto permettera' di modellare sistemi parzialmente specificati che saranno costituiti da componenti per le quali viene fornita una descrizione dettagliata e specifiche astratte che descriveranno il contesto dove le componenti andranno ad operare. Utilizzando la nozione di "accordo" tra contesti e implementazioni reali, proponiamo di sviluppare una procedura di raffinamento progressivo (una sorta di rely-guarantee) per lo sviluppo di programmi. La procedura garantira' che le proprieta' verificate ad un livello di astrazione saranno preservate dopo il raffinamento.
La relazione di accordo, informalmente descritta sopra, sara' formalmente definita mediante un'equivalenza comportamentale. Inoltre, al fine di garantire la validità delle formule dopo il raffinamento dei contesti, questa equivalenza dovra' essere provata coerente con l'equivalenza indotta dalla logica.
Dopo aver condotto la sperimentazione su Klaim (per questo calcolo e' stata già definita una logica modale che puo' essere utilizzata per specificare e verificare proprieta' di sistemi), analizzeremo l'applicabilita' dello stesso approccio ad altri linguaggi per processi mobili, come Dpi o Djoin. Vogliamo anche analizzare le relazioni tra la logica per Klaim e la logica spaziale per gli Ambienti Mobili e per valutare l'impatto di queste logiche su linguaggi per i quali non sono state pensate. Questo portera' alla definizione di un framework comune per la specifica e la verifica di proprieta' per sistemi distribuiti e mobili.
Studieremo inoltre estensioni delle logiche per descrivere e verificare proprietà quantitative dei sistemi, puntando anche a studiarne l'impatto sulle variant quantitative dei linguaggi per global computing come StocKlaim.
Svilupperemo anche strumenti prototipali per la verifica automatica di proprieta' di componenti e sistemi aperti.

Equivalenze indotte dalle logiche e loro relazioni con equivalenze comportamentali
All'interno di questa tematica ci concentreremo su due differenti task, ossia lo studio di nuove equivalenze comportamentali e quello di nuovi costrutti linguistici.
Nella teoria dei processi, due processi sono considerati equivalenti se questi non possono essere distinti da nessun contesto che li puo' accogliere. Comunque, in presenza di tipi, distribuzione o caratteristiche higher-order le nozioni ordinarie di azioni osservabili sono troppo forti. Qualche risultato per questo problema esiste, anche se applicati a singoli calcoli specifici. Il nostro obiettivo e' quello di arrivare ad un framework generale ed uniforme nel quale diversi sistemi di tipo e calcoli fondazionali possano essere adattati, e nel quale i risultati esistenti siano riconducibili a casi speciali.
I nostri modelli base saranno i sistemi di transizione etichettati. Comunque, allo scopo di utilizzare le tecniche sviluppate per descrivere sistemi di interesse saranno necessarie delle innovazioni considerevoli. Infatti, sara' necessario rivisitare metodologie esistenti per utilizzare i sistemi di transizioni etichettati al fine di elaborare equivalenze comportamentali sia di tipo testing che basate su bisimulazione.
Programmiamo di cercare la giusta nozione di equivalenza definendo un interessante insieme di osservabili di base, messi a punto per componenti mobili autonome, per analizzare gli effetti della ricerca di questi osservabili in tutti i contesti prevedibili. Due processi saranno considerati equivalenti se questi mostreranno gli stessi osservabili di base in tutti i contesti ragionevoli. Paragoneremo quindi le equivalenze ottenute con quelle esistenti che certamente garantiscono una piu' maneggevole tecnica di prova.
Programmiamo inoltre di usare le semantiche osservazionali per l'analisi e il ragionamento su applicazioni di GC. Queste semantiche potrebbero essere sfruttate, ad esempio, per stabilire l'allocazione ottima sulla rete di componenti, servizi di rete e risorse, e per provare proprieta' di protocolli di sicurezza distribuiti implementati utilizzando meccanismi crittografici.
Intendiamo poi progettare nuove astrazioni per la programmazione, e quindi nuovi costrutti di programmazione con le loro controparti fondazionali, per legare i servizi alle componenti e gestire la sicurezza garantendo la necessaria Qualita' del Servizio (QoS). Questa e' una richiesta chiave nelle applicazioni mobili. Le nuove primitive per la QoS dovrebbero fornire meccanismi adeguati alla gestione di caratteristiche tipiche quali l'acquisizione di risorse, la tolleranza ai guasti, le scadenze temporali e la possibilita' di comporre specifiche QoS differenti ed eventualmente contrastanti. Differenti aspetti di QoS possono introdurre diverse viste del sistema; investigheremo le possibili interazioni (e conflitti) tra le diverse viste all'interno dei ben noti modelli del GC, come Dpi e Ambient. Legheremo le primitive di alto livello per la specifica di QoS con i meccanismi per la gestione delle risorse in modo da misurarne disponibilita' e uso. Klaim sara' utilizzato come ambiente di test e di valutazione per lo sviluppo dei nuovi costrutti linguistici per la programmazione QoS e per lo sviluppo di modelli semantici che possono essere utilizzati per sperimentare QoS programmabili, senza considerare le attuali complesse tecnologie di rete disponibili.