Contenuto
Ti trovi in: HOME »Programmi, progetti e risultati »I progetti »PRIN - Programmi di ricerca di Rilevante Interesse Nazionale»Programma di ricerca»Unità di ricercaINIZIO_TESTO_DA_INDICIZZARE
UNITA' DI RICERCA
italiano - english
Bibliografia
1. D. Awduche, J. Malcolm, J. Agogbua, M. O’Dell, and J. McManus. Rfc2702: Requirements for traffic engineering over MPLS. Technical report, Network Working Group, 1999.2. G. Bella and S. Bistarelli. Protocol analysis using soft constraints. Invited talk at S.R.I. Security group, Menlo Park, USA, February 2001.
3. G. Bella and S. Bistarelli. Soft Constraints for Security Protocol Analysis: Confidentiality. In Proc. of PADL’01, LNCS 1990, pages 108–122, 2001.
4. S. Bistarelli. Semirings for Soft Constraint Solving and Programming, volume 2962 of LNCS. Springer, 2004.
5. S. Bistarelli, H. Fargier, U. Montanari, F. Rossi, T. Schiex, and G. Verfaillie. Semiring-based CSPs and Valued CSPs: Frameworks, properties, and comparison. CONSTRAINTS: An international journal. Kluwer, 4(3):199–240, 1999.
6. S. Bistarelli and S. Foley. Analysis of integrity policies using soft constraints. In Proc. of IEEE Workshop Policies for Distributed Systems and Networks, pages 77–80, June 2003.
7. S. Bistarelli and S. Foley. A constraint based framework for dependability goals: Integrity. In Proc. of 22nd International Conference on Computer Safety, Reliability and Security (SAFECOMP2003), volume 2788 of Lecture Notes in Computer Science, pages 130–143. Springer, 2003.
8. S. Bistarelli, S. N. Foley, and B. O’Sullivan. Detecting and eliminating the cascade vulnerability problem from multi-level security networks using soft constraints. In Proceedings Innovative Applications of Artificial Intelligence Conference (IAAI04). ACM Press, 2004. To appear.
9. S. Bistarelli, S. N. Foley, and B. O’Sullivan. Modelling and detecting the cascade vulnerabiliy problem using soft constraints. In Proc. ACM Symposium on Applied Computing (SAC 2004), pages 383–390. ACM Press, 2004.
10. S. Bistarelli, J. Kelleher, and B. O’Sullivan. Tradeoff Generation using soft constraints. In Springer, editor, Recent Advances in Constraints, Joint ERCIM/CoLogNET International Workshop on Constraint Solving and Constraint Logic Programming, CSCLP’03, Selected Papers, volume 3010 of Lecture Notes in Computer Science, pages 124–139, 2003.
11. S. Bistarelli, U. Montanari, and F. Rossi. Constraint Solving over Semirings. In Proc. IJCAI95, pages 624–630, San Francisco, CA, USA, 1995. Morgan Kaufman.
12. S. Bistarelli, U. Montanari, and F. Rossi. Semiring-based Constraint Solving and Optimization. JACM, 44(2):201–236, 1997.
13. S. Bistarelli, U. Montanari, and F. Rossi. Soft concurrent constraint programming. ACM Transactions on Computational Logic (TOCL), 2001. To Appear.
14. S. Bistarelli, U. Montanari, and F. Rossi. Soft concurrent constraint programming. In Proc. ESOP, April 6 - 14, 2002, Grenoble, France, LNCS, pages 53–67. Springer-Verlag, 2002.
15. S. Bistarelli and B. O’Sullivan. A theoretical framework for tradeoff generation using soft constraints. In Springer, editor, Research and Development in Intelligent Systems XX, Proceedings of AI-2003, the Twenty-third SGAI International Conference on Knowledge-Based Systems and Applied Artificial Intelligence, BCS Conference Series ’Research and Development in Intelligent Systems xx’, pages 69–82, 2003.
16. M. Calisti and B. Faltings. Distributed constrained agents for allocating service demands in multi-provider networks,. Journal of the Italian Operational Research Society, XXIX(91), 2000. Special Issue on Constraint-Based Problem Solving.
17. S. Chen and K. Nahrstedt. Distributed QoS routing with imprecise state information. In Proc. 7th IEEE International Conference on Computer, Communications and Networks (ICCCN’98), pages 614–621, 1998.
18. D. Clark. Rfc1102: Policy routing in internet protocols. Technical report, Network Working Group, 1989.
19. J. Fitch and L. Hoffman. A shortest path network security model. Computers and Security, 12(2):169–189, 1993.
20. L. Gong and X. Qian. The complexity and composability of secure interoperation. In Proceedings of the Symposium on Security and Privacy, pages 190–200, Oakland, CA, May 1994. IEEE Computer Society Press.
21. E. Gray. American national standard T1.523-2001, telecom glossary 2000. published on the Web at http://www.its.bldrdoc.gov/projects/telecomglossary2000, 2001.
22. S. Gritalis and D. Spinellis. The cascade vulnerability problem: The detection problem and a simulated annealing approach to its correction. Microprocessors and Microsystems, 21(10):621–628, 1998.
23. J. Horton, R. Harland, E. Ashby, R. Cooper,W. Hyslop, B. Nickerson, W. Stewart, and O. Ward. The cascade vulnerability problem. Journal of Computer Security, 2(4):279–290, 1993.
24. R. Jain and W. Sun. QoS/Policy/ConstraintBased routing. In Carrier IP Telephony 2000 Comprehensive Report. International Engineering Consortium, 2000.
25. G. Lowe. An Attack on the Needham-Schroeder Public-Key Authentication Protocol. Information Processing Letters, 56(3):131–133, 1995.
26. J. Millen and M. Schwartz. The cascading problem for interconnected networks. In 4th Aerospace Computer Security Applications Conference, pages 269–273, Dec. 1988.
27. T. Schiex. Possibilistic constraint satisfaction problems, or “how to handle soft constraints?”. In Proc. 8th Conf. of Uncertainty in AI, pages 269–275, 1992.
28. TNI. Trusted computer system evaluation criteria: Trusted network interpretation. Technical report, National Computer Security Center, 1987. Red Book.
29. Cousot, P. and Cousot, R. Systematic design of program analysis frameworks. In Proc. Sixth ACM Symp. Principles of Programming Languages (POPL ’79). ACM Press, New York, 269–282, 1979.
30. Cousot, P. and Cousot, R. Abstract Interpretation Frameworks. Journal of Logic Programming 2(4):511–549, 1992.
31. G. Fil`e, R. Giacobazzi and F. Ranzato A Unifying View on Abstract Domain Design ACM Computing Surveys 28(2):333-336, 1996.
32. R. Giacobazzi, F. Ranzato, F. Scozzari Making Abstract Interpretations Complete Journal of the ACM 47(2):361–416, 2000.
33. F. Fioravanti, A. Pettorossi, and M. Proietti. Verification of sets of infinite state systems using program transformation. In A. Pettorossi (ed.), Proc. LOPSTR 2001, LNCS 2372, pp. 111–128. Springer, 2002.
34. F. Fioravanti, A. Pettorossi, and M. Proietti. Automatic Proofs of Protocols via Program Transformation. In Proceedings of the International Workshop on Monitoring, Security, and Rescue Techniques in Multi-Agents Systems (MSRAS ’04), June7-9, 2004, Poland, 2004.
35. MAP group. The MAP transformation system. Available from: http://www.iasi.rm.cnr.it/~proietti/system.html, 1995–2004.
36. M. Abadi Security protocols and specifications. In Proceedings of FOSSACS ’99, pages 1-13, 1999
37. R. Giacobazzi and F. Scozzari A logical model for relational abstract domains. ACM Transactions on Programming Languages (TOCL), 20(5):1067–1109, 1998
38. F. Scozzari Logical optimality of groundness analysis Theoretical Compiter Science 277(1-2):149–184, 2002
39. L. Aceto and D. Murphy. Timing and causality in process algebra. Acta Informatica, 33(4):317–350, 1996.
40. J. Baeten and J. Bergstra. Real time process algebra. Formal Aspects of Computing, 3(2):142–188, 1991.
41. G. Berry and G. Gonthier. The esterel programming language: Design, semantics and implementation. Science of Computer Programming, 19(2):87–152, 1992.
42. P. Bremond-Gregoire and I. Lee. A Process Algebra of Communicating Shared Resources with Dense Time and Priorities. Theoretical Computer Science, 189(1-2):169–219, 1997.
43. P. Caspi, N. Halbwachs, D. Pilaud, and P. Raymond. The synchronous dataflow programming language LUSTRE. In Special issue on Another Look at Real-time Systems, volume 79 of Proceedings of the IEEE, pages 1305–1319. IEEE Computer Society Press, 1991.
44. F. S. de Boer, M. Gabbrielli, and M. C. Meo. A Timed CCP Language. Information and Computation, 161(1):45–83, 2000.
45. M. Fisher. An introduction to Executable Temporal Logics. Knowledge Engineering Review, 6(1):43–56, 1996.
46. M. Hennessy and T. Regan. A temporal process algebra. Information and Computation, 117:221–239, 1995.
47. Z. Manna and A. Pnueli. The temporal logic of reactive systems. Springer-Verlag, 1991.
48. V. A. Saraswat, R. Jagadeesan, and V. Gupta. Timed Default Concurrent Constraint Programming. Journal of Symbolic Computation, 22(5-6):475–520, 1996.
49. F. S. de Boer, M. Gabbrielli and M. C. Meo. Proving Correctness of Timed Concurrent Constraint Programs. ACM Transactions on Computational Logic (TOCL), 5(4), 2004.
Programma di ricerca
Vincoli e preferenze come formalismo unificante per l'analisi di sistemi informatici e la soluzione di problemi realiUniversità di riferimento
Università degli Studi "G. d'Annunzio" CHIETI-PESCARA - SCIENZE - CHIETI(CH)Responsabile dell'Unità di ricerca
Stefano BISTARELLIDescrizione
La proposta di ricerca ha le basi sulle conoscenze già acquisite dai componenti dell'unità nei campi dei vincoli soft, dell'astrazione e della concorrenza.L'attività da una parte mirerà ad estendere il formalismo dei vincoli soft e dall'altra parte studierà possibili utilizzi di vincoli soft con astrazione e concorrenza per lo studio di sistemi e applicazioni.
In particolare, nostro scopo è lo studio di sistemi ed applicazioni nei campi della sicurezza informatica, e nell'analisi e valutazione del rischio in sicurezza. Ci proponiamo più in dettaglio i seguenti obiettivi:
Estensione del framework dei Vincoli Soft
---------------------------------------
Il framework dei vincoli basati su semiring (semiring-based CSP (SCSP)) [12, 4, 11, 5, 14, 13] è capace di rappresentare molte classi di vincoli soft (fuzzy, pesati, probabilistici, multicriteria, ...), a seconda del significato dato ai valori associati ad ogni tupla (interpretati come livelli di preferenza, di importanza o costi). I vincoli soft basati su semiring sono così chiamati perchè basati proprio su una sottostante struttura di semiring che definisce l'insieme delle preferenze, l'ordinamento tra queste e la modalità di combinarle. Questo concetto è molto generale e può essere istanziato al fine di ottenere molte delle classi di vincoli soft già proposte, i loro algoritmi di risoluzione e anche di nuovi.
Tuttavia, il framework, pur ricco, non è sufficiente quando deve essere rappresentato non solo ciò che l'utente desidera ma anche ciò che non desidera.
Inoltre il framework necessita ancora molto studio riguardo agli algoritmi risolutivi.
** Risultati attesi: **
Ci si propone di arricchire la struttura di semiring sia dal punto di vista dell'insieme di preferenze (in modo da rappresentare non solo valori positivi per ciò che l'utente desidera ma anche negativi per ciò che l'utente non desidera), che dal punto di vista degli operatori.
In particolare saranno introdotti altri operatori (con semantica in qualche modo opposta agli operatori "+" e "x") che saranno utili per introdurre l'uso dì vincoli soft in nuovi ambiti applicativi. Un ambito di particolare interesse sembra quello dei Data Base a vincoli. Qui un operatore opposto al "+" sembra necessario per estendere al caso soft la nozione di differenza insiemistica.
Ci si propone anche di studiare e modificare vari algoritmi risolutivi usati nel caso dei vincoli classici e verificare la loro applicazione nel caso di vincoli soft.
Vincoli Soft per l'analisi di sistemi con sicurezza multilivello
----------------------------------------------
La sicurezza di una rete è basata non solo sulla sicurezza delle sue componenti e delle interconnessione dirette tra loro, ma anche sulla potenziale possibilità che i sistemi possono avere di interoperare indirettamente attraverso le connessioni di rete. Tale possibilità può infatti potenzialmente creare dei "cascading path" [28] che violano la sicurezza dei sistemi attraverso le connessioni di rete. In [9, 8] è mostrato come la programmazione con vincoli fornisce un approccio naturale per esprimere i vincoli necessari per assicurare la sicurezza multilivello attraverso la rete. In particolare i vincoli soft possono essere usati per evidenziare ed eliminare i cascading path nella rete che violano la sicurezza.
L'approccio con vincoli soft sembra fornire un avanzamento rispetto alle tecniche usate per risolvere questo problema. La ricerca attualmente studia come evidenziare i "cascading paths" e come eliminarli riconfigurando la rete. Se evidenziare il problema può essere fatto facilmente [26, 23, 19, 20], l'eliminazione delle vuulnerabilità eliminando il minimo numero di connessioni e' un problema NP-completo [23, 22, 20].
Usando la programmazione con vincoli soft e' possibile evidenziare l'insieme di tutti i cascading path e quindi ottenere una soluzione minimale (anche se non ottima) in tempo polinomiale.
** Risultati attesi: **
Il modello a vincoli può fornire una descizione naturale di una arbitraria rete a sicurezza multilivello. Ogni soluzione del modello rappresenta un cascading path nella rete fornendo molte più informazioni sulle vulnerabilità degli approcci classici e fornendo informazioni per la loro eliminazione.
Usando un modello a vincoli possiamo utilizzare le tecniche risolutive sviluppate in questo campo per trovare l'insieme dei cascading path con uno sforzo ragionevole, e quindi eliminare il problema in tempo polinomiale.
Ci proponiamo di applicare la tecnologia a vincoli ad alcuni casi reali, iniziando alcune collaborazioni con società interessate. Siamo in trattativa per collaborazioni su questi argomenti.
Analisi Quantitativa di Politiche di Integrità
----------------------------------
Una politica di integrità definisce le situazioni in cui le modifiche alle informazioni sono autorizzate e attuate dai meccanismi di sicurezza del sistema. In complessi sistemi applicativi è però possibile che una politica di integrità sia specificata in maniera non corretta e, come conseguenza, un utente sia autorizzato a modificare informazioni che possono portare ad una inattesa compromissione del sistema. In [6, 7] è stata proposta una tecnica quantitativa scalabile che usa la risoluzione di vincoli per modellare ed analizzare l'efficacia delle politiche di integrità di un sistema applicativo.
** Risultati Attesi: **
Piuttosto che tentare di modellare il comportamento completo del sistema e dell'infrastruttura, nell'approccio basato su vincoli, solo quei componenti che sono considerati rilevanti per la politica di sicurezza hanno bisogno di essere modellati imponendo dei vincoli sulle parti del sistema rilevanti per la sicurezza. In questa maniera è possibile risolvere la consistenza delle politiche di sicurezza come un problema di soddisfazione di vincoli. Inoltre, usando vincoli soft diventa possibile effettuare un'analisi quantitativa delle policy.
Un'analisi quantitativa fornisce una misura a grana fine di quanto sia sicuro un sistema, piuttosto che utilizzare una misura grossolana (vero/falso) fornita dai convenzionali vincoli 'crisp'.
Analisi Quantitativa di Protocolli di Sicurezza
-------------------------------------
I protocolli di sicurezza prescrivono la maniera in cui i soggetti remoti presenti su una rete di computer devono interagire per ottenere specifici obiettivi di sicurezza. Un obiettivo principale dei protocolli è la confidenzialità, che garantisce che un messaggio rimane incomprensibile a soggetti "maliziosi". Un altro obiettivo cruciale è l'autenticazione, che garantisce la partecipazione di un soggetto ad una sessione di protocollo. Questi obiettivi sono formalizzati con una semplice alternativa si/no nella letteratura esistente. In questa maniera è possibile solo affermare se una chiave è confidenziale oppure no, o se un soggetto si autentica con un altro oppure no.
D'altro canto, l'esperienza mostra che la sicurezza nel mondo reale è basata su livelli di sicurezza piuttosto che su garanzie categoriche e definitive di sicurezza. In particolare, i livelli di sicurezza caratterizzano gli obiettivi di confidenzialità e di autenticazione di un protocollo. In riferimento al primo di questi obiettivi, ricordiamo che messaggi diversi richiedono specifici livelli di protezione contro la divulgazione [21].
Ad esempio, una password di un utente richiede un livello di protezione maggiore di una chiave di sessione, che viene usata per una sola sessione di protocollo. Intuitivamente, una password dovrebbe essere "più confidenziale" di una chiave di sessione. Inoltre, un attacco alla confidenzialità basato su criptoanalisi online non dovrebbe essere imputato al design del protocollo. E' abbastanza sorprendente che gli obiettivi di confidenzialità e di autenticazione di un protocollo siano formalizzati con una semplice alternativa si/no nella letteratura esistente.
** Risultati Attesi: **
La motivazione della nostra ricerca è lo sviluppo di una nozione quantitativa degli obiettivi di sicurezza (confidenzialità, autenticazione, delega, ecc.). Ci proponiamo inoltre di estendere il nucleo esistente [3, 2], e di dimostrare la validità della nostra idea su protocolli largamente diffusi (come abbiamo fatto per Kerberos, ad esempio). In Kerberos, la nostra analisi preliminare del protocollo evidenzia il fatto che la perdita di una chiave di autorizzazione sarebbe più grave della perdita di una chiave di servizio, e che l'autenticazione del responder con l'initiator è più debole dell'autenticazione dell'initiator con il responder.
Il prossimo passo sarà la meccanizzazione del framework. Infatti, poiché abbiamo a che fare esclusivamente con quantità illimitate ma finite, il framework può essere automatizzato utilizzando il model checking.
Verifica di Protocolli di Sicurezza
------------------------------------------
Ci si propone di studiare i vantaggi e gli svantaggi derivanti dall'applicazione di tecniche basate sulla programmazione logica con vincoli all'analisi, la specifica, la verifica e l'attuazione di proprietà di sicurezza in sistemi multiagente.
Particolare attenzione sarà posta sulla specifica e sullo studio di politiche di autorizzazione in ambienti distribuiti attraverso l'uso dei vincoli.
** Risultati attesi: **
Ci si propone di ottenere risultati teorici e sperimentali riguardo l'uso della programmazione logica con vincoli come framework per la costruzione e la validazione di modelli di autorizzazione distribuiti in sistemi multiagente.
In particolare, concentreremo la nostra attenzione sui problemi che nascono dalla composizione e dall'interoperabilita' tra politiche di autorizzazione appartenenti ad organizzazioni diverse.
Completezza dei domini astratti per la verifica di protocolli di sicurezza
---------------------------------------
Un protocollo di sicurezza ([36]) è un metodo per trasmettere informazioni attraverso la rete. Il ruolo principale dei protocolli di sicurezza è di garantire l'autenticità e la segretezza della comunicazione.
Altre proprietà richieste possono riguardare il riconoscimento o l'integrità del sistema. I metodi comunemente utilizzati per analizzare le proprietà di sicurezza sono basati sul controllo del flusso di informazione. L'idea è di partizionare l'informazione in classi di sicurezza e di garantire che non vi siano flussi di informazione tra le varie classi. Questo problema viene tipicamente risolto fissando una logica particolare o un type system, oppure utilizzando tecniche di model checking basate sulla semantica operazionale.
** Risultati attesi: **
Noi vogliamo fornire delle tecniche formali per la progettazione sistematica di domini astratti orientati alle proprietà di sicurezza, e quindi di rendere applicabili le tecniche di trasformazione dei domini [32] all'analisi dei protocolli di comunicazione. Le tecniche di trasformazione dinamica del dominio di analisi giocano un ruolo chiave nel caso delle proprietà di sicurezza, dove non è sufficiente dimostrare che il sistema soddisfi una certa specifica (correttezza dell'analisi) bensì deve essere garantito che il protocollo resista agli attacchi. La novità introdotta è l'inferenza attiva dell'ambiente circostante, che rende necessario l'utilizzo di tecniche dinamiche di modifica dell'analisi, in accordo all'evoluzione dell'ambiente. Si intendono quindi definire ed implementare delle operazioni di trasformazione dei domini (raffinamenti e semplificatori) per la progettazione di analisi ottimali (con il migliore tradeoff tra la complessità computazionale e la precisione dell'analisi). Esempi di analisi ottimali basate su varie logiche sono gi state considerate in molte applicazioni dell'interpretazione astratta (vedi, ad esempio, [37, 38]).
La stessa idea può essere estesa all'analisi di sicurezza, sfruttando le strutture logiche alla base delle specifiche dei protocolli.
Metodologia di analisi uniforme
-------------------------------
Le metodologie utilizzate per analizzare i protocolli di sicurezza e le politiche di integrità sono differenti ma strettamente correlate. Da una parte c'à la nozione di "ambiente" dentro la quale la politica viene implementata, dall'altra c'è l'attaccante che mira a violare il protocollo. L'idea base da usare per integrare i due approcci è quella di considerare, in entrambi i framework, la nozione di "modello ideale" che rappresenta la corretta configurazione della politica e la corretta esecuzione del protocollo. Si tratterà poi di confrontare la poltica e la "implementazione" del protocollo con tale modello.
**** Risultati attesi ****
Abbiamo in mente di sviluppare un approccio uniforme allo studio degli attacchi ai protocolli di sicurezza e dei bug sulle politiche di integrità. Pensiamo anche di svuluppare una implementaione che sarà utile per controllare automaticamente protocolli e politiche rispetto a questa nuova nozione di sicurezza. Pensiamo di partire da una lista di protocolli di sicurezza e da un insieme di politiche, da utilizzare come test per la nostra teoria.
E` importante sottolineare che la metodologia proposta potrebbe riconoscere nuovi bug, e dare una misura a bug o attacchi già noti.
In particolare, le nozioni di "attack detection", "attack suspicion" e "attack retaliation" saranno studiate in dettaglio.
Analisi di rischi di sicurezza e tradeoff tra privacy ed efficienza
-------------------------------------------------------------------
Una importante nuova area di ricerca è collegata alla analisi di rischio di sicurezza. Pensiamo di usare i vincoli soft per rappresentare le attività che necessitano di protezione e le minacce che potrebbero causare dei danni.
L'uso di vincoli soft è necessario per rappresentare il "costo" associato a ogni specifica minaccia o attività. Inoltre, la probabilità delle varie minacce deve essere presa in considerazione. Una volta che il sistema è stato modellato, la nozione di tradeoff [15,10] potrebbe essere usata per modificare parzialmente la configurazione del sistema.
Un'altra preoccupazione è la privacy. Durante l'esecuzione, un agente potrebbe non voler rivelare troppa informazione. Pertanto, si viene a creare un tradeoff, potenzialmente importante, tra la tutela della privacy e il potenziamento dell'efficienza della ricerca. In questo lavoro, mostriamo come misure quantitative della perdita di privacy posso essere fatto all'interno del framework del soddisfacimento di vincoli distribuito.
***risultati attesi***
Vogliamo mostrare come gli agenti posso fare inferenze sui problemi o sottoproblemi di altri agenti a partire da comunicazioni che non trasportano nessuna informazione privata in maniera esplicita. Ciò può avvenite usando dei ragionamenti basati su vincoli, in un framework costituito da un CSP ordinario, che è noto solo parzialmente, e un sistema di CSP ombra che rappresentano varie forme di conoscenza probabilistica. Questo tipo di ragionamento, combinato con l'elaborazione della consistenza degli archi, può velocizzare la ricerca sotto condizioni di comunicazione limitata, allo stesso tempo compromettendo la tutela della privacy.
In alcuni casi, un piccola quantità di informazione privata è richiesta per migliorare l'efficienza della ricerca; con l'uso di euristiche più sofisticate, la ricerca può essere migliorata anche sotto condizioni di comunicazione minimale. Allo stesso tempo, questi metodi consentono, talvolta, di inferire informazioni nascoste, sollevando nuove problematiche riguardanti la privacy.
In quest'area pensiamo di intraprendere una notevole mole di lavoro. Vorremmo creare un modello per rappresentare sia informazione di sicurezza che aspetti economici (tipicamente il costo della minaccia e il costo delle patch o delle contromisure di sicurezza). In questo contesto, la teoria della probabilità e la teoria delle possibilità saranno usate per trattare il problema dell'incertezza.



