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
INIZIO_TESTO_DA_INDICIZZARE

PROGRAMMA DI RICERCA 2004

italiano - english
Unità di Ricerca
Programmi di ricerca simili:
Classificazione scientifico-disciplinare
Classificazione brevettuale
  • PHYSICS
    • CHECKING-DEVICES
      • TIME OR ATTENDANCE REGISTERS; REGISTERING OR INDICATING THE WORKING OF MACHINES; GENERATING RANDOM NUMBERS; VOTING OR LOTTERY APPARATUS; ARRANGEMENTS, SYSTEMS OR APPARATUS FOR CHECKING NOT PROVIDED FOR ELSEWHERE (finger printing A61B5/103; indicating or recording apparatus for measuring in general, analogous apparatus but in which the input is not a variable to be measured, e.g. a hand operation, G01D; clocks, clock mechanisms G04B, G04C; time-interval measuring G04F; counting mechanisms per se G06M)
    • COMPUTING; CALCULATING; COUNTING (score computers for games A63; combinations of writing applicances with computing devices B43K29/08)
      • COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS [N0004]
    • MEASURING (counting G06M); TESTING
      • MEASURING ELECTRIC VARIABLES; MEASURING MAGNETIC VARIABLES (measuring physical variables of any kind by conversion into electric variables, see Note (4) following the title of class G01; measuring diffusion of ions in an electric field, e.g. electrophoresis, electro-osmosis G01N; investigating non-electric or non-magnetic properties of materials by using electric or magnetic methods G01N; indicating correct tuning of resonant circuits H03J3/12; monitoring electronic pulse counters H03K21/40; monitoring operation of communication systems H04)
Classificazione geografica
Bibliografia
[AB02] M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. ACM POPL 2002, pp 33-44, 2002.

[ACB+01] R. Alur, C. Belta, F. Ivancic, V. Kumar, M. Mintz, G.J. Pappas, H. Rubin, J. Schug. Hybrid Modeling and Simulation of Biomolecular Networks. Proceedings of 4th Int Workshop Hybrid Systems: Computation and Control, 18-32, 2001.

[ACH+95] R. Alur, C. Courcobetis, N. Halbwachs, T.A. Henzinger, P.H. Ho, X. Nicollin, A. Oliviero, J. Sifakis, S. Yovine. The algorithmic Analysis of Hybrid systems. TCS, 138(1):3-34, 1995.

[BHRZ03] R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. SAS'03, LNCS 2694, 2003.

[BHZ02] R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. TCS 277(1-2):3-46, 2002.

[BHZ03] R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. VMCAI 2004, LNCS 2937, 2003.

[BRZH02] R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. SAS'02, LNCS 2477, 2002.

[BPR02] T. Ball, A. Podelski and S. K. Rajamani. Relative Completeness of Abstraction Refinement for Software Model Checking. TACAS02, LNCS 2280 158-172, 2002.

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

[CGL94] E. Clarke, O. Grumberg, D. Long. Model Checking and Abstraction. ACM TOPLAS 16(5):1512-1542, 1994.

[CGP99] E.M. Clarke, O. Grumberg, D.A. Peled. Model Checking. MIT Press, 1999.

[CFGPR97] A. Cortesi, G. File', R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. ACM TOPLAS 19(1):7-47, 1997.

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

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

[CC94] P. Cousot and R. Cousot. Higher-order abstract interpretation. IEEE ICCL'94, 95-112. 1994.

[CC99] P. Cousot. The Calculational Design of a Generic Abstract Interpreter. NATO ASI Series. 1999.

[CC00] P. Cousot, R. Cousot. Temporal abstract interpretation. ACM POPL, pp. 12-25, 2000.

[CC02] P. Cousot, R. Cousot. On abstraction in software verification. CAV'02, LNCS 2404, 37-56, 2002.

[CH78] P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. ACM POPL 1978.

[DGG97] D. Dams, R. Gerth, O. Grumberg. Abstract Interpretation of Reactive Systems. ACM TOPLAS 19(2):253-291, 1997.

[DL93] S. Debray and N.-W. Lin. Cost analysis of logic programs. ACM Transactions on Programming Languages and Systems, 15(5):826-875, 1993.

[Del03] G. Delzanno. Constraint-Based Verification of Parameterized Cache Coherence Protocols. Formal Methods in System Design 23(3): 257-301 (2003)

[DRV02] G. Delzanno, J.F. Raskin, L. Van Begin. Towards the Automated Verification of Multithreaded Java Programs. TACAS 2002: 173-187

[DW00a] A. Di Pierro, H. Wiklicky. Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation. ACM PPDP'00, 2000, 127-138.

[DW00b] A. Di Pierro, H. Wiklicky. Measuring the Precision of Abstract Interpretations. LOPSTR'00, LNCS 2042, 2001. 147-164.

[FGR96] G. File', R. Giacobazzi, and F. Ranzato. A unifying view on abstract domain design. ACM Computing Surveys, 28(2), 1996.

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

[FGM00] R. Focardi, R. Gorrieri, and F. Martinelli. Non Interference for the Analysis of Cryptographic Protocols. ICALP'00, LNCS 1853, 2000.

[GM04] R. Giacobazzi and I. Mastroeni. Abstract Non-Interference. ACM POPL'04, 186-197. 2004.

[GQ01] R. Giacobazzi and E. Quintarelli. Incompleteness, counterexamples and refinements in abstract model-checking. SAS'01, LNCS 2126, 2001.

[GR97] R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. ICALP'97, LNCS 1256, 771-781. 1997.

[GR98unif] R. Giacobazzi and F. Ranzato. Uniform closures: order-theoretically reconstructing logic program semantics and abstract domain refinements. Inform. and Comput. 145(2):153-190, 1998.

[GR02] R. Giacobazzi, F. Ranzato. States vs. traces in model checking. SAS'02, LNCS 2477, pp. 461-476, 2002.

[GRS00] R. Giacobazzi and F. Ranzato and F. Scozzari. Making abstract interpretations complete. J. of the ACM. 47(2):361-416, 2000.

[GS98] R. Giacobazzi and F. Scozzari. A logical model for relational abstract domains. ACM TOPLAS 20(5):1067-1109, 1998.

[GM82] J. A. Goguen and J. Meseguer. Security Policies and Security Models. IEEE Symposium on Security and Privacy (SSP'82), 11-20, 1982.

[GLM03] R. Gorrieri, E. Locatelli, and F. Martinelli. A simple language for real-time cryptographic protocol analysis. ESOP'03, LNCS 2618, pp. 114-128. Springer-Verlag, 2003.

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

[HM00] T. Henzinger, R. Majumdar. A classification of symbolic transition systems. STACS 00, 13-34, 2000.

[J92] T.P. Jensen. Disjunctive strictness analysis. IEEE LICS'92, 174-185. 1992.

[JN95] N.D. Jones, F. Nielson. Abstract Interpretation: A Semantic-Based Tool for Program Analysis. Handbook of LICS, Oxford, 1995.

[LM04] F. Levi, S. Maffeis. On Abstract Interpretation of Mobile Ambients. Information and Computation, 188, 2004, 179-240.

[LS03] F. Levi, D. Sangiorgi. Mobile Safe Ambients. TOPLAS, 25(1), 2003, 1-69.

[LGSBB95] C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1-36, 1995.

[Low02] G. Lowe. Quantifying information flow. IEEE Computer Security Foundations Workshop, pp.18-31, 2002.

[LSV03] N. Lynch, R. Segala, F. Vaandrager. Hybrid I/O Automata. Information and Computation, 185:105-157, 2003.

[MMP92] O. Maler, Z. Manna, and A. Pnueli. From Timed to Hybrid Systems. REX Workshop ``Real-Time: Theory in Practice'', LNCS 600, 447-484. 1992.

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

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

[Min01] A. Miné. The octagon abstract domain. 8th Working Conference on Reverse Engineering WCRE'01, 310-319, 2001. IEEE.

[M00] D. Monniaux. Abstract Interpretation of Probabilistic Semantics. Proceedings of SAS'00, LNCS 1824, 2000, 322-339.

[M01] D. Monniaux. An abstract Monte-Carlo method for the analysis of probabilistic programs. ACM-POPL 2001, pp. 93-101, 2001.

[NN02] H.R. Nielson and F. Nielson. Flow logic: a multi-paradigmatic approach to static analysis. The essence of computation: complexity, analysis, transformation. Springer. 2002.

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

[Ran02] F. Ranzato. On the completeness of model checking. ESOP'01, LNCS 2028, pp. 137-154, 2001.

[RT04] F. Ranzato,F. Tapparo. Strong preservation as completeness in abstract interpretation. ESOP'04, LNCS 2986, pp. 18-32, 2004.

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

[SM03] A. Sabelfeld and A.C. Myers. Language-based information-flow security. IEEE J. on selected ares in communications. 21(1):5-19, 2003.

[VS00] D. Volpano and G. Smith. Verifying secrets and relative secrecy. ACM POPL 2000 pp. 268-276, 2000.

[ZHB02] E. Zaffanella, P. M. Hill, and R. Bagnara. Decomposing non-redundant sharing by complementation. Theory and Practice of Logic Programming, 2(2):233-261, 2002.
Parole Chiave
INTERPRETAZIONE ASTRATTA; ANALISI STATICA DI PROGRAMMI; DOMINI ASTRATTI; SEMANTICA; VERIFICA DI PROGRAMMI

AIDA - Interpretazione Astratta: Progettazione e Applicazioni

Università degli Studi di Verona
Abstract
L'interpretazione astratta e' una teoria generale per l'approssimazione di sistemi dinamici, ampiamente utilizzata ad esempio per derivare formalmente strumenti di analisi statica e verifica di programmi a partire dalla loro semantica. In AIDA, l'interpretazione astratta e' vista come teoria fondamentale ed unificante per la progettazione di metodologie e lo sviluppo di strumenti per assicurare l'interoperabilita', la composizionalita', l'affidabilita', la robustezza, e la sicurezza di sistemi software. L'obiettivo iniziale del progetto AIDA e' di mobilitare, unificare, galvanizzare e rafforzare la comunita' italiana dell'interpretazione astratta attraverso un obiettivo comune che consiste nella realizzazione di un'unica piattaforma avanzata per la certificazione di sistemi attraverso interpretazione astratta. Siamo particolarmente interessati alla certificazione di flussi sicuri di informazione, robustezza e affidabilita' di sistemi complessi che coinvolgono componenti software e che hanno un potenziale comportamento ibrido. Affronteremo questo problema raffinando gli esistenti metodi propri dell'interpretazione astratta nell'ambito dell'analisi statica di programmi e nella sicurezza, integrandole con descrizioni basate sui vincoli di sistemi dal numero infinito di stati e metodi di verifica come il model checking. Il risultato verra' ottenuto individuando un modello comune per la progettazione dell'interpretazione astratta nell'analisi statica do programmi, nella >>>

Coordinatore Scientifico del Programma di Ricerca
Roberto GIACOBAZZI Università degli Studi di VERONA
Obiettivo del Programma di Ricerca
Garantire l'affidabilita' e la sicurezza dei sistemi informatici e' una sfida fondamentale per le societa' moderne. Ci affidiamo a sistemi che pervadono la vita dell'uomo e sono sempre piu' complessi; nello stesso tempo sperimentiamo, talvolta in modo spettacolare, come i metodi tradizionali di validazione, ad esempio il testing, possano fallire, nonostante il loro costo elevato, nel compito di assicurare le garanzie richieste: il fallimento di Ariane 5 nel giugno 1996 e' un esempio famoso. Questo giustifica l'interesse crescente per tecnologie flessibili e basate sulla semantica per l'analisi, la verifica e la manipolazione di programmi in ogni fase dello sviluppo dei sistemi SW. L'interpretazione astratta puo' giocare un ruolo importante in questa prospettiva. In AIDA l'interpretazione astratta verra' utilizzata come la teoria fondamentale per definire metodologie e per sviluppare strumenti che assicurino interoperabilita', composizionalita', scalabilita', affidabilita', robustezza e sicurezza del software e dei sistemi. Lo scopo iniziale del progetto AIDA e' di mobilitare, unificare, galvanizzare e rinforzare la comunita' italiana di interpretazione astratta verso un obiettivo comune: la creazione di un'unica piattaforma per la certificazione automatica tramite interpretazione astratta. L'Italia ha una comunita' attiva da tempo nell'interpretazione astratta, come e' provato dal AIDA che comprende 7 universita', piu' di 25 ricercatori permanenti coinvolti direttamente >>>

Risultati parziali attesi
I risultati attesi in questa fase sono:
- Una ben definita algebra dei trasformatori di domini astratti, che includa le proprieta' rilevanti delle astrazioni codificate come trasformatori di domini astratti, come preservazione forte nel model checking astratto di sistemi discreti e ibridi riguardo a frammenti della logica temporale, assenza di falsi allarmi in domini astratti numerici e relazionali, e composizionalita' per il test di regressione (tutti i WP)
- Condizioni precise per l'invertibilita' di domini astratti e relativi algoritmi per invertire raffinamenti di domini astratti nel senso della compressione di domini, ovvero verso un'operazione che restituisce, quando esiste, il piu' astratto dominio che ha lo stesso raffinamento del dominio in input (WP1, WP4 e WP6)
- Estensione dell'algebra dei trasformatori di domini a strategie di punto fisso, come tecniche di widening/narrowing (WP1, WP4, e WP5)
- Una caratterizzazione delle proprieta' dei sistemi ibridi come proprieta' delle loro astrazioni (WP4)
- Una tassonomia di astrazioni nel model checking astratto sotto il requisito della preservazione forte relativamente al frammento del mu-calcolo (WP6).I risultati attesi da questa fase sono:
- Miglioramento dei domini per l'analisi attribute-independent di programmi su domini numerici (WP1)
- Miglioramento dei domini per l'analisi relazionale di programmi su domini numerici (WP1 e WP5)
- Il progetto di domini >>>

Durata
24 mesi
Base di partenza scientifica nazionale o internazionale
L'interpretazione astratta e' una nota teoria per approssimare la semantica di sistemi dinamici [CC77]. Introdotta dai Cousot [CC77] come teoria adeguata sia al progetto che alla dimostrazione di correttezza di analizzatori statici di programmi, negli ultimi anni l'interpretazione astratta e' diventata molto diffusa come tecnica generale per la descrizione e la formalizzazione di computazioni astratte in diverse aree dell'informatica. In AIDA siamo interessati allo sviluppo di metodi che siano comuni alle diverse applicazioni dell'interpretazione astratta dall'analisi statica di programmi, alla sicurezza, alla verifica e al testing per sistemi discreti/ibridi.

- Progetto di domini astratti e loro applicazioni
Il successo dell'interpretazione astratta e' dato dalla semplice, ma rigorosamente definita, idea per cui la specifica del comportamento di un sistema, ad esempio un programma, a diversi livelli di astrazione, e' data da una opportuna astrazione della sua semantica formale [C76th,CC777,JN95,NNH99]. In questo progetto siamo interessati nell'uso dell'idea che sta alla base dell'interpretazione astratta, ovvero l'analisi di sistemi attraverso l'approssimazione della loro semantica, come paradigma concreto e adeguato sia per il progetto che per per la specifica di nuovi metodi di certificazione sia per componenti SW che per sistemi dinamici ibridi. Una caratteristica fondamentale dell'interpretazione astratta e' che gran parte delle proprieta >>>