Validation 2002

Giornate di lavoro su validazione di sistemi informatici 

Venerdi 22 - Sabato 23 Novembre 2002

Dipartimento di Informatica e Scienze dell'Informazione dell'Universita' di Genova

• Program (lista provvisoria)
• Mailing list/participants (lista provvisoria)
• Lista Hotel (nota: blocco di camere prenotate fino all'8/11)
• How to Reach DISI

Program

• Friday 22: Morning Session
• Friday 22: Afternoon Session
• Saturday 23: Morning Session
• Saturday 23: Afternoon Session

• 9:15-10 Invited Tutorial: Algorithmic Verification of Infinite-state Systerms

Prof. Ahmed Bouajjani (Paris 7)
 
• 10-10:30 Symbolic Model Checking: Overview and Applications

Alessandro Cimatti
 
• 10:30-11 Testing and Model Checking (slides)

Alessandro Fantechi


• 11-11:30 Coffee break

 
• 12:30-13 Applicazioni di QBF a Verifica Formale

Enrico Giunchiglia


• 11:30-12 Automata-based Model Checking and Combined Automata

Angelo Montanari
 
• 12-12:30 Models and Efficient Data Structures for Verification of Infinite-state Systems

Jean-Francois Raskin


• 13-14:30 Lunch

• 14:30-15 Completeness in Abstract Interpretation and Abstract Model Checking

Roberto Giacobazzi
 
• 15-15:30 TBA

Riccardo Focardi


• 15:30-16 TB (Related paper)

Salvatore La Torre

• 16-16:30 Coffee break

 
• 16:30-17:45 On the Formalization and Comparison of Coordination Models and Languages (slides)
  

Gianluigi Zavattaro
 
• 17-17:30 Proof Theory for (timed) Concurrent Constraint Programming

Maurizio Gabbrielli
 
• 17:30-18 Abstract Model Checking and Strong Preservation

Francesco Ranzato
 
• 18-18:30 Domain Compression for Complete Abstractions and Abstract Model Checking

Isabella Mastroeni

• 9:30-10 An On-the-Fly Model-Checker for Security Protocol Analysis

Luca Viganò


• 10-10:30 Confidentiality Levels and Deliberate/indeliberate Protocol Attacks

Stefano Bistarelli
 
• 10:30-11 Availability of Protocol Goals

Giampaolo Bella
 
• 11-11:30 Coffee break

 
• 11:30-12 Symbolic Partial Model Checking

Fabio Martinelli
 
• 12-12:30  Constraint-based analysis of Security Protocols (slides)

Sandro Etalle
 
• 12:30-13 SAT-based Model-Checking of Security Protocols

Alessandro Armando e Luca Compagna
 
• 13-14:30 Lunch

Saturday 23: Afternoon Session
 

• 14:30-15 Model Checking for Mobile Systems and Security Protocols.

Gabriele Lenzini
 
• 15-15:30 Analisi statica del pi-calcolo e verifica di protocolli

Gilberto Filè e Alberto Griggio
 
 
• 16-16:30 Coffee break

 
• 16:30-17 Automatic verification of timed concurrent constraint programs

Moreno Falaschi and Alicia Villanueva
 
• 17-17:30 Feature Interaction

Claudio Castellini
 
• 17:30-18 BDD-Driven First-Order Satisfiability Procedures

Silvio Ranise

• Algorithmic Verification of Infinite-state Systerms - Prof. Ahmed Bouajjani (Paris 7)

We present different infinite-state models and the motivation behind the consideration of their verification problem.
These models can be classified into two (closely related) categories: extended automata and rewrite systems.
We overview the existing algorithmic techniques for tackling their verification problems, based on symbolic reachability analysis:
well-quasi orderings, acceleration techniques, transitive closures, and widening operators.

Slides (PDF)

 
• SAT-based Model-Checking of Security Protocols - Alessandro Armando e Luca Compagna

We provide a fully automatic translation from security protocol specifications into propositional logic which can be effectively
used to find attacks to protocols.  Our approach results from the combination of a reduction of protocol insecurity problems to planning
problems and well-known SAT-reduction techniques developed for  planning.  We also propose a set of transformations on
protocol insecurity problems whose application has a dramatic effect on the size of the propositional encoding obtained with our
SAT-compilation technique. We describe a model-checker for security protocols based on our
ideas and show that attacks to a set of well-known authentication protocols are quickly found by state-of-the-art SAT solvers.

Slides (PDF)
 
 
• Domain Compression for Complete abstractions - Isabella Mastroeni

We introduce the operation of domain compression for
complete refinements of finite abstract domains. This provides a
systematic method for simplifying abstract domains in order to isolate
the most abstract domain, when it exists, whose refinement toward
completeness for a given semantic function returns a given domain.
Domain compression is particularly relevant to compare abstractions in
static program analysis and abstract model checking. In this latter case
we consider domain compression in predicate abstraction of transition
systems.

Slides (PDF)

 
•  Proof Planning for Feature Interactions: a preliminary report - Claudio Castellini

In this talk I report on an initial success obtained in investigating the Feature Interaction problem (FI) via proof planning.
FIs arise as an unwanted/unexpected behaviour in large telephone networks and have recently attracted interest not only
from the Computer Science community but also from the industrial world. So far, FIs have been solved mainly via approximation
plus finite-state methods (model checking being the most popular); in our work we attack the problem via proof planning in
First-Order Linear Temporal Logic (FOLTL), therefore making use of no finite-state approximation or restricting assumption about
quantification. We have integrated the proof planner lambda-CLAM with an object-level FOLTL theorem prover called FTL,
and have so far re-discovered a feature interaction in a basic (but far from trivial) example.

Web Link

• An On-the-Fly Model-Checker for Security Protocol Analysis - Luca Viganó

I introduce the on-the-fly model-checker OFMC, a state-of-the-art tool for analyzing security protocols. For example, OFMC can find
attacks in a test-suite consisting of 36 well-known flawed protocols in less than a minute of total CPU time. OFMC owes its success to
the combination of two ideas. The first is the modeling of protocols using lazy data-types in a higher-order functional programming
language, which allows for the automated analysis of security properties using infinite-state model checking, where the model is
explicitly built, on-the-fly, in a demand-driven fashion. The second is the integration of several search optimizations that
significantly reduce the infinite search tree associated with a protocol without excluding any attacks.

The AVISPA Project home page

  
• Analisi statica del pi-calcolo e verifica di protocolli - Gilberto Filé e Alberto Griggio

Viene descritta un'analisi statica relativamente semplice del pi-calcolo.
Per dimostrare la sua correttezza viene introdotta una nuova visione della semantica del pi-calcolo in cui si esplicita la sostituzione
calcolata dalle regole  di comunicazione  e cioè CLOSE e COM.  Si presenta anche un'applicazione dell'analisi alla verifica di
proprietà di no-leak di protocolli espressi in pi-calcolo.
 
 
• Automatic verification of timed concurrent constraint programs - Moreno Falaschi and Alicia Villanueva

Reactive systems are essential for crucial industrial applications. In this paper we consider timed concurrent
constraint (tccp) languages which are suitable for specifying real time applications, such as embedded systems,
safety critical applications, communication protocols, etc.  tccp is a concurrent constraint declarative language that allows
the user to specify very intuitively reactive systems. The problem of formal verification of reactive systems is becoming
increasingly important. Model checking is a classical technique which allows to verify finite state systems with a huge number of
states in an automatic way. In this paper we propose an approach which exploits the computation model of tccp.
Constraint based computations allows us to define a methodology for applying a model checking algorithm to (a class of) infinite state systems.
We extend the classic algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to
the tccp Structure which we define in this work for modeling the program behaviour. We define a restriction on the time in
order to get a finite model and develop some illustrative examples.
 
• Availability of Protocol Goals - Giampaolo Bella

A new principle for prudent design of security protocols is developed to extend and complement the existing ones.
Called goal availability, the principle requires that a given protocol goal be confirmed by a formal guarantee that the
principals can invoke in practice. In consequence, the guarantees must be based on assumptions that the principals are
able to verify. Analysing known protocols in the light of the new principle highlights unknown features. For example, an
established BAN-logic claim is undermined, and some weaknesses of a modern smart card protocol are discovered. Our
findings support the general claim that checking a protocol against goal availability helps discover unspotted lacks of explicitness
in the protocol messages. The reported protocol analyses are all machine assisted, but goal availability
serves for protocol analysis in general.

Alessandro Armando (DIST Genova)
Giampaolo Bella (DMI Catania)
Stefano Bistarelli (CNR Pisa)
Ahmed Bouajjani (Paris 7)
Marco Bozzano (IRST Trento)
Claudio Castellini (DIST Genova)
Alessandro Cimatti (IRST Trento)
Luca Compagna (DIST Genova)
Mila Dalla Preda (Dip. Informatica Verona)
Pasquale De Lucia (DIST Genova)
Giorgio Delzanno (DISI Genova)
Sandro Etalle (U. Twente)
Moreno Falaschi (DIMI Udine)
Alessandro Fantechi (DSI Firenze)
Riccardo Focardi (DSI Venezia)
Maurizio Gabbrielli (Dip. Informatica Bologna)
Pierre Ganty (U. Bruxelles)
Alexandre Genon (U. Bruxelles)
Roberto Giacobazzi (Dip. Informatica Verona)
Enrico Giunchiglia (DIST Genova)
Alberto Griggio (UNIPD)
Salvatore La Torre (Un. Salerno)
Gabriele Lenzini (IEI CNR)
Marco Maratea (DIST Genova)
Maurizio Martelli (DISI Genova)
Fabio Martinelli (CNR Pisa)
Fabio Massacci (DIT Trento)
Isabella Mastroeni (Dip. Informatica Verona)
Angelo Montanari ((DIMI Udine)
Massimo Narizzano (DIST Genova)
Marco Pistore (DIT Trento)
Alberto Policriti (DIMI Udine)
Silvio Ranise (INRIA)
Francesco Ranzato (UNIPD)
Jean-Francois Raskin (U. Bruxelles)
Giuseppe Rosolini (DISI Genova)
Roberto Segala (Dip. Informatica Verona)
Alan Smaill (University of Edinburgh)
Armando Tacchella (DIST Genova)
Luca Viganò (Institut für Informatik U. Friburgo)
Alicia Villanueva (DIMI Udine)
Gianluigi Zavattaro (Dip. Informatica Bologna)

Un primo blocco di 15 camere e' stato bloccato fino all'8 Novembre presso

Hotel Sauli
Viale Sauli,5 I - 16121 Genova
email: htl.sauli@mclink.it
Tel.:+39 010 561397 Fax + 39 010 590092
 

L'Hotel Sauli e' convenzionato con l'Universita' di Genova. Il prezzo di una singola e' 62 Euro (colazione inclusa).
Inoltre e' a due passi dalla Stazione Brignole e dal centro di Genova.
Il DISI e' facilmente raggiungibile in autobus (piu breve tratto a piedi) in 15/20 minuti.
Vedi istruzioni dettagliate per raggiungere il dipartimento (treno/bus/aereo/macchina).

Altri hotel convezionati (menzionare DISI/Universita' di Genova):

Hotel Astoria
Piazza Brignole, 4
(phone +39 010 873316, fax +39 8317326)
email: info@hotelastoria-ge.com
http://www.hotelastoria-ge.com/
Prezzo singola: 68 euro, 110 con breakfast

Le tariffe seguenti si intendono per camera e colazione a buffet (IVA inclusa)

Hotel Britannia
Via Balbi 38
tel.010/26991 fax 010/2462942
e-mail:britannia@britannia.it
camera singola BASIC Euro 74 camera singola SUPERIOR Euro 84
camera doppia BASIC Euro 104 camera doppia SUPERIOR Euro 114

Hotel Moderno Verdi
P.zza G.Verdi 5
tel.010/5532104 fax 010/581562
e-mail:info@modernoverdi.it
camera singola Euro 90 camera doppia Euro 130 Junior suite (per una o due persone) Euro 155

Hotel Metropoli
P.zza Fontane Marose
tel.010/2468888 fax 010/2468686
e-mail:metropoli.ge@bestwestern.it
camera singola Euro 72 camera doppia uso singola Euro 85 camera doppia Euro 108