MINISTERO DELL'ISTRUZIONE, DELL'UNIVERSITÀ E DELLA RICERCA
DIPARTIMENTO PER L'UNIVERSITÀ, L'ALTA FORMAZIONE ARTISTICA, MUSICALE E COREUTICA E PER LA RICERCA SCIENTIFICA E TECNOLOGICA
PROGRAMMI DI RICERCA SCIENTIFICA DI RILEVANTE INTERESSE NAZIONALE
RICHIESTA DI COFINANZIAMENTO (DM n. 287 del 23 febbraio 2005)

PROGRAMMA DI RICERCA - MODELLO A
Anno 2005 - prot. 2005015785
PARTE I

1.1 Programma di Ricerca afferente a

 
1. Area Scientifico Disciplinare    01: Scienze matematiche e informatiche  100%   


1.2 Titolo del Programma di Ricerca


Testo italiano

Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile


Testo inglese
Logical Foundations of Distributed Systems and Mobile Code


1.3 Abstract del Programma di Ricerca


Testo italiano

Il moderno sviluppo di programmi software è sempre più spesso rivolto al servizio di applicazioni distribuite, situate a vari livelli di astrazione, da protocolli di comunicazione a livello IP per dispositivi mobili, come il protocollo IPv6, a transazioni commerciali e sistemi di commercio elettronico. Gli ambienti computazionali in cui questi programmi operano hanno una struttura inerentemente dinamica ed estensibile, sono caratterizzati dall'assenza di strutture di controllo centralizzate e sono costruiti a partire da reti fisiche e/o virtuali con una topologia complessa, connettività dinamica e servizi di entità e qualità variabile.

Il ruolo dei metodi formali di specifica, analisi e verifica del software è chiaramente critico in questo contesto in quanto, date le dimensioni delle applicazioni e la complessità dell'ambiente computazionale sottostante, lo sviluppo di software non può prescindere da una fase rigorosa di validazione prima che il software stesso venga posto in uso. Ciononostante, i metodi classici di specifica e le tecniche di analisi esistenti non sono efficaci in questi contesti. In primo luogo, l'assenza di controllo centralizzato, che distingue i sistemi aperti, invalida l'efficacia dei metodi di verifica correnti in quanto questi ultimi troppo spesso si basano sull'esistenza di assunzioni precise, ed affidabili, sulla struttura e sul comportamento di _tutte_ le componenti del sistema da analizzare. In secondo luogo, diversi aspetti osservabili delle computazioni in sistemi aperti, quali ad esempio i fallimenti dovuti a time-out, ritardi dovuti a sovraccarico di linea, parametri di qualità del servizio e altre proprietà legate all'uso di risorse, sono trattati in modo largamente approssimativo nelle tecniche correnti.

Lo scopo del progetto è di far avanzare lo stato dell'arte sulle tecniche proprie della teoria della concorrenza per l'analisi e la verifica del software, così da rendere tali tecniche efficaci nell'analisi di proprietà complesse e in presenza di ipotesi più deboli sulle componenti del sistema. Più specificatamente, l'attività di ricerca si incentrerà sui seguenti temi:

. lo studio di nuovi modelli astratti, ma espressivi, basati su calcoli di processi, per descrivere computazioni distribuite in sistemi con mobilità di nomi e di codice.
. lo sviluppo di tecniche formali per l'analisi e la verifica di processi operanti in contesti con struttura decentralizzata, trust limitato e conoscenza parziale riguardo ai componenti del sistema.

Al fine di mantenere il progetto focalizzato, e di monitorarne il progresso verso i suoi obiettivi, le teorie e le tecniche sviluppate al suo interno saranno valutate su casi di studio rappresentativi dei sistemi di riferimento.


Testo inglese
Modern computer programs are increasingly being developed in support of distributed applications at different levels of abstractions, from IP-level communication protocols for mobile devices, such as IPv6, to application-level business transactions and e-commerce systems. The computing environments in which such programs operate are inherently open-ended, characterized by the absence of centralized structures, and built upon physical or virtual networks with complex structure and dynamic communication capabilities and services.

The role of formal methods for specification, analysis and verification is indisputable in this context as, given the size of the applications, and the complexity of the underlying computing environments, software development may not forego rigorous assessment before deployment. Yet, classical specification methods and verification techniques do not scale here. Firstly, the absence of centralized control, distinctive of open systems, invalidates the effectiveness of traditional verification methods which too often rely on the existence of precise, and reliable, assumptions on the structure and behavior of all system components to be analyzed and validated. Secondly, a number of core observables properties for computations in open systems, such as such as failures due to time-outs, delays due to shortage of communication bandwidth, quality of service parameters for communication links and other resource-centric parameters, remain largely unaddressed by current specification methods and analysis techiques.

The purpose of the project is to advance the state of the art on concurrency theoretic techniques for software analysis and verification, so as to make them more expressive and effective under the weaker and possibly partial assumptions on structure and behavior distinctive of the systems and applications of interest. More specifically, our research will focus on:
. the study of new expressive concurrency theoretic models for distributed computation in systems with name and code mobility;
. the development of formal techniques for the analysis and verification of process behavior in contexts with decentralized structure, limited trust, and partial knowledge about the context's components.

To keep the project focussed, and monitor its progress towards its objectives, the theories and techniques developed will be tested on a set of case studies representative of the systems of interest.


1.4 Durata del Programma di Ricerca

24 Mesi  


1.5 Settori scientifico-disciplinari interessati dal Programma di Ricerca

 

INF/01 - Informatica 


1.6 Parole chiave


Testo italiano

CALCOLI TIPATI PER CODICE MOBILE ; EQUIVALENZE COMPORTAMENTALI ; SISTEMI DI TRANSIZIONE ETICHETTATI ; SISTEMI DI TIPO PER IL CONTROLLO DELLE RISORSE ; LOGICHE TEMPORALI E SPAZIALI PER LA CONCORRENZA


Testo inglese
TYPED CALCULI FOR MOBILE CODE ; BEHAVIORAL EQUIVALENCES ; LABELLED TRANSITION SYSTEMS ; TYPES FOR RESOURCE CONTROL ; TEMPORAL AND SPATIAL LOGICS FOR CONCURRENCY


1.7 Coordinatore Scientifico del Programma di Ricerca

BUGLIESI
(Cognome)
 
MICHELE
(Nome)
 
Professore Associato
(Qualifica)
 
31/05/1962
(Data di nascita)
 
BGLMHL62E31L483K
(Codice di identificazione personale)
 
INF/01 - Informatica
(Settore scientifico-disciplinare)
 
Università "Cà Foscari" di VENEZIA
(Università)
 
Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(Facoltà)
 
Dipartimento di INFORMATICA
(Dipartimento)
 
041-2348437
(Prefisso e telefono)
 
041-2348419
(Numero fax)
 
michele@dsi.unive.it
(Indirizzo posta elettronica)
 


1.8 Curriculum scientifico


Testo italiano

Michele Bugliesi è Professore Associato all'Università di Venezia "Ca' Foscari" dal Settembre 2000. In Maggio 2004 è stato dichiarato idoneo per la posizione di professore ordinario (posizione che attualmente ancora non ricopre). In passato è stato Ricercatore Confermato all'Università di Padova, (Dicembre 1992 - Ottobre 1998), e di Venezia (Novembre 1998 - Agosto 2000). Ha avuto posizioni di visiting researcher all'università del Sussex (Maggio 2003 e Agosto 2004), è stato professore invitato all'Ecole Normale Superieure di Parigi (Febbraio 2000), e visiting lecturer a Boston University (Gennaio - Maggio 1999).

Michele Bugliesi ha preso parte a numerosi progetti di ricerca finanziati dai principali enti italiani e internazionali, tra cui la Comunità Europea con il programma ESPRIT, la NSF statunitense, e il Ministero Italiano dell'Università e Ricerca. È stato coordinatore della parte Italiana di una azione intergrata Galileo negli anni 2001 -2002, e attualmente è coordinatore scientifico dell'unità di Venezia per il Progetto MyThS (FET-GC IST-2001-32617) finanziato dalla Comunità Europea per gli anni 2002-2005 (siti: ENS Paris, Univ. of Venice, Univ. of Sussex).

Negli ultimi anni è stato coinvolto come membro dei comitati di programma delle seguenti conferenze: FOSSACS'05, EXPRESS'05, FMOODS'05, FCS'04, CSFW'03, FMOODS'03. Nell'anno 2006 sarà membro del comitato di programma di ESOP'06, e General Chair per ICALP'06. È attualmente membro dello Steering Committee del Workshop FOOL (Foundations of Object-Oriented Languages).

Bugliesi è autore di più di 50 articoli in riviste e conferenze internazionali. In Luglio 2004 è classificato alla posizione 7705 nella lista Citeseer degli autori più citati nell'area di Computer Science (la posizione è 4160 nella classifica normalizzata per anni di pubblicazione).

In passato le sue ricerche si sono focalizzate sullo studio dei fondamenti semantici delle estensioni di linguaggi dichiarativi con costrutti per la modularità, e su teorie di tipi e calcoli fondazionali per sistemi orientati agli oggetti. In [10] ha collaborato allo sviluppo di un algoritmo di inferenza di complessità O(n^3) per un sistema di tipo del primo ordine per un calcolo ad oggetti con relazione di sottotipo variante: il sistema generalizza tutti i sistemi di tipo della stessa classe presenti in letteratura. In una serie di lavori successivi ha studiato teorie di tipo per calcoli ad oggetti con primitive per l'estensione di oggetti mediante l'aggiunta di metodi. In particolare, il lavoro descritto in [15] fornisce una caratterizzazione di un sistema di tipo basato su row-polimorfismo in termini di polimorfismo match bounded. Basandosi su tale caratterizzazione, il lavoro descritto in [8] chiude un problema aperto nella letteratura sugli object encodings fornendo per la prima volta una interpretazione di oggetti estensibili in lambda calcolo di ordine superiore che preserva la relazione di sottotipo e soddisfa la proprietà di adeguatezza computazionale.

Più di recente, le sue ricerche si sono incentrate su sistemi concorrenti distribuiti. Nell'ambito del progetto MyThS, Bugliesi ha sviluppato teorie di tipi avanzate per l'analisi di protocolli di autenticazione (di messaggi ed entità) [3,6] e metodi per l'analisi di protocolli di fair exchange basati su teorie algebriche di equivalenza [2]. Nell'ambito della programmazione mobile e distribuita, Bugliesi ha ideato, in collaborazione con altri autori, il calcolo dei Boxed Ambients, ampiamente citato in letteratura. In una serie di lavori [9,11,12,13,1] ha studiato i fondamenti semantici e teorie di tipi per questo calcolo, sviluppando sistemi di tipi per l'analisi del controllo degli accessi alle risorse ed il flusso di informazione.


Testo inglese
Michele Bugliesi has been Associate Professor at the University of Venice "Ca' Foscari" since Sept 2000. In May 2004 he qualified for the position of Full Professor (position not yet effective).
Previously, he has been tenured researcher in Computer Science at the University of Padova (Dec 1992 - Oct 1998), and Venice (Nov 1998 - Aug 2000). He has held research/teaching positions at the University of Sussex (May 2003, August 2004), Ecole Normale Superieure in Paris (Feb 2000), and Boston University (Jan - May 1999).

Michele Bugliesi has partecipated in several research projects, funded by major national and international funding agencies among which EU under the ESPRIT program, NSF, and the Italian Ministry of Scientific and Technological Research (formelrly MURST). He is currently the Scientific Coordinator of the Venice site of the Project `MyThS (FET-GC IST-2001-32617) funded by EU (years 2002-2005, sites: ENS Paris, Univ of Venice, Univ of Sussex).

He has served as program committee member for international conferences and workshops: recently, for FOSSACS'05, EXPRESS'05, FMOODS'05, FCS'04, CSFW2003, FMOODS03. In 2006 he will serve as program committee member for ESOP06, and General Chair for ICALP'06.

He is the author of over 50 articles in international journals and conferences. As of July 2004, he is ranked 7705 in the Citeseer list of the top cited authors in Computer Science (4160 in the list normalized by publication year).

His past research has focussed on the semantics of modular extension of declarative languages, and typed theoretical calculi for object-oriented systems. He co-developed [10] an O(n^3) inference algorithm for a first-order object-type system with variant subtyping that generalises all previous first-order object-types systems in the literature. In series of papers the studied the typed foundations for object-calculi with primitives for object extension by way of method additions. In particular, the work in [15] provides a characterisation of row-polymorphism in terms of match-bounded polymorphism. Based on that, [8] closes an open problem on object encodings by defining the first subtype preserving and computationally adequate interpretation of extensible objects into a higher-order lambda-calculus with polymorphic types, recursive types and subtyping.

More recently his research has centred on formal calculi for concurrent distributed systems. Within project MyThS, he co-developed advanced typed theories for the analysis of entity and message authentication [3,6] and of behavioral theories for the analysis of fair exchange [2]. He is the co-inventor of the calculus of Boxed Ambients which has been highly influential in the area. In a series of papers [9,11,12,13,1] he co-developed typed theories for access control and information flow, as well as the semantic foundations for the calculus.


1.9 Pubblicazioni scientifiche più significative del Coordinatore del Programma di Ricerca

1. BUGLIESI M., CRAFA S., MERRO M., SASSONE V. (in stampa). Communication and Mobility Control in Boxed Ambients. INFORMATION AND COMPUTATION. ISSN: 0890-5401 To appear.  
2. BUGLIESI M., ROSSI S. (2005). Non Interference Proof Techniques for the Analysis of Cryptographic Protocols. JOURNAL OF COMPUTER SECURITY. vol. 13 pp. 83-113 ISSN: 0926-227X  
3. BUGLIESI M., FOCARDI R., MAFFEI M (2005). Analysis of Typed Analyses of Authentication Protocols. CSFW 2005 - Computer Security Foundation Workshop. Giugno 2005 In corso di stampa.  
4. BUGLIESI M., CASTAGNA G., CRAFA S. (2004). Access Control for Mobile Agents: the Calculus of Boxed Ambients. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS. vol. 26 pp. 57-124 ISSN: 0164-0925  
5. BUGLIESI M., COLAZZO D., CRAFA S. (2004). Type Based Discretionary Access Control. CONCUR 2004. August (vol. LNCS 3170 pp. 225-239).  
6. BUGLIESI M., RICCARDO FOCARDI, MATTEO MAFFEI (2004). Compositional Analysis of Authentication Protocols. ESOP 2004. April (vol. LNCS 2986 pp. 140-154).  
7. BUGLIESI M., CRAFA S., PRELIC A., SASSONE V. (2003). Secrecy in Untrusted Networks. LECTURE NOTES IN COMPUTER SCIENCE. (vol. 2719 pp. 969-983). (ICALP'03, Int. Colloquium on Automata Languages and Programming).  
8. BONO V., BUGLIESI M., CRAFA S. (2002). Typed Interpretations of Extensible Objects. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. vol. 3(4) pp. 562-603 ISSN: 1529-3785  
9. BUGLIESI M., CRAFA S., MERRO M, SASSONE V. (2002). Communication Interference in Mobile Boxed Ambient. FSTTCS'02. (vol. LNCS 2556 pp. 71-84).  
10. BUGLIESI M., PERICAS-G S. (2002). Type Inference for Variant Object Types. INFORMATION AND COMPUTATION. vol. 177(1) pp. 2-27 ISSN: 0890-5401  
11. BUGLIESI M., CASTAGNA G. (2001). Secure Safe Ambients. 28th ACM Symp. on Principles of Progrogramming Languages. Boston, Jan. 2001 (pp. 222-235). ACM Press.  
12. BUGLIESI M., CASTAGNA G., CRAFA S. (2001). Boxed Ambients. TACS'01 Theoretical Aspects of Computer Software, 4th International Symposium. Senday, Oct.2001 (vol. 2215 of LNCS pp. 38-63).  
13. BUGLIESI M., CASTAGNA G., CRAFA S. (2001). Reasoning about Security in Mobile Ambients. CONCUR 01 - Concurrency Theory, 12th International Conference,. Aug 2001 (vol. 2154 of LNCS pp. 102-120).  
14. BONO V., BUGLIESI M. (1999). Matching for the Lambda Calculus of Objects. THEORETICAL COMPUTER SCIENCE. vol. 212 pp. 101-140 ISSN: 0304-3975  
15. BONO V., BUGLIESI M., LIQUORI L., DEZANI-CIANCAGLINI M. (1999). A subtyping for Extensible Incomplete Objects. FUNDAMENTA INFORMATICAE. vol. 38(4) pp. 325 - 364 ISSN: 0169-2968 June 1999.  


1.10 Elenco delle Unità di Ricerca

Unità  Responsabile Scientifico  Qualifica  Settore Disc.  Università  Dipart./Istituto  Mesi Uomo 
I  BUGLIESI MICHELE  Professore Associato  INF/01  Università "Cà Foscari" di VENEZIA  Dip. INFORMATICA  12 
II  COPPO MARIO  Professore Ordinario  INF/01  Università degli Studi di TORINO  Dip. INFORMATICA  11 
III  DE NICOLA ROCCO  Professore Ordinario  INF/01  Università degli Studi di FIRENZE  Dip. SISTEMI E INFORMATICA  12 
IV  SANGIORGI DAVIDE  Professore Ordinario  INF/01  Università degli Studi di BOLOGNA  Dip. SCIENZE DELL'INFORMAZIONE  13 


1.11 Mesi uomo complessivi dedicati al programma


Testo italiano

     Numero  Mesi uomo
1° anno 
Mesi uomo
2° anno 
Totale mesi uomo 
Personale universitario dell'Università sede dell'Unità di Ricerca  11  59  58  117 
Personale universitario di altre Università  2  6  6  12 
Titolari di assegni di ricerca  1  4  4  8 
Titolari di borse  Dottorato  8  48  24  72 
Post-dottorato  1  6  0  6 
Scuola di Specializzazione  0       
Personale a contratto  Assegnisti  2  10  17  27 
Borsisti  0       
Dottorandi  0       
Altre tipologie  0       
Personale extrauniversitario  3  6  8  14 
TOTALE     28  139  117  256 


Testo inglese
     Numero  Mesi uomo
1° anno 
Mesi uomo
2° anno 
Totale mesi uomo 
University Personnel  11  59  58  117 
Other University Personnel  2  6  6  12 
Work contract (research grants, free lance contracts)  1  4  4  8 
PHD Fellows & PHD Students  PHD Students  8  48  24  72 
Post-Doctoral Fellows  1  6  0  6 
Specialization School  0       
Personnel to be hired  Work contract  2  10  17  27 
PHD Fellows & PHD Students  0       
PHD Students  0       
Other tipologies  0       
No cost Non University Personnel  3  6  8  14 
TOTALE     28  139  117  256 



PARTE II

2.1 Obiettivo del Programma di Ricerca


Testo italiano

L'esecuzione remota è un paradigma classico della ricerca sui sistemi distribuiti, che mira a sviluppare tecniche per supportare la condivisione del potere computazionale tra macchine allocate su diversi nodi di una rete, e/o dispositivi mobili. I progressi recenti nella tecnologia delle comunicazioni hanno creato rinnovato interesse e nuovi problemi per questo paradigma di programmazione.

Il moderno sviluppo di programmi software è sempre più spesso rivolto al servizio di applicazioni distribuite, situate a vari livelli di astrazione, da protocolli di comunicazione a livello IP per dispositivi mobili, come il protocollo IPv6, a transazioni commerciali e sistemi di commercio elettronico. Gli ambienti computazionali in cui questi programmi operano sono costruiti a partire da reti fisiche e/o virtuali con una struttura complessa, connettività dinamica e servizi di entità e qualità variabile. Inoltre, a tutti i livelli di astrazione, tali ambienti hanno una struttura inerentemente dinamica ed estensibile, sono caratterizzati dall'assenza di strutture centralizzate di controllo, di gestione di trust e di autorizzazione.

Il ruolo dei metodi formali di specifica ed analisi del software è indiscutibile: date le dimensioni delle applicazioni e la complessità dell'ambiente computazionale sottostante, lo sviluppo di software non può prescindere da una validazione rigorosa prima che il software stesso venga posto in uso. Ciononostante, è semplice convincersi che i metodi classici di specifica e di analisi sono largamente inefficaci in questi contesti. In primo luogo, l'assenza di controllo centralizzato, tipico dei sistemi aperti, invalida l'efficacia dei metodi tradizionali di verifica in quanto questi troppo spesso si basano sull'esistenza di assunzioni precise, ed affidabili, sulla struttura e sul comportamento di tutte le componenti del sistema da analizzare. In secondo luogo, diversi aspetti osservabili delle computazioni in sistemi aperti, quali fallimenti dovuti a time-out, ritardi dovuti a sovraccarico di linea, parametri di qualità del servizio e altre proprietà legate all'uso di risorse, sono trattati in modo largamente approssimativo nelle tecniche correnti.


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.



Testo inglese
Remote execution is an old and venerable topic in research on distributed systems, targeted at the development of techniques to support the sharing of computing power among distributed machines. The new advances in telecommunication tecnology have created revived interest and new challenges for this programming paradigm.

Modern computer programs are increasingly being developed to support distributed applications and protocols at different levels of abstractions, from IP-level communication protocols for mobile devices, such as IPv6, to application-level business transactions and e-commerce systems. The computing environments in which such programs operate are built upon physical or virtual networks with complex structure and dynamic communication capabilities and services. In addition, at all levels of abstractions these environments are inherently open-ended, and characterized by the absence of centralized structures of control, trust, and authorization.

The role of formal methods for specification, analysis and verification is indisputable in this context as, given the size of the applications, and the complexity of the underlying computing envronments, software development may not forego rigorous assessment before deployment. Yet, classical specification methods and verification techniques do not necessarily scale here: the absence of centralized control, distinctive of open systems, invalidates the effectiveness of traditional verification methods which too often rely on the existence of precise, and reliable, assumptions on the structure and behavior of all system components. Classical specification and verification techniques also fall short of providing adequate characterizations of core observable properties of computations in open systems, such as failures due to time-outs, delays due to shortage of communication bandwidth, metrics to establish quality of service parameters for communication links and other resource-centric parameters.


Objectives and approach
The purpose of the project is to advance the state of the art on concurrency theoretic techniques for software analysis and verification, so as to make them (i) more expressive, hence able to capture the relevant observable properties of distributed computations, and (ii) effective under the weaker and possibly partial assumptions on structure behavior distinctive of the systems and applications of the computing environments of interest. Generally stated, the objective of the project is twofold, and includes:

. The study of abstract models of mobile computation in distributed environments, based on process calculi. Such models will support formal reasoning on code execution and migration, context exploration and adaptive behavior based on new, resource-oriented observables and associated behavioral equivalences.
. The development of formal techniques, based on types and logical systems, for the specification and verification of concurrent program behavior. Such techniques should make it possible to express the admission/authorization policies for code migration to remote computational environments and, dually, to control the mechanisms of access, negotiation, monitoring, protection and use of the local resources available at such environments.

Our approach will be centred on theory, with the goal of isolating core unifying notions to yield effective techniques for analysis and verification tools, but at the same time complemented by work on case studies to assess the theoretical results and evaluate their advance.

The theoretical work we plan draws on operational models and proof-theoretic tools for analysis and verification. The theory of concurrency has long provided powerful foundational tools for reasoning on the (contextual) behavior of concurrent processes, and for analyzing and specifying their behavior by means of type and logical systems. Consolidated progress has been made over the years on applying these tools on first-order process calculi and, to some extent, also to calculi for name mobility like the pi-calculus.
In the context of the present proposal, we seek to extend the existing techniques to processes and systems whose components are mobile, distributed, open, (partially) typed, possibly untrusted.
We propose to use types and logical formulas as interfaces, or as contracts, expressing and governing the negotiation for resource acquisition between processes and their environments. The use of coinductive and logical characterizations of the corresponding behavioral equivalences will then provide finitary representations of contexts and serve as the basis for formal analysis of the observable effects of process execution in such contexts. Innovation will be required to find adequate characterizations of resource usage and management - bounds, protection, authorization, confinement. Similarly, novel techniques will be needed to formalize mechanisms for client code to discover and acquire its resources, by migrating over a distributed network with dynamic spatial structure and connectivity and dynamic access/authorization rights.
Static analysis, based on type and logical (inference) systems, is our proposed solution to reduce the overhead incurred by executions that need to self-tune on the basis of the context information. Such analysis will contribute to provide verifiable certificates for client code to prove that it complies with the access control policies of its hosting environment. Similarly, they will provide estimates of resource usage to help minimize the cost of the run-time accesses to context information.

The techniques and tools developed will be put to test on a set of case studies. While finding relevant cases of study is in itself an objective of the project, we already have plans to work on two, largely orthogonal scenarios. The first concerns the specification and analysis of protocols to regulate communication and routing in wireless ad-hoc networks. While ad-hoc networks are interesting in themselves for the mobility-intensive nature, the routing protocols are relevant for the project as they are cooperative in nature and require adequate forms of trust to be established among the peers that participate in the routing. As such, these protocols provide a significant example of the consequences of absence of centralized control and trust in distributed computations. The second scenario addresses the nowadays common practice by users to dowload code to run on their devices --laptops, PDAs, etc. The focus here will be on techniques to detect and anticipate various security threats, from attacks to the privacy and integrity of data to denial-of-service attacks based on over-use of system resources, mounted by malicious agents hosted in the downloaded code.

The purpose of the work on case studies is twofold. On one hand, it will help concretely stimulate and steer the theoretical work by providing problem-specific challenges and continued feedback to the activities in workpackages WP1-3. On the other side, it will provide a measurable indicator to evaluate the project's progress towards its objectives and to assess the quality of its results.

The structure and a detailed account of the project activities is given the workplan section of the present proposal.



2.2 Base di partenza scientifica nazionale o internazionale


Testo italiano

Tipi, logiche e tecniche di ragionamento equazionale si stanno affermando come strumenti efficaci per l'analisi di computazioni distribuite e di sistemi aperti. Alcune tematiche di particolare rilevanza per la presente proposta riguardano l'uso di tipi e logiche per la descrizione delle risorse e delle loro modalità di utilizzo e l'impiego di teorie equazionali tipate per caratterizzare proprietà osservazionali dei processi e la loro struttura spaziale. Nel seguito descriveremo brevemente una parte della letteratura rilevante in questo ambito.


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].



Testo inglese
Types, logics and advanced techniques for equational reasoning are emerging as powerful tools for the analysis of distributed computations and open systems. Areas of particular relevance to the present proposal are related to the ability of types and logics to talk about resources and their usage, of typed equational theories to characterize observational properties of processes and their capture the spatial structure of systems. We briefly outline some relevant background below.


Type systems
Resource and mobility control, in diverse incarnations, has been the focus of extensive foundational research in type theory. Topics considered include the ability to read from and to write to a channel [PS96], the control of the location of channel names [YH99], the guarantee that distributed agents will access resources only when allowed to do so [HR02,CGZ01,BCC01,HMR03], the control of interference [LS03], the control of mobility, based on type-based permissions [DS00,MS02,CGG02,CDGS03], the guarantee of safety within local computational environments [CGG02], their secrecy [CGG00], the control on the flow and sharing of information, based on content and context [Mye99,CDV03].

With few exceptions, most of these systems rely on classical typing techniques whereby all the system components are type-checked under the same global typing assumptions. This is clearly unrealistic in distributed and dynamic environments as the ones of interest to the project. One solution to overcome this limitation is to rely on cryptographic primitives to protect trusted (i.e. typed) migrating agents against the untrusted sites they traverse, and to rely on a type system that separates trusted and untrusted code, while allowing safe interactions with untrusted sites [BCPS03]. An alternative solution is to rely on dynamic type checking, to contrast and validate the local assumptions made about remote components when such components interact [BC01,HR02,DFPV00]. In some cases [BC01,CDGS03] dynamic typing techniques have been formulated in terms of type inference systems extracting typing informations from untyped code to approximate the code's behavior. Such techniques are especially relevant, and effective, for systems which admit principal types, or typings, a property which is essential for compositional type analysis [W02].

Other static analysis techniques have been applied to extract information on the behavior of terms of typed or untyped calculi with mobility. Relevant references include flow analysis [DLB00,BDNN01], abstract interpretation [HJNN99], modal logics [CG00].

A complementary line of research on type systems focuses on the certification of bounds on resource consumption. Relevant references include the following ones: [Hof02,HJ03] introduce a notion of resource type representing an abstract unit of space, and uses a linear type system to guarantee linear space consumption; [CW00] enforces quantitative bounds on time usage using a typed assembly language; [IK02] puts forward a general formulation of resource usage analysis; more recently [CEI+05] proposes a new resource management paradigm that combines static and dynamic checks in a novel way. Briefly, the approach is based on the use of explicit language constructs to dynamically verify the availability of the required resources, and static analysis to verify that the dynamic checks enforce the resource intended bounds policies. In the context of distributed and concurrent calculi, relevant references include [GHS02], which presents a calculus in which resources may be moved across locations provided suitable space is available at the target location; [TZH02,BBDS03], which use typing systems to control resource usage and consumption; and [CGT02], which uses static techniques to analyze the behavior of finite control processes, i.e., those with bounded capabilities for ambient allocation and output creation.


Behavioral equivalences
Behavioral equivalences equate processes that "behave in the same way" in all contexts, that is, under all environments in which they could possibly be used. The behavior of processes is determined by how they interact with, or affect, such environments. In classical theories of concurrency (where processes are undistributed, untyped) the behavior is represented by the actions that the processes can perform, and formalized in the framework of Structural Operational Semantics. Thus processes are deemed equivalent if they can "perform the same actions".

Equivalence is particularly useful as a tool for justifying program transformations, ("we can validly replace P by Q because they have the same behavior in all contexts"), performed either by programmers during system development or by optimizing phases of compilers. Such transformations require equivalences relations to be congruences, i.e. preserved by all operators of the underlying calculi, a property that is also fundamental to perform compositional reasoning on complex systems.

Several notions of behavioral equivalence on processes have been defined (see for instance van Glabbeek's review [Gla93]). Among these, testing equivalence [DeHe84] and bisimulation equivalence [Pa81] have emerged as the most useful and stable. Beginning with work of Hennessy and Milner [HeMi85], they have been closely coupled with the use of various modal logics to characterize equivalent processes in terms of equi-satisfaction of modal process properties, and algebraic theories to transform finite-state equivalent processes by means of rewriting techniques. Another form of techniques developed for equivalence checking are operational techniques based on co-induction. This is especially important in the case of bisimulation, and includes strengthenings of the co-induction principle underlying bisimulation, called "up-to techniques" [Mil89,San98].

All of this is well-understood for the `classical' case of simple, CCS-like process calculi and, to some extent, for pure calculi of mobility like the pi-calculus (by pure we mean that there is mobility since names can be communicated, but there are no type and no
primitives for distribution). Even in the pi-calculus, however, tools for analysis have had a limited development compared to that for classical process calculi.
Theories of behavioral equivalences for calculi of code and agent mobility, with distributed locations and complex network topologies have received increasing but still limited attention in the recent literature. Initial work in this area [LS03,BCMS04] shows that mobility and distribution have deep impact on classical problems in the theory of concurrency, such as interference, with serious effects on the algebraic theory and algorithms for verification. Mobility also creates unexpected difficulties in modelling simple notions of bisimilarity, and in providing coinductive characterizations of contextual equivalences [GHS02,CZ02,MZ03]. Similar difficulties arise when types are employed to discipline behavior with forms of access control [PiSa00], and to control code mobility [HMR03, HRY03].
Behavioral equivalences for process calculi have also been studied in the approach known as "logical semantics" in which the elements of a calculus are interpreted as the set (filter) of the properties they satisfy. These properties are usually expressed as types, thus establishing a duality between a term of the calculus and its types (properties), which often represent approximate process behaviors. This idea has been investigated in several papers on the theory of process calculi. Filter models have been built for the pi-calculus [HH97, DDG99], Ambient Calculi [CD02,MZ04] and extensions of ambient calculi with objects [BdL03]; the equational theories of these models have been related to observational equivalences among processes. Relations between type systems underlying filter models and labelled transition systems exist as it is shown in [MZ04].


Specification logics
The work on logics for distributed systems has evolved along several directions in the recent literature. The ambient logic [CG00] is a modal logic, solidly based on the ambient calculus, that can talk about space as well as time. It has logical operators that can be used to make assertions about locations and their names, and express their properties. A related approach has been taken for KLAIM, with temporal logics employed to specify and verify dynamic properties of mobile agents running over a wide area network. Spatial/temporal logics are also useful for the analysis of open systems, where components can be dynamically connected to interact with network services. Of particular interest in this context is the novel approach to model dynamic open systems based on bigraphs [JM04], which are emerging as a generalisation of several process calculi.

Modal and temporal logics have been proved useful formalisms for specifying and verifying properties of concurrent and different tools have been developed to support such activities. Hennessy-Milner Logic, mu-calculus, CTL, CTL*, ACTL have proved to be useful tools for describing and establishing properties of concurrent systems described as process calculi. Following the work of Hennessy and Milner [HeMi85], various correspondences have been established in [BCG88], where two equivalences over Kripke structures (node-labeled transition systems) are related to two variants of CTL* and in [DV95] where CTL and HML are related to branching bisimulation.

The increasing use of wide area networks and pervasiveness of computing, together with the introduction of new programming paradigms and languages that model interactions among different (possibly mobile) actors have created revived interest in the study of new logics. For the new class of programs, like for concurrent formalisms, it is crucial to have tools for establishing deadlock freeness, liveness and correctness with respect to given specifications. However, for this new class of systems, it is also important to establish other properties such as resources allocation, access to resources and information disclosure. To this purpose, the use of temporal logics for specifying and verifying dynamic properties of mobile systems has been advocated and pursued. Properties are specified by means of temporal and spatial modalities and then verified, either proof-theoretically, or with the aid of model checkers. In the proof system approach, inference rules are provided in order to build proofs that establish the satisfaction of formulae by systems. In the model checking approach, a methodology is introduced to verify automatically whether a system belongs to the to the formal model of a formula.

Logics for process calculi with mobility have been studied in various papers. Below we briefly outline the references to the literature that are relevant to our present purposes.

[MPW93] introduces a modal logic for the pi-calculus. This logic aims at capturing different equivalences between processes and at establishing the differences between late and early bisimulation. It is based on Hennessy-Milner Logic (HML) but it has no operators for recursion. In [D96] a HML-like logic with recursion for pi-calculus is presented. This logic is equipped with a tableau-based proof system but has no operator for dealing with spatial properties and agent mobility.

[CG00] presents a modal logic for Mobile Ambients. It is a modal logic, solidly based on the Ambient calculus, that can talk about space as well as time. It has logical operators that can be used to make assertions about locations and their names, and can express also rather intensional properties [San01]. The work on spatial logics for distributed systems has since then evolved in several directions. [CC01] introduces a variant of the Ambient logic, tailored for asynchronous pi-calculus. This very interesting logic is equipped with operators for spatial and temporal properties, and for compositional specification of systems properties. In [CG01], new operators for expressing logical properties of name restrictions have been added. This logic supports the specification of spatial configurations and of a variety of properties of mobile computation, including security properties.

[DL04] develops a temporal logic for specifying properties of Klaim [DFP98]. The logic is inspired by Hennessy-Milner Logic and the mu-calculus, but has novel features that capture state properties and the impact of actions and movements over the different sites. The logic is equipped with a complete proof system that enables one to prove properties of mobile systems.

Temporal logics have also been studied in connection with the automaton-theoretic approach to concurrent system based on verification by model checking. History Dependent (HD) automata, which are able to allocate and deallocate names dynamically, have been introduced and proved effective for the verification of (finite fragments of) calculi with causality, locality and mobility [FGMP04].

[CMS05] proposes a spatial logic built on bigraphs. As it is equipped with a contextual operator, the logic can characterise both closed systems (processes) and open systems (contexts). It can describe also the composition of contexts and the separation of resources. Thanks to the generality of bigraphs, such a logic aims at embedding and contextualising the spatial logics proposed up to now.



2.2.a Riferimenti bibliografici

[BBDS03] F. Barbanera, M.Bugliesi, M. Dezani, V. Sassone.
A Calculus of Bounded Capacities. LNCS 2896, 2003.

[BdL03] F. Barbanera, U. de' Liguoro.
Type Assignment for Mobile Objects. ENTCS 84, 2003.

[BC01] M. Bugliesi, G. Castagna. Secure Safe Ambients. POPL 2001.

[BCC01] M. Bugliesi, G. Castagna, S. Crafa.
Reasoning about security in mobile ambients.
CONCUR 2001, LNCS 2154, 2001.

[BCC04] M. Bugliesi, G. Castagna, S. Crafa.
Access Control for Mobile Agents: the Calculus of Boxed Ambients.
ACM TOPLAS, 26(1):57-124, 2004.

[BCG88] M.C. Browne, E.M. Clarke, O. Grumberg.
Characterizing finite Kripke structures in propositional temporal logic. TCS 59, 1,2, 1988.

[BCMS04] M. Bugliesi, S. Crafa, M. Merro, V. Sassone.
Communication and Mobility Control in Boxed Ambients.
I&C 2005. To appear.

[BCPS03] M. Bugliesi, S. Crafa, A. Prelic, V. Sassone.
Secrecy in Untrusted Networks. ICALP 2003, LNCS 2719, 2003.

[BDNN01] C. Bodei, P. Degano, F. Nielson, H. Riis Nielson.
Static analysis for the pi -calculus with applications to security.
I&C 168, 2001.

[CC01] L. Caires and L. Cardelli.
A Spatial Logic for Concurrency (Part I), TACS 2001, LNCS 2215, 2001.

[CD02] M. Coppo, M. Dezani.
A fully abstract model for higher-order mobile ambients.
LNCS 2294, 2002.

[CDGS03] M. Coppo, M. Dezani, E. Giovanetti, I. Salvo.
M3 Mobility Types for Mobile Processes in Mobile Ambients.
ENTCS 78, 2003.

[CDV03] T.Chothia, D.Duggan, J.Vitek.
Type-Based Distributed Access Control. CSFW-16 2003.

[CEI+05] A. Chander, D. Espinosa, N. Islam, P. Lee, G. Necula.
Enforcing Resource Bounds via Static Verification of Dynamic Checks.
ESOP'05, LNCS 3444, 2005.

[CG00] L. Cardelli, A. D. Gordon.
Anytime, Anywhere. Modal Logics for Mobile Ambients.
POPL'00. ACM Press, 2000.

[CG01] L. Cardelli and A. D. Gordon.
Logical Properties of Name Restriction.
TLCA'01, LNCS 2044, 2001.

[CGG00] L. Cardelli, G. Ghelli, A. D. Gordon.
Secrecy and Group Creation.
CONCUR'00, LNCS 1877, 2000.

[CGG02] L. Cardelli, G. Ghelli, A. D. Gordon.
Types for Mobile Ambients.
I&C, 186(2) 194-235 (2003).

[CGT02] W. Charatonik, A. D. Gordon, J-M. Talbot.
Finite-control mobile ambients. ESOP 2002, LNCS 2305, 2002.

[CGZ01] G. Castagna, G. Ghelli, F. Zappa Nardelli.
Typing Mobility in the Seal Calculus. CONCUR'01, LNCS 2154. 2001

[CMS05] G. Conforti, D. Macedonio, V. Sassone.
BiLogics: Spatial-Nominal Logics for Bigraphs. ICALP'05. To appear.

[CR05] S. Crafa and S. Rossi.
A Theory of Noninterference for the pi-calculus.
TGC'05, LNCS. To appear, 2005.

[CZ02] G. Castagna, F. Zappa Nardelli.
The Seal Calculus Revisited: Contextual Equivalence and Bisimilarity. FSTTCS'02, LNCS 2556, 2002.

[CW00] K. Crary, S. Weirich. Resource bound certification.
POPL'00. ACM Press, 2000.

[D96] M. Dam. Model Checking Mobile Processes.
I&C, 129(1), pp. 35-51, 1996.

[DDG99] F. Damiani, M. Dezani-Ciancaglini, P. Giannini.
A filter model for mobile processes. MSCS 9(1): 63-101 (1999)

[DeHe84] R. De Nicola, M. Hennessy.
Testing Equivalences for Processes. TCS 34, 1984.

[DFP98] R. De Nicola, G. L. Ferrari, R. Pugliese.
KLAIM: A Kernel Language for Agents Interaction and Mobility.
IEEE Transactions on Software Engineering, 1998, 24(5),315-330.

[DL04] R. De Nicola, M. Loreti. A Modal Logic for Mobile Agents.
ACM TOCL 5(1), 2004.

[DLB00] P.Degano, F.Levi, C.Bodei.
Safe Ambients: Control Flow Analysis and Security. LNCS 1961, 2002.

[DFPV00] R. De Nicola, G. Ferrari, R. Pugliese, B. Venneri.
Types for Access Control. TCS 240(1):215-254, 2000.

[DV95] R. De Nicola, F. Vaandrager.
Three logics for Branching Bisimulation. JACM, 42(2): 458-487, 1995.

[DS00] M. Dezani-Ciancaglini, I. Salvo.
Security Types for Mobile Safe Ambients. ASIAN'00, LNCS 1961, 2000.

[FGMP04] G. Ferrari, S. Gnesi, U. Montanari, M. Pistore.
A Model Checking Verification Environment for Mobile Processes.
ACM Tosem, 2004.

[GC99] A. Gordon, L. Cardelli.
Equational Properties of Mobile Ambients.
MSCS 12, 2002 (Also in FoSSaCs '99).

[GHS02] J.C. Godskesen, T. Hildebrandt, V. Sassone.
A Calculus of Mobile Resources. CONCUR'02, LNCS 2421, 2002.

[Gla93] R.J. van Glabbeek.
The linear time branching time spectrum (part II).
LNCS 715, 1993.

[HeLi95] M. Hennessy, H. Lin. Symbolic bisimulations. TCS 138, 1995.

[HeMi85] M. Hennessy, R. Milner.
Algebraic laws for nondeterminism and concurrency. JACM 32(1), 1985, 137-161.

[HH97] T. Hartonas, M. Hennessy.
Full Abstractness for a Functional/Concurrent Language with Higher-Order Value-Passing. I&C 145(1), 1998, 64-106.

[HJ03] M. Hofmann, S. Jost.
Static Prediction of Heap Space Usage for First-Order Functional Programs. POPL'03. ACM Press, 2003.

[HJNN99] R. R. Hansen, J. G. Jensen, F. Nielson, H. R. Nielson.
Abstract Interpretation of Mobile Ambients. SAS'99, LNCS 1694, 1999.

[HMR03] M. Hennessy, M. Merro, J. Rathke.
Towards a Behavioural Theory of Access and Mobility Control in Distributed System. TCS 322(3): 615-669, 2004.

[Hof02] M. Hofmann. The strength of non size-increasing computation.
POPL'02. ACM Press, 2002.

[HPJ02] Y. C. Hu, A. Perrig, D. Johnson.
Ariadne: A secure on-demand routing protocol for ad hoc networks. MobiCom 2002.

[HR02] M. Hennessy, J. Riely.
Resource Access Control in Systems of Mobile Agents. I&C 173, 2002, 82-120.

[HRY03] M. Hennessy, J. Rathke, N. Yoshida.
Safedpi: a language for controlling mobile code.
FOSSACS'03, LNCS 2620, 2003.

[IK02] A. Igarashi, N. Kobayashi. Resource usage analysis.
POPL 02. ACM Press, 2002.

[J02] D. B. Johnson, D. A. Maltz, Y.-C. Hu.
The dynamic source routing protocol for mobile ad-hoc networks (DSR). Internet draft, MANET working group, Feb. 2002.

[JM04] O. H. Jensen, R. Milner.
Bigraphs and mobile processes (revised).
Univ. of Cambridge, Tech. Report UCAM-CL-TR-580. Feb 2004.

[LS03] F. Levi, D. Sangiorgi.
Controlling Interference in Ambients.
ACM TOPLAS 25(1), 2003. Also in POPL'00.

[Mil89], R. Milner.
Communication and Concurrency. Prentice Hall, 1989.

[MPW93] R. Milner, J. Parrow, D. Walker.
Modal logics for mobile processes. TCS 114, 1993.

[MS02] M. Merro, V. Sassone.
Typing and Subtyping Mobility in Boxed Ambients.
CONCUR'02, LNCS 2421, 2002.

[Mye99] A.C. Myers.
Mostly-Static Decentralized Information Flow Control.
PhD thesis, TR MIT/LCS/TR-783. Jan. 1999.

[MZ03] M. Merro, F. Zappa Nardelli.
Bisimulation Proof Techniques for Mobile Ambients.
ICALP'03, LNCS 2719, 2003.

[MZ04] I. Margaria, M. Zacchi.
A Filter Model for Safe Ambients. ENTCS 2004.

[Pa81] D.M. Park.
Concurrency on Automata and Infinite Sequences.
LNCS 104, 1981.

[PiSa00] B. Pierce, D. Sangiorgi.
Behavioral Equivalence in the Polymorphic Pi-Calculus.
JACM, 47, 2000.

[PRD02] C. E. Perkins, E. M. Royer, S. R. Das.
Ad-hoc on-demand distance vector (AODV) routing.
IETF Internet draft, MANET working group, Jan.2002.

[PS96] B. Pierce and D. Sangiorgi.
Typing and Subtyping for Mobile Processes.
JMSCS, 6(5), 1996.

[S05] K. Sanzgiri, D. LaFlamme, B. Dahill, B. N. Levine, C. Shields, E. M. Belding-Royer.
Authenticated Routing for Ad Hoc Networks.
IEEE Journal on Selected Areas in communications, 23(3) March 2005.

[San01] D. Sangiorgi.
Extensionality and Intensionality of the Ambient Logic
POPL'01. ACM Press, 2001.

[San98] D. Sangiorgi.
On the bisimulation proof method. JMSCS 8, 1998.

[SW01] D. Sangiorgi, D. Walker.
The pi-calculus: a Theory of Mobile Processes.
Cambridge University Press, 2001.

[TZH02] D. Teller, P. Zimmer, D. Hirschkoff.
Using ambients to control resources. CONCUR'02, LNCS 2421, 2002.

[YH99] N. Yoshida, M. Hennessy.
Subtyping and locality in distributed higher order mobile processes.
CONCUR'99, LNCS 1664. 1999.

[W02] Joe Wells.
The essence of principal typings.
ICALP'02, LNCS 2380, 2002.


2.3 Descrizione del Programma di Ricerca e del ruolo delle Unità operative locali
Descrizione del Programma di Ricerca


Testo italiano

Il programma di ricerca si articola in tre workpackages di contenuto teorico, orientati allo sviluppo di tecniche formali per la specifica, l'analisi e la verifica di sistemi distribuiti. Le attività saranno organizzate sulla base dei seguenti temi:

* Sistemi di Tipo (WP1): questo workpackage è orientato verso lo sviluppo di tecniche di assegnazione di tipo funzionali allo sviluppo di codice certificato e fortemente tipato. Il nostro approccio si conforma all'approccio noto con il nome di language-based security, prossimo alla pratica corrente di arricchire il codice mobile con certificati basati su tipi che ne asseriscono le autorizzazioni e i diritti di accesso/uso delle risorse, da verificare a destinazione da parte di entità ritenute affidabili.

* Equivalenze Comportamentali (WP2): questo workpackage si concentra sullo sviluppo di equivalenze e teorie equazionali sofisticate per i processi mobili e per i contesti che li racchiudono. Questo tema è particolarmente rilevante per gli obiettivi della presente proposta, dato che le teorie delle equivalenze costituiscono un elemento essenziale nella formalizzazione e costruzione di metodi di verifica di prorietà importanti di varia natura, quali ad esempio la sicurezza del flusso di informazione, la segretezza e l'autenticazione, nella dimostrazione di corretettezza di trasformazioni di codice, nelle tecniche di confronto di espressività di formalismi.

* Logiche di Specifica (WP3): questo workpackage complementa il lavoro in WP1 e WP2 sviluppando sistemi logici finalizzati alla specifica ed alla verifica. Integra WP1 permettendo di caratterizzare, tramite operatori modali spaziali e temporali, l'allocazione e l'accesso alle risorse, la rivelazione di informazioni, e varie proprietà topologiche dell'ambiente computazionale, che potranno quindi essere verificate mediante un approccio basato su sistemi di prova e/o con l'aiuto di model-checker. Rappresenta un complemento di WP2 in quanto fornisce nozioni alternative di equivalenza, basate sulla equisoddisfacibilità di formule logiche, e permette di caratterizzare proprietà estensionali/comportamentali nonchè intensionali/spaziali dei sistemi di interesse.

Un workpackage ulteriore sarà dedicato allo sviluppo di casi di studio rispetto ai quali valutare le tecniche ed i metodi sviluppati nel progetto. In questo modo sarà anche garantita una valutazione costante delle attività del progetto e dei progressi fatti verso gli obiettivi complessivi.

Tutti i workpackage saranno attivi durante tutto il progetto, con attività interconnesse e obiettivi complementari. Essi si fondano su modelli operazionali di processi e risorse, espressi in termini di calcoli di processi di alto livello, o, più astrattamente, di sistemi di transizione etichettati costruiti sulla base delle azioni visibili e degli effetti osservabili dell'esecuzione i nell'ambiente computazionale di interesse.

A seguire diamo una descrizione più dettagliata della struttura ed delle attività di ciascuna unità.


WP1 - Sistemi di Tipi.
La nostra ricerca si svilupperà lungo due direzioni complementari. Da un lato, svilupperemo sistemi di tipo in grado di assicurare che siano rispettati i vincoli sulle autorizzazioni, le restrizioni globali sull'accesso alle risorse e i limiti all'uso delle risorse stesse imposti dagli ambienti di computazione agli agenti mobili che li visitano. Dall'altro lato, studieremo nuove tecniche che permettano di esprimere politiche decentralizzate e discrezionali per la gestione delle "capability" e della loro propagazione nel sistema. Caratteristica distintiva di entrambe le attività sarà la necessità di affrontare problematiche legate all'assenza di conoscenza, controllo e "trust" definiti centralmente, caratteristica propria dei sistemi di interesse per questa proposta di ricerca.

*Controllo della mobilità e gestione delle risorse. Proporremo varie estensioni dei sistemi di tipo attuali per il controllo dell'accesso alle risorse e della mobilità del codice, al fine di fornire meccanismi per monitorare e vincolare la mobilità dei processi all'interno di aree prestabilite, così da evitare spostamenti verso nodi giudicati inaffidabili. Tali sistemi dovranno consentire di modificare dinamicamente i diritti di accesso e i privilegi del codice mobile sulla base del comportamento del codice stesso, del sito da cui proviene e del livello di trust delle locazioni che il codice ha attraversato durante la sua esecuzione. Il nostro obiettivo è quindi un sistema che permetta di caratterizzare il comportamento del codice mobile per mezzo di tipi ed effetti che descrivono le capability tramite le quali il codice può operare sulle risorse. Ci concentreremo su tecniche di analisi basate su di una descrizione del comportamento dei processi che assegna capability e risorse ad opportune classi di sicurezza, e quindi estenderemo il nostro lavoro sviluppando sistemi basati su tipi dinamici e dipendenti.

Svilupperemo inoltre sistemi di tipo in grado di limitare l'utilizzo delle risorse. La ricerca in questo ambito, per quanto riguarda i sistemi concorrenti e distribuiti, ha una storia recente [TZH02,BBDS03]. 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).

Per trattare sistemi nei quali non si possa assumere la disponibilità di conoscenza, controllo e trust centralizzati, si svilupperanno nuovi meccanismi e protocolli per determinare le credenziali del codice mobile e per definire la negoziazione di autorizzazioni. È naturale che questa attività di negoziazione avvenga in corrispondenza dei "contorni" (boundary): i contorni sono quindi entità speciali, per cui ne proporremo ed analizzeremo differenti formalizzazioni. Possiamo prefigurare due soluzioni possibili.

Da un lato, saranno sviluppate tecniche che integrano il typing locale, statico del codice mobile, con un'attività di type checking dinamica, just in time, svolta in corrispondenza dei contorni al fine di certificare il codice in arrivo. Dato che le informazioni di tipo relative al codice in questione possono essere parziali, inesatte o addirittura mancanti, particolare attenzione verrà rivolta allo sviluppo di sistemi di inferenza e di ricostruzione dei tipi. Sarà centrale, in questa attività , lo sviluppo di teorie di tipi che ammettano tipi principali, al fine di guidare l'inferenza e la ricostruzione dei tipi e di permettere l'analisi composizionale dei tipi.

Un approccio alternativo che intendiamo studiare si fonda sulla certificazione del codice in arrivo sulla base di "guardiani" associati a nodi ed entità computazionali, o membrane. Queste entità sono in grado di gestire eventuali tentativi di effettuare azioni non consentite e di trasferire processi al loro interno. Le due soluzioni verranno messe a confronto sulla base dei meriti e del potere espressivo.

* Controllo decentralizzato dell'information-flow e delle capability. Questa linea di ricerca è complementare all'attività sul controllo dell'accesso alle risorse e la integra con lo sviluppo di tecniche che permettono di imporre limitazioni sulla propagazione delle capability tra i componenti di un sistema. Pi๠precisamente, intendiamo sviluppare sistemi di tipi che permettono la gestione dinamica e decentralizzata dei diritti di accesso, e la propagazione selettiva delle capability basata sulla "clearance" e sul livello di trust dei destinatari.
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), 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 che intendiamo studiare riguarda l'implementazione delle politiche di gestione delle risorse di interesse in calcoli di processi di basso livello, dotati di primitive per la crittografia. Pi๠precisamente, proponiamo di implementare la distribuzione controllata dei diritti di accesso tramite una distribuzione corrispondente di "term-level capability", protette mediante cifratura con chiavi segrete note soltanto agli utenti specifici che possono riceverle (oppure con le chiavi pubbliche di quegli utenti). Per verificare l'adeguatezza di questa tecnica 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.

Un'attività connessa riguarda lo studio di tecniche di tipo per esprimere politiche di information-flow basate sulla declassificazione. Le politiche di sicurezza che intendiamo rappresentare dovrebbero permettere di specificare il cambiamento dinamico dei livelli a cui sono assegnate le risorse, nonchè di associare tali cambiamenti a condizioni dinamiche. L'impatto di tali politiche sarà valutato in termini di nozioni raffinate di non-interference, formalizzate tramite corrispondenti nozioni di equivalenza osservazionale.


WP2 - Equivalenze comportamentali
Le equivalenze comportamentali, basate su tecniche di testing e bisimulazione, sono state largamente sviluppate nel contesto dei calcoli di processi classici del prim'ordine ed estese, in alcuni casi, a calcoli puri sviluppati per modellare la mobilità di nomi come ad esempio il pi-calcolo. Negli ultimi anni sono stati fatti diversi progressi che hanno portato a consolidare le tecniche operazionali basate su metodi coinduttivi e "up-to", o basati su tracce. Lo scopo di questo workpackage è di sviluppare tecniche simili per sistemi i cui componenti sono mobili, distribuiti, aperti, (parzialmente) tipati e non necessariamente affidabili. La nostra attività si svilupperà seguendo diverse linee di ricerca interdipendenti che sono presentate in dettaglio nel seguito.

Equivalenze con tipi e distribuzione. Nella teoria dei processi, due processi vengono considerati equivalenti se non possono essere distinti da nessun contesto nel linguaggio dato. Mentre questa nozione di equivalenza puಠavere un'elegante lettura dichiarativa/estensionale, la quantificazione su tutti i possibili contesti osservati la rende difficile da usare nelle dimostrazioni; di conseguenza vengono utilizzate versioni rafforzate basate sull'osservazione delle azioni che un processo puಠeffettuare [SW01]. In presenza di tipi, distribuzione e caratteristiche di ordine superiore, la nozione ordinaria di osservazione di azioni ਠmolto pi๠forte, ed il significato dell'affermazione "due processi eseguono le stesse azioni" è poco chiaro. Per esempio non è chiaro quale delle azioni eseguite dai processi debbano essere considerate rilevanti, o uguali, dato che la distribuzione e i tipi possono implicare l'equivalenza di azioni molto diverse tra loro dal punto di vista strettamente sintattico. Esistono alcuni risultati preliminari ma sono applicabili solamente a pochi calcoli specifici. L'idea invece sarebbe quella di costruire un framework generale che si possa applicare a diversi sistemi di tipi e calcoli di processi, e che permetta di dedurre come casi speciali i risultati ottenuti fino ad ora. Si farà un uso esteso dei sistemi di transizione etichettati, ma sarà necessaria una notevole innovazione per utilizzare queste tecniche descrittive nei sistemi in questione. L'utilizzo di queste tecniche nello sviluppo di equivalenze comportamentali basate sulla bisimulazione richiederà inoltre l'estensione delle metodologie esistenti con nuovi sviluppi ed idee. Questo non riguarda solamente la definizione delle equivalenze stesse e le prove delle loro proprietà di congruenza, ma anche lo sviluppo di migliori tecniche coinduttive come ad esempio la bisimulazione-up-to, che nel pi-calcolo si è dimostrata essenziale per portare a termine molte dimostrazioni.

Tecniche per la verifica automatica, la minimizzazione ed la dimostrazione di equivalenze. Questa linea di ricerca riguarda lo studio di tecniche di tipo diverso che permettano lo sviluppo di strumenti formali per meccanizzare la (o aiutare nella) costruzione di dimostrazioni, nonchè di tecniche per migliorare l'efficienza di questi strumenti. I tipi possono risultare molto utili in questo contesto, dato che consentono di ridurre lo spazio degli stati sul quale si lavora per costruire la dimostrazione: per esempio alcuni tipi garantiscono che le comunicazioni non sono "preemptive", una proprietà di confluenza parziale che permette di analizzare solo un sottoinsieme dei possibili comportamenti dei processi. Verranno anche utilizzate tecniche simboliche [HeLi95] per migliorare lo sviluppo di prove di equivalenza basate sull'abilità di fornire rappresentazioni finitarie del grafo di esecuzione. Un'ulteriore linea di ricerca riguarderà lo studio di asiomatizzazioni per calcoli tipati e/o distribuiti. Per alcune varianti di calcoli di processi sono state definite opportune assiomatizzazioni. Queste forniscono insiemi completi di leggi algebriche che caratterizzano diverse nozioni di equivalenza comportamentale. Sarebbe interessante estendere queste nozioni in modo da tener conto di aspetti di tipizzazione e di distribuzione spaziale dei processi. Diverse problematiche cruciali per realizzare questa estensione sono tuttora aperte. Una difficoltà è legata alla legge di espansione (che permette di esprimere la composizione di processi paralleli come la somma delle loro azioni individuali). Questa legge, in genere, non vale, o vale solo in un contesto limitato, in presenza di tipi e distribuzione. Un'ulteriore problematica riguarda il fatto che la rappresentazione della migrazione di processi attraverso diverse locazioni è un aspetto inerentemente di ordine superiore (sia se che si utilizzino costrutti espliciti per la migrazione, sia che questa sia rappresentata con primitive di comunicazione).

*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. 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.

*Logical Relations. Le logical relations sono tecniche potenti, largamente utilizzate nel settore della semantica denotazionale dei linguaggi di programmazione ad alto livello per dimostrare proprietà comportamentali come la terminazione (ad esempio, per verificare che la computazione per un certo termine avrà fine), e la parametricità (ad esempio, per dimostrare che due termini che possono manipolare diversi tipi di valori non sono distinguibili). Infatti, nei linguaggi ad alto livello tipati e di ordine superiore le relazioni logiche sono a volte l'unico strumento disponibile per dimostrare proprietà osservazionali (alcuni esempi si possono trovare in [Pit98]). Riteniamo che le relazioni logiche possano essere utilizzate con successo anche nel settore dei linguaggi tipati per processi. Un lavoro preliminare al fine di utilizzare le relazioni logiche nel contesto dei processi è stato presentato in [San02], ma il linguaggio risultante ha ancora una caratterizzazione funzionale; un ulteriore approfondimento è necessario per modellare tipologie di processi pi๠generali.

Costruzione di modelli a filtro. Un'ulteriore linea di ricerca nel contesto di questo workpackage ha l'obiettivo di studiare l'impatto delle tecniche per costruire modelli a filtro sull'individuazione di nozioni interessanti di equivalenza comportamentale. Alcuni esperimenti in questa direzione sono già stati fatti e sono disponibili nella letteratura sui sistemi distribuiti con processi mobili [DDG99,CD02,MZ04]. Il nostro obiettivo è quello di indagare la possibilità di definire modelli a filtro per calcoli con tipi dinamici, e di confrontare le equivalenze così indotte con quelle definite utilizzando tecniche standard, come quelle operazionali basate su bisimulazione e tracce.


WP3 - Logiche di Specifica.
Le logiche modali stanno giocando un ruolo sempre più centrale nella formalizzazione e nella verifica di proprietà dinamiche di sistemi mobili e distribuiti. L'allocazione e l'accesso alle risorse, la diffusione dell'informazione, e le diverse proprietà topologiche sono specificate per mezzo di operatori modali spaziali e temporali e quindi verificate con sistemi di prova e/o con il supporto di model checker. Più in dettaglio, le attività del workpackage procederanno secondo due direzioni.

*Logiche modali per proprietà spaziali e temporali di sistemi aperti. Questo tema di ricerca si focalizzerà sull'uso delle logiche per ragionare sul comportamento dei processi in sistemi aperti, e per controllare le loro interazioni. Questa linea di lavoro ha due obiettivi complementari che condividono motivazioni e tecniche. Da un lato, miriamo a sviluppare logiche per la specifica e verifica di proprietà comportamentali di processi operanti in ambienti parzialmente sconosciuti/parzialmente specificati. Il framework che noi prefiguriamo dovrebbe consentire una presentazione operazionale di sistemi parzialmente specificati composti da componenti concrete (i.e. completamente specificate), e contesti astratti che rappresentano l'ambiente che racchiude tali componenti. L'uso di equivalenze comportamentali (o preordini) per definire nozioni di accordo tra contesti astratti e componenti concrete, dovrebbe portare ad un framework logico che consenta il raffinamento dei sistemi per passi successivi. Il sistema logico sottostante dovrà fornire un meccanismo uniforme per specificare le proprietà comportamentali delle componenti concrete e dei contesti astratti, e tecniche effettive per verificare il preservarsi delle proprietà comportamentali di interesse durante la procedura di raffinamento. Al fine di garantire il mantenimento delle specifiche logiche del sistema durante il raffinamento del contesto, si dovrà dimostrare che l'equivalenza comportamentale che definisce la nozione di accordo è adeguata (e fully-abstract) rispetto all'equivalenza indotta dalla logica. Una linea parallela di lavoro mirerà a sviluppare strumenti per l'analisi comportamentale di sistemi aperti basati su sistemi di transizione simbolici. L'obiettivo qui è quello di analizzare il comportamento dei sistemi aperti, ossia contesti con buchi, senza che questi vengano istanziati esplicitamente, ma piuttosto stabilendo le proprietà che i processi da inserire nei buchi dovranno soddisfare. I requisiti che un componente dovrebbe soddisfare (ossia, le azioni che questo è in grado di eseguire o le risorse di cui avrà bisogno) per potersi inserire nel contesto saranno espressi tramite formule logiche; questo influenzerà la nozione di equivalenza comportamentale. Come parte di questa ricerca, studieremo anche logiche capaci di esprimere nozioni di freshness, una proprietà centrale per la specifica di sistemi in grado di generare risorse nuove o segrete.

*Espressività e decidibilità delle logiche spaziali. Questa linea di ricerca coinvolge questioni più fondazionali riguardanti l'espressività e la decidibilità di alcune delle logiche spaziali attualmente studiate in letteratura. Una caratteristica peculiare di queste logiche è la loro intensionalità , che rende la nozione di equivalenza associata alla logica più fine dell'equivalenza indotta dalla semantica operazionale standard. Questo è in singolare contrasto con ciò che accade nelle logiche modali classiche, la cui caratterizzazione risulta correlare le equivalenze logiche e comportamentali (tipicamente espresse come bisimulazioni) esistenti. L'obiettivo della nostra ricerca è di indagare sulle conseguenze di questa intensionalità sul problema della decidibilità delle logiche. Puntiamo a definire logiche spaziali che siano in accordo con la semantica operazionale, esattamente come accade per le logiche modali classiche e la bisimilarità . A complemento del nostro lavoro sull'espressività , intendiamo inoltre studiare logiche che si prestino ad esprimere proprietà spaziali e comportamentali di modelli grafici e di sistemi di riscrittura di grafi. Queste tecniche saranno poi applicate per ragionare sui calcoli per sistemi distribuiti con mobilità , e specificatamente per esprimere proprietà topologiche quali: "due dati processi saranno sempre connessi mediante un canale", o "un agente che richiede un servizio sarà prima o poi connesso ad esso".


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.


Giustificazione della richiesta di finanziamento Il finanziamento richiesto dal consorzio verrà utilizzato per assumere due assegnisti di ricerca, uno per 12 mesi a metà tempo per tutta la durata del progetto, e l'altro per 15 mesi a tempo pieno con inizio al mese 9. La parte rimanente del finanziamento verrà utilizzata per spese addizionali sostenute dai contraenti principali per hardware (desktop e laptop), diffusione dei risultati (tasse di iscrizione a conferenze, spese di viaggio e di sussistenza), visite reciproche tra membri del progetto e collaborazioni sui temi del progetto con personale esterno.


Struttura del consorzio Il progetto sarà intrapreso da un consorzio di quattro unità di ricerca, un consorzio volontariamente piccolo, sia nel numero dei contraenti che nella grandezza dei team,in modo da semplificare la gestione del progetto su un piccolo insieme di obiettivi comuni ben definiti, e mantenere il progetto centrato sui suoi scopi.


Risultati Attesi
Anticipiamo i seguenti contributi dei diversi workpackage. Dove non altrimenti specificato, i contributi si baseranno su articoli tecnici pubblicati o sottoposti a revisione per la pubblicazione in riviste e/o atti di conferenze internazionali, e daranno conto dei principali risultati raggiunti nei corrispondenti argomenti di ricerca.

  . Certificati "type-based" per il controllo della mobilità ed il confinamento di agenti.

  . Osservabili "resource-centric" per equivalenze comportamentali in sistemi distribuiti con mobilità.

  . Inferenza e ricorstruzione di tipi per codice mobile.

  . Analisi di politiche per la gestione di risorse.

  . Teorie algebriche e assiomatizzazione in presenza di mobilità.

  . Specifica e raffinamento di sistemi aperti basati su logiche modali.

  . Controllo degli accessi mediante tipi in sistemi aperti.

  . Tecniche coinduttive per la bisimulazione in calcoli concorrenti distribuiti.

  . Ottimizzazione guidata dai tipi per algoritmi e strumenti di verifica.

Inoltre, ai mesi 12 e 24 produrremo dei rapporti tecnici che descrivono in dettaglio lo stato di avanzamento dei lavori sui casi di studio. In particolare, produrremo i seguenti documenti:

  . Mobilità e comunicazione in reti ad-hoc: specifiche formali e tecniche di verifica.

  . Protezione di risorse e di dati mediante certificazione di codice mobile.


Coordinamento e auto-valutazione
Il progetto sarà gestito in modo semplice ma efficace per assicurare l'avanzamento lungo le linee di lavoro proposte. Il coordinamento sarà assicurato dal Project Coordination Board (PCB), composto dal Project Coordinator (PC) e dai tre Workpackage Leaders (WPL). I responsabili scientifici delle unità del progetto svolgeranno il ruolo di WPL, come anticipato precedentemente: ciascun WPL è responsabile del coordinamento del lavoro tecnico di un workpackage, e assicura che gli obiettivi del workpackage siano raggiunti in modo da permettere la stesura dei deliverable finali. Ci saranno degli incontri regolari, almeno due volte all'anno, dei membri del PCB, in modo da assicurare un monitoraggio constante dell'avanzamento del progetto. Il PCB inviterà esperti di chiara fama, esterni al progetto, ad agire da project advisor, nel ruolo di revisori della qualità scientifica e della rilevanza dei risultati prodotti.

La valutazione avverrà in coincidenza con i naturali punti cardine del progetto ai mesi 8, 16 e 24. I meeting di progetto, tramite presentazioni dei risultati ai membri e agli advisor del progetto, costituiranno i momenti di valutazione. Nell'organizzazione di questi meeting cercheremo di massimizzare la coordinazione con progetti analoghi, in modo da aumentare la diffusione dei risultati e lo scambio di idee.



Testo inglese
The research plan is structured around three theory-centered workpackages directed towards the development of specification methods and analysis and verication techniques. The activities will be organized along three disciplines and themes:

  * Typing Systems (WP1): this workpackage targets the development of typing techniques to assist the deployment of certified, strongly typed, code. Our approach here adheres to the approach that has become known as language-based security, and is increasingly being associated with the practice of packaging code with type-based certificates forauthorization, access and resource usage to be checked by trusted verifiers prior to execution.

  * Behavioral Equivalences (WP2): this workpackage focuses on the development of advanced equivalence theories for migrating processes and their enclosing contexts. This study is particularly relevant to the purpose of the present proposal, as equivalence theories are instrumental to formalize and verify important computational properties related to information-flow security, secrecy and authentication, to establish the correctness of transformation (e.g. compilation) techniques, to reason on expressiveness, ... and more.

  * Specification Logics (WP3): this workpackage complements the work in WP1 and WP2 by developing logical theories for specification and verification. It complements WP1 by providing powerful temporal and spatial modalities to characterize resources allocation and access, information disclosure, and diverse topological properties of the computational environments, to be verified proof-theoretically and/or with the aid of model checkers. It complements WP2 by providing alternative notions of equivalence, based on the equi-satisfaction of logical formulas, and by characterizing extensional/behavioral properties as well as intentional/spatial properties of the systems of interest.

An orthogonal workpackage, focussed on concrete cases of study will provide challenges and feedback to the techniques developed. This complementary activity will thus ensure constant moninoring of the project advance, assess its progress towards the intended objectives. All workpackages will run throughout the project focussing on their inter-dependent themes and progressing towards their objectives. They all draw on operational models of processes and resources. These models will take the form of high-level process calculi or, more abstractly, of labelled transition systems built around the visible actions and observables effects of process execution in the computational environments of interest.


WP1 - Typing Systems
Our research will proceed along two complementary directions. On one side, we will design type systems to enforce the authorization constraints and the system-wide resource access restrictions and usage bounds placed by computational environments on the code they host. On the other side, we will investigate new techniques to express decentralized, discretionary policies to control the administration of capabilities and their propagation among the components of the system. Distinctive of both activities will be the need to accommodate techniques to address the lack of centralized knowledge, control and trust characteristic of the systems of interest in this proposal. Our activities will be organized along the topics we discuss next.

  * Mobility control and resource management. We will investigate extensions of current type systems for resource access and code mobility control to provide mechanisms for monitoring and restricting process mobility within confined areas, so as to prevent migrations on malicious nodes. Such systems should provide ways to dynamically tune the access rights and privileges of migrating code on the basis of the code's behavior, its originating site, the (trust level of) the locations traversed during its execution. The systems we target should make it possible to characterize the behavior of mobile code by means of types and effects describing the capabilities available for the code to operate on resources. We shall focus on analyses in which process behavior is described by putting capabilities and resources in security classes, and then refine our work by developing systems with dynamic and dependent types.

  We will also devise systems to enforce bounds on the use of resources. Work on resource bounds has initiated only recently in the literature on concurrent and distributed systems [TZH02,BBDS03]. Our plan is to investigate how to extend the ideas and techniques of [HJ03,CW00,CEI+05] to concurrent settings. This is a rather innovative, and challenging task for at least two reasons. On the one side, the existing techniques do not scale naturally to concurrent languages and systems due to the inherent nondeterminsm of resource allocation in this setting. On the other side, current process calculi lack explicit representation for resource boundedness and its import on the ability of processes to allocate new resources (channels, locations), use, deallocate and garbage collect them. Similarly, virtually no literature is available on typing techniques to specify and enforce the associated QoS requirements for communication channels or availability of resources.

  To cope with systems in which no centralized knowledge, control, and trust may be assumed, we will devise novel mechanisms and protocols to establish the credentials of migrating code and to define the negotiation of authorization rights. A natural place for such negotiation activity to take place is at location boundaries: boundaries are therefore very special entities, for which we will explore different formalizations. We envision two solutions for that.

  On one side, we will develop techniques that complement local, static typing of migrating code, with dynamic, just in time type checking to be performed at location boundaries to certify the visiting code. Since the type information of such code could be partial, inaccurate or missing, specific emphasis will be given to the development of type inference and reconstructing systems. Central to this activity will be the study of type theories which admit principal types, or typings, to guide type inference and reconstruction, and to support compositional type analyses.

  As an alternative approach, we will investigate solutions for certifying incoming code based on equipping nodes and computing entities with guardians, or membranes, that should be able to react to, or to manage, attempts to perform forbidden actions and to spawn processes over to them. We shall contrast the relative merits and expressive power of the two solutions.

  * Decentralized information-flow and capability control. This line of work complements the activity on resource access control by devising techniques to place restrictions on the propagation of capabilities across system locations and components. Specifically, we target the development of type systems that provide for decentralized and dynamic administration of access rights, and the selective propagation of capabilities based on the clearance and trust level of the intended recipients. Drawing inspiration from existing work [CDV03,HR02,Mye99], we plan to develop type theories to control the dynamic flow of resources and capabilities among system components, and study their extensions required to express policies for down/upgrading of the access rights.

  The plan here is to extend the work in [BCC04] in two, largely orthogonal directions: on one side, to port them to calculi with explicit locations and distribution, such as the Dpi calculus; on the other side, we will extend our current framework to capture more flexible policies, personalized on specific users and services, by relying on system with dynamic and dependent types.

  We will also investigate the implementation of the resource management policies of interest in low-level process calculi equipped with cryptographic primitives. Specifically, the solution we envision here is based on implementing the selective distribution of access rights by a corresponding distribution of term-level capabilities protected by encryption under secret keys only known to the intended receiver users (or else under those users' public keys). To assess the adequacy of this implementation schema, we will then develop systematic techniques to contrast the untyped equivalences of the low-level cryptographic calculi with the typed equivalences of the high-level, and typed, source calculi.

  A related activity targets the development of typing techniques to express information-flow policies based on declassification. The security policies we intend to model should support the specification of dynamic changes of the levels to which resources may be assigned, and predicate such changes to dynamic conditions. The import of such policies will be assessed in terms of refined notions of non-interference, formalized by means of corresponding observation equivalences.


WP2 - Behavioral Equivalences
Behavioral equivalences, based on testing and bisimulation, are well understood for the case of classical, first-order process calculi and, to some extent, also for pure calculi for name mobility like the pi-calculus. Consolidated progress has been made over the years on operational techniques based on co-inductive methods and up-to techniques, or traces. This workpackage seeks to develop similar techniques for systems whose components are mobile, distributed, open, (partially) typed, possibly untrusted.
Our activities will develop along several inter-dependent directions, detailed below.

  * Equivalences with types and distribution. In process theory, two processes are equal if they cannot be distinguished by any context expressed in the given process calculus. While this notion of equivalence has an elegant declarative/extensional flavor, the quantification over all possible observing contexts makes it rather awkward to use in proofs: thus one employs stronger versions based on the actions a process can perform [SW01]. However, in presence of types, distribution, or higher-order features the ordinary notion of action is much too strong, and the very meaning of "two processes perform the same actions" is unclear. For instance, it is unclear which actions of processes should be considered relevant, or equal, as distribution and types may imply the equivalence of syntactically very different actions. Some initial results on this problem exist, but they only apply to few, specific, calculi. We target the development of a general, uniform, framework in which several type systems and foundational calculi can be accommodated, and in which the existing results can be extracted as special cases.

  We will make extensive use of labelled transition systems, but considerable innovation will be required in order to use these descriptive techniques on the systems of interest. The use of these techniques in the elaboration of bisimulation-based behavioral equivalences will also require novel developments of existing methodologies. This includes not only the definition of the equivalences themselves and the proofs of their congruence properties, but also the development of enhanced co-inductive techniques such as the so-called ``bisimulation-up-to'' techniques that in the pure pi-calculus have been shown to be essential for carrying out proofs.

  * Techniques for automatic verification, minimization and equivalence checking. This line of work studies the use of different techniques to support the development of formal tools for mechanizing (or assisting) equivalence proofs, and of techniques to increase the efficiency of such tools. Types may prove very effective in this context, as they may help prune the proof search-space: for instance, certain types guarantee that communications are not preemptive, a partial confluence property, in the presence of which only parts of process behaviors need to be explored. Symbolic techniques [HeLi95] will also be employed to assist the development of equivalence proofs based on the ability to provide finitary representations of the execution graphs.

  A further line of work will explore axiomatizations of typed and/or distributed calculi. Axiomatizations have been developed for a variety of classical process calculi, giving complete sets of algebraic laws characterizing various notions of behavioral equivalence. There would be significant interest in extending these to take typing and spatial distribution into account. Serious challenges arise here to extend the results currently available in first-order process calculi. One difficulty is related to the expansion law (by which parallel process composition may be expressed as the sum of their individual actions) which is usually not available, or only limitedly available, with types or distribution. A further challenging problem is in the inherently higher-order nature of the actions characterizing the migration of processes across locations (via explicit movement, or communication)

* Behavioral equivalences for information-flow security. Our goal is to develop accurate and efficient techniques for specifying and enforcing security policies that control information flow while also allowing information release (i.e., declassification) where appropriate. This in turn requires the development of adequate formalisms for expressing such policies in a way that enables their automatic verification. The starting point for this investigation will be the characterization of non-interference in these calculi, which we have proposed recently in [CR05]. The security policies we intend to model should support the specification of dynamic changes of the levels through which resources may be assigned, and to predicate such changes to the verification of suitable conditions.

  * Logical relations. Logical relations are a powerful technique, widespread in the denotational semantics of traditional sequential languages, for proving behavioral properties such as termination (for instance, to ensure that the computation of a term will terminate), and parametricity (for instance, to prove that two terms that can manipulate different types of values are indistinguishable). Indeed, in typed higher-order sequential languages sometimes logical relations are at present the only viable techniques to prove behavioral properties (some examples are for instance in [Pit98]). We believe that logical relations could be equally useful in languages of typed processes. Some initial work in transplanting logical relations to processes is [San02], but the resulting language is still rather functional; work is needed in order to capture more general process patterns.

  * Filter model constructions. A further line of work in this workpackage studies the impact of filter model constructions in capturing interesting notions of behavioral equivalences. Some experiments in that direction have already been carried out in the literature on mobile and distributed systems [DDG99,CD02,MZ04]. Our goal here is to investigate the possibility of defining filter models for calculi with dynamic types and to compare their induced equivalences with the ones defined with more standard, operational techniques based on bisimulations and traces.


WP3 - Specification Logics.
Modal logics are playing an increasingly central role in the formalization and verification of dynamic properties of mobile and distributed systems. Resources allocation and access, information disclosure, and diverse topological properties are specified by means of temporal and spatial modalities and then verified proof-theoretically and/or with the aid of model checkers. Recent progress has also being made on the development of logics equipped with contextual operators to be employed for compositional specification of open systems. Drawing on this body of work, the activities of this workpackage will proceed along two directions.

  * Modal logics for behavioral and spatial properties of open systems. This research theme focuses on the use of logics to reason on the behavior of processes in open systems, and to control their interaction. This line of work has two complementary objectives which share motivations and techniques.

  On one side, we aim at developing logics to specify and verify behavioral properties of processes operating in partially unknown/unspecified environments. The framework we envision relies on operational presentations of partially specified systems composed of concrete (i.e. fully specified) components, and abstract contexts representing the enclosing environments of such components. By relying on behavioral equivalences (or preorders) to define notions of agreement between abstract contexts and concrete components, we aim at developing a logical framework for stepwise system refinement. The underlying logical system should provide uniform mechanisms for specifying the behavioral properties of the concrete components and of the abstract contexts, and effective ways to verify the preservation of the behavioral properties of interest along the refinement process. In order to guarantee the preservation of logical specification of the system through context refinement, the behavioral equivalences defining the notion of agreement should be proved to be adequate (and fully abstract) with respect to the equivalence induced by the logic.

  A parallel line of work aims to develop behavioral analysis of open systems based on symbolic transition systems. The goal here is to analyze the behavior of open terms, i.e. contexts with holes, without instantiating them explicitly, but rather by predicating on the properties expected of the processes to be `plugged into' the holes. Modal formulae will be employed to define requirements that a component should meet (e.g., the actions it can perform or the resources it will ask for) to be allowed to instantiate one of the context holes, thus influencing the notion of behavioral equivalence. As part of this research, we will also investigate logics capable of expressing notions of freshness which is central for the specification of systems with fresh or secret resources.

  * Expressiveness and decidability of spatial logics. This line of work involves more foundational questions of expressiveness and decidability of some of the spatial logics currently studied in the literature.
A distinctive feature of such logics is their intensionality, which makes the associated notion of logical equivalence much finer than the equivalences induced by standard operational semantics. This is in striking contrast with the situation for classical modal logics, for which characterization results relating logics and operational equivalences (typically forms of bisimilarity) exist. The goal of our research here is to investigate the consequences of this intensionality on decidability problems for the logics. We aim at defining spatial logics that agree with operational semantics, just like classical modal logics do with bisimilarity. A direction of work we envision here is to introduce a notion of "transparency" for the logical operators so as to prevent the logic to directly observe the entire structure of the model, and thus reflect the computational properties of contexts, which can be `opaque' and do not allow the inspection of their contents.
As a complement to our work on expressiveness, we also plan to investigate logics to express behavioral and spatial properties of graphical models. Such techniques will later be applied to reason on calculi for distributed systems with mobility, and specifically on topological properties such as: "two given processes will be always connected by a channel", "no untrusted agent will ever be co-located with a secret resource" or "an agent asking for a service will be eventually connected to it".


Case Studies
While it will be a specific objective of this workpackage to isolate interesting examples and benchmarks for the techniques and methods developed by the project, as we mentioned earlier in the proposal we already have specific plans in that direction.

A first scenario we will address concerns the analysis of protocols to regulate communication and routing in wireless ad-hoc networks. In such networks there is no fixed infrastructure such as base stations or mobile switching centers: mobile devices (or nodes) cooperate to forward packets for each other. Nodes that are physically located within their transmission range communicate directly via wireless links, while those that are far apart rely on other nodes to relay messages as routers. The network route from some sender node to a destination node may require a number of intermediate nodes to forward packets to create a "multi-hop" path from this sender to this destination. The features of ad-hoc networks make traditional fixed-network routing protocols inadequate. Indeed, most ad-hoc routing protocols are cooperative by nature, and rely on implicit trust-your-neighbor relationships to route packets among participating nodes. This naive trust model allows malicious nodes to paralyze an ad-hoc network by inserting erroneous routing updates, replaying old routing information, changing routing updates, or advertising incorrect routing information. For example, two protocols that are under consideration by the IETF for standardization, Dynamic Source Routing (DSR) [J02], Ad-hoc On-demand Distance Vector routing protocol (AODV) [PRD02], and "secure" protocols based on them, such as Ariadne [HPJ02] and Authenticated Routing for Ad hoc Networks (ARAN) [S05], allow attackers to easily advertise falsified route information, to redirect routes, and to mount other security attacks. While the correctness of such protocols is still typically established by way of simulation, the added-value of rigourous models for such protocols, to be then analyzed and formally verified is self-evident.

The second scenario we envision addresses an increasingly common practice by which users dowload code to run on their devices --laptops, PDAs, etc. Downloaded code may include software updates, applications, games, active web pages, and more. All these are potential home to viruses worms and other malicious code that may corrupt data on the host system, may violate privacy, or deny service to other applications by overusing system resources. The latter problem is particularly relevant for small devices with limited computational power. While the research in analysis techniques for mobile code execution has developed powerful tools for data corruption (such as bytecode verification) the enforcement of resource bounds is considerably less developed, and flexible techniques to address this problem are still largely unavailable. Similarly, several techniques for bytecode verification are developed for sequential code, and fail to address the effects of nondeterminism and concurrency in the analysis.


Structure of the consortium
The project will be undertaken by a consortium of four research units, a purposely small consortium -- both in the number of contractors and in the size of the teams -- so as to ease project management on a small set of clearly defined common goals, and keep the project very focused on its objectives. We detail the role of each unit below, in the dedicated section of the proposal, leaving a more detailed description of the research by each unit on the specific themes of the project is given in part B of the proposal.


Justification of funding
The consortium asks funding to employ two reserch fellows on the project, one for 12 months, working part time on the project for its full duration, the other for 15 months working full time and starting at month 9. The remaining funding request is for additional costs incurred by the contractors on additional admnistrative overheads, hardware (PCs) for PhD students, dissemination (conference fees, travel and subsistence), exchange visits, and research collaborations on the themes of the project with external personnel.


Expected Results
We anticipate the following deliverables for the theory-centred workpackages. When not otherwise specified, each deliverable will be based on technical articles published, or submitted for publication, in international journals and/or conference proceedings, and will provide insight into the most significant achievements on the corresponding subject of research.

  . Type-based certificates for mobility control and confinement.

  . Resource-centric observables for behavioral equivalences in distributed calculi with mobility.

  . Type inference and reconstraction for mobile code.

  . Analysis and enforcement of resource bounds policies.

  . Algebraic theories and Axiomatizations in the presence of name and code mobility.

  . Specification and refinement of open systems based on modal logics.

  . Type-based access control and resource bounds in untrusted networks.

  . Coinductive techniques for bisimulation in calculi with explicit distribution.

  . Type-driven optimizations for verification algorithms and tools.

In addition, at months 12 and 24, we will deliver reports detailing the progress of the work on the case studies. More precisely, we anticipate the following deliverables:

  . Mobility and communication in ad-hoc networks: formal specification and verification.

  . Resource and data protection via mobile code inspection and certification.


Management and self-evaluation
The project will employ a simple but effective management practice. Coordination will be ensured by the Project Coordination Board (PCB), composed by the Project Coordinator (PC) and three Workpackage Leaders (WPL). The principal investigators of the project contractors will act as WPLs, as outlined earlier on: WPLs are responsible for coordinating the technical work of a workpackage, and ensure that the workpackage's objectives are achieved with timely production of deliverables. Regular meetings of the PCB, at least twice a year, will ensure constant monitoring of the project progress. The PCB will invite renowned personalities, external to the project, to act as project advisors, whose role is to review the scientific quality and relevance of the project's production.

Evaluation will take place in rounds coincident with the natural milestones of the project at months 12 and 24. Project meetings, with presentation of results to project members and to the project advisors will mark the evaluation rounds.




Descrizione del ruolo delle Unità operative locali


Testo italiano

Unità I
BUGLIESI Michele
 
Questa unità, spesso denominata Unità C nella proposta, contribuirà con la propria esperienza riconosciuta a livello internazionale su tecniche di verifica per protocolli crittografici, se su analisi di proprietà sicurezza e controllo degli accessi basate su sistemi di tipo e equivalenze comportamentali. Oltre ad essere attiva sui workpackages WP1-3, l'unità coordinerà il lavoro sui casi di studio. In questo modo assicurerà una effettiva azione di coordinamento del progetto attuata mediante il monitoraggio costante progresso delle attività e della qualità dei risultati prodotti. 
Unità II
COPPO Mario
 
Questa unità, spesso denominata Unità T nella proposta, ha competenze riconosciute a livello mondiale su teorie di tipi e, più di recente, su algebre di processi per sistemi distribuiti. L'unità contribuirà a tutte le attività del progetto ed in particolare, in forza della propria esperienza su tecniche di analisi basate su teorie dei tipi, si prenderà carico del coordinamento del relativo workpackage WP1. 
Unità III
DE NICOLA Rocco
 
Questa unità, denominata Unità L nella proposta, metterà a disposizione le proprie competenze riconosciute a livello internazionale su semantiche per algebre di processi, sul progetto di linguaggi di coordinamento in ambienti mobili, e linguaggi di specifica basati su logiche modali e temporali. Oltre a fornire contributi su tutte le tematiche del progetto, questa unità coordinerà le attività sul workpage WP3. 
Unità IV
SANGIORGI Davide
 
Questa unità, denominata Unità E nella proposta, ha esperienza e competenza riconosciute a livello internazionale su tecniche coinduttive per la caratterizzazione di equivalence comportamentali (tipate e non) e le relazioni di queste con logiche spaziali. Oltre ad essere attiva sui workpakages WP1-3 il contributo prevalente al progetto sarà sulle equivalenze comportamentali relative al workpackage WP2 del cui coordinamento l'unità si farà carico. 


Testo inglese
Unit I
BUGLIESI Michele
 
This unit, referred to as Unit C in the proposal, will contribute its world-renowned competence in verification techniques for cryptographic protocols, and on security and resource access control analysis based on type systems and behavioral equivalences. In addition to being active on Workpackages 1-3, Unit C will lead the work on case studies, thus effectively coordinating the activities of the project as a whole, by ensuring constant monitoring on the project's progress and continuing feedback to the other workpackages. 
Unit II
COPPO Mario
 
This unit, referred to as Unit T in the proposal, has world-recognized competence on foundational type theories and, more recently, on ambient-based calculi for distributed systems. Unit T will contribute to all of the reseach themes of the project; furthremore, given its expertise on type-based analyses, it will take the lead on the activities in the workpackage WP1. 
Unit III
DE NICOLA Rocco
 
This unit, referred to as Unit L in the proposal, will contribute its world-recognized expertise on process semantics, on languages for coordination and mobility, and on specification languages based on modal and temporal logics. In addition to its contribtions to the other project activities, unit L will coordinate the work on WP3 thus taking the lead of the work on specification logics. 
Unit IV
SANGIORGI Davide
 
This unit, referred to as Unit E in the proposal, has world-known competence on (typed) coinductive techniques and their relationships with spatial logics. In addition to being active on Workpackages 1-3, this unit's most prominent contributions to the project will be on the behavioral equivalences addressed in WP2, of which unit E will take the leadership. 



PARTE III
3.1 Spese delle Unità di Ricerca

  Unità I  Unità II  Unità III  Unità IV 
Grandi Attrezzature  0  0  0  0 
Materiale inventariabile  4.000  4.000  9.000  2.300 
Materiale di consumo e funzionamento  4.000  3.500  4.000  3.600 
Spese per calcolo ed elaborazione dati  0  0  1.000  0 
Personale a contratto  23.000  0  0  18.000 
Servizi esterni  0  1.500  3.000  0 
Missioni  12.000  14.000  10.000  9.100 
Pubblicazioni  0  0  1.000  0 
Partecipazione / Organizzazione convegni  4.000  4.000  3.000  7.000 
Altro   3.000  6.000  2.000  5.000 
TOTALE 50.000  33.000  33.000  45.000 


3.2 Costo complessivo del Programma di Ricerca

  Unità I  Unità II  Unità III  Unità IV 
RD+RA (fondi di Ateneo)  15.000  10.000  10.000  13.500 
Cofinanziamento di altre amministrazioni pubbliche, private o fondazioni  0  0  0  0 
Cofinanziamento richiesto al MIUR  35.000  23.000  23.000  31.500 
Costo totale del programma  50.000  33.000  33.000  45.000 


   Euro   
Costo complessivo del Programma   161.000 
 
Risorse complessivamente disponibili all'atto della domanda (RD + RA)   48.500 
 
Cofinanziamento di altre amministrazioni pubbliche, private o fondazioni   0 
 
Cofinanziamento richiesto al MIUR   112.500 



(per la copia da depositare presso l'Ateneo e per l'assenso alla diffusione via Internet delle informazioni riguardanti i programmi finanziati e la loro elaborazione necessaria alle valutazioni; D. Lgs, 196 del 30.6.2003 sulla "Tutela dei dati personali")




Firma _____________________________________   Data 15/04/2005 ore 18:24