RICERCA ITALIANA     

Programma di ricerca

Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile

Università di riferimento

Università "Cà Foscari" di VENEZIA - INFORMATICA - VENEZIA(VE)

Responsabile dell'Unità di ricerca

Michele BUGLIESI

Descrizione

La nostra unità è coinvolta su tutti i temi del progetto. In particolare, fornirà i propri contributi sulle seguenti tematiche:

   - Systemi di tipo per la gestione delle risorse
   - Equivalenze comportamentali e proprietà di sicurezza
   - Logiche modali per la specifica di proprietà comportamentali e spaziali di sistemi aperti

Inoltre, dato il ruolo di coordinamento all'interno del progetto, la nostra unitaà investirà una quota significativa di lavoro nella valutazione delle tecniche e dei metodi sviluppati all'interno del progetto mediante su specifici casi di studio.

Sistemi di tipo per la gestione delle risorse
Il nostro lavoro su questo tema procederà in due direzioni parallele.

Una prima linea di ricerca si pone come obiettivo lo sviluppo di sistemi di tipo che forniscano supporto per politiche decentralizzate e dinamiche di gestione delle risorse che regolino l'amministrazione dei diritti di accesso, la propagazione/revoca delle "capabilities", la modifica della proprietà delle risorse e/o dei ruoli degli utenti. Traendo ispirazione da [CDV03,HR02,Mye99] e dal nostro stesso lavoro presentato in [BCC04] ci proponiamo di sviluppare teorie di tipo che controllino staticamente il flusso dinamico delle risorse e delle "capabilities" attraverso le componenti del sistema.
Questo lavoro sarà basato su politiche discrezionali di controllo degli accessi (DAC) [McCMN90], che permettano ai proprietari delle risorse di assegnare a loro discrezione diritti di autorizzazione diversi a utenti diversi. In particolare, intendiamo sviluppare la tecnica introdotta in [BCC04] in due direzioni. Da un lato extendendola a sistemi e calcoli con una nozione esplicita di locazione e di distribuzione, come per esempio il Dpi calcolo; dall'altro lato sviluppando sistemi con tipi dinamici e dipendenti per ottenere politiche più flessibili basate su distribuzione di specifici servizi a specifici utenti.
Un altro aspetto della ricerca che intendiamo sviluppare riguarda lo studio dell'implementazione delle politiche di gestione delle risorse di interesse in calcoli dei processi di basso livello dotati di primitive per la crittografia. Piu' precisamente, proponiamo di implementare la distribuzione controllata dei diritti di accesso tramite una distribuzione corrispondente di "term-capabilities" protette mediante cifratura con chiavi segrete conosciute soltanto dagli utenti specifici che possono riceverle (oppure con le chiavi pubbliche di quegli utenti). Per verificare l'adeguatezza di questo metodo di implementazione, svilupperemo tecniche sistematiche per confrontare le equivalenze (non tipate) del calcolo crittografico di basso livello con le equivalenze tipate del calcolo sorgente di alto livello e tipato.

Una linea di ricerca parallela riguarda lo studio di sistemi di tipo per limitare l'utilizzo delle risorse. Il lavoro di ricerca in questo campo si è sviluppato soltanto di recente [TZH02] e noi stessi abbiamo affrontato questo tema in [BBDS03], ma i risultati ottenuti sono ancora piuttosto iniziali. Il nostro obiettivo qui è l'estensione delle idee e delle tecniche presentate in [HJ03,CW00,CEI+05] ai sistemi concorrenti e distribuiti. Questa linea di studio è fortemente innovativa, ed il problema interessante per due motivi complementari. Da un lato, le tecniche disponibili in letteratura non si estendono naturalmente al caso di linguaggi e sistemi concorrenti per l'inerente non-determinismo delle richieste di allocazione di memoria in questi sistemi. Dall'altro lato, le algebre di processi correnti non forniscono meccanismi per la rappresentazione esplicita di computazioni con risorse limitate, in cui siano osservabili, e quantificabili, i limiti e ed i vincoli sulla capacità dei processi di allocare, utilizzare, deallocare e recuperare mediante "garbage collection" nuove risorse (come ad esempio canali e locazioni).

Equivalenze comportamentali e proprietà di sicurezza
Il nostro obiettivo su questo tema è quello di sviluppare tecniche accurate ed efficienti che consentano di specificare e garantire il rispetto di politiche di sicurezza che controllano il flusso delle informazioni permettendo però il rilascio di informazioni private/segrete (declassification) ove necessario. Ciò naturalmente richiede lo sviluppo di formalismi adatti ad esprimere tali politiche in modo tale da poter essere automaticamente verificate.

Importanti passi iniziali in questa direzioni sono stati compiuti in [BPR04] in cui sviluppiamo, per un linguaggi tipo CCS, un framework per la specifica di politiche di sicurezza che permettono il rilascio di informazioni sensibili (declassification), parametricamente rispetto all'osservazione di interesse. Il nostro piano qui è di estendere il framework corrente al caso del pi calcolo oppure più in generale, al caso di calcoli con mobilità. Il punto di partenza per il nostro lavoro sarà la nuova caratterizzazione della non-interferenza in questi calcoli che abbiamo recentemente proposto in [CR05]. Le politiche di sicurezza che intendiamo modellare dovrebbero rendere possibile la variazione dinamica dei livelli di sicurezza assegnati alle risorse e/o agli utenti, in funzione di diverse condizioni sullo stato delle risorse e della computazione. Una caratteristica importante per le proprietà di sicurezza ottenute come istanze di questo framework è la persistenza, che garantisca che le proprietà sono preservate dalle transizioni che formalizzano l'esecuzione. La persistenza è infatti una proprietà centrale per il trattamento del downgrading, poichè essa consente di rilevare i flussi di informazione indesiderati che si verificano dopo i passi di downgrading [Mul00].

Una ulteriore linea di ricerca riguarda lo studio di meccanismi di composizione di processi e di raffinamento di sistemi. Studieremo in particolare tecniche che permettano di garantire che le operazioni di composizione e raffinamento preservino le proprietà di sicurezza delle componenti e sistemi di partenza. Questo aspetto del nostro programma condivide motivazioni ed obiettivi con le attività dell'Unità L: ci aspettiamo di ottenere benefici significativi dalla cooperazione all'interno del progetto.

Il nostro lavoro sull'equivalenza comportamentale coinvolgerà anche attività di carattere più fondazionale su tecniche per l'assiomatizzazione e tecniche coinduttive per sistemi higher-order. Tale lavoro verrà svolto in stretta collaborazione con l'Unità E.

Logiche modali per la specifica di proprietà comportamentali e spaziali di sistemi aperti
La nostra linea di ricerca sarà sviluppata in collaborazione con l'unità L. Essa riguarda lo sviluppo e lo studio di logiche che consentano di specificare il comportamento di componenti di sistemi e dei loro contesti, ed allo stesso tempo di controllare le loro interazioni. Relativamente alla nostra unità, l'attività sarà focalizzata sullo studio di logiche per bigrafi [JM04], che costituiscono un nuovo modello formale per sistemi aperti e dinamici e che si sta affermando come una generalizazione dei calcoli di processi. Il nostro lavoro in questo contesto si propone di raffinare la logica spaziale per bigrafi definita recentemente in [CMS05]. In particolare, l'obiettivo è quello di estendere la logica per ottenere maggiore estensionalità: l'idea è quella di introdurre una nozione di "trasparenza" per gli operatori logici in modo da svincolare la descrizione logica di un sistema da alcuni aspetti della struttura del sistema stesso, e così ottenere una caratterizzazione precisa delle capacità computazionali dei contesti, che possono per l'appunto essere "opachi" e quindi non permettere l'ispezione della propria struttura.

Casi di studio
Il progresso delle attività su modelli e tecniche portato avanti nei WP1-3 verrà valutato su casi di studio rappresentativi dei sistemi di riferimento per il progetto. Se da un lato rappresenta un obiettivo specifico di questa attivita l'identificare esempi interessanti per valutare le tecniche sviluppate nel progetto, dall'altro lato abbiamo già piani definiti in tal senso

Un primo scenario che studieremo riguarda l'analisi dei protocolli che regolano la comunicazione ed il "routing" in reti wireless "ad hoc". In una rete ad-hoc, non c'è un'infrastruttura fissa come nel caso delle stazioni base e dei centri di "switch" mobile nelle reti di telefonia mobile: i dispositivi mobili (o nodi) cooperano tra di loro per inoltrare i pacchetti lungo la rete. I nodi che sono fisicamente vicini, ovvero sono posizionati entro il raggio di copertura, possono comunicare, mentre quelli che sono distanti devono contare su altri nodi perché fungano da tramite e inoltrino i pacchetti comportandosi come router. L'itinerario seguito dal pacchetto dal mittente al ricevente può richiedere il passaggio attraverso nodi intermedi, ai quali è richiesto di ritrasmettere il pacchetto in questione generando un percorso "multi-hop".
Queste caratteristiche salienti delle reti ad-hoc rendono inadeguati i protocolli tradizionali usati nelle reti fisse. Infatti, la maggior parte dei protocolli di routing per le reti ad-hoc è di natura cooperativa e presuppone un implicito rapporto di fiducia tra nodi vicini quando si tratta di instradare uno o più pacchetti. Questo modello ingenuo di fiducia reciproca permette ai nodi "cattivi" di paralizzare una rete ad-hoc inserendo aggiornamenti sbagliati sui percorsi di routing, oppure riutilizzando le informazioni di un vecchio percorso di routing, modificando gli aggiornamenti del percorso, o rendendo pubbliche informazioni di percorso errate. Per esempio, due protocolli che sono allo studio dallo IETF per diventare uno standard, il protocollo Dynamic Source Routing (DSR) [J02], il protocollo Ad-hoc On-demand Distance Vector routing protocol (AODV) [PRD02], e le loro varianti "sicure", quali Ariadne [HPJ02] e ARAN (Authenticated Routing for Ad hoc Networks) [S05], permettono agli attaccanti di rendere pubbliche informazioni errate sul percorso di routing, di dirottare i pacchetti spediti dai nodi intermedi, e di lanciare gli attacchi di denial-of-service. Ad oggi, le valutazioni di correttezza per tali protocolli sono essenzialmente basate su simulazione. Risulta peraltro del tutto evidente l'importanza di possedere modelli formali per tali protocolli da poter utilizzare in verifiche semi-automatiche.

Il secondo scenario che utilizzeremo come base per le nostre valutazioni riguarda la pratica sempre più frequente da parte gli utenti di scaricare codice dalla rete per eseguirlo sui propri dispositivi, portatili, palmari, ecc. Il codice così scaricato può essere di natura molto varia e si presta facilmente ad essere utilizzato da virus e "worms" come veicolo per introdursi nel sistema allo scopo di manipolare dati, violare la privaci o tentare attacchi di "denial of service" mediante un sovra utilizzo delle risorse di sistema, problema quest'ultimo particolarmente rilevante per dispositivi di dimensioni e capacità computazionali limitate. Se da un lato la ricerca nel campo delle tecniche di analisi per codice movile ha contribuito a sviluppare strumenti potenti per prevenire attacchi all'integrità dei dati (un tipico esempio sono le tecniche di verifica del bytecode), dall'altro lo studio di metodi per imporre limiti sull'uso di risorse è ancora in fase iniziale.