MINISTERO DELL'UNIVERSITÀ E DELLA RICERCA
DIREZIONE GENERALE PER IL COORDINAMENTO E LO SVILUPPO DELLA RICERCA
PROGRAMMI DI RICERCA SCIENTIFICA DI RILEVANTE INTERESSE NAZIONALE
RICHIESTA DI COFINANZIAMENTO (DM n. 1175 del 18 settembre 2007)

PROGETTO DI RICERCA - MODELLO A
Anno 2007 - prot. 200793N42R

1 - Titolo del Progetto di Ricerca


Testo italiano
SOFT - Tecniche formali orientate alla sicurezza


Testo inglese
SOFT - Security-Oriented Formal Techniques


2 - Durata del Progetto di Ricerca

24 Mesi  


3 - Area Scientifico-disciplinare

01: Scienze matematiche e informatiche  100%   


4 - Settori scientifico-disciplinari interessati dal Progetto di Ricerca

INF/01 - Informatica 


5 - Coordinatore Scientifico

FOCARDI  RICCARDO 
Professore Associato confermato   30/01/1970  FCRRCR70A30A944O 
Università "Ca' Foscari" di VENEZIA 
Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI 
Dipartimento di INFORMATICA 
041-2348438
(Prefisso e telefono)
 
041-2348419
(Numero fax)
 
focardi@dsi.unive.it 

* il progetto partecipa alla riserva del 10% di cui al punto 7 dell'art. 3

6 - Curriculum scientifico


Testo italiano
Riccardo Focardi ha conseguito, nel marzo 1993, la laurea in Scienze dell'Informazione e, nel febbraio 1999, il Dottorato di Ricerca in Informatica presso l'Università degli Studi di Bologna. Dall'ottobre 1996 al dicembre 2002, è stato ricercatore presso il dipartimento di Informatica dell'Università Ca' Foscari di Venezia e, dal dicembre 2002, è Professore Associato presso lo stesso dipartimento. Gli interessi di ricerca di Riccardo Focardi includono: la specifica di proprietà di sicurezza di sistemi e reti e la loro verifica formale ed automatica, lo studio di modelli matematici e di linguaggi per descrivere il comportamento di sistemi concorrenti e distribuiti. È autore di più di 60 pubblicazioni tra riviste e congressi internazionali nel settore. Ha partecipato a progetti nazionali ed europei nel campo della sicurezza informatica e, per questi ultimi, ha svolto anche attività come revisore. È stato membro di numerosi comitati di programma di conferenze internazionali, tra cui IEEE Symposium of Security and Privacy, International Workshop on Issues in the Theory of Security (Program Chair nel 2007) e IEEE Computer Security Foundations Workshop che, divenuto Symposium nel luglio 2007, è l'evento di riferimento per lo studio di metodi formali applicati alla sicurezza (Program Chair nel 2003, 2004 e General Chair nel 2006 e 2007). Ha inoltre organizzato la seconda e terza "International School On Foundations Of Security Analysis And Design". Dal 1999 è membro e segretario del IFIP Working Group 1.7 "Theoretical Foundations of Security Analysis and Design" e dal 2005 è nell'editorial board del Journal of Computer Security (IOS Press). È infine docente titolare dei corsi di "Sicurezza", "Sistemi Operativi B" e "Laboratorio di Sistemi Operativi" presso i corsi di Laurea triennale e specialistica in Informatica dell'Università Ca' Foscari di Venezia.


Testo inglese
Riccardo Focardi received the "Laurea" degree and the PhD in Computer Science from the University of Bologna, Italy, in 1993 and 1999, respectively. From October 1996 to December 2002, he has been Assistant Professor at the department of computer science of the University of Venice, Italy. Since December 2002, he is Associate Professor at the same department. Research interests of Riccardo Focardi include: the specification of security properties of concurrent systems and their formal and automated verification; the investigation of mathematical models and of languages for the description of concurrent and distributed systems. He has published more than 60 research papers on these topics, in international journals and conferences. He has been involved into national and European projects on Computer Security, and, for the latter, he has also served as a reviewer. He has been member of many program committees of international conferences, among which the IEEE Symposium of Security and Privacy, the International Workshop on Issues in the Theory of Security (Program Chair in 2007) and the IEEE Computer Security Foundations Workshop, upgraded to Symposium in July 2007, and representing the reference event for the study of foundational issues in computer security (Program Chair in 2003, 2004 and General Chair in 2006 and 2007). Riccardo Focardi has organized the second and third "International Schools on Foundations of Security Analysis and Design" (FOSAD). Since 1999 he is member and secretary of IFIP Working Group 1.7 "Theoretical Foundations of Security Analysis and Design" and since 2005 he is member of the editorial board of the Journal of Computer Security (IOS Press). He teaches "Security", "Operating Systems B" and "Operating Systems Lab" courses for the Computer Science "Laurea triennale" (Bachelor) and "Laurea specialistica" (Master) of University Ca' Foscari of Venice, Italy.


7 - Pubblicazioni scientifiche più significative del Coordinatore Scientifico

1. BRAGHIN C, CORTESI A, FOCARDI R. (2007). Information Flow Security in Boundary Ambients. INFORMATION AND COMPUTATION. ISSN: 0890-5401. to appear.  
2. M. BACKES, A. CORTESI, FOCARDI R., M. MAFFEI. (2007). A Calculus of Challenges and Responses. 5th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE'07). November 2007. ACM Press.  
3. M. BUGLIESI, FOCARDI R., M. MAFFEI. (2007). Dynamic Types for Authentication. JOURNAL OF COMPUTER SECURITY. vol. 15 (6), pp. 563-617 ISSN: 0926-227X.  
4. FOCARDI R., R. LUCCHI, G. ZAVATTARO. (2006). Secure shared data-space Coordination Languages: a Process Algebraic survey. SCIENCE OF COMPUTER PROGRAMMING. vol. 63(1), pp. 3-15 ISSN: 0167-6423. Elsevier.  
5. FOCARDI R., S. ROSSI. (2006). Information Flow Security in Dynamic Contexts. JOURNAL OF COMPUTER SECURITY. vol. 14(1), pp. 65-110 ISSN: 0926-227X.  
6. C. BODEI, P. DEGANO, FOCARDI R., C. PRIAMI. (2005). Authentication primitives for secure protocol specifications. FUTURE GENERATION COMPUTER SYSTEMS. vol. 21(4), pp. 645-653 ISSN: 0167-739X.  
7. FOCARDI R. (2005). Static Analysis of Authentication. LECTURE NOTES IN COMPUTER SCIENCE. vol. 3655, pp. 109-132 ISSN: 0302-9743. Foundations of Security Analysis and Design III, Tutorial Lectures.  
8. FOCARDI R., MAFFEI M., PLACELLA F. (2005). Inferring Authentication Tags. 2005 IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS Workshop on Issues in the Theory of Security (WITS'05).  
9. FOCARDI R., ROSSI S, SABELFELD A. (2005). Bridging Language-Based and Process Calculi Security. LECTURE NOTES IN COMPUTER SCIENCE. vol. 3441, pp. 299-315 ISSN: 0302-9743. 8th International conference on Foundations of Software Science and Computation Structure (FoSSaCS).  
10. M. BUGLIESI, FOCARDI R., M. MAFFEI. (2005). Analysis of Typed Analyses of Authentication Protocols. 18th IEEE Computer Security Foundation Workshop (CSFW2005). (pp. 112-125). ISBN/ISSN: 0-7695-2340-4.  
11. ANNALISA BOSSI, FOCARDI R., CARLA PIAZZA, SABINA ROSSI. (2004). Verifying persistent security properties. COMPUTER LANGUAGES, SYSTEMS AND STRUCTURES. vol. 30(3-4), pp. 231-258 ISSN: 1477-8424. Elsevier.  
12. BUGLIESI M., FOCARDI R., MAFFEI M. (2004). Authenticity by Tagging and Typing. 2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE 2004). October 2004. (pp. 1-12). ACM Press.  
13. CHIARA BRAGHIN, AGOSTINO CORTESI, FOCARDI R., FLAMINIA L. LUCCIO, CARLA PIAZZA. (2004). Nesting analysis of mobile ambients. COMPUTER LANGUAGES, SYSTEMS AND STRUCTURES. vol. 30(3-4), pp. 207-230 ISSN: 1477-8424. Elsevier.  
14. FOCARDI R., ROBERTO GORRIERI, FABIO MARTINELLI. (2004). Classification of Security Properties (Part II: Network Security). LECTURE NOTES IN COMPUTER SCIENCE. vol. 2946, pp. 331-396 ISSN: 0302-9743. In Foundation of Security Analysis and Design - Tutorial Lectures.  
15. MICHELE BUGLIESI, FOCARDI R., MATTEO MAFFEI. (2004). Compositional Analysis of Authentication Protocols. LECTURE NOTES IN COMPUTER SCIENCE. vol. 2986, pp. 140-154 ISSN: 0302-9743. European Symposium on Programming (ESOP 2004).  
16. A. BOSSI, FOCARDI R., C. PIAZZA, AND S. ROSSI. (2003). Bisimulation and Unwinding for Verifying Possibilistic Security Properties. LECTURE NOTES IN COMPUTER SCIENCE. vol. 2575 ISSN: 0302-9743. VMCAI 2003.  
17. A. BOSSI, FOCARDI R., C. PIAZZA, AND S. ROSSI. (2003). Refinement Operators and Information Flow Security. International IEEE Conference on Software Engineering and Formal Methods. (pp. 44-53). IEEE Press.  
18. C. BRAGHIN, A. CORTESI, FOCARDI R., F. L. LUCCIO AND CARLA PIAZZA. (2003). Complexity of Nesting Analysis in Mobile Ambients. LECTURE NOTES IN COMPUTER SCIENCE. vol. 2575 ISSN: 0302-9743. VMCAI 2003.  
19. C. BRAGHIN, A. CORTESI, S. FILIPPONE, FOCARDI R., F. L. LUCCIO AND CARLA PIAZZA. (2003). BANANA: A Tool for Boundary Ambients Nesting ANAlysis. LECTURE NOTES IN COMPUTER SCIENCE. ISSN: 0302-9743. Tools and algorithms for the Construction and Analysis of Systems (TACAS' 03).  
20. C.BODEI, P.DEGANO, FOCARDI R., C.PRIAMI. (2003). Authentication Primitives for Protocol Specifications. LECTURE NOTES IN COMPUTER SCIENCE. vol. 2763, pp. 49-65 ISSN: 0302-9743. PaCT'03.  
21. FOCARDI R., GORRIERI R., MARTINELLI F. (2003). Real-Time Information Flow Analysis. IEEE JOURNAL ON SELECTED AREAS IN COMMUNICATIONS. vol. 21(1) ISSN: 0733-8716.  
22. FOCARDI R., R. GORRIERI, F. MARTINELLI. (2003). A Comparison of Three Authentication Properties. THEORETICAL COMPUTER SCIENCE. vol. 291(3) ISSN: 0304-3975.  
23. MICHELE BUGLIESI, FOCARDI R., MATTEO MAFFEI. (2003). Principles for Entity Authentication. LECTURE NOTES IN COMPUTER SCIENCE. vol. 2890, pp. 294-307 ISSN: 0302-9743. Fifth International Conference PERSPECTIVES OF SYSTEM INFORMATICS (PSI 2003).  
24. BODEI C., DEGANO P., FOCARDI R., PRIAMI C. (2002). Primitives for Authentication in Process Algebras. THEORETICAL COMPUTER SCIENCE. vol. 283(2) ISSN: 0304-3975.  
25. C. BRAGHIN, A. CORTESI, FOCARDI R. (2002). Security Boundaries in Mobile Ambients. COMPUTER LANGUAGES. vol. 28(1) ISSN: 0096-0551.  
26. FOCARDI R., S. ROSSI. (2002). Information Flow Security in Dynamic Contexts. 15th IEEE Computer Security Foundations Workshop (CSFW 2002). IEEE press.  
27. DURANTE A., FOCARDI R., GORRIERI R. (2000). A Compiler for Analysing Cryptographic Protocols Using Non-Interference. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY. vol. 9(4), pp. 489-530 ISSN: 1049-331X.  
28. FOCARDI R., GORRIERI R, MARTINELLI F. (2000). Non Interference for the Analysis of Cryptographic Protocols. LECTURE NOTES IN COMPUTER SCIENCE. vol. 1853 ISSN: 0302-9743. 27th International Colloquium on Automata, Languages and Programming (ICALP'00).  
29. FOCARDI R., GORRIERI R. (1997). The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING. vol. 23(9), pp. 550-571 ISSN: 0098-5589.  
30. FOCARDI R., GORRIERI R. (1995). A Classification of Security Properties for Process Algebras. JOURNAL OF COMPUTER SECURITY. vol. 3(1), pp. 5-33 ISSN: 0926-227X.  


8 - Elenco delle Unità operative

Unità  Responsabile dell'Unità di Ricerca  Qualifica  Ente  Impegno 
I  FOCARDI Riccardo  Professore Associato confermato   Università "Ca' Foscari" di VENEZIA  72 
II  BODEI Chiara  Professore Associato non confermato   Università degli Studi di PISA  80 
III  VIGANO' Luca  Professore Associato non confermato   Università degli Studi di VERONA  96 


9 - Abstract del Progetto di Ricerca


Testo italiano
La sicurezza dei sistemi software è una questione cruciale in un mondo sempre più permeato dall'Information Technology. Il numero di servizi, accessibili via reti di natura telematica, che aiutano ad affrontare attività quotidiane va aumentando, come testimoniato dal sempre crescente numero di espressioni come e-banking, e-commerce ed e-government, ove il prefisso 'e' ne sostanzia la dimensione elettronica. Tali servizi richiedono sia lo scambio di informazioni confidenziali che la condivisione di risorse computazionali e presentano forti requisiti di sicurezza, data la grande rilevanza delle informazioni trattate e il contesto fortemente distribuito e insicuro, quale è Internet, in cui esse tipicamente operano. Si rivela importante, ad esempio, stabilire l'autenticità dei messaggi scambiati, la loro segretezza, le identità delle parti in causa, e anche avere garanzie che le diverse componenti del sistema interagiscano correttamente, senza violare le proprietà desiderate.
D'altra parte autorevoli enti, come il CERT della Carnegie Mellon University, riportano un numero sempre crescente di segnalazioni relative alla vulnerabilità dei sistemi informatici, spesso dovute a problemi nella progettazione e realizzazione del software. La soluzione tipica è quella di riparare tali "falle" rendendone più difficile l'utilizzo da parte degli attaccanti, ma questo approccio non va certamente alla radice del problema. Un approccio complementare è, invece, quello di modellare e verificare i requisiti di sicurezza fin dalla specifica di un sistema software, al fine di ridurre al minimo le vulnerabilità sul prodotto finale. L'adozione di tecniche formali può quindi giocare un ruolo molto importante per individuare possibili problemi di sicurezza fin dalle prime fasi di sviluppo, per capirne a fondo le cause e per rimuoverli prima che altre scelte progettuali ci costringano a "inventare" rimedi a posteriori, non sempre possibili e soddisfacenti. L'interesse nei metodi formali per la sicurezza è comprovato da una comunità internazionale sempre più attiva, e dal numero crescente di nuovi workshop e convegni internazionali su tale tema.
Lo scopo di questo progetto è di creare un consorzio formato da 3 Università già attive nella ricerca su metodi formali per la sicurezza e su tecniche per la verifica di proprietà di programmi e protocolli, e focalizzare le proprie energie su obiettivi comuni di ricerca. Si intende operare a largo spettro su diverse problematiche di sicurezza, focalizzando principalmente l'attenzione su tecniche di verifica statiche a livello di linguaggio, che permettano di comprendere e verificare la sicurezza a partire dalla specifica formale di un programma, senza la necessità di analizzarne l'esecuzione. Riteniamo, infatti, che questo approccio sia particolarmente promettente, sia perché si presta ad essere automatizzato tramite algoritmi di verifica efficienti sia per la migliore comprensione degli obiettivi e dei meccanismi di sicurezza che esso fornisce sia a livello di specifica che di programmazione. Ci occuperemo sia di proprietà di alto livello (o livello applicazione), come il controllo dei flussi di informazione e la sicurezza nel "Service-Oriented Computing", sia di proprietà di livello più basso (o livello comunicazione), come l'autenticazione, la segretezza e la non-ripudiabilità su reti di calcolatori e su reti ad-hoc. Considereremo sia modelli simbolici "standard" che modelli computazionali e causali, che ci permetteranno, rispettivamente, di modellare più concretamente aspetti crittografici e di formalizzare proprietà di sicurezza in termini di relazioni esplicite causa-effetto.
Come illustrato in dettaglio nelle sezioni seguenti (si vedano, in particolare, le sezioni 13 sulla descrizione del lavoro e 15 sui risultati attesi), il nostro progetto è di natura fondazionale, visto che si concentra sulla definizione e sullo sviluppo di metodologie formali per l'analisi di diversi aspetti della sicurezza informatica. Quando possibile, comunque, dimostreremo la valenza dei nostri risultati tramite concreti casi di studio provenienti da applicazioni pratiche.


Testo inglese
Security of software systems is a critical issue in a world where Information Technology is becoming more and more pervasive. The number of services for everyday life that are provided via electronic networks is rapidly increasing, as witnessed by the longer and longer list of words with the prefix "e", such as e-banking, e-commerce, e-government, where the "e" substantiates their electronic nature. These kinds of services usually require the exchange of sensible data and the sharing of computational resources, thus needing strong security requirements because of the relevance of the exchanged information and the very distributed and untrusted environment, the Internet, in which they operate. It is important, for example, to ensure the authenticity and the secrecy of the exchanged messages, to establish the identity of the involved entities, and to have guarantees that the different system components correctly interact, without violating the required global properties.
Unfortunately, many authoritative security-related organizations as, e.g., the CERT at Carnegie Mellon University, report a growing number of computer system vulnerabilities which are often the result of exploits against defects in the design or code of software. The approach most commonly employed to address such defects is to attempt to a posteriori "repair the flaw" by making it more difficult for those defects to be exploited. This solution, however, does not certainly get to the root cause of the problem and threat. A complementary approach is, instead, to model and verify security requirements from the very first specification of software systems, so to reduce as much as possible the presence of vulnerabilities on the final product. The use of formal techniques can thus play an important role to reveal possible security flaws from the very first phases of software development, to understand in depth the causes, and to remove them before it is too late and it becomes necessary to invent, if possible, some retroactive remedy. The interest in formal methods for security is confirmed by a very active international community, and by the increasing number of new international workshops and conferences on the topic.
The aim of this project is to put together a consortium of 3 Universities which are already active in the fields of formal methods for security and of software and protocol verification, and which will focus their effort on common research targets. We intend to broadly work on many different aspects of security, mainly focusing on "language-based" techniques, which have the advantage of verifying security of programs directly on their formal specification, without the need of analysing their execution. We believe that this approach is particularly appealing both because it can often be automated through efficient verification algorithms and because it gives the programmer a clear comprehension of security requirements and mechanisms. We will consider both high (i.e., application) level properties as, e.g., information flow and "Service-Oriented" security, and low (i.e., communication) level properties as, e.g., authentication, secrecy and non-repudiation on standard and ad-hoc networks. We will also study how results achieved on "standard" symbolic models scale to computational and causal models, the former providing a more concrete representation of cryptography and the latter expressing security properties in terms of explicit cause-and-effect relations.
As illustrated in more detail in the following sections (see, in particular, the sections 13 on the description of work and 15 on the expected results), our project is of a foundational nature, since it focuses on the definition and development of formal methodologies for the analysis of various aspects of information security. Whenever possible, however, we will assess our results to proof-of-concept case studies taken from practical applications.


10 - Parole chiave

Parola chiave (in italiano)  Parola chiave (in inglese) 
1. METODI FORMALI PER LA SICUREZZA  FORMAL METHODS FOR SECURITY 
2. NON INTERFERENZA  NON INTERFERENCE 
3. PROTOCOLLI E SERVIZI PER LA SICUREZZA  SECURITY PROTOCOLS AND SERVICES 
4. SICUREZZA NEI LINGUAGGI  LANGUAGE-BASED SECURITY 
5. VERIFICA STATICA E DINAMICA  STATIC AND DYNAMIC VERIFICATION 


11 - Obiettivi finali che il Progetto si propone di raggiungere


Testo italiano
La sicurezza dell'informazione è un tema sempre più attuale e rilevante, dato il crescente utilizzo di elaboratori e di reti per applicazioni critiche quali il commercio elettronico, l'home banking, l'acquisto di beni digitali e la fruizione, in genere, di servizi in linea. Diventa quindi sempre più importante capire a fondo i requisiti di sicurezza delle attuali applicazioni distribuite, e studiare metodi per la verifica automatica di tali requisiti.
Lo scopo principale del progetto SOFT è lo studio dei fondamenti della sicurezza informatica e lo sviluppo di metodi formali per la specifica e verifica di proprietà di sicurezza di programmi, sistemi e reti di elaboratori. SOFT comprende 3 Università con 11 ricercatori permanenti, 10 tra dottorandi, assegnisti e post-doc, 2 ricercatori di un ateneo estero e 2 contratti di 6-8 mesi specificatamente richiesti sul programma di ricerca, per un totale di 25 ricercatori. Le unità di ricerca sono caratterizzate da forti competenze su metodi formali per la sicurezza, analisi statica, interpretazione astratta, verifica di proprietà di programmi e semantica della concorrenza. La presenza, inoltre, di due ricercatori della Saarland University di Saarbrücken, e di un dottorando in co-tutela con la Ecole Polytechnique di Palaiseau dimostrano un'apertura verso importanti gruppi di ricerca europei nel settore.
Intendiamo operare a largo spettro su diverse problematiche di sicurezza lavorando sia su proprietà di alto livello (o livello applicazione), come il controllo dei flussi di informazione e la sicurezza nel "Service-Oriented Computing", sia su proprietà di livello più basso (o livello comunicazione), come l'autenticazione, la segretezza e la non-ripudiabilità su reti di calcolatori e su reti ad-hoc. Per quanto riguarda i metodi formali utilizzati, ci concentreremo principalmente su tecniche statiche a livello di linguaggio, che permettano di comprendere e verificare la sicurezza a partire dalla specifica o dal codice di un programma, senza la necessità di analizzarne l'esecuzione. Riteniamo, infatti, che questo approccio sia particolarmente promettente, sia perché si presta ad essere automatizzato tramite algoritmi di verifica efficienti sia per la migliore comprensione degli obiettivi e dei meccanismi di sicurezza che esso fornisce già a livello di specifica o di programmazione.

Il programma di ricerca è suddiviso in fasi e work-package. I work-package si riferiscono a obiettivi specifici del progetto e saranno descritti più avanti. Le fasi, invece, scandiscono il flusso logico e temporale delle attività e corrispondono ad una "agenda standard" nello sviluppo di metodi formali per la sicurezza:

Fase 1 - Linguaggi e modelli per la sicurezza.
Si studieranno linguaggi e modelli orientati alla sicurezza, in cui sia possibile definire e verificare politiche e proprietà per la sicurezza dell'informazione.

Fase 2 - Proprietà di sicurezza.
Si studieranno e si formalizzano proprietà di sicurezza sui linguaggi e modelli definiti durante la fase precedente.

Fase 3 - Tecniche di analisi.
Si studieranno tecniche di analisi per le proprietà e i linguaggi sopra descritti. Tali tecniche saranno principalmente statiche. Si intende, inoltre, implementare ed estendere tool di analisi basati sulle tecniche sopra menzionate.

Ogni work-package interesserà una o più fasi, a seconda della base di partenza e dello stato della ricerca.

WP1 - Sicurezza delle Reti di Comunicazione. Siamo interessati all'analisi di protocolli crittografici tramite interpretazione astratta, sistemi di tipi, control-flow analysis e semantiche causali (vedi anche WP4). Vogliamo estendere lo studio di protocolli crittografici ad applicazioni distribuite basate su crittografia, integrandolo opportunamente con le tecniche di analisi dei programmi studiate in WP2. Svilupperemo nuovi linguaggi e calcoli di processi per la descrizione di sistemi distribuiti che permettano di ragionare su aspetti di sicurezza. Svilupperemo una logica per formalizzare proprietà locali e globali di sistemi distribuiti. Ci interesseremo, infine, di modelli per la sicurezza in reti ad-hoc.

WP2 - Sicurezza a Livello Applicazione. Studieremo diversi aspetti di sicurezza di programmi tramite interpretazione astratta: in particolare, siamo interessati a problemi di verifica di non-interferenza in presenza di attaccanti attivi e su sistemi di calcolo probabilistici; ci occuperemo di confidenzialità e, in particolare, dei "covert channel" noti come "termination channel", in cui l'attaccante ottiene informazioni osservando la terminazione del programma, e di "timing channel" (vedi anche WP3). Studieremo proprietà relative al raffinamento sicuro di programmi che permettano di ottenere uno sviluppo passo-passo di applicazioni sicure a partire da specifiche astratte. Ci interesseremo, infine, dello studio di primitive per la composizione sicura di clienti e servizi nell'ambito del "Service-Oriented Computing".

WP3 - Aspetti Quantitativi della Sicurezza. Intendiamo studiare come alcune delle proprietà affrontate in WP1 e WP2 scalino su modelli più "fini", in cui tempo e probabilità vengono esplicitamente considerati. Studieremo tecniche per individuare e rimuovere attacchi basati sul tempo, trasformando il programma in modo da preservare il comportamento di input/output originale ma modificandone la temporizzazione. Intendiamo, inoltre, sviluppare nuove tecniche di analisi per la sicurezza computazionale di protocolli crittografici. Da un lato studieremo tecniche basate su tipi ed effetti per la correttezza di protocolli basati sulla libreria per operazioni crittografiche di Backes-Pfitzmann-Waidner, dall'altro approfondiremo lo studio della correttezza dell’approccio simbolico rispetto all’approccio computazionale utilizzando le relazioni di simulazione approssimate di Segala e Turrini. Infine, laddove il modello formale si rivela inadeguato a catturare aspetti piu' concreti e legati alla implementazione, vorremmo riuscire ad adattare in modo controllato il modello affiche' possa invece farlo. Cercheremo quindi di avvicinarci agli aspetti solitamente trattati nell'approccio computazionale, senza lasciare la prospettiva formale.

WP4 - Modelli Causali per la Sicurezza. La formalizzazione di varie proprietà di sicurezza può trarre beneficio dal ragionare in termini di causalità tra eventi. Nell'autenticazione tra entità, ad esempio, l'autenticazione da parte del verificatore dovrebbe essere causata dall'esecuzione del protocollo da parte del dichiarante. Intendiamo dare una nuova semantica causale ai protocolli crittografici che permetta di osservare direttamente la relazione di causa ed effetto tra la conclusione del protocollo, e quindi l'autenticazione, e la corrispettiva esecuzione del protocollo da parte dell'entità da autenticare. Intendiamo considerare sia modelli true concurrent come le event structure, sia modelli basati su Proved Transition Systems.


Testo inglese
Information security is becoming more and more relevant given the increasing usage of computers and networks for critical applications as, e.g, e-commerce, home-banking, purchase of digital goods and, in general, on-line services. It becomes thus very relevant to understand in depth the security requirements of distributed applications and to investigate methods for the automated verification of such requirements. The primary aim of the SOFT project is the study of foundations of information security and the development of formal methods for the specification and verification of security properties of programs, systems and computer networks. SOFT includes 3 Universities with 11 permanent researchers, 10 among PhD students and post-docs, 2 researchers from a foreign University and 2 contracts of 6-8 months specifically requested on this project research, for a total of 25 researchers. Research units are characterized by strong skills in formal methods for security, static analysis, abstract interpretation, verification of program properties and semantics of concurrency. The presence of two researchers from Saarland University of Saarbrücken and a PhD student co-tutored with the Ecole Polytechnique of Palaiseau shows the connection with important European research groups in the field.
We intend to cover many different aspects of security working both on high (i.e., application) level properties as, e.g., information flow and "Service-Oriented" security, and on low (i.e., communication) level properties as, e.g., authentication, secrecy and non-repudiation on standard and ad-hoc networks. Regarding formal methods, we mainly intend to investigate "language-based" techniques, which have the advantage of verifying security of programs directly on the code, without the need of analysing their execution. We believe that this approach is particularly appealing both because it can often be automated through efficient verification algorithms and because it gives the programmer a clear comprehension of security requirements and mechanisms.

The research plan is divided into phases and work-packages. Work-packages refer to specific targets of the project and will be described below. Phases, instead, reflect the logical and temporal scheduling of activities, corresponding to a "standard agenda" of the development of formal methods for security:

Phase 1 - Security oriented languages and models.
We will study security oriented languages, i.e., languages specifically developed for the specification and verification of security properties.

Phase 2 - Security properties.
We will study and formalize security properties on the languages defined in the previous phase.

Phase 3 - Analysis techniques.
We will study analysis techniques for the properties and languages described above. These techniques will mainly be language-based. We will implement and extend verification tools based on the above mentioned techniques.

Every work-package will involve one or more phases, depending on the starting point of the work-package and on the state of the art in the area.

WP1 - Communication and Network Security. We are interested in the analysis of cryptographic protocols through abstract interpretation, type systems, control flow analysis and causal semantics (see also WP4). We plan to extend the study of cryptographic protocols to distributed applications based on cryptography, by integrating this study with the program analysis techniques developed in WP2. We will propose new security-oriented languages and process calculi for distributed systems. We will develop a logic for expressing local and global properties of distributed systems. Finally, we will study security models for ad-hoc networks.

WP2 - Application Security. We will study different aspects of program security through abstract interpretation: in particular, we are interested in models and methods for verifying non-interference in presence of active attackers and in probabilistic computations; we will deal with confidentiality and, in particular, both with "termination covert channels" in which the attacker gets information by observing the program termination, and with "timing covert channels" (see WP3). We will study properties for the secure refinement of programs in order to achieve a step-by-step development of secure applications, starting from abstract specifications. Finally, we will study primitives for the secure composition of clients and services in the setting of "Service-Oriented Computing".

WP3 - Quantitative Aspects of Security. We intend to study how properties of WP1 and WP2 scale on finer-grained models, in which time and probabilities are explicitly modeled. We will study techniques to detect and remove timing attacks, by transforming a program so that its timing behaviour is corrected while the input/output behaviour is preserved. We also intend to develop new analysis techniques for computational security of cryptographic protocols. On the one hand, we will develop type-based techniques for the correctness of protocols expressed on the cryptographic library proposed by Backes-Pfitzmann-Waidner; on the other hand, we will study soundness results of the symbolic model with respect to the computational model, through the work on approximated simulation relations of Segala and Turrini. Finally, when the formal model results inadequate to capture more concrete aspects, we would like to smoothly adapt it in such a way that these can be instead captured in the refined model. In other words, we will try to get closer to the aspects typically addressed in the computational approach, without leaving the formal perspective.

WP4 - Causal models for security. In the formalization of security properties it might be beneficial to reason in terms of causality among events. For example, in entity authentication we have that authentication should always be caused by the actual execution of the protocol by the claimant. We intend to give a new causal semantics to cryptographic protocols which enables us to directly observe the causality between the protocol conclusion, i.e., the authentication, and the corresponding execution by the authenticated entity. In doing this, we will investigate both true-concurrent models like, e.g., event structures, and models of causality based on proved transition systems.


12 - Stato dell'arte


Testo italiano
Il progetto SOFT si occuperà di diverse tematiche relative ai metodi formali per la sicurezza che introduciamo, nel seguito, menzionando per ognuna di esse i principali risultati presenti in letteratura. Per facilitare la connessione con gli obiettivi del progetto, le tematiche sono state raggruppate in base all'attinenza con i quattro work-package.

- Sicurezza delle Reti di Comunicazione

I protocolli crittografici sono uno degli strumenti fondamentali per garantire sicurezza sulle reti di elaboratori. Nel momento in cui la rete di comunicazione è di grandi dimensioni, e quindi non controllabile localmente, risulta infatti necessario proteggere le informazioni in transito sulla rete tramite tecniche crittografiche. Nonostante le ridottissime dimensioni del codice, tali protocolli sono spesso soggetti ad attacchi in grado di sovvertire la logica del protocollo invalidandone le proprietà di sicurezza attese, senza necessariamente attaccare i sottostanti meccanismi crittografici. Esiste una sconfinata letteratura sull'analisi e verifica di protocolli crittografici, ma solo un piccolo sottoinsieme di tali lavori è basato sull'analisi statica (language-based). In [A99,AB05], ad esempio, viene studiata la segretezza dell'informazione e in [BBDNN05, BFM07, GJ04] l'autenticazione tramite sistemi di tipi e analisi control-flow. Intendiamo approfondire lo studio di tali tecniche focalizzando l'attenzione sull'interpretazione astratta e sulla control flow analysis di protocolli crittografici e lo studio di primitive astratte di comunicazione che permettano di rendere la programmazione indipendente dalla realizzazione crittografica. Inoltre, ci proponiamo di estendere l’analisi simbolica dei protocolli [AVISPA,Bla01,RSGLR00] in modo da consentire la specifica e verifica di una classe più ampia di protocolli e loro proprietà rispetto a quelli attualmente considerati, nonché di diversi modelli di attacco, estendendo lavori esplorativi quali [HDMV05,HDMVB06].
Ci interesseremo, infine, della sicurezza su reti "Ad-hoc". Una rete ad-hoc mobile e' un sistema autonomo costituito da dispositivi che comunicano tra di loro via radio e che sono liberi di muoversi arbitrariamente e in maniera imprevedibile. La nozione di trust in reti ad-hoc è un'area nuova e stimolante [Gli04,PM06] a causa dell'assenza di una infrastruttua di rete fissa, della mobilita' dei nodi, del limitato raggio d'azione della trasmissione, della condivisione del medium, e della vulnerabilità fisica dei dispositivi. Vorremmo sviluppare modelli formali per il trust nelle reti ad-hoc e integrare questi modelli in un calcolo di processi per reti ad-hoc [NH06,Mer07,God07] sviluppando una teoria appropriata per provare formalmente proprietà di sicurezza.

- Sicurezza a Livello Applicazione

Il controllo dei flussi di informazione nei programmi e nei sistemi è un tema piuttosto studiato nell'ambito della teoria della sicurezza. Lo scopo è il controllo delle informazioni denominate "segrete", onde evitare che esse fluiscano verso livelli di utenza non privilegiati e quindi non autorizzati all'accesso delle informazioni stesse. La Non-Interferenza è una delle proprietà di riferimento per realizzare questo tipo di controllo e fu introdotta da Goguen e Meseguer in [GM82]. Essa richiede che la modifica dei dati di alto livello non abbia alcun effetto osservabile a livello più basso o, in altre parole, non interferisca con i livelli inferiori. Esistono moltissime varianti ed estensioni della Non-Interferenza su process calculi e su semplici linguaggi imperativi. Si veda, ad esempio, [BCF02, BCFLP04, FG95, FRS05, GM04, MSZ06, RWW96, RS01, SS00, SM03, SV98]. Focalizzeremo la nostra attenzione sullo studio di Information Flow security in applicazioni distribuite con crittografia, sul raffinamento sicuro di programmi, sulla sicurezza in (frammenti multithreaded di) Java, sull'estensione della non-interferenza astratta [GM04] ad attaccanti più potenti.
La sicurezza risulta cruciale anche nell'ambito del "Service Oriented Computing", in cui le applicazioni si ottengono assemblando componenti, i servizi appunto, distribuiti lungo la rete. I servizi sono aperti, ovvero l'ambiente operativo, i clienti e gli ulteriori servizi non sono completamente specificati. Da qui la necessità di ricorrere ad appositi meccanismi per ottenerne la composizione e coordinazione sicura. I Web Services [S02], basati su tecnologie XML, sono l'esempio più significativo e meglio sviluppato di questo paradigma. Intendiamo estendere i risultati di [BDF06a, BDF06b], in cui si introduce un approccio basato su descrizioni semantiche e una metodologia che rende automatico il processo di scoperta di servizi e la pianificazione della loro composizione sicura. Ci proponiamo inoltre di estendere i modelli e le tecniche sviluppati per i protocolli crittografici ai servizi per la sicurezza. Esistono diversi approcci preliminari [BMPV06,SAMOA] ma nessuno ha raggiunto la maturità necessaria.

- Aspetti Quantitativi della Sicurezza

Recentemente, sono state studiate tecniche che permettono, lavorando a livello di analisi formale, di ottenere risultati anche su modelli computazionali, modelli in cui la sicurezza è definita in termini più classici come resistenza ad un qualsiasi attacco probabilistic polynomial-time, senza quindi considerare la crittografia come inattaccabile (si veda ad esempio [AR00, BCK05, BPW03, L05]). L'analisi formale simbolica descritta fino ad ora permette analisi più semplici e automatizzabili rispetto ai modelli computazionali, e risulta quindi interessante capire se i risultati simbolici scalano sui modelli computazionali, e sotto quali assunzioni crittografiche questo avviene. L'approccio language-based, anche in questo caso, non è stato ancora indagato approfonditamente. Un interessante articolo in questa direzione è [L05] in cui viene proposto un sistema di tipi per la segretezza dei messaggi e, tramite una semantica basata sulla "simulatable cryptographic library" [BPW03], si ottiene la scalabilità dei risultati dal modello simbolico a quello computazionale. Intendiamo sviluppare un'analisi statica basata su [BFM07] per verificare autenticazione su protocolli che usano la "simulatable cryptographic library".
Intendiamo inoltre considerare modelli ibridi che combinino i due approcci: simbolico e computazionale. Esiste già una letteratura in merito [PW01,CCKLLPS06,MRST06,CP07] dalla quale emerge anche un ruolo fondamentale del non determinismo, la cui risoluzione arbitraria può portare a conclusioni indesiderate. I problemi da risolvere sono dunque la gestione del non determinismo e lo studio di tecniche di analisi gerarchica che tengano conto di aspetti computazionali. Un recente caso di studio [ST07] ha analizzato un noto protocollo di autenticazione utilizzando i Probabilistic Automata e una nuova nozione di computationally bounded approximated simulation, che permette al sistema astratto di simulare passi di computazione a meno di un errore trascurabile. Il lavoro costituisce un valido punto di partenza per lo studio di verifica composizionale gerarchica della sicurezza.

- Modelli Causali per la Sicurezza

Nell'ambito dello studio di protocolli crittografici, sono state proposte tecniche in cui le dipendenze causali tra eventi giocano un ruolo estremamente importante [BCM07,CW01,FHG98,P99]. Ne sono esempi gli strand spaces [FHG98] in cui le dipendenze causali sono rese esplicite, e il metodo induttivo di Paulson [P99] in cui le dipendenze sono conseguenza di regole induttive. I Proved Transition Systems [DP92,DP99] sono modelli capaci di catturare la causalità. Li possiamo immaginare come una sorta di rappresentazione compatta delle computazioni, in grado di contenere tutta l’informazione rilevante che si può codificare. Le transizioni sono decorate con etichette che codificano le dimostrazioni, ovvero i passi necessari nella deduzione dell’azione appena eseguita. Ispezionando tali etichette è possible inferire le dipendenze causali, rappresentate con un insieme di riferimenti alle transizioni precedenti. Utilizzando come punto di partenza la semantica arricchita in [BetAl05], intendiamo approfondire lo studio delle semantiche causali basate su Proved Transision Systems e su modelli true-concurrent per l'analisi di protocolli crittografici.
La Distributed State Temporal Logic (DSTL) [MSS04] permette di mettere in relazione causale proprietà che valgono in componenti distinte di un sistema. La logica include un operatore primitivo per specificare eventi, rendendo possibile mescolare condizioni ed eventi nelle formule che definiscono la specifica del sistema. La capacità di usere esplicitamente gli eventi aumenta la capacità espressiva e la semplicità delle specifiche logiche, e sembra essere particolarmente adeguata per descrivere proprietà di sicurezza. Partendo da [MS04], intendiamo indagare ed estendere l'utilizzo della DSTL per specificare e verificare applicazioni in cui le componenti presentano requisiti di sicurezza.


Bibliografia

[A99] M. Abadi. Secrecy by Typing in Security Protocols. Journal of the ACM, 46(5):749–786, 1999.

[AB05] M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102–146, 2005

[AR00] M. Abadi and P. Rogaway. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In proc. of IFIP TCS 2000 (LNCS 1872) pp. 3–22.

[AVISPA] The AVISPA Project. www.avispa-project.org

[BBDNN05] C.Bodei, M.Buchholtz, P.Degano, F.Nielson, H.R.Nielson. Static Validation of Security Protocols. JCS 13(3), 2005.

[BCF02] C.Braghin, A. Cortesi, and R. Focardi. Security Boundaries in Mobile Ambients. Computer Languages, 28(1):101-127, 2002

[BCFLP04] C. Braghin, A. Cortesi, R. Focardi, F.L. Luccio, and C. Piazza. Nesting Analysis of Mobile Ambients. Computer Languages, Systems & Structures 30(3-4):207-230, 2004

[BCK05] M. Baudet, V. Cortier and S. Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries, In Proc. of ICALP'05. LNCS 3580. pp. 652-663.

[BCM07] M. Backes, A. Cortesi, M. Maffei. Abstracting Multiplicity in Cryptographic Protocols. In Proc. of IEEE CSF'07, pp. 355-369

[BDF06a] M.Bartoletti, P.Degano, G.L.Ferrari. Plans for service composition. Proc. of WITS, 2006.

[BDF06b] M.Bartoletti, P.Degano. G.L.Ferrari. Types and effects for secure orchestration. Proc. of IEEE CSFW, 2006.

[BetAl5] C.Bodei, M.Buchholtz, P.Degano, M.Curti, C.Priami, F.Nielson, H.R.Nielson. On Evaluating the Performance of Security Protocols specified in Lysa. Proc. of PACT05, LNCS 3606.

[BFM07] M. Bugliesi, R. Focardi and M. Maffei. Dynamic Types for Authentication, Journal of Computer Security, IOS Press, 15(6):563-617, 2007

[Bla01] B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. IEEE CSFW’01

[BMPV06] M. Backes, S. Moedersheim, B. Pfitzmann, L. Vigano`. Symbolic and Cryptographic Analysis of the Secure WS-Reliable Messaging Scenario. In Proc. of FOSSACS’06. LNCS 3921.

[BPW03] M. Backes, B. Pfitzmann, and M. Waidner. A Universally Composable Cryptographic Library. In proc. of ACM CCS 2003, pp. 220-230.

[CCKLLPS06] R. Canetti, L. Cheung, D. Kirli Kaynar, M. Liskov, N. A. Lynch, O. Pereira, R. Segala: Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols. In Proc. of DISC’06. LNCS 4167, pp 238-253.

[CP07] K. Chatzikokolakis, C. Palamidessi. Making Random Choices Invisible to the Scheduler. In Proc. of CONCUR’07. LNCS 4703, pp. 42-58.

[CW01] F.Crazzolara, G.Winskel. Events in Security Protocols. In ACM CCS, 2001.

[DP92] P.Degano, C.Priami. Proved Trees. In Proc. of ICALP'92.

[DP99] P.Degano, C.Priami. Non Interleaving Semantics for Mobile Processes. TCS 216, 1999.

[FG95] R. Focardi and R. Gorrieri, A Classification of Security Properties for Process Algebras, Journal of Computer Security, 3(1):5-33, 1995

[FHG98] F.J.T. Fábrega, J.C.Herzog, J.D.Guttman. Strand spaces: Why is a security protocol correct? JCS 7(2-3), 1999.

[FRS05] R. Focardi, S. Rossi, A. Sabelfeld: Bridging Language-Based and Process Calculi Security. In Proc. of FoSSaCS 2005 pp. 299-315. LNCS 3441

[GJ04] A. D. Gordon and A. Jeffrey. Types and effects for asymmetric cryptographic protocols. Journal of Computer Security, 12(3-4):435–483, 2004

[Gli04] V.D.Gligor. Security of Emergent Properties in Ad-Hoc Networks. Security Protocols Workshop 2004

[GM04] R. Giacobazzi and I. Mastroeni. Abstract Non-Interference. POPL'04

[God07] J.C. Godskesen. A Calculus for Mobile Ad Hoc Networks. COORDINATION'07

[HDMV05] P. Hankes Drielsma, S. Moedersheim, L. Vigano`. A Formalization of Off-Line Guessing for Security Protocol Analysis. LPAR04

[HDMVB06] P. Hankes Drielsma, S. Moedersheim, L. Vigano`, D. Basin. Formalizing and Analyzing Sender Invariance. FAST’06

[L05] P. Laud. Secrecy types for a simulatable cryptographic library. In Proc. of the 12th ACM CCS '05. New York, NY, 26-35.

[MRST06] J. C. Mitchell, A. Ramanathan, A. Scedrov, V. Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. TCS 353, 2006

[MSZ06] A. C. Myers, A. Sabelfeld, and S. Zdancewic. Enforcing Robust Declassification. Journal of Computer Security, 14(2):157-196, 2006.

[NH06] S.Nanz, C.Hankin. A Framework for Security Analysis of Mobile Wireless Networks. TCS 367, 2006

[Mer07] M.Merro. On the Observational Theory of Mobile Ad-Hoc Networks. Information and Computation, to appear.

[MSS04] C.Montangero, L. Semini and S. Semprini. Logic Based Coordination for Event-Driven Self-Healing Distributed Systems. Proc. of COORDINATION'04, LNCS 2949.

[MS04] C.Montangero, L. Semini. Formalizing an Adaptive Security Infrastructure in Mobadtl. Proc. of FCS'04.

[P99] L.C.Paulson. Proving security protocol correct. Proc. of Lics, 1999.

[PM06] A.A. Pirzada, C.McDonald. Trust Establishment in Pure Ad-Hoc Networks. Wireless Personal Communication 379, 2006

[PW01] B. Pfitzmann, M. Waidner: A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission. IEEE Symposium on S&P 2001

[RS01] P. Ryan and S. Schneider, Process algebra and Non-Interference, Journal of Computer Security 9(1/2):75–103, 2001.

[RSGLR00] P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. Modelling and Analysis of Security Protocols. 2000

[RWW96] A.W. Roscoe, J.C.P. Woodcock and L. Wulf, Non-Interference through determinism, Journal of Computer Security 4(1):27-54, 1996.

[S02] M.Stal. Web services: Beyond component-based computing. Comms. Of the ACM 55(10), 2002.

[SAMOA] Samoa: Formal Tools for Securing Web Services. http://research.microsoft.com/projects/samoa/.

[SS00] A. Sabelfed and D. Sands, Probabilistic Noninterference for multi-threaded programs, in: Proc. of IEEE CSFW 2000, pp.200-215.

[SM03] A. Sabelfeld and A.C. Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communication 21(1):5-19, 2003.

[ST07] R. Segala, A. Turrini. Approximated Computationally Bounded Simulation Relations for Probabilistic Automata. IEEE CSF07

[SV98] G. Smith and D.M. Volpano, Secure information flow in a multi-threaded imperative language, in: Proc. of 25th ACM POPL, pp.355-364, 1998


Testo inglese
SOFT project will focus on diverse research topics related to the application of formal methods to security, that we shortly describe below. To clarify the connection with project targets we have grouped topics depending on the specific work-package they belong to.

- Communication and Network Security

Cryptographic protocols are one of the fundamental mechanisms for achieving security on computer networks. Wide-area networks are, in fact, not controllable and there is a need to protect sent/received data through cryptographic techniques. Even if these protocols are often just a few lines of codes, many attacks subverting the protocol logic and invalidating the expected security properties have been found. These attacks are not necessarily based on cryptographic flaws and can be reproduced even when cryptography is considered as a fully reliable black box. In the literature we find a huge amount of contributions on the analysis and verification of security protocols, but only a few of them follow a language-based approach, i.e., are based on static-analysis. We mention here some relevant papers on secrecy [A99,AB05] and authentication [BBDNN05, BFM07, GJ03, GJ04]. We intend to go on on this line of research by focussing on abstract interpretation and control flow analysis of cryptographic protocols and abstract communication primitives to make programming independent of cryptographic implementation. Moreover, we also aim to extend the symbolic protocol analysis approach [AVISPA,Bla01,RSGLR00] in order to allow for the specification and verification of a larger class of protocols and properties than currently possible, as well as of different attackers models, extending preliminary work such as [HDMV05,HDMVB06].
We will finally consider security on Ad-hoc networks. A Mobile Ad-Hoc Network is an autonomous system composed of devices communicating with each other via radio transceivers. Mobile devices are free to move randomly and organize themselves arbitrarily; thus, the network's wireless topology may change rapidly and unpredictably. Trust establishment in the context of ad-hoc networks is still an open and challenging field [Gli04,PM06], because of lack of a fixed networking infrastructure, high mobility of the devices, limited range of the transmission, shared wireless medium, and physical vulnerability. We would like to develop formal models of trust that fit the constrains of ad-hoc networking, integrating these models in a process calculus for ad-hoc networks [NH06,Mer07,God07], thus developing an appropriate theory to formally prove security properties.

- Application Security

Controlling information flow in programs and systems is a fundamental security issue whose theoretical foundations have been extensively studied. The aim is to control secret information so that it cannot flow towards unprivileged users who do not have the clearance to access it. Non-Interference is one of the reference properties for achieving this kind of control, and it was introduced by Goguen and Meseguer in [GM82]. The main idea is to require that any possible modifications of high level data have no observable effects at lower levels or, in other words, do no interfere with lower views of the system. In literature, we find many variants and extensions of Non-Interference on process calculi and simple imperative languages; see, e.g., [BCF02, BCFLP04, FG95, FRS05, GM04, MSZ06, RWW96, RS01, SS00, SM03, SV98]. Our research will specifically focus on Information Flow Security of distributed programs with cryptography, secure refinement of programs, security of (a multi-threaded fragment of) Java and extending the abstract non-interference framework [GM04] in order to deal with more powerful attackers.
Security also plays a crucial role in Service Oriented Computing. In this scenario, applications are built by assembling stand-alone components distributed over a network, called services. Services are open, i.e., built with little or no knowledge about their operating environment, their clients, and further services. Therefore, their secure composition and coordination may require peculiar mechanisms. Web Services [S02] built upon XML technologies are probably the most illustrative and well developed example of this paradigm. We intend to extend the results of [BDF06a, BDF06b], where we propose an approach based on semantic descriptions and a methodology which automates the process of discovering services and planning their composition in a secure way. Moreover, we plan to scale up the techniques developed for protocol analysis to security services. There are a number of preliminary approaches in this direction [BMPV06,SAMOA], but none of them has yet reached the required maturity.

- Quantitative Aspects of Security

There are recent papers studying how formal analysis scales to computational security, a model of security requiring resistance over all the possible probabilistic polynomial-time attacks. This model, differently from Dolev-Yao, does not consider cryptography as a secure black box (see, e.g., [AR00, BCK05, BPW03, L05]). A formal symbolic analysis, à la Dolev-Yao, is typically simpler and easier to automate with respect to computational models. It is thus appealing to understand how symbolic formal results scale to these models and under which cryptographic assumptions this may happen. Even in this setting, the language-based approach has not been extensively studied. An interesting paper in this direction is [L05], which proposes a type system for message secrecy. It exploits a semantics based on the "simulatable cryptographic library" [BPW03] to scale the results to computational models. We intend to develop a static analysis based on [BFM07] for the verification of authentication protocols using the "simulatable cryptographic library".
We also intend to explore hybrid models that combine the two approaches: symbolic and computational. There is already a related literature [PW01,CCKLLPS06,MRST06,CP07] that in particular highlights a fundamental role of nondeterminism, for which an arbitrary resolution may lead to undesired conclusions. Thus, the main open problems are a correct management of nondeterminism and the study of hierarchical techniques that take care of computational aspects as well. The recent case study [ST07] analyses a simple and well known authentication protocol using Probabilistic Automata and a new notion of computationally bounded approximated simulation that allows an abstract system to emulate computational steps of a concrete system up to some negligible error. This case study constitutes a significant starting point for developing hierarchical and compositional proof methods for security.

- Causal models for security

In the literature on cryptographic protocols analysis, we find some recent approaches in which the causal dependencies among events play a very important role [BCM07,CW01,FHG98,P99]. Strand spaces [FHG98] are a well known method in which causal dependencies are made explicit. In the inductive method of [P99], dependencies are instead a consequence of inductive rules. Proved Transition systems [DP92,DP99] represent an extension of transition systems towards causality. Proved Transition Systems can be considered as a sort of compact representation of computations, containing all the possible encodable and relevant information. Transitions are enriched with labels encoding their proofs, i.e. the steps involved in the deduction process of the action just executed. By inspecting the transition labels, it is possible to infer the causal dependencies, represented through a set of references to previous transitions. Starting from the enhanced semantics of [BetAl05], we intend to investigate the possible application of causal semantics based on Proved Transition Systems and on true-concurrent models, to the analysis of cryptographic protocols.
The Distributed State Temporal Logic (DSTL) [MSS04] permits to causally relate properties, which might hold in distinguished components of a system, in an asynchronous setting. The logic includes a primitive operator to specify events, thus allowing us to mix conditions and events in the specification formulae. The ability to deal with events explicitly enhances the expressiveness and simplicity of logical specifications, and seems especially adequate in the case of security properties specification. Starting from [MS04], we intend to further investigate the use of DSTL for the specification and verification of applications in which components presents various security requirements.


References

[A99] M. Abadi. Secrecy by Typing in Security Protocols. Journal of the ACM, 46(5):749–786, 1999.

[AB05] M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102–146, 2005

[AR00] M. Abadi and P. Rogaway. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In proc. of IFIP TCS 2000 (LNCS 1872) pp. 3–22.

[AVISPA] The AVISPA Project. www.avispa-project.org

[BBDNN05] C.Bodei, M.Buchholtz, P.Degano, F.Nielson, H.R.Nielson. Static Validation of Security Protocols. JCS 13(3), 2005.

[BCF02] C.Braghin, A. Cortesi, and R. Focardi. Security Boundaries in Mobile Ambients. Computer Languages, 28(1):101-127, 2002

[BCFLP04] C. Braghin, A. Cortesi, R. Focardi, F.L. Luccio, and C. Piazza. Nesting Analysis of Mobile Ambients. Computer Languages, Systems & Structures 30(3-4):207-230, 2004

[BCK05] M. Baudet, V. Cortier and S. Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries, In Proc. of ICALP'05. LNCS 3580. pp. 652-663.

[BCM07] M. Backes, A. Cortesi, M. Maffei. Abstracting Multiplicity in Cryptographic Protocols. In Proc. of IEEE CSF'07, pp. 355-369

[BDF06a] M.Bartoletti, P.Degano, G.L.Ferrari. Plans for service composition. Proc. of WITS, 2006.

[BDF06b] M.Bartoletti, P.Degano. G.L.Ferrari. Types and effects for secure orchestration. Proc. of IEEE CSFW, 2006.

[BetAl5] C.Bodei, M.Buchholtz, P.Degano, M.Curti, C.Priami, F.Nielson, H.R.Nielson. On Evaluating the Performance of Security Protocols specified in Lysa. Proc. of PACT05, LNCS 3606.

[BFM07] M. Bugliesi, R. Focardi and M. Maffei. Dynamic Types for Authentication, Journal of Computer Security, IOS Press, 15(6):563-617, 2007

[Bla01] B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. IEEE CSFW’01

[BMPV06] M. Backes, S. Moedersheim, B. Pfitzmann, L. Vigano`. Symbolic and Cryptographic Analysis of the Secure WS-Reliable Messaging Scenario. In Proc. of FOSSACS’06. LNCS 3921.

[BPW03] M. Backes, B. Pfitzmann, and M. Waidner. A Universally Composable Cryptographic Library. In proc. of ACM CCS 2003, pp. 220-230.

[CCKLLPS06] R. Canetti, L. Cheung, D. Kirli Kaynar, M. Liskov, N. A. Lynch, O. Pereira, R. Segala: Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols. In Proc. of DISC’06. LNCS 4167, pp 238-253.

[CP07] K. Chatzikokolakis, C. Palamidessi. Making Random Choices Invisible to the Scheduler. In Proc. of CONCUR’07. LNCS 4703, pp. 42-58.

[CW01] F.Crazzolara, G.Winskel. Events in Security Protocols. In ACM CCS, 2001.

[DP92] P.Degano, C.Priami. Proved Trees. In Proc. of ICALP'92.

[DP99] P.Degano, C.Priami. Non Interleaving Semantics for Mobile Processes. TCS 216, 1999.

[FG95] R. Focardi and R. Gorrieri, A Classification of Security Properties for Process Algebras, Journal of Computer Security, 3(1):5-33, 1995

[FHG98] F.J.T. Fábrega, J.C.Herzog, J.D.Guttman. Strand spaces: Why is a security protocol correct? JCS 7(2-3), 1999.

[FRS05] R. Focardi, S. Rossi, A. Sabelfeld: Bridging Language-Based and Process Calculi Security. In Proc. of FoSSaCS 2005 pp. 299-315. LNCS 3441

[GJ04] A. D. Gordon and A. Jeffrey. Types and effects for asymmetric cryptographic protocols. Journal of Computer Security, 12(3-4):435–483, 2004

[Gli04] V.D.Gligor. Security of Emergent Properties in Ad-Hoc Networks. Security Protocols Workshop 2004

[GM04] R. Giacobazzi and I. Mastroeni. Abstract Non-Interference. POPL'04

[God07] J.C. Godskesen. A Calculus for Mobile Ad Hoc Networks. COORDINATION'07

[HDMV05] P. Hankes Drielsma, S. Moedersheim, L. Vigano`. A Formalization of Off-Line Guessing for Security Protocol Analysis. LPAR04

[HDMVB06] P. Hankes Drielsma, S. Moedersheim, L. Vigano`, D. Basin. Formalizing and Analyzing Sender Invariance. FAST’06

[L05] P. Laud. Secrecy types for a simulatable cryptographic library. In Proc. of the 12th ACM CCS '05. New York, NY, 26-35.

[MRST06] J. C. Mitchell, A. Ramanathan, A. Scedrov, V. Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. TCS 353, 2006

[MSZ06] A. C. Myers, A. Sabelfeld, and S. Zdancewic. Enforcing Robust Declassification. Journal of Computer Security, 14(2):157-196, 2006.

[NH06] S.Nanz, C.Hankin. A Framework for Security Analysis of Mobile Wireless Networks. TCS 367, 2006

[Mer07] M.Merro. On the Observational Theory of Mobile Ad-Hoc Networks. Information and Computation, to appear.

[MSS04] C.Montangero, L. Semini and S. Semprini. Logic Based Coordination for Event-Driven Self-Healing Distributed Systems. Proc. of COORDINATION'04, LNCS 2949.

[MS04] C.Montangero, L. Semini. Formalizing an Adaptive Security Infrastructure in Mobadtl. Proc. of FCS'04.

[P99] L.C.Paulson. Proving security protocol correct. Proc. of Lics, 1999.

[PM06] A.A. Pirzada, C.McDonald. Trust Establishment in Pure Ad-Hoc Networks. Wireless Personal Communication 379, 2006

[PW01] B. Pfitzmann, M. Waidner: A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission. IEEE Symposium on S&P 2001

[RS01] P. Ryan and S. Schneider, Process algebra and Non-Interference, Journal of Computer Security 9(1/2):75–103, 2001.

[RSGLR00] P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. Modelling and Analysis of Security Protocols. 2000

[RWW96] A.W. Roscoe, J.C.P. Woodcock and L. Wulf, Non-Interference through determinism, Journal of Computer Security 4(1):27-54, 1996.

[S02] M.Stal. Web services: Beyond component-based computing. Comms. Of the ACM 55(10), 2002.

[SAMOA] Samoa: Formal Tools for Securing Web Services. http://research.microsoft.com/projects/samoa/.

[SS00] A. Sabelfed and D. Sands, Probabilistic Noninterference for multi-threaded programs, in: Proc. of IEEE CSFW 2000, pp.200-215.

[SM03] A. Sabelfeld and A.C. Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communication 21(1):5-19, 2003.

[ST07] R. Segala, A. Turrini. Approximated Computationally Bounded Simulation Relations for Probabilistic Automata. IEEE CSF07

[SV98] G. Smith and D.M. Volpano, Secure information flow in a multi-threaded imperative language, in: Proc. of 25th ACM POPL, pp.355-364, 1998


13 - Articolazione del Progetto e tempi di realizzazione


Testo italiano
Procediamo ora alla descrizione dettagliata del programma di ricerca, suddiviso in work-package e fasi. Le fasi scandiscono il flusso logico e temporale delle attività. Si noti, però, che la presenza di tematiche diverse all'interno dello stesso work-package consente di portare avanti differenti ricerche contemporaneamente, anche su fasi diverse. In sezione 15, per ogni work-package, indicheremo i principali risultati attesi. Tali risultati saranno sufficientemente specifici da poter essere verificati e costituiranno, quindi, lo strumento primario per la valutazione dell'avvenuto raggiungimento degli obiettivi del progetto.

WP1 - Sicurezza delle Reti di Comunicazione.

Unità coinvolte: Pisa, Venezia, Verona.

Fase 1

Modelli formali per il trust e calcoli per reti ad-hoc: svilupperemo modelli logici di trust allo scopo di formalizzare la natura dinamica e variabile delle relazioni di trust tra le diverse componenti delle reti distribuite, con particolare attenzione al soddisfacimento dei vincoli specifici delle reti ad hoc. A tale scopo, considereremo innanzitutto il contesto delle reti ad hoc mobili in ambienti ostili, per poi considerare le reti ad-hoc auto-organizzate. Lavoreremo anche all'integrazione di questi modelli in un calcolo di processi per reti ad-hoc sviluppando una teoria appropriata per provare formalmente proprietà di sicurezza.

Fase 2

Logiche orientate alla sicurezza: svilupperemo una nuova logica temporale per agenti comunicanti che fornisca un linguaggio intuitivo e allo stesso tempo espressivo per formalizzare proprietà locali (agent-specific) e globali (system-wide) di sistemi distribuiti. Questa logica verrà utilizzata per l'analisi di protocolli di sicurezza ed allo stesso tempo per formalizzare e provare meta-proprietà di vari modelli per protocolli crittografici. La logica sarà integrata in un tool chiamato AVISPA e descritto in Fase 3.

Fase 3.

Analisi di protocolli crittografici: Intendiamo continuare lo studio, avviato in [BCFM07], di calcoli di processi per protocolli di autenticazione in cui i messaggi cifrati vengono astratti in sfide o risposte su un calcolo privo di crittografia. Di fatto, il protocollo crittografico viene astratto in un protocollo contenente speciali messaggi di sfida e risposta inviati e ricevuti su un modello Dolev-Yao, astrazione di quello usuale. Formalizzeremo l'astrazione in termini di interpretazione astratta in modo da ottenere risultati generali sulle astrazioni stesse e sulla preservazione delle proprietà di sicurezza tra il calcolo concreto e quello astratto. Studieremo tecniche di verifica efficienti su tali astrazioni. Inoltre, intendiamo analizzare i protocolli anche utilizzando l'analisi control-flow, che, in generale, fornisce approssimazioni (chiamate soluzioni) sicure e calcolabili del comportamento dei processi. Punto di partenza e' l'analisi data in [BBDNN05]. Oltre ai vantaggi delle tecniche statiche, questo approccio presenta l'ulteriore vantaggio che una sola analisi basta per svariate proprietà: controlli diversi su una stessa soluzione permettono di verificare infatti proprietà diverse, senza dover ricorrere ad una nuova analisi. Infine, ricorreremo a semantiche simboliche per facilitare sia lo sviluppo di metodi di verifica effettivi sia il trattamento dei problemi di incompletezza tipici della verifica di proprietà di sicurezza.

Tool di verifica: AVISPA e' un tool integrato per la convalida automatica di protocolli di sicurezza e applicazioni per sistemi distribuiti. È stato utilizzato con successo su protocolli industriali come IKE, SET, e altri protocolli in corso di standardizzazione. AVISPA può essere sensibilmente migliorato, specialmente per quanto riguarda le tecniche formali su cui si basa. Ad esempio, l'estensione di queste tecniche formali a linguaggi più naturali per modellare proprietà di sicurezza renderebbe il tool di più facile comprensione ad utenti non esperti. Inoltre abbiamo iniziato a studiare la possibile integrazione di AVISPA con tecniche di riduzione e semplificazione ispirate dalla riduzione di ordine parziale e alla interpretazione astratta. Queste tecniche, insieme a tecniche di astrazione forniranno le basi per l'applicazione di AVISPA all'analisi formale e automatica di proprietà di sicurezza per Web services e più in generale nell'area del "Service Oriented Computing", che considereremo in WP2.
In tool per l'analisi control-flow presentato in [BBDNN05] e' completamente automatico e termina sempre in un tempo polinomiale nella dimensione della specifica del protocollo. Le nuove analisi proposte al punto precedente verranno quindi supportate tramite opportune estensioni di tale tool, in accordo con il fatto che una singola analisi si può facilmente adattare per trattare proprietà diverse.

WP2: Sicurezza a Livello Applicazione

Unità coinvolte: Pisa, Venezia, Verona.

Fase 1

Calcoli per sistemi distribuiti: Intendiamo estendere, con primitive di comunicazione crittografiche, semplici linguaggi imperativi, allo scopo di integrare l'analisi dei protocolli crittografici con l'analisi Information-Flow delle componenti locali studiata in WP2. Studiare proprietà dei protocolli e dei programmi in unico framework chiarificherà le relazioni tra le proprietà definite nei due diversi contesti e permetterà di definire librerie per lo sviluppo di applicazioni distribuite. Si lavorerà nella direzione di garantire al programmatore un buon livello di astrazione e trasparenza rispetto alla effettiva realizzazione crittografica. Questo obiettivo è fortemente correlato al WP1.

Calcoli e linguaggi per "Service-Oriented Computing": studieremo primitive linguistiche orientate alla sicurezza dei clienti e dei servizi. La selezione dei servizi non dovrebbe essere basata sui "nomi" (es. l'identità del produttore del servizio), ma sulle proprietà di cui essi godono. Intendiamo, quindi, sviluppare ulteriormente il meccanismo di chiamata per proprietà originariamente proposto in [BDF05], considerando anche altre proprietà di sicurezza (es. information-flow) e aspetti non-funzionali (es. transazioni, qualità del servizio).
Svilupperemo, inoltre, linguaggi e metodi formali basati su “abstract model-checking” per la specifica formale di servizi di sicurezza. Questo permettera di modellare e ragionare su proprieta' e servizi di sicurezza, sia a livello di rete sia a livello di applicazione, includendo non solo "authentication" e "secrecy", ma anche "authorization", controllo degli accessi, “policies”, “trust” e "identity management" e cosi` via, oltre a nuovi modelli dell’attaccante quali quelli considerati in [HDMV05,HDMVB06].

Fase 2

Raffinamento sicuro di programmi: analizzeremo varie operazioni di raffinamento su linguaggi imperativi orientati alla sicurezza, quali la specializzazione di componenti astratte, la cancellazione di scelte non-deterministiche e la sostituzione di sottocomponenti. Per ciascuna operazione considereremo diverse proprietà di sicurezza ed identificheremo le condizioni sotto le quali l'operazione e' applicabile. Per ottenere questo risultato intendiamo percorrere la stessa linea seguita nell'ambito delle process algebra in [BFPR04] dove prima viene definito un framework generale per la definizione di proprietà di non interferenza e poi vengono individuate condizioni sufficienti per il loro mantenimento durante i passi di raffinamento.

Fase 3

Analisi di applicazioni distribuite: Svilupperemo sistemi di tipi dinamici per la verifica di applicazioni distribuite con crittografia. In particolare, ci interesseremo di integrare sistemi di tipi per protocolli crittografici con sistemi di tipi per programmi scritti in semplici linguaggi imperativi. Ispirandoci a [BFM07], utilizzeremo dei tag nei messaggi cifrati per trasportare, in modo affidabile, informazioni sulle caratteristiche di sicurezza dei vari messaggi scambiati. Basandoci su questa informazione dinamica, verificabile da chi riceve il messaggio, definiremo un sistema di tipi dinamici per l'analisi di sicurezza di applicazioni distribuite con primitive crittografiche. Questo obiettivo si colloca tra il WP1 e il WP2.

Analisi di "Service-Oriented Computing": Ci occuperemo del problema di orchestrare un'applicazione basata su servizi, garantendo che non se ne abortisca l'esecuzione per colpa di azioni che tentano di violare la sicurezza. Questo problema di pianificazione consiste nel selezionare dalla rete quei servizi che svolgono il compito richiesto, e al contempo rispettano i vincoli di sicurezza imposti. Estenderemo alcune proposte presenti in letteratura, basate su sistemi di tipi e model-checking, a scenari dinamici dove i servizi possono essere pubblicati dinamicamente e divenire temporaneamente non disponibili. Intendiamo inoltre trattare la composizione di servizi assieme ai protocolli per la sicurezza ed alle relazioni di affidabilità, al fine di garantire che un servizio certificato non cambi il proprio codice a tempo di esecuzione.

Non-interferenza astratta: siamo interessati a studiare i problemi di trasformazione del codice con particolare riferimento a modelli e metodi per la verifica di non-interferenza in presenza di attaccanti attivi, su sistemi di calcolo probabilistici e su basi di dati. L'idea di fondo è quella di vedere l'interpretazione astratta e la non-interferenza astratta come schema unificante per esprimere sia i modelli di attacco al sistema (attivo attraverso malware o passivo attraverso osservazione semantica) che il tipo di informazione nascosta (e.g., nei dati protetti) e come questa si evolve durante la computazione (information-flow analysis). L'obiettivo è quello di ottenere una teoria unificante basata su interpretazione astratta per derivare in un unico schema concettuale algoritmi efficaci per proteggere il codice ed i dati e verificarne la sicurezza.

WP3 - Aspetti Quantitativi della Sicurezza

Unità coinvolte: Pisa, Venezia, Verona.

Fase 1 e 2

Calcoli per protocolli crittografici: svilupperemo un calcolo di processi per protocolli crittografici con semantica basata sulla libreria crittografica di Backes, Pfitzmann e Waidner [BPW03]. La libreria crittografica è dotata di due semantiche, la prima simbolica e la seconda computazionale. È stato dimostrato che, in generale, una proprietà di sicurezza soddisfatta dalla semantica simbolica è soddisfatta anche da quella computazionale. Quindi le prove effettuate sulla semantica simbolica sono automaticamente valide anche sulla reale implementazione crittografica. Tale calcolo incorporerà i tipi per autenticazione definiti in [BFM07] allo scopo di estendere tale analisi su modelli computazionali di sicurezza.

Modelli ibridi: studieremo un modello ibrido che serva per l’analisi gerarchica e composizionale di protocolli complessi, che fornisca una base comune all’analisi di protocolli nei modelli puramente simbolici/computazionali o ibridi, e che permetta lo studio della correttezza dell’approccio simbolico rispetto all’approccio computazionale. Il punto di partenza sarà il lavoro sulle relazioni di simulazione approssimate di Segala e Turrini [ST07]. Intendiamo, in particolare, raffinare la nozione di simulazione approssimata per renderla più generale e adatta all'analisi di un'ampia gamma di protocolli; studiare le relazioni che sussistono tra simulazioni approssimate, inclusioni di linguaggi approssimate e metriche; studiare l'impatto del non determinismo nello studio di simulazioni approssimate; valutare, infine, gli studi sui modelli mediante casi di studio.

Modelli simbolici estesi: ad alto livello, un messaggio all’interno di un protocollo si compone di campi: ogni campo rappresenta un certo valore, come il nome di un agente, un nonce, o una chiave. Un’algebra di processo può facilmente modellare una tale struttura. Tuttavia, ad un livello più concreto, un messaggio non è nient’altro che una mera sequenza di bit. In questa visione, chi riceve un messaggio deve decidere come interpretare la stringa di bit, cioè come decomporre la stringa in sottostringhe da associare ai campi attesi del messaggio. Questo livello di granularità non è facile da cogliere per un calcolo di processo standard, in cui i termini sintattici sono usati per modellare astrattamente un messaggio, con l’ipotesi che i messaggi vengano interpretati correttamente. Intendiamo studiare tecniche per modellare i campi di un messaggio di un protocollo ad un livello di astrazione che consenta di rappresentare formalmente le possibili confusioni di tipo. Utilizzeremo il calcolo di processi LySa [BBDNN05] come punto di partenza per questo studio.

Fase 3

Sistemi di tipi per sicurezza computazionale di protocolli: Studieremo come estendere il sistema di tipi di [BFM07] al calcolo proposto in Fase 1. Studieremo anche estensioni ad altre proprietà di sicurezza come ad esempio la non-ripudiabilità.

WP4 - Modelli Causali per la Sicurezza.

Unità coinvolte: Pisa, Venezia.

Fase 1

Calcoli con semantica causale per protocolli crittografici: La formalizzazione di varie proprietà di sicurezza può trarre beneficio dal ragionare in termini di causalità tra eventi. Nell'autenticazione tra entità, ad esempio, l'autenticazione da parte del verificatore dovrebbe essere causata dall'esecuzione del protocollo da parte del dichiarante. Intendiamo dare una semantica causale ai calcoli per protocolli crittografici considerati in WP1. Tale semantica permetterà di osservare direttamente la relazione di causa ed effetto tra la conclusione del protocollo, e quindi l'autenticazione, e la corrispettiva esecuzione del protocollo da parte dell'entità da autenticare. Intendiamo considerare sia modelli true concurrent come le event structure, sia modelli basati su proved transition systems. I proved transition systems si possono immaginare come una sorta di rappresentazione compatta delle computazioni, in grado di contenere tutta l'informazione che si può codificare. Le transizioni sono arricchite con etichette che codificano le dimostrazioni. Ispezionando tali etichette, è possibile inferire le dipendenze causali, di solito rappresentate con un insieme di riferimenti alle transizioni precedenti. Ci confronteremo con altri modelli causali in letteratura [BCM07,CW01,FHG98,P99].

Fase 2

Proprietà di sicurezza su modelli causali: daremo nuove formalizzazioni di proprietà di sicurezza in "stile" causale. Ad esempio, l'autenticazione tra entità verrà espressa come la presenza esplicita di una dipendenza causale dell'evento di autenticazione rispetto all'evento di inizio del protocollo da parte dell'entità autenticata. Le formalizzazioni classiche, invece, verificano l'esistenza implicita di tale causalità esplorando che un'azione precede l'altra in tutte le possibili tracce di esecuzione.

Logiche orientate alla sicurezza: Prevediamo anche di sperimentare una formalizzazione logica della sicurezza, usando la Distributed State Temporal Logic (DSTL) [MSS04]. Tale formalismo permette mettere in relazione causale proprietà che valgono in componenti distinte, in un contesto asincrono. In passato DSTL è stata usata con successo per specificare e verificare applicazioni in cui le componenti avevano svariati requisiti di sicurezza [MS04]. Inoltre la logica include un operatore primitivo per specificare eventi: rendendo possibile mescolare dunque condizioni ed eventi nelle formule che definiscono la specifica del sistema. La capacità di usare esplicitamente gli eventi aumenta la capacità espressiva e la semplicità delle specifiche logiche, e sembra essere particolarmente adeguata per descrivere proprietà di sicurezza.

Fase 3

Verifica di protocolli basata su semantiche causali: intendiamo studiare come le tecniche di verifica studiate in WP1 possano essere applicate ai calcoli con semantica causale considerati in questo WP. In particolare, riteniamo che la verifica di protocolli di autenticazione potrà semplificarsi notevolmente su questo tipo di modelli, grazie all'informazione esplicita sulla causalità degli eventi.


Testo inglese
We now give a detailed description of the research plan, which is structured into work-packages and phases. Phases correspond to the logical and temporal scheduling of the activities. Notice, however, that the presence of different topics in the same work-package makes it possible to concurrently develop research on different phases. In Section 15, for each work-package, we will list the main expected results. These expected results are specific enough to be verified and will constitute the primary criteria for the evaluation of the success of the project.

WP1 - Communication and Network Security

Units involved: Pisa, Venice, Verona.

Phase 1

Formal models of trust and calculi for ad-hoc networks: We will develop logical models of trust that will allow us to specify formally the dynamic and variable nature of trust relationships between the components of distributed networks, satisfying in particular the constraints peculiar to ad-hoc networking. To this end, we will start within the context of mobile ad-hoc networks in hostile environments, and then move to self-organized mobile ad hoc networks. We will also work at integrating these models in a process calculus for ad-hoc networks, by developing an appropriate process calculus theory to formally prove security properties.

Phase 2

Security-oriented logics: We will develop a new temporal logic for communicating agents providing an intuitive but expressive language for formalizing both local (agent-specific) and global (system-wide) properties of distributed communicating processes. This logic will be used for object-level security protocol analysis and also for rigorously formalizing and proving meta-level properties of different protocol models. The logic will be integrated into the AVISPA Tool, described in Phase 3.

Phase 3

Security protocols analysis: We intend to go on with the study of process calculi for authentication protocols in which ciphertexts are abstracted into challenges and responses on a special calculus without cryptography [BCFM07]. The cryptographic protocol is abstracted into a protocol composed only of challenges and responses sent and received in a Dolev-Yao model that is an abstraction of the usual one. We will formalize this abstraction of cryptography in terms of a standard abstract interpretation. This will allow us to prove general results of abstractions and to automatically achieve results about preservation of security properties from the abstract calculus to the "concrete" one. We will study efficient verification techniques on the achieved abstractions. Furthermore, we intend to analyze protocols by using the Control Flow Analysis technique that provides safe and computable approximations (called solutions) of the process behaviour. We use, as a starting point, the analysis given in [BBDNN05], that is shown to be sufficient to identify several security flaws in classical protocols. Besides the usual pros of the static technique, this approach offers the advantage that a single analysis suffices for a variety of properties: different inspections of a solution permit to check different security properties of a protocol, with no need of re-analyzing it several times. Finally, we will adopt symbolic semantics to simplify the development of effective verification techniques and to address incompleteness issues typical of security verification.

Verification tools: AVISPA is an integrated, push-button tool for the automated validation of Internet security protocols and applications, which allows industry and standardization organizations to automatically verify or detect errors in Internet security protocols and applications they develop. It has been successfully applied to a number of industrial network protocols including IKE, SET, and various other protocols currently being standardized. There is considerable room for further improvements to AVISPA and, in particular, to the formal techniques underlying it. For example, extending these techniques with "more natural" languages for modeling security properties, as well as the belief and knowledge of the agents partaking in the protocol executions, will be fundamental for making the tool more expressive and at the same time more easily understandable by the non-experts. Also, we have begun investigating the integration in the AVISPA Tool of simplification and reduction techniques inspired by partial-order reduction and abstract interpretation. These techniques, together with abstraction techniques, will provide the basis for the application of AVISPA to the automated formal analysis of Web Services for security and, more general, of security services and applications in the area of Service Oriented Computing, which we will consider in WP2.
The tool for Control Flow Analysis presente in [BBDNN05] is fully automatic and always terminates in polynomial time in the size of the protocol specification. The proposed new Control Flow Analyses will be supported by suitable extensions of this tool, according to the fact that a single analysis can be easily adapted to address different properties.

WP2 - Application Security

Units involved: Pisa, Venice, Verona.

Phase 1

Calculi for distributed systems: We intend to extend, with cryptographic communication primitives, simple imperative languages with the aim of integrating the analysis of cryptographic protocols with the information flow analysis of local programs studied in WP2. Studying properties of protocols and programs in a unique framework will clarify the relation among the properties defined in the two different settings and will allow us to investigate libraries for the development of distributed applications. We will work in the direction of achieving a high level of abstraction and transparency with respect to the actual cryptographic implementation. This target is tightly connected with WP1.

Calculi for "Service-Oriented Computing": we will study linguistic primitives for the protection of both clients and services. An important aspect is that the selection of services should not be based on "names" (e.g. the identity of the service deployer), but on the properties that the selected services can be proved to enjoy. We plan to further develop the call-by-property invocation mechanism originally proposed in [BDF05], by considering other security properties (e.g. information-flow), and non-functional aspects (e.g. transactions, QoS).
We will also develop formal languages and techniques based on abstract model-checking to support the formal specification of security services and requirements. This will provide the ability to model and reason about security properties of services, both at network and application level, including not just authentication and secrecy, but also authorization, access control, policies, trust, identity management, and so on, as well as new attacker models such as [HDMV05,HDMVB06].

Phase 2

Secure stepwise refinement of software: we will analyze various refinement operations on security-oriented imperative languages, such as the specialization of abstract components, the elimination of nondeterministic choices and the replacement of subcomponents. For each operation we will consider different security properties and identify the conditions under which the operation is safely applicable in order to preserve such properties. To obtain this result, we intend to follow an approach similar to the one applied in a process algebraic setting [BFPR04] where we first defined a general framework for the definition of noninterference and then provided sufficient conditions for their preservation under refinement.

Phase 3

Distributed application analysis: We will develop dynamic type systems for the validation of distributed programs with cryptography. In particular, we will integrate type systems for cryptographic protocols with type systems for programs expressed in imperative languages. Inspired by [BFM07], we will adopt tags inside ciphertexts to transport, in a trusted way, information about the security levels of exchanged data. Based on this dynamic information, verifiable when receiving messages, we will define a dynamic type-system for the analysis of distributed application security. This target is in between WP1 and WP2.

Service-Oriented Computing analysis: We will study how to orchestrate a service-based application while guaranteeing that no executions will abort because of some security violation. This is called the planning problem, and it amounts to selecting from the network those services that accomplish the requested task, while respecting the security constraints on demand. We will extend some proposals in the literature based on types and model-checking, to dynamic scenarios in which services may be published on-the-fly and may become temporarily unavailable. We also intend to consider the combination of semantic-based service composition with security protocols and trust relationships, with the aim of guaranteeing that certified services will not arbitrarily change their code on the fly.

Abstract Non-Interference: we are interested in studying code transformation problems in particular for the derivation of models and methods for verifying non-interference in presence of active attackers, in probabilistic computations and data bases. The common pattern is that of considering abstract interpretation and abstract non-interference as a unifying framework to describe both models of attackers (active attackers as malware and passive attackers as semantic observations) and the amount of information hidden (e.g., in private data) and how this flows while programs run. The goal is to derive a unifying theory based on abstract interpretation useful for deriving effective algorithms for protecting code and data and verifying its security.

WP3 - Quantitative Aspects of Security

Units involved: Pisa, Venice, Verona.

Phase 1 and 2

Calculi for cryptographic protocols: we will develop a process calculus for expressing cryptographic protocols equipped with a semantics based on the simulatable cryptographic library by Backes, Pfitzmann and Waidner [BPW03]. This cryptographic library is equipped with two semantics: the former resembles the Dolev-Yao model, the latter follows the computational model. It has been proved that, in general, any security property satisfied by the formal semantics is also satisfied by the computational one. Hence proofs on the Dolev-Yao-like semantics scale down to the concrete cryptographic implementation. The new calculus will include the authentication types of [BFM07] with the aim of extending such an analysis to computational models of security.

Hybrid models: We will study a model that is suitable for the compositional and hierarchical analysis of complex protocols, provides a common support for analysis within models that are either purely computational/symbolic or hybrid and permits a rigorous study of soundness results of the symbolic model with respect to the computational model. The starting point is the work on approximated simulation relations of Segala and Turrini [ST07]. In this context we plan the following:
generalize the notion of approximated simulation to extend the range of modelled protocols; study the relationship among approximated simulations, approximated language inclusion and metrics; study the impact of nondeterminism on the theory of approximated simulations; evaluate the model through case studies.

Enhanced symbolic models: abstractly, a message in a protocol consists of fields: each field represents some value, such as the name of a principal, a nonce or a key. A process calculus can easily model this structure. Nevertheless, at a more concrete level, a message is nothing but a raw sequence of bits. In this view, the recipient of a message has to decide the interpretation of the bit string, i.e. how to decompose the string into substrings to be associated to the expected fields of the message. This level of granularity is more difficult to capture for a standard process calculus, where syntax terms are used to abstractly model message, under the assumption that messages are correctly interpreted. We intend to study techniques to model the fields of protocol messages so that type misinterpretations are formally represented. We will use the process calculus LySa [BBDNN05] as a starting point of this research.

Phase 3

Type systems for computational security of protocols: We will study how to extend the type system of [BFM07] to the new calculus discussed in Phase 1. We will also study extensions to different security properties like, e.g., non-repudiability.

WP4 - Causal models for security.

Units involved: Pisa, Venice.

Phase 1

Calculi for security protocols with causal semantics: In the formalization of security properties it might be beneficial to reason in terms of causality among events. For example, in entity authentication we have that authentication should always be caused by the actual execution of the protocol by the claimant. We intend to give a causal semantics to the calculi for cryptographic protocols studied in WP1. This semantics will enable us to directly observe the causality between the protocol conclusion, i.e., the authentication, and the corresponding execution by the authenticated entity. In doing this, we will investigate both true-concurrent models like, e.g., event structures, and models of causality based on proved transition systems. Proved transition systems can be considered as a sort of compact representation of computations, containing all the possible encodable information. Transitions are enriched with labels encoding their proofs. By inspecting the transition labels, it is possible to infer the causal dependencies, usually represented through a set of references to previous transitions. We will compare with other causal models in literature [BCM07,CW01,FHG98,P99].

Phase 2

Security properties on causal models: we will give new formalization of security properties based on causality. For example, entity authentication will be expressed as the presence of an explicit causal dependency of the authentication event from the event representing the actual execution of the protocol by the claimant. The classic formalizations, instead, verify the presence of such a causality by checking that the latter event precedes the former in every possible execution trace.

Security oriented logics: We plan also to experiment a formalization of security using the Distributed State Temporal Logic (DSTL) [MSS04]. This formalism permits to causally relate properties, which might hold in distinguished components of a system, in an asynchronous setting. This approach has been proved useful to support the specification and verification of applications where components have different security requirements [MS04]. Moreover, it includes a primitive operator to specify events: allowing us to mix conditions and events in the specification formulae. The ability to deal with events explicitly enhances the expressiveness and simplicity of logical specifications, and seems especially adequate in the case of security properties specification.

Phase 3

Protocol verification with causal semantics: we intend to study how the different techniques developed in WP1 might be applied to the calculi with causal semantics considered in this WP. We believe, for example, that the verification of authentication protocols will greatly benefit from the explicit information about causal relationships among events.


14 - Ruolo di ciascuna unità operativa in funzione degli obiettivi previsti e relative modalità di integrazione e collaborazione


Testo italiano
Data la presenza di molti interessi comuni tra le sedi, ci saranno probabili nuove collaborazioni, e sarà nostro interesse incentivarle il più possibile. In particolare:

imm ins 0

WP1: C'è un forte interesse comune, tra tutte le unità, allo studio di tecniche di analisi di protocolli crittografici (fase 3). In particolare crediamo sarà possibile collaborare sulle tematiche specifiche dell'analisi statica e simbolica di protocolli crittografici, viste anche le precedenti collaborazioni tra Venezia e Pisa su argomenti analoghi. Verona sarà l'unità responsabile delle fasi 1 e 2, portando avanti la ricerca sulle reti ad-hoc e sulle logiche orientate alla sicurezza. Non si escludono, comunque, possibili collaborazioni anche su queste tematiche, ad esempio tra Verona e Pisa per quanto concerne la specifica di proprietà di sicurezza tramite logiche temporali (vedi WP4).

imm ins 1

WP2: C'è interesse comune, tra tutte le unità, allo studio della sicurezza di applicazioni distribuite. Tutte le unità intendono infatti utilizzare la ricerca fatta nel WP1 per studiare nuove primitive che rendano la programmazione il più possibile indipendente dalla effettiva realizzazione crittografica. Questo verrà fatto sia in applicazioni "standard" che in paradigmi "Service-Oriented". Si prevede quindi una proficua interazione tra tutte le unità. Venezia sarà responsabile della parte di "raffinamento sicuro" mentre Verona porterà avanti la ricerca sulla non-interferenza astratta.

imm ins 2

WP3: In questo work-package tutte le unità lavoreranno indipendentemente su diversi aspetti quantitativi della sicurezza, strettamente correlati: Venezia studierà una semantica basata sulla libreria crittografica di Backes, Pfitzmann e Waidner, per un calcolo per protocolli crittografici; Verona studierà modelli ibridi in cui si possano combinare l'approccio simbolico e quello computazionale; Pisa estenderà calcoli per protocolli crittografici in modo da catturare alcuni aspetti "concreti", come gli attacchi type-flaw, in un contesto puramente simbolico. Anche se non ci sarà una diretta collaborazione tra le unità, riteniamo che queste tre ricerche si complementino l'un l'altra, e ogni unità potrà quindi beneficiare dai risultati ottenuti dalle altre due. Anche in questo caso non escludiamo la nascita di nuove collaborazioni.

imm ins 3

WP4: C'è forte intesse comune tra le sedi di Pisa e Venezia sullo studio di semantiche causali per l'analisi di protocolli crittografici. Vediamo quindi una probabile collaborazione sull'argomento, anche alla luce delle precedenti collaborazioni tra le due sedi su argomenti simili. Anche se Verona non partecipa a questo work-package, non escludiamo possibili nuove collaborazioni, ad esempio con Pisa, per quanto concerne la specifica di proprietà di sicurezza tramite logiche temporali (vedi WP1).


Testo inglese
Given the presence of many common interests among the research units, it will be likely to have new collaborations and we will stimulate them as much as possible. In particular:

imm ins 0

WP1: There is a strong common interest, among the three units, on the investigation of analysis techniques for security protocols (Phase 3). In particular, we believe that it will be possible to collaborate on the static and symbolic analysis of security protocols, given also the successful previous collaborations between Pisa and Venice on similar topics. Verona will be responsible for Phases 1 and 2 on ad-hoc networks and security-oriented logics. We do not exclude possible new collaborations on these topics, e.g., between Pisa and Verona on the specification of security properties using temporal logics (see WP4).

imm ins 1

WP2: There is a strong common interest, among the three units, on the invertigation of distributed application security. All the units, in fact, intend to exploit the results of WP1 to study new primitives that make programming independent of the low level cryptographic implementation. This will be done both in "standard" distributed applications and in "Service-Oriented" ones. We thus foresee a fruitful collaboration among the units. Venice will be responsible for the "secure stepwise refinement" part, while Verona will develop the research on Abstract Non-Interference.

imm ins 2

WP3: In this work-package, all the units will work on different, but related, quantitative aspects of security: Venice will study a semantics for a calculus of protocols, based on the simulatable cryptographic library by Backes, Pfitzmann and Waidner; Verona will study hybrid models in which it is possible to combine the symbolic and the computational approaches; Pisa will enhance calculi for protocols so to model more "concrete" aspects, like type-flaw attacks, in a purely symbolic setting. Even if there will be no direct collaboration, we believe that these three research lines will smoothly complement each other and, consequently, every unit will benefit from the results of the other two. Even in this case, we do not exclude possible new collaborations.

imm ins 3

WP4: There is a strong common interest between Pisa and Venice about the study of causal semantics for the analysis of cryptographic protocols. We thus foresee a collaboration on this topic, given also the existing previous joint works between the two Universities on similar topics. Even if Verona does not participate in this work-package, we do not exclude possible new collaborations, e.g., with Pisa on the specification of security properties using temporal logics (see WP1).


15 - Risultati attesi dalla ricerca, il loro interesse per l'avanzamento della conoscenza e le eventuali potenzialità applicative


Testo italiano
Indichiamo, nel seguito, i principali risultati attesi per ogni work-package. Tali risultati sono volutamente molto specifici in modo da poter essere verificati, e costituiranno, quindi, lo strumento primario per la valutazione dell'avvenuto raggiungimento degli obiettivi del progetto. L'interesse per l'avanzamento della conoscenza è stato illustrato in modo estensivo nelle sezioni 12 e 13.

Risultati attesi WP1

Fase 1
- nuovi modelli formali per il trust nelle reti ad-hoc ed integrazione di tali modelli in calcoli di processi.
Fase 2
- una nuova logica temporale per esprimere proprietà di sicurezza di agenti comunicanti.
Fase 3
- definizione di un'interpretazione astratta di protocolli di autenticazione sfida-risposta;
- definizione di nuove analisi control-flow per protocolli di sicurezza;
- estensione del tool presentato in [BBDNN05] alle nuove analisi control-flow;
- utilizzo di tecniche simboliche e di raffinamento per la verifica di proprietà di sicurezza;
- estensione di AVISPA alla logica descritta in fase 2;
- studio di altre possibili estensioni di AVISPA a tecniche sviluppate in questo WP.


Risultati attesi WP2

Fase 1
- definizione di linguaggi imperativi orientati alla sicurezza con primitive di comunicazione crittografiche;
- nuove primitive astratte di comunicazione che permettano di rendere la programmazione indipendente dalla realizzazione crittografica.
Fase 2
- definizione di un framework generale per il raffinamento sicuro di programmi;
- nuove formalizzazioni di proprietà di sicurezza sui calcoli definiti nella fase 1.
Fase 3
- definizione di sistemi di tipi dinamici per la sicurezza di applicazioni distribuite con crittografia;
- estensioni a proprietà nuove e ad aspetti non-funzionali del meccanismo di chiamata per proprietà nel Service-Oriented Computing;
- estensione di tecniche di orchestrazione esistenti a scenari in cui i servizi possono essere pubblicati dinamicamente o diventare non disponibili;
- estensione della non-interferenza astratta ad attaccanti attivi e su sistemi di calcolo probabilistici;
- applicazione della non-interferenza astratta alle basi di dati e al data mining.


Risultati attesi WP3

Fase 1
- nuovo calcolo per protocolli crittografici con semantica simbolica e computazionale basata sulla libreria crittografica di Backes, Pfitzmann e Waidner [BPW03];
- nuovo modello ibrido per protocolli crittografici, in grado di combinare gli approcci simbolico e computazionale;
- estensione dell'algebra di processi LySa per la rappresentazione formale di attacchi basati sulla confusione di tipo.
Fase 2
- nuove formalizzazioni di proprietà di sicurezza sui calcoli definiti nella fase 1.
Fase 3
- sistemi di tipo per protocolli crittografici con semantica simbolica e computazionale.


Risultati attesi WP4

Fase 1
- nuove semantiche causali per calcoli noti di protocolli.
Fase 2
- nuove formalizzazioni di proprietà di sicurezza in stile causale;
- nuove formalizzazioni di proprietà di sicurezza tramite la DSTL.
Fase 3
- specializzazione di tecniche precedentemente studiate sulle nuove semantiche, con particolare attenzione ai protocolli di autenticazione.


Testo inglese
For each work-package we give a list of the main expected results. These results are intentionally very specific, so to be verifiable, and will constitute the primary criteria for the evaluation of the success of the project. The contribution of these results with respect to the state of the art has been extensively illustrated in sections 12 and 13.


Expected results for WP1

Phase 1
- new formal models of trust for ad-hoc networks and integration of these models into suitable process calculi.
Phase 2
- a new security-oriented temporal logic for communicating processes.
Phase 3
- definition of an abstract interpretation of challenge-response authentication protocols;
- definition of new Control Flow Analyses for security protocols;
- extension of the verification tool proposed in [BBDNN05] to the new Control Flow Analyses;
- use of symbolic techniques and refinement for the verification of security properties;
- extension of AVISPA to the logic described in phase 2;
- investigation of possible extensions of AVISPA to other techniques developed in this WP.


Expected results for WP2

Phase 1
- definition of security-oriented imperative languages with cryptographic communication primitives;
- new abstract communication primitives that make programming independent of cryptographic implementation.
Phase 2
- new general framework for secure stepwise refinement of programs;
- new formalizations of security properties on languages and calculi defined in phase 1.
Phase 3
- new dynamic type systems for the security of distributed applications with cryptography;
- extension of the call-by-property invocation mechanism of Service-Oriented Computing to other security properties and non-functional aspects;
- extension of existing orchestration techniques to scenarios in which services may be published on-the-fly and may become temporarily unavailable;
- extension of abstract Non-Interference in order to deal with active attackers able to exploit probabilistic techniques;
- application of abstract Non-Interference to data bases and data mining.


Expected results for WP3

Phase 1
- a new calculus for cryptographic protocols, with both a symbolic and a computational semantics based on the simulatable cryptographic library by Backes, Pfitzmann and Waidner [BPW03];
- a new hybrid model for security protocols combining symbolic and computational aspects;
- an extension of the process calculus LySa which is able to deal with type misinterpretation attacks.
Phase 2
- new formalizations of security properties on languages and calculi defined in phase 1.
Phase 3
- Type systems for cryptographic protocols with both a symbolic and a computational semantics.


Expected results for WP4

Phase 1
- new causal semantics for existing calculi of cryptographic protocols.
Phase 2
- new causality-based formalizations of security properties;
- new formalizations of security properties using the logic DSTL.
Phase 3
- specializations of already studied techniques to the new semantics, with special attention to authentication protocols.


16 - Elementi e criteri proposti per la verifica dei risultati raggiunti


Testo italiano
Il successo del progetto potrà essere misurato in termini di raggiungimento dei risultati attesi elencati in sezione 15. Tali risultati produrranno principalmente pubblicazioni su riviste o in atti di conferenze del settore, e rapporti tecnici di ricerca. Stimando una pubblicazione per ogni risultato atteso, possiamo quindi prevedere circa 25 pubblicazioni totali sulle tematiche specifiche di questo progetto.
Riteniamo inoltre fondamentale l'interazione tra le unità e l'apertura verso la comunità nazionale ed internazionale di ricerca nel settore. Sarà quindi di primaria importanza l'organizzazione di workshop di progetto allo scopo di divulgare i risultati mantenere viva l'attività di ricerca. Abbiamo, a tale scopo, previsto l'organizzazione di un workshop in ognuna delle tre sedi: Pisa, Venezia e Verona. Ci impegneremo, inoltre, nell'organizzazione di seminari tematici anche tenuti da ricercatori esterni. Il successo di tali workshop e seminari potrà costituire un'altro elemento di valutazione della riuscita del progetto.


Testo inglese
The success of the project may be measured in terms of the achieved expected results which are listed in section 15. These results will mainly produce journal and conference publications and technical reports. By estimating one publication for each result, we foresee about 25 publications on the specific topics of this project.
We also consider extremely important the interaction among the units and with the national and international research communities. It will be thus very important to organize project workshops to divulge the achieved results and stimulate the research activity. To this aim, we have foreseen one workshop for each site: Pisa, Venice and Verona. We also intend to organize seminars on the project topics, also inviting external researchers. The success of these workshops and seminars might be considered as an extra criterion for evaluating the project.


17 - Mesi persona complessivi dedicati al Progetto di Ricerca

    Numero  Impegno
1° anno 
Impegno
2° anno 
Totale mesi persona 
Componenti della sede dell'Unità di Ricerca  11  69  69  138 
Componenti di altre Università /Enti vigilati  0  0  0  0 
Titolari di assegni di ricerca  2  10  10  20 
Titolari di borse  Dottorato  5  28  28  56 
Post-dottorato  0       
Scuola di Specializzazione  0       
Personale a contratto  Assegnisti  1  0  6  6 
Borsisti  1  4  4  8 
Altre tipologie  0       
Dottorati a carico del PRIN da destinare a questo specifico progetto  0  0  0  0 
Altro personale  3  10  10  20 
TOTALE     23  121  127  248 


18 - Costo complessivo del Progetto articolato per voci

Voce di spesa  Unità I  Unità II  Unità III  TOTALE
Materiale inventariabile  2.500  5.000  4.000  11.500
Grandi Attrezzature  0  0  0  0
Materiale di consumo e funzionamento  4.500  4.000  3.500  12.000
Spese per calcolo ed elaborazione dati  0  0  0  0
Personale a contratto  10.000  10.000  0  20.000
Dottorati a carico del PRIN da destinare a questo specifico progetto  0  0  0  0
Servizi esterni  0  0  0  0
Missioni  15.500  9.000  18.000  42.500
Pubblicazioni  0  0  0  0
Partecipazione / Organizzazione convegni  9.500  10.000  9.500  29.000
Altro   0  0  0  0
TOTALE 42.000  38.000  35.000  115.000


19 - Prospetto finanziario suddiviso per Unità di Ricerca

  Unità I  Unità II  Unità III  TOTALE
a.1) finanziamenti diretti, disponibili da parte di Università/Enti vigilati di appartenenza dei ricercatori dell'unità operativa  12.600  11.400  3.500  27.500
a.2) finanziamenti diretti acquisibili con certezza da parte di Università/Enti vigilati di appartenenza dei ricercatori dell'unità operativa   0  0  7.000  7.000
b.1) finanziamenti diretti disponibili messi a disposizione da parte di soggetti esterni  0  0  0  0
b.2) finanziamenti diretti acquisibili con certezza, messi a disposizione da parte di soggetti esterni  0  0  0  0
c) cofinanziamento richiesto al MUR   29.400  26.600  24.500  80.500
TOTALE 42.000  38.000  35.000  115.000





(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 31/10/2007 ore 13:52