Vai al contenuto| Home page|

   Ti trovi in: HOME »Programmi, progetti e risultati »I progetti »PRIN - Programmi di ricerca di Rilevante Interesse Nazionale»Programma di ricerca»Unità di ricerca
INIZIO_TESTO_DA_INDICIZZARE

UNITA' DI RICERCA

italiano - english
Bibliografia
[Abadi99] Martin Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749--786, 1999.

[AG97] M. Abadi and A.D. Gordon. A Calculus for Cryptographic Protocols: the Spi Calculus. In Fourth ACM Conference on Computer and Communications Security, pages 36-47. ACM Press, 1997.

[BP] D. E. Bell, L. J. L. Padula. Secure Computer Systems: Unified Exposition and Multics Interpretation. ESD-TR-75-306, MITRE-MTR-2997.

[BDNN01] C. Bodei, P. Degano, F. Nielson, and H. Riis Nielson. Static analysis for secrecy and non-interference in networks of processes. In Proc. International Conference on Parallel Computing Technologies, LNCS 2127, pages 27-41. Springer-Verlag, 2001.

[BDNN98] Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne Riis Nielson. Control Flow Analysis for the pi-calculus. In Proc. CONCUR 98, LNCS 1466, pages 84-98. Springer-Verlag, 1998.

[BDNN01a] Chiara Bodei, Pierpaolo Degano, F. Nielson, and H. Riis Nielson. Static Analysis for the pi-calculus with Applications to Security. Information and Computation, 165:68-92, 2001.

[BDNN01b] Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne Riis Nielson. Static Analysis for Secrecy and Non-Interference in Networks of Processes. In Proc. PaCT 01, LNCS 2127, pages 27-41. Springer-Verlag, 2001.

[BDNN99] Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne Riis Nielson. Static Analysis of Processes for No Read-Up and No Write-Down. In Proc. FoSSaCS 99, LNCS 1578, pages 120-134. Springer-Verlag, 1999.

[BCF02] Chiara Braghin, Agostino Cortesi, and Riccardo 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 and Structures, 2004. To appear.

[BCC01] Michele Bugliesi, Giuseppe Castagna, and Silvia Crafa. Boxed Ambients. In Proc. of the 4th Int. Conference on Theoretical Aspects of Computer Science (TACS 01), LNCS 2215, pages 38-63. Springer-Verlag, 2001.

[BFPR02] A. Bossi, R. Focardi, C. Piazza, and S. Rossi. Transforming Processes to Ensure and Check Information Flow Security. In Proc. Int. Conference on Algebraic Methodology and Software Technology AMAST'02), LNCS 2422, pages 271-286. Springer-Verlag, 2002.

[BFPR03a] A. Bossi, R. Focardi, C. Piazza, and S. Rossi. A Proof System for Information Flow Security. In M. Leuschel, editor, Logic Based Program Development and Transformation, LNCS 2664, pages 199- 18. Springer-Verlag, 2003.

[BFPR03b] A. Bossi, R. Focardi, C. Piazza, and S. Rossi. Refinement Operators and Information Flow Security. In Proc. 1st IEEE Int. Conference on Software Engineering and Formal Methods (SEFM'03), IEEE Computer Society Press, pages 44-53, 2003.

[BFPR04] A. Bossi, R. Focardi, C. Piazza, and S. Rossi. Verifying Persistent Security Properties. Computer Languages Systems and Structures. In Press, 2004.

[CCH00] A. Cortesi, B. Le Charlier, P. Van Hentenryck, Combinations of abstract domains for logic programming: open product and generic pattern construction. Science of Computer Programming 38(1-3):27-71(2000)

[CFGP97] A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, F. Ranzato: Complementation in Abstract Interpretation. TOPLAS 19(1): 7-47 (1997)

[CG98] Luca Cardelli and Andrew D. Gordon. Mobile Ambients. In Proc. of Foundations of Software Science and Computation Structures (FoSSaCS), LNCS 1378, pages 140-155. Springer-Verlag, 1998.

[CC77] P. Cousot, R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. ACM POPL'77, pp. 238-252, ACM Press, 1977.

[CC79] P. Cousot, R. Cousot. Systematic design of program analysis frameworks. In Proc. ACM POPL'79, pp. 269-282, ACM Press, 1979.

[C96] Patrick Cousot. Abstract Interpretation. In ACM Computing Surveys, 28(2):324-328, June 1996.

[C07] Patrick Cousot. Program Analysis: The Abstract Interpretation Perspective. SIGPLAN Notices, Volume 32, 1997, Pages 73-76.

[DLB00] Pierpaolo Degano, Francesca Levi, and Chiara Bodei. Safe Ambients: Control Flow Analysis and Security. In Jifeng He and Masahiko Sato, eds., Proc. of ASIAN 00, LNCS 1961, pages 199-214. Springer, December 2000.

[DS00] Mariangiola Dezani-Ciancaglini and I.Salvo. Security Types for Mobile Safe Ambients. In Jifeng He and Masahiko Sato, editors, Proc. of ASIAN 00, LNCS 1961, pages 215 236. Springer, December 2000.

[FG01] R. Focardi and R. Gorrieri. Classification of Security Properties (Part I: Information Flow). In Foundations of Security Analysis and Design, LNCS 2171, Springer, 2001.

[FG01] R. Focardi and R. Gorrieri. Classification of Security Properties (Part II: Network Security). In Foundations of Security Analysis and Design, LNCS 2946, Springer, 2004.

[FGM00] R. Focardi, R. Gorrieri, and F. Martinelli. Non Interference for the Analysis of Cryptographic Protocols. In Proc. of Int. Colloquium on Automata, Languages and Programming, LNCS 1853, pages 744--755. Springer-Verlag, 2000.

[GJ02] Andrew D. Gordon and A. Jeffrey. Types and effects for asymmetric cryptographic protocols. In Proc. of the 15th IEEE Computer Security Foundations Workshop (CSFW 2002), pages 77-91, 2002.

[GJ01a] Andrew D. Gordon and A. Jeffrey. Authenticity by typing for security protocols. In Proc. of the 14th IEEE Computer Security Foundations Workshop (CSFW 2001), pages 145-159, 2001.

[GJ01b] Andrew D. Gordon and A. Jeffrey. Typing correspondence assertions for communication protocols. In Proc. of the 17th Conference on the Mathematical Foundations of Programming Semantics, pp. 99-120, Elsevier ENTCS 45, 2001.

[GM82] J. A. Goguen, J. Meseguer. Security Policies and Security Models. In Proc. of the IEEE Symposium on Security and Privacy (SSP'82), IEEE Computer Society Press, pages 11-20, 1982.

[GLM03] R. Gorrieri, E. Locatelli, and F. Martinelli. A simple language for real-time cryptographic protocol analysis. In Proc. of European Symposium on Programming (ESOP'03), LNCS 2618, pp. 114-128. Springer-Verlag, 2003.

[HR02] M. Hennessy and J. Riely. Information Flow vs. Resource Access in the Asynchronous Pi-calculus. ACM Transactions on Programming Languages and Systems, 24(5):566-591, 2002.

[McC87] D. McCullough. Specifications for Multi-Level Security and a Hook-Up Property. In Proc. of the IEEE Symposium on Security and Privacy (SSP'87), IEEE Computer Society Press, pages 161-166, 1987.

[MPW92] R. Milner, J. Parrow, and J. Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1-77, September 1992.

[McL94] J. McLean. Security Models. Encyclopedia of Software Engineering, 1994.

[M89] J. K. Millen. Finite-State Noiseless Covert Channels. In Proc. of the Computer Security Foundations Workshop II, the MITRE Corporation, IEEE Computer Society Press, pages 81-86, 1989.

[HJNN99] R. R. Hansen, J. G. Jensen, F. Nielson, and H. Riis Nielson. Abstract Interpretation of Mobile Ambients. In Proc. of Static Analysis Symposium (SAS 99), LNCS 1694 , pages 134-148. Springer-Verlag, 1999.

[LS00] Francesca Levi and Davide Sangiorgi. Controlling Interference in Ambients. In Proc. 28th ACM Symposium on Principles of Programming Languages (POPL 00), pages 352-364, 2000.

[NS01] F. Nielson and H. Seidl. Control-flow analysis in cubic time. In Proc. ESOP'01, number 2028 in Lecture Notes in Computer Science, pages 252-268. Springer-Verlag, 2001.

[NNH99] F. Nielson, H.R.Nielson, and C. Hankin, Principles of Program
Analysis. 1999.

[OH90] C. O'Halloran. A Calculus of Information Flow. In Proc. of the uropean Symposium on Research in Security and Privacy, AFCET, pages 80--187, 1990.

[RS01] P. Y. A. Ryan and S. Schneider. Process Algebra and on-Interference. Journal of Computer Security, 9(1/2):75--103, 001.

[RVA00] V. Ramachandran, P. Van Hentenryck, A. Cortesi: Abstract Domains for Reordering CLP(RLin) Programs. Journal of Logic Programming 42(3): 217-256 (2000)

[SM03] A. Sabelfeld and A. C. Myers. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21(1):5 19, IEEE Computer Society Press, 2003.

[S86] D. Sutherland. A Model of Information. In Proc. of the 9th National Computer Security Conference, pages 175--183, 1986.

[Z97] A. Zakinthinos, E. S. Lee. A General Theory of Security Properties. In Proc. of the IEEE Symposium on Security and Privacy (SSP'97), IEEE Computer Society Press, pages 74--102, 1997.

Programma di ricerca

AIDA - Interpretazione Astratta: Progettazione e Applicazioni
Università di riferimento
Università "Cà Foscari" di VENEZIA - INFORMATICA - VENEZIA(VE)
Responsabile dell'Unità di ricerca
Agostino CORTESI
Descrizione
L'attivita di ricerca dell'unita' di Venezia si svolgera' all'interno dei seguenti Workpackages: Workpackage WP1. Analisi Statica Task VE_1 Domini astratti Vi sono diversi approcci all'analisi statica basata su grammatiche, ad esempio domini di tipo regolare, vincoli su insiemi, e schemi ad albero. Indipendentemente dal diverso potere espressivo e dalla diversa complessita' di questi approcci, vi sono vari trade-offs tra precisione ed efficienza. Si puo' ad esempio scegliere tra grammatiche deterministiche o grammatiche non-deterministiche, e tra domini ad altezza finita specializzati sul programma da analizzare o domini ad altezza infinita provvisti di operatori di widening e tecniche implementative quali la tabulazione. Ci si propone di studiare questo tipo di problematiche sia dal punto di vista teorico che sperimentale, e di considerare la combinazione di domini basati su grammatiche con altri tipi di domini quali quelli basati su astrazioni aritmetiche. La progettazione di domini composti richiede metodi avanzati di raffinamento e di semplificazione, quali il prodotto ridotto, il prodotto tensoriale, l'operatore di complemento e l'operatore di compressione di domini. Siamo quindi interessati ad introdurre un'algebra di tali operatori che possa essere di supporto alla progettazione sistematica di domini astratti simbolici adattabili rispetto a precisione e costo computazionale. Il nostro obiettivo e' quello di immergere le proprieta' semantiche nei domini astratti cosi' che il risultato dell'applicazione di tali operatori ai domini garantisca all'analisi caratteristiche di modularita', di completezza e di reversibilita'. Workpackage WP2: Sicurezza Il nostro obiettivo e' quello di sviluppare metodi di analisi statica precisi ed efficienti finalizzati a garantire la sicurezza del software, in particolare la confidenzialita' dei dati e la protezione delle risorse. Particolare enfasi verra' data su tecniche che provano l'assenza di flussi di informazione indesiderati in sistemi concorrenti, distribuiti ed in sistemi per la mobilita' (ad esempio quando si descrivono protocolli crittografici in Mobile Ambient Calculus). Studieremo inoltre lo sviluppo di opportuni formalismi per esprimere politiche di sicurezza che possano essere verificate automaticamente mediante tecniche di analisi statica. Task VE_2.1 Approccio Semantico Operazionale: Immersione Lo schema generale proposto in [BFPR04] consente di studiare in modo uniforme un'ampia classe di proprieta' di sicurezza. Lo schema e' parametrico rispetto a due relazioni semantiche: una equivalenza osservazionale ed una nozione di raggiungibilita'. In particolare e' stato mostrato come risultati di composizionalita' applicabili alle proprieta' considerate siano connessi alle condizioni di unwinding usate per istanziare lo schema. E' anche stato osservato come la composizionalita' sia cruciale per la definizione di sistemi di prova (si veda [BFPR03a]) che costruiscono solo processi sicuri. Purtroppo lo schema non fornisce un metodo diretto per il confronto delle proprieta' di sicurezza ottenute da diverse istanze dello stesso. Al fine di analizzare tale aspetto intendiamo studiare un'immersione del nostro schema in un reticolo di domini di interpretazione astratta. Per raggiungere questo risultato il nostro punto di partenza sara' l'analisi della corrispondenza tra equivalenze osservazionali e domini astratti. Un primo vantaggio dell'immersione sara' la possibilita' di sfruttare tecniche di interpretazione astratta nella fase di verifica. Inoltre, si potrebbe giungere alla scoperta di nuove proprieta' semplicemente dal completamento del reticolo. Intendiamo anche analizzare le relazioni tra l'immersione del nostro schema nell'ambito dell'interpretazione astratta e lo schema di interpretazione astratta descritto nel lavoro presentato al POPL'04 "Abstract Non-Interference" da Giacobazzi e Mastroeni. Tale confronto potrebbe da una parte consentire una integrazione dei due schemi da un punto di vista teorico; dall'altra suggerire una combinazione di algoritmi e tecniche di verifica provenienti dalle aree di Analisi Statica e Verifica Dinamica (Model Checking). Per esempio, la tecnica descritta da Giacobazzi e Mastroeni per derivare il dominio "piu' preciso" rispetto a cui un dato programma e' sicuro richiama il problema di raffinamento stabile di partizioni che e' alla base della computazione efficiente di relazioni di bisimulazione. Task VE_2.2 Approccio Semantico Operazionale: Estensioni e Confronti Un aspetto ortogonale che intendiamo studiare e' una generalizzazione del nostro schema che consenta l'analisi di processi a stati infiniti (ovvero molti grandi). Tale generalizzazione puo' essere ottenuta sfruttando nuovamente tecniche di interpretazione astratta al fine di mappare modelli infiniti (molto grandi) in modelli finiti, similmente a quanto gia' fatto nell'area di Abstract Model Checking. Partendo da questo risultato e utilizzando tecniche di rappresentazione standard intendiamo estendere il nostro schema per includere diversi linguaggi, ad esempio linguaggi imperativi. In particolare semantiche concrete e astratte di linguaggi di programmazione possono essere date in termini di sistemi di transizione etichettati (LTS) semplicemente rappresentando tutte le evoluzioni delle possibili computazioni. In ultima analisi il nostro schema di proprieta' di sicurezza si basa solamente sulla nozione di LTS (arricchita con equivalenze osservazionali e nozioni di raggiungibilita'). Quindi e' molto naturale sfruttarlo nell'analisi di semantiche basate su LTS. Tuttavia per assicurare l'applicabilita' delle nostre tecniche di verifica (cioe' per mantenere sotto controllo la dimensione del LTS) e' necessario analizzare accuratamente l'uso/combinazione di diverse semantiche astratte. Molti sistemi di tipi sono stati proposti per analizzare/verificare la sicurezza di programmi scritti in vari linguaggi di programmazione (si veda [SM03]). I sistemi di tipi possono essere visti come particolare domini di interpretazione astratta, quindi un'estensione del nostro schema basata su semantiche astratte/concrete potrebbe permettere un confronto delle nostre tecniche di verifica con tecniche basate su controllo dei tipi. Task VE_2.3 Approccio Control-Flow:Raffinamento di Domini astratti e Ottimizzazione degli algoritmi Intendiamo raffinare i domini astrtti dell'analisi descritta in [BCF02], usando informazione contestuale per confinare gli effetti ed i valori degli oggetti del sistema. Tuttavia, il costo di una maggiore precisione dell'analisi viene usualmente pagato in termini di efficienza dell'analisi. La complessita' in tempo e spazio sono punti chiave per valutare la scalabilita' dell'analisi, e meritanodi essere approfondite. In [BCFLP04] abbiamo introdotto due nuovi algoritmi che migliorano la complessita' sia in tempo che in spazio rispetto a [NS01]. Intendiamo studiare come questi miglioramente possano essere generalizzati ad una classe piu' ampia di analisi control-flow. Task VE_2.4 Approccio Control-Flow: Confronti Diverse tecniche di analisi statica, formalizzate in termini di Type Systems o di Analisi Control-Flow, sono state applicate all'analisi di proprieta' di sicurezza di programmi scritti in Mobile Ambient Calculus. Questi approcci sono strettamente legati e calcolano informazione simile sul comportamento run-time dei processi. Entrambi gli approcci sono dimostrati corretti rispetto ad una semantica formale, ma poiche' sono espressi con formalismi assai diversi, risulta difficile un loro confronto sistematico (sia a livello di astrazione di proprieta' che a livello di algoritmi). Siamo convinti che studiando in modo approfondito la relazione tra Interpretazione Astratta e la tecnica di Control-Flow analisi basata su Flow-Logic sia possibile utilizzare la teoria dell'Interpretazione Astratta come formalismo unificante per confrontare i due approcci (type systems e control-flow) e per stabilire a quali classi di proprieta' si applichi meglio l'una o l'altra tecnica.