Metodi Formali per la Sicurezza

GORRIERI	ROBERTO
(cognome)	(nome)
Universitą degli Studi di BOLOGNA	Facoltą di SCIENZE MATEMATICHE FISICHE e NATURALI
(universitą)	(facoltą)
K05B	Dipartimento di SCIENZE DELL'INFORMAZIONE
(settore scient.discipl.)	(Dipartimento/Istituto)

gorrieri@cs.unibo.it
(E-mail)

FOCARDI	RICCARDO
(cognome)	(nome)

Ricercatore	30/01/1970	FCRRCR70A30A944O
(qualifica)	(data di nascita)	(codice di identificazione personale)

Universitą "Cą Foscari" di VENEZIA	Facoltą di SCIENZE MATEMATICHE FISICHE e NATURALI
(universitą)	(facoltą)
K05B	Dipartimento di INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

041-2908438	041-2908419	focardi@dsi.unive.it
(prefisso e telefono)	(numero fax)	(E-mail)

Testo italiano

• Laurea in Scienze dell'Informazione, presso l'Universita' degli Studi di Bologna. Voto di Laurea: 110/110 e lode, marzo 1993.
  
• Nell'ottobre 1996, a seguito della vincita di concorso, ha preso servizio come ricercatore per il raggruppamento K05B presso il dipartimento di Informatica dell'Universita' Ca'Foscari di Venezia.
  
• Dottorato di Ricerca in Informatica presso l'Universita' degli Studi di Bologna, febbraio 1999.
  
• I suoi interessi di ricerca riguardano principalmente la specifica di proprieta' di sicurezza di sistemi concorrenti e la loro verifica formale; la classificazione, comparazione e verifica automatica delle varie proprieta', con applicazione a casi concreti e l'analisi automatica di protocolli crittografici. Altre ricerche correlate riguardano la generazione di strumenti per la verifica automatica di proprieta' di sicurezza di sistemi descritti in algebre di processi; lo studio di modelli matematici per descrivere il comportamento di sistemi concorrenti e distribuiti; i linguaggi per la descrizione di processi e loro semantica.
  
• Membro e segretario (dal 1999) del IFIP Working Group 1.7 ``Theoretical Foundations of Security Analysis and Design'', http://www.dsi.unive.it/IFIPWG1_7/
  
• E' titolare dei corsi di "sistemi di elaborazione dell'informazione (Sicurezza)" e "Laboratorio di Informatica (Ingegneria del Software)" presso il corso di Laurea in Informatica, Universita' Ca' Foscari di Venezia.
  
• Membro dei comitati di programma delle seguenti conferenze: 14th IEEE Computer Security Foundations Workshop (CSFW'00), luglio 2001 (Cape Breton); Workshop on Issues in the Theory of Security (WITS '00), luglio 2000 (Ginevra); Verification Workshop: What are the verification problems? What are the deduction techniques? (con IJCAR 2001), giugno 2001 (Siena).
  
• Organizzatore della "Second International School On Foundations Of Security Analysis And Design (FOSAD 2001), settembre 2001, Bertinoro.
  

Testo inglese

• "Laurea" in Computer Science, University of Bologna, March 1993.
  
• Since October 1996, he joined the Computer Science department of Ca'Foscari University, Venice, as Assistant Professor.
  
• PhD in Computer Science, University of Bologna, February 1999.
  
• His research interests mainly concern the specification and formal verification of security properties for concurrent systems; the classification and automatic verification of various security properties, with application to real-world cases; the automatic verification of cryptographic protocols. He is also active in the following fields: implementation of semantic-based tools for the automatic verification of security properties for systems specified through process calculi; mathematical models for the description of concurrent and distributed systems; languages for the description of processes and their semantics.
  
• Since 1999, he is member and secretary of IFIP Working Group 1.7 ``Theoretical Foundations of Security Analysis and Design'', http://www.dsi.unive.it/IFIPWG1_7/
  
• He currently teaches "Security" and "Software Engineering Lab." courses at the Computer Science department of Ca' Foscari University, Venice.
  
• Member of the program committees of the following conferences: 14th IEEE Computer Security Foundations Workshop (CSFW'00), July 2001 (Cape Breton); Workshop on Issues in the Theory of Security (WITS '00), July 2000 (Geneva); Verification Workshop: What are the verification problems? What are the deduction techniques? in connection with IJCAR 2001, June 2001 (Siena).
  
• He is organising the "Second International School On Foundations Of Security Analysis And Design (FOSAD 2001), September 2001, Bertinoro.
  

1. 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.
2. 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.
3. FOCARDI R., GORRIERI R. (1995). A Classification of Security Properties for Process Algebras. JOURNAL OF COMPUTER SECURITY. vol. 3(1), pp. 5-33.
4. BODEI C., DEGANO P., FOCARDI R., PRIAMI C. (?). Primitives for Authentication in Process Algebras. THEORETICAL COMPUTER SCIENCE. To appear.
5. FOCARDI R., GORRIERI R., MARTINELLI F. (2000). Non Interference for the Analysis of Cryptographic Protocols. 27th International Colloquium on Automata, Languages and Programming (ICALP'00). (vol. LNCS 1853). Geneva, July 2000.

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						2001	2002
Personale docente:
1	FOCARDI	RICCARDO	INFORMATICA	Ricercatore	K05B	5 (ore: 685)	8 (ore: 1100)
2	BOSSI	ANNALISA	INFORMATICA	Prof. ordinario	K05B	6 (ore: 825)	5 (ore: 685)
3	BUGLIESI	MICHELE	INFORMATICA	Prof. associato	K05B	3 (ore: 411)	6 (ore: 825)
4	COCCO	NICOLETTA	INFORMATICA	Prof. associato	K05B	5 (ore: 685)	6 (ore: 825)
5	CORTESI	AGOSTINO	INFORMATICA	Prof. associato	K05B	3 (ore: 411)	8 (ore: 1100)
6	ROSSI	SABINA	INFORMATICA	Ricercatore	K05B	6 (ore: 825)	6 (ore: 825)
Altro personale:

1.8.2 Personale universitario di altre Universitą

Nº	Cognome	Nome	Universitą	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
							2001	2002
Personale docente:
1	VALENTINI	SILVIO	PADOVA	MATEMATICA PURA E APPLICATA	Prof. associato	A01A	4 (ore: 550)	5 (ore: 685)
Altro personale:
2	MAIETTI	MARIA EMILIA	PADOVA	MATEMATICA PURA E APPLICATA	Borsista		0	5 (ore: 685)

1.8.3 Titolari di assegni di ricerca

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo
					2001	2002

1.8.4 Titolari di borse per Dottorati di Ricerca e ex L. 398/89 art.4 (post-dottorato e specializzazione)

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo
1.	CRAFA	SILVIA	INFORMATICA	2003	11  (ore: 1507)

1.8.5 Personale a contratto da destinare a questo specifico programma

Nº	Qualifica	Costo previsto	Mesi uomo
1.	contratto di ricerca	7	4  (ore: 550)

1.8.6 Personale extrauniversitario dipendente da altri Enti

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Mesi uomo

Testo italiano

Definizione formale e analisi statica di proprieta' di sicurezza

Testo inglese

Formalization ad static analysis of security properties

Testo italiano
METODI FORMALI ; PROTOCOLLI SICURI ; FLUSSO DI INFORMAZIONE ; NON-INTERFERENZA ; INTERPRETAZIONE ASTRATTA ; SISTEMI DI TIPI

Testo inglese
FORMAL METHODS ; SECURITY PROTOCOLS ; INFORMATION FLOW SECURITY ; NON-INTERFERENCE ; ABSTRACT INTERPRETATION ; TYPE SYSTEMS

Testo italiano

La grande diffusione di sistemi distribuiti, dove risorse e dati sono condivisi tra utenti situati in vaste aree geografiche, ha aumentato enormemente l'interesse nelle problematiche di sicurezza. In questo contesto e' infatti possibile che un utente ottenga dalla rete programmi insicuri i quali, una volta eseguiti all'interno del proprio sistema, potrebbero causare effetti non prevedibili e dannosi. Inoltre potrebbe essere possibile che un sistema completamente protetto al suo interno, risulti vulnerabile in attivita' critiche come il commercio elettronico o l'home banking, a causa di meccanismi non sicuri per la comunicazione remota. Per poter dimostrare la correttezza di un certo meccanismo di sicurezza, e' molto importante definire in modo preciso e formale la proprieta' di interesse. Recentemente ci sono state molte proposte di definizioni formali di proprieta' relative alla sicurezza; si vedano, ad esempio, [AG99, AA99, BDFP99, BDFP01, BDNN99, DMP00, FGM00b, MMS97, LR97, LL98, PP97, SV98, SS98].
Uno degli approcci formali alla sicurezza nei calcolatori e nelle reti, presente in letteratura, e' basato sulle algebre di processi. I protocolli crittografici e i sistemi concorrenti vengono descritti, ad esempio, in CSP [LL98, SS98], SPA [FG95], CryptoSPA [FM99, FGM00b], pi-calculus e spi-calculus [AG99]; le proprieta' di sicurezza sono quindi definite sulla base di relazioni di equivalenza e di raffinamento tra termini e possono essere provate tramite dimostrazione classiche "a mano" [AG99, SS98] o per mezzo di appositi strumenti automatici [LL98, DFG00, PP97, MMS97]. Il proliferare di differenti modelli e formalizzazioni di proprieta' di sicurezza ha anche stimolato vari tentativi di confronto fra i diversi approcci [FF96, FM99, FGM00a, FGM00b]; e' comunque necessario ancora molto lavoro per poter giungere ad una visione globale ed uniforme di come una proprieta', legata alla sicurezza, possa effettivamente essere specificata e verificata.
Un altro approccio formale alla sicurezza e' quello basato su tecniche di analisi statica [SV98, BDNN99, AA99, BCA01]. In linea di principio, il vantaggio piu' importante di tali tecniche e' quello di rendere la verifica piu' efficiente; inoltre consentono di scrivere programmi sicuri per costruzione, ad esempio, quando e' possibile dimostrare che l'analisi effettuata implica proprieta' dinamiche di interesse. Inoltre, l'analisi statica puo' essere a volte applicata direttamente a situazioni pratiche; un tipico esempio e' la verifica "al volo" di una proprieta' su un programma scaricato dalla rete, e quindi potenzialmente insicuro.
Tra le varie tecniche di analisi statica, consideriamo l'interpretazione astratta, i metodi di verifica e i sistemi di tipi. L'interpretazione astratta fornisce un modello formale approssimato, basato sulla semantica, dell'esecuzione del programma. L'impatto di questa tecnica sull'ottimizzazione di compilatori e' ben nota in letteratura. Molti domini (ad esempio [CFW96, RVC99, LCRC99, PLC01]) e molti operatori (ad esempio [CFRPR97, CFW98, CLV00]) sono stati progettati allo scopo di catturare proprieta' di programmi, aumentando la precisione o riducendo la complessita', modularizzando l'analisi attraverso reffinamento, semplificazione e decomposizione di domini. Cio' nonostante, l'applicazione di questa tecnica alle problematiche di sicurezza e di certificazione di programmi non ha ricevuto finora adeguata attenzione da parte della comunita' scientifica.
Le tecniche di verifica hanno lo scopo di dimostrare la correttezza di programmi e forniscono il supporto per la loro certificazione; contemporaneamente possono dare linee-guida per lo sviluppo e il design di programmi [BC99, BR99, EBC99, BER99, BERS01]. Recentemente e' stato proposto un nuovo approccio alla verifica di proprieta' di protocolli crittografici, basato sulla definizione di una logica e di un sistema di prova che fornisce un metodo per inserire asserzioni all'interno di un protocollo, nello stile della logica di Hoare per i programmi sequenziali imperativi [DMP00]. Un aspetto interessante delle condizioni Pre/Post, e' la proprieta' di composizionalita': essa consente di focalizzare l'attenzione su proprieta' locali e, successivamente, comporre tali proprieta' per ottenere una prova di correttezza.
I sistemi di tipi sono stati applicati in diversi campi, dai linguaggi di programmazione fino ai fondamenti della matematica costruttiva [BV92,V96], comprendendo le estensioni della teoria intuitionistica dei tipi di Martin-Loef [MV99], fino al caso di teorie di tipi basate sulla logica lineare classica e intuizionistica [MdPR00] e di generalizzazione del lambda calcolo tipato [V01]. Nei linguaggi di progammazione e nei sistemi, i tipi classificano termini (espressioni, comandi o processi, in base al particolare linguaggio di programmazione considerato) a seconda della loro struttura statica: sulla base di tale classificazione, la tipizzazione forte costiuisce una prova formale che alcuni invarianti saranno verificati, a tempo di esecuzione, da tutti i programmi o sistemi ben tipati [BB99, BBDL99, BCC00, BP01].
Differenti nozioni di tipi e, analogamente, differenti sistemi di tipi, possono essere definiti a seconda della scelta degli invarianti. Questi ultimi, a loro volta, dipendono dalla particolare nozione di "osservabile" che si sta considerando. I sistemi di tipi per la sicurezza sono ottenuti considerando una nozione di "osservabile" che corrisponde alla proprieta' di sicurezza di interesse. Tre articoli recenti in quest'area evidenziano altrettante linee di ricerca che meritano di essere percorse: (i) non-interferenza e flussi di informazione [SV98], (ii) protocolli crittografici [AA99], e (iii) controllo degli accessi [HR00].

Testo inglese

The wide diffusion of distributed systems, where resources and data are shared among users located almost everywhere in the world, has enormously increased the interest in security issues. In this context, it is likely that a user gets some (possibly) malicious programs from an untrusted source on the net and executes them inside its own system with unpredictable results. Moreover, it could be the case that a system completely secure inside, results to be insecure when performing critical activities such as electronic commerce or home banking, due to a "weak" mechanism for remote connections. It is important to precisely define security properties in order to have formal statements of the correctness of a security mechanism. In the recent years there have been a number of proposals of formal definitions of security properties, see for instance [AG99, AA99, BDFP99, BDFP01, BDNN99, DMP00, FGM00b, MMS97, LR97, LL98, PP97, SV98, SS98].
One of the formal approaches to computer and network security is based on process calculi. Cryptographic protocols and concurrent systems are described, e.g., through CSP [LL98, SS98], SPA [FG95], CryptoSPA [FM99, FGM00b], pi-calculus and spi-calculus [AG99]. Then, security properties are typically defined as equivalences or refinement relations between particular terms, and are thus verified on the specifications. Such a verification may be either a hand-written formal proof [AG99, SS98] or the output of some semantics-based automatic tool [LL98, DFG00, PP97, MMS97]. Some effort has also been devoted to the formal comparison of some of the above models for security [FF96, FM99, FGM00a, FGM00b], but a lot of work is still needed in this direction to provide a uniform view on how particular security properties could be formalized and verified.
Another formal approach to security is the one based on static analysis techniques [SV98, BDNN99, AA99, BCA01]. Giving a way for statically verifying a security property has, in principle, the advantage of making the checking of the properties more efficient; moreover it allows us to write programs which are secure-by-construction, e.g., when the performed analysis is proved to imply some behavioural security properties. Moreover, static analysis can be sometimes directly applied to practical situations, e.g., it may permits to check a certain property directly on the code downloaded from the (insecure) network.
Among static analysis techniques, we consider abstract interpretation, verification methods and type systems.
Abstract interpretation is a general static analysis methodology which provides a formal semantic-based approximated model of program execution. The impact of this methodology on compiler optimization is well known both in literature and in practice. A number of domains (e.g.,[CFW96, RVC99, LCRC99, PLC01]), and a number of operators (e.g., [CFRPR97, CFW98, CLV00]) have been designed to capture program properties and to systematically improve precision, reduce complexity, and modularize analyses by refining, simplifying and decomposing domains. However, not much work has been done yet to apply this technique to develop semantic-based tools addressing security and other forms of program certification issues.
Verification techniques aim both at proving program correctness and supporting program certification, and may give guidelines in program design [BC99, BR99, EBC99, BER99, BERS01]. A very recent and promising approach for formal verification of protocol properties is based on the definition of a logic and a proof system, which provide a method for attaching assertions to protocol actions in a manner resembling Hoare logic for sequential imperative programs [DMP00]. An interesting aspect of Pre/Post specifications is the compositionality property: we can first focus on local properties and then compose them to derive correctness protocol proofs.
Type systems have been applied in a wide range of fields, from programming languages to foundations of constructive mathematics [BV92,V96], including extensions of Martin-Loef's intuitionistic type theory [MV99], to the case of type theories based on classical and intuitionistic linear logic [MdPR00] and also more general typed lambda calculi [V01].
In programming languages and systems, types classify terms (i.e., expressions, commands or processes depending on the programming language under consideration) according to their static structure: based on that classification, strong typing provides a formal guarantee that certain run-time invariants will be verified by the dynamic execution of any well-typed program or system [BB99, BBDL99, BCC00, BP01].
Different notions of types and, correspondingly, different type systems may be defined depending on the choice of the invariants. The invariants, in turn, depend on the notion of observable one has in mind. Type systems for security results from defining the observables to be the security properties of interest in a protocol or system. Three recent papers in this area reflect three different research streams that deserve to be further investigated: (i) information flow and noninterference [SV98], (ii) cryptographic protocols [AA99], and (iii) resource access control [HR00].

[AA99] M. Abadi: Secrecy by Typing in Security Protocols. Journal of ACM, 46(5):749-786. 1999
[AG99] M. Abadi and A. D. Gordon,A Calculus for Cryptographic Protocols: The Spi Calculus Information and Computation 148,vol. 1 (January 1999), pages 1-70.
[BB99] V. Bono and M. Bugliesi. Matching for the Lambda Calculus of Objects. Theoretical Computer Science 212(1-2) 101-140, Feb. 1999.
[BBDL99] V. Bono, M. Bugliesi, L. Liquori and M. Dezani-Ciancaglini. A Subtyping for Extensible, Incomplete Objects. Fundamenta Informaticae, 38(4) 325--364, June 1999.
[BC99] Bossi A., Cocco N., Successes in Logic Programs, in P. Flener ed., Proceedings of LOPSTR'98, Springer-Verlag LNCS 1559, (1999).
[BCA01] M. Bugliesi and G. Castagna. Secure Safe Ambients. Proc. 28th ACM Symposium on Principles of Programming Languages (POPL'01), 222-235, London. 2001.
[BCC00] M. Bugliesi, G. Castagna, S. Crafa. Typed Mobile Objects. In proc. 11th Int. Conference on Concurrency Theory (CONCUR'00), LNCS 1877, 504-520.
[BDFP99] C. Bodei, P. Degano, R. Focardi and C. Priami, Authentication via localized names, in Proc. of 12th IEEE Computer Security Foundations Workshop (CSFW'99), (P. Syverson Ed.), IEEE press, Mordano (Italy), June 1999.
[BDFP01] C. Bodei, P. Degano, R. Focardi and C. Priami, Primitives for Authentication in Process Algebras. Theoretical Computer Science. To appear (2001).
[BDNN99] B. Bodei, P. Degano, F. Nielson and H. Riis Nielson, Static Analysis of
Processes for No Read-Up and No Write-Down, in proc. of 2nd FoSSaCS'99, LNCS, Springer, March 1999, Amsterdam.
[BERS01] A. Bossi, S. Etalle, S. Rossi, J.-G. Smaus. Semantics and Termination of Simply-moded Logic Programs with Dynamic Scheduling. To appear in Proc. European Symposium on Programming, ESOP2001, LNCS, Genova, 2001.
[BER99] A. Bossi, S. Etalle, S. Rossi. Properties of Input-Consuming Derivations. Electronic Notes of Theoretical Computer Science, volume 30, n. 1, 1999.
[BP01] M. Bugliesi and S. Pericas. Type Inference for Variant Object Types. Information and Computation, To appear.
[BR99] A. Bossi and S. Rossi. Specialising Logic Programs wrt Pre/Post Specifications, in P. Flener ed., Proceedings of LOPSTR'98, Springer-Verlag LNCS 1559, 159-178 (1999).
[BV92] Bossi A., Valentini S., An intuitionistic theory of types with assumptions of high-arity variables;Annals of Pure and Applied Logic, 57 (1992), pp.: 93-149
[CFRPR97] A. Cortesi, G. File', R. Giacobazzi, C. Palamidessi, and F. Ranzato, Complementation in Abstract Interpretation, ACM Transactions on Programming Languages and Systems, vol.19(1), pp. 7-47. (1997).
[CFW96] A.Cortesi, G.File' and W.Winsborough, Optimal Groundness Analysis Using Propositional Logic, The Journal of Logic Programming, vol. 27(2), pp.137-167. (1996)
[CFW98] A. Cortesi, G. File', and W. Winsborough, The Quotient of an Abstract Interpretation, Theoretical Computer Science, vol. 202(1-2), pp.163--192 (1998).
[CLV00] A.Cortesi, and B.Le Charlier, and P.Van Hentenryck, Combinations of Abstract Domains for Logic Programming: Open Product and Generic Pattern Construction, Science of Computer Programming, Vol 38(1--3), pp. 27-71 (2000).
[DFG00] A. Durante, R. Focardi and R. Gorrieri, A Compiler for Analysing Cryptographic Protocols Using Non-Interference. ACM Transactions on Software Engineering and Methodology. vol. 9(4), pp. 489-530 (2000).
[DMP00] N. Durgin, J. Mitchell, D. Pavlovic. Protocol composition and correctness. Workshop on Issues in the Theory of Security (WITS '00)
[EBC99] Etalle S., Bossi A. e Cocco N., Termination of Well-Moded Programs. Journal of Logic Programming, 38(2): 243-257, 1999.
[FF96] R. Focardi, Comparing Two Information Flow Security Properties, Proceedings of Ninth IEEE Computer Security Foundations Workshop (CSFW'96), (M. Merritt Ed.),IEEE press, Kenmare (Ireland), June 1996.
[FG95] R. Focardi and R. Gorrieri A Classification of Security Properties for Process Algebras, Journal of Computer Security, 3(1): 5-33, 1995.
[FG97] R. Focardi and R. Gorrieri, The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties, IEEE Transactions on Software Engineering, Vol. 23, No. 9, September 1997.
[FGM00a] R. Focardi, R. Gorrieri, F. Martinelli. Message Authentication through Non Interference. In Proc. of the 8th International Conference on Algebraic Methodology and Software Technology (AMAST '00), Lecture Notes in Computer Science 1816, Springer-Verlag, pp. 258-272, Iowa City (USA), May 2000.
[FGM00b] R. Focardi, R. Gorrieri and F. Martinelli. Non Interference for the Analysis of Cryptographic Protocols. 27th International Colloquium on Automata, Languages and Programming (ICALP'00), LNCS 1853, Geneva, July 2000.
[FGM00c] R. Focardi, R. Gorrieri, F. Martinelli, Information Flow Analysis in a Discrete Time Process Algebra, in procs. of 13th IEEE Computer Security Foundations Workshop (CSFW13), (P.Syverson ed), IEEE CS Press, 170-184, 2000.
[FM99] R. Focardi and F. Martinelli, A Uniform Approach for the Definition of Security Properties. In proc. of World Congress on Formal Methods (FM'99), LNCS 1708, pp. 794-813, Toulouse (France), September 1999.
[GJ01] A. Gordon and A. Jeffrey. Authenticity by typing for security protocols. To appear in proc. of CSFW14, 2001.
[HR00] M. Hennessy, J. Riely. Information Flow vs. Resource Access in
the Asynchronous Pi-Calculus. ICALP 2000: 415-427
[LCRC99] B. Le Charlier, C. Leclere, S. Rossi, A. Cortesi, Automated Verification of Prolog Programs, The Journal of Logic Programming, Special Issue on Synthesis, Transformation and Analysis of Logic Programs. Vol.39(1-3), pp. 3-42 (1999).
[LL98] G. Lowe, Casper: A Compiler for the Analysis of Security Protocols, Journal of Computer Security, Volume 6, pages 53-84, 1998.
[LR97] G. Lowe and B. Roscoe, Using CSP to Detect Errors in the TMN Protocol. IEEE Transactions on Software Engineering, volume 23, number 10 ,1997.
[MdPR00] Maietti M.E. , de Paiva V. and Ritter E. Categorical Models for Intuitionistic and Linear Type Theory, proceedings "Foundations of Software Science and Computation Structures", LNCS 1784 (2000), pages 223-238.
[MMS97] J. C. Mitchell, M. Mitchell and U. Stern, Automated Analysis of Cryptographic Protocols Using Murphi, Proceedings of the 1997 IEEE Symposium on Research in Security and Privacy, IEEE Computer Society Press", 1997.
[MV99] Maietti M.E., Valentini S., Can you add power-sets to Martin-Loef intuitionistic set theory?; Mathematical Logic Quarterly, 45 (1999), pp.: 521-532
[PP97] L. C. Paulson, Proving Properties of Security Protocols by Induction, Proceedings of 10th Computer Security Foundations Workshop (CSFW'97), S. Foley Ed., IEEE Press, Rockport, Massachusetts (USA), June 1997.
[PLC01] I. Pollet, B. Le Charlier, and A. Cortesi, Distinctness and Sharing Domains for Static Analysis of Java Programs, in Proc. European Conference on Object Oriented Programming ECOOP 2001, Budapest, june 2001 (to appear).
[RVC99] V.Ramachandran, P.Van Hentenryck, and A.Cortesi, Abstract Domains for Reordering CLP(RLin) Programs, The Journal of Logic Programming, Vol 41(3), pp. 217-256 (2000).
[SS98] S. Schneider, Verifying authentication protocols in CSP, IEEE Transactions on Software Engineering, Vol. 24, No. 9, September 1998.
[SSA00] A. Sabelfeld, D. Sands. Probabilistic Noninterference for Multi-threaded Programs. In proc. of 14th IEEE Computer Security Foundation Workshop (CSFW14), Cambridge, pag. 200-214, July 2000.
[SV98] G. Smith, D.M. Volpano: Secure Information Flow in a Multi-Threaded Imperative Language. In Proc. of POPL 1998: 355-364.
[V96] S.Valentini, The formal development of non-trivial programs in constructive type theory, in "Second International Conference on Massively Parellel Computing Systems", Ischia, maggio 1996, pp. 570-577.
[V01] Valentini S., An elementary proof of strong normalization for intersection types, Archive for Mathematical Logic, to appear.

Testo italiano

Il gruppo di ricerca di questa unita' e' caratterizzato da una solida esperienza nel campo della sicurezza, della verifica dinamica di proprieta' di sicurezza, dell'interpretazione astratta, della manipolazione e verifica di programmi, della teoria dei tipi e dei sistemi di tipi.
Ci aspettiamo che l'interazione tra questi diversi campi porti a contributi scientifici rilevanti nell'area dei metodi formali per la sicurezza. Molte proprieta' proposte in letteratura, ad esempio in [FGM00b, FM99] saranno studiate attraverso varie tecniche di analisi statica: interpretazione astratta, metodi di prova e sistemi di tipi. Questo e' interessante per due diversi aspetti; potrebbe infatti: (i) indicare nuove (e piu' efficienti) tecniche di verifica per proprieta' precedentemente formalizzate, (ii) suggerire nuove caratterizzazioni e formalizzazioni di proprieta' di sicurezza. Poiche' l'analisi statica e' basata sulla semantica, si potrebbero infatti identificare nuove nozioni determinate dalla logica sottostante, e non necessariamente basate su equivalenze osservazionali/comportamentali. Questo costituirebbe un approccio complementare per la formalizzazione di sicurezza nelle algebre di processi.
Piu' in dettaglio, il programma di ricerca di questa unita' si focalizzara' sui seguenti obiettivi:
(1) Caratterizzazione di proprieta' comportamentali di programmi, che sono significative dal punto di vista della sicurezza (segretezza, integrita', autenticazione, ...) e della certificazione (limiti di accesso alle risorse, correttezza dei tipi, ...), dando particolare risalto alle proprieta' che maggiormente possono essere testate con tecniche di analisi statica.
(2) Analisi statica di non-interferenza: la non-interferenza e' una proprieta' tipica di sicurezza rigurdante l'impossibilita' per una parte del sistema (il livello alto) di interferire con un'altra parte del sistema (il livello basso). E' stata studiata attraverso sistemi di tipi in linguaggi imperativi [SV98, SSA00] e nel pi-calculus [HR00], e anche attraverso tecniche di controllo di flusso sia nel pi-calculus che nello spi-calculus [BDNN99]. Intendiamo studiare la formalizzazione e l'analisi della proprieta' di non-interferenza in algebre di processi piu' semplici, ad esempio CryptoSPA, e in calcoli per mobilita', ad esempio Ambient Calculus. L'analisi sara' effettuata attraverso intrpretazione astratta, metodi di prova e sistemi di tipi.
(3) Analisi statica di protocolli crittografici: ci sono pochi risultati rigurdanti questo argomento specifico [AA99,GJ01] che merita pertanto di essere approfondito. In particolare, i risultati che speriamo di ottenere nel punto precedente potrebbero essere applicati anche all'analisi di protocolli, sfruttando la teoria sviluppata in [FM99, FGM00b], dove viene proposto uno schema generale basato su non-interferenza per la modellizzazione di proprieta' di protocolli crittografici. Grazie a tale teoria, le tecniche di analisi statica sviluppate per la non-interferenza si applicherebbero direttamente all'analisi di protocolli crittografici.
(4) Strumenti di verifica: una delle applicazioni della ricerca effettuata nei punti precedenti, sara' lo sviluppo di un analizzatore astratto che supporti la certificazione di protocolli e di Java byte code. Intendiamo, inoltre, studiare nuove tecniche per estendere i tool di verifica presentati in [DFG00, FG97] e basati su tecniche dinamiche/comportamentali. In particolare svilupperemo un tool di verifica basato su sistemi di transizione etichettati simbolici, che dovrebbe ridurre in modo sostanziale il problema tipico, nella verifica dinamica, dell'esplosione dello spazio degli stati. Considereremo anche modelli estesi con probabilita'/tempo allo scopo di verificare proprieta' nello stile di [FGM00c].
(5) Confronto di tecniche di analisi statica: lo studio di come le varie tecniche di analisi statica possano essere applicate per l'individuazione di problemi di sicurezza fornira' anche un buon banco di prova per confrontare tali tecniche. Questo non e' uno degli obiettivi principali del progetto ma potrebbe, tuttavia, fornire interessanti spunti riguardo ai vantaggi e alle potenzialita' delle differenti tecniche di analisi statica.
(6) Nuovi modelli per sicurezza: molte proprieta' di sicurezza di programmi possono essere espresse in pi-calculus e spi-calculus. Intendiamo definire un nuovo sistema di tipi per un formalismo che estende tali algebre di processi con tipici lambda-termini, allo scopo di esprimere computazione di funzioni. L'obiettivo e' quello di definire nuove nozioni formali di sicurezza di programmi e nuovi strumenti per la loro verifica.

Testo inglese

The research team of this unit is characterized by a solid experience in the fields of security, dynamic/behavioural verification of security properties, abstract interpretation, semantics-based program manipulation and verification, type theory and type systems.
We expect that the cross-fertilization of these different backgrounds will lead to significant scientific contributions in the area of formal methods for security. Many security properties proposed, e.g., in [FGM00b, FM99], will be approached through different static analysis techniques, namely abstract interpretation, proof methods and type systems. This could be interesting at least in two respects: (i) it could provide new (more efficient) verification techniques for already formalized security properties, (ii) it could suggests new ways of characterizing particular security properties: starting from a static analysis perspective, it could be possible to identify new security notions determined by the underlying logic and not necessarily based on behavioural equivalences. This could be a complementary approach to the formalization of security in process calculi.
Specifically, the research program of the unit will be focussed on the following list of goals:
(1) Characterization of behavioural program properties that are significant for program security (secrecy, integrity,authenticity,...) and certification (resource-usage bounds, type-safety,...), focusing on the ones that may benefit by static analysis techniques.
(2) Static analysis of Non-interference: Non-interference is a typical security property which requires that a part of a system (high level) has no way of interfering with another part of the system (low level). It has been studied through type systems in imperative languages [SV98, SSA00] and in the pi-calculus [HR00]; and also through control flow in pi and spi-calculus [BDNN99]. We intend to study its formalization and analysis also in simpler process calculi, e.g. CryptoSPA, and in calculi for mobility, e.g., Ambient Calculus. The analysis will be performed through abstract interpretation, proof methods and type systems.
(3) Static analysis of cryptographic protocols: there are few results regarding this topic [AA99,GJ01] and we intend to explore also this line of research. In particular, the results we hope to obtain for point 2 above could be applied also to protocols by exploiting the theory of [FM99, FGM00b] where a general scheme based on non-interference is proposed for modelling cryptographic protocol properties. Through such a theory, general static analysis techniques for Non-Interference would also apply to the analysis of cryptographic protocols.
(4) Verification tools: the development of prototypes of abstract analyzers that support protocol and Java byte code certification will be one of the possible applications of the research. We also intend to study new techniques for extending the dynamic/behavioural verification tools of [DFG00, FG97]. In particular we will develop a tool based on symbolic labelled transition systems, which should substantially reduce the typical state-explosion problem of behavioural verification. We will also consider models extended with probability/time in order to check properties like the ones proposed in [FGM00c].
(5) Comparison of static analysis techniques: the study of how different static analysis techniques could be applied for detecting security flaws, could also provide a good case-study for comparing such techniques. This is not one of the main aim of the present project but could nevertheless provide new insight into the merits and potentiality of various static analysis approaches.
(6) New models for security: many properties concerning program security can be expressed in pi-calculus and spi-calculus. We want to define a new type system for a calculus which extendes these calculi with more usual lambda terms in order to express functional computation. Our aim is to give new formal notions of program security and new formal tools to test it.

Nº	Anno di acquisizione	Descrizione
		Testo italiano	Testo inglese

Attrezzatura I
Descrizione

valore presunto (milioni)   percentuale di utilizzo per il programma

Attrezzatura II
Descrizione

valore presunto (milioni)   percentuale di utilizzo per il programma

QUADRO RD

4.1.1 Altro

QUADRO RA

4.2.1 Altro

Firma ____________________________________________

(per la copia da depositare presso l'Ateneo e per l'assenso alla diffusione via Internet delle informazioni riguardanti i programmi finanziati; legge del 31.12.96 n° 675 sulla "Tutela dei dati personali")