---

T1 - Constraint Solving as Verification Procedure
This activity is part of the subtask 2.2 "Innovative Use of Existing
Constraint Systems" of CoVer.

Verification problems are directly represented as `satisfiability'
problems in a given constraint language which are then checked
directly by a constraint solver. This approach requires a preliminary
(possibly automated) analysis to express the system property to be
checked in terms of the constraint language accepted by the solver.
This may require the use of abstract interpretation techniques and
therefore a tight integration with Task 3, "Abstract Interpretation",
is envisaged here. In this context we will investigate the use of
solvers for a variety of domains that are ubiquitous in computer science:
SAT solvers, specialized solvers for Integer Linear Programming,
satisfiability procedures for the quantifier-free theory of equality
with uninterpreted function symbols, for the theory of lists, and for
the theory of arrays with/without extensionality.

Obj 1 - "SAT-based Bounded Model-Checking"

We will investigate the use of SAT solvers for checking safety
properties of communication protocols. The key idea of the approach
is to reduce the (bounded) reachability problem (i.e. reachability in
k steps) to a propositional satifiability problem which can then be
checked by a state-of-the SAT solver. The translation to
propositional logic must be effective and 'constructive' at the same
time. By 'effective' we mean that the resulting proposional formula
must be of a tractable size (both in number of proposional variables
and clauses) so to be solved in a reasonable amount of time and
resources by state-of-the-art SAT solvers. By 'constructive' we mean
that from any model of the resulting propositional formula it must be
always possible to reconstruct an execution trace witnessing the
reachability. Preliminary experiments have given interesting results
on security protocols [A+02]. Further work is necessary to obtain
compact protocol encodings (e.g. by exploiting invariants) and to
broaden the applicability of the approach to a wider class of
communication protocols.

Obj 2 - "IP-based Static Analysis of Parametric Concurrent Systems"
We will investigate the applicability of modern integer programming
techniques for the static analysis of concurrent systems and
communication protocols.

Linear Integer Programming techniques find a natural application to
the static analysis of parameterized concurrent systems and
communication protocol. In fact, their properties can often be
formulated in terms of combinatorial problems derived by the
description of the original system in terms of Petri Nets-like models.
Based on this property, integer programming techniques or, via a
relaxation, linear programming methods like the symplex can be applied
dirtectly to establish a given system property. Standard linear
programming techniques cannot be applied, however, to extensions of
Petri Net like models (e.g. with richer communication mechanisms), or,
to large protocol description. Our goal here is to investigate the
applicability of modern integer programming techniques like heuristics
based on cutting-planes for the static analysis of large protocols and
concurrent systems, and to investigate new classes of systems that can
be verified efficiently via static methods.

Obj 3 - "Constraint Solving for the Verification of Complex Hardware Circuits"

In some important application areas (e.g. hardware verification),
model checking can be done by verifying whether any given
implementation of the system at hand enjoys some behavioral
specification. For instance, in [BD94] both the behavioral
specification of the ALU and its three-stage pipeline implementation
are described by means of transition functions which are compactly
described by nested if-then-else expressions (ite's for short) whose
atomic formulae are constraints in the combination of the theory of
arrays and theory of equality with uninterpreted function symbols. As
a result, the formula expressing the fact that the implementation
satisfies the specification consists of an equality between ite's
which can be readily checked by a solver resulting from the
combination of a SAT solver, a satisfiability procedure for the theory
of arrays, and a satificability procedure for the quantifier-free
theory of equality with uninterpreted function symbols. The research
unit will work at the design and development of satifiability
procedures for these theories as well as to their combination,
following the methodology described in [ARR01,ARR02]. The
combination of SAT solvers with constraints solvers is particularly
promising as there is already evidence that it can lead to the
construction of very efficient solvers out of simpler ones
[ACG99,ACGGT02].

T2 - Constraint-based Model Checking
This activity is part both of the subtask 2.1 "Specialized Constraint
Solvers for Verification" and 2.2 "Innovative Use of Existing
Constraint Solvers"

An alternative way constraint programming can be used for the purpose
of automated verification is based on the so-called Constraint-based
Model Checking paradigm. In this approach the standard model checking
technology based on OBDDs (a symbolic representation of Boolean
formulas) is replaced by model checking algorithms based on constraint
solvers for heterogeneous data structure. Differently from a direct
use of constraint solving, in this setting constraints are viewed as a
symbolic representation of possiblty infinite sets of system
configurations; constraint solvers are used then at every step of a
fixpoint computation to simplify intermediate results. As an example,
this method can be used to study reachability problems for reactive
systems consisting of a collection of clocks and properties
represented via linear inequalities describing conditions on the
clocks. A property is established only at the end of the fixpoint
computation. The main problem of this approach is the so-called
symbolic state explosion, due to the possible huge size of the
constraints that are computed in the intermediate steps.

Obj 4: Data Structures for Constraint-based Model Checking

Our objective here is the definition of decision diagrams-like
representations of numerical constraints (e.g. intervals, linear
inequalities) that can be embedded into symbolic model checking
algorithms. Our starting points are the graph-based data structures
used to represent difference constraints (DDDs) and upward-closed sets
of tuples (CSTs). The goal here is to enlarge the class of arithmetic
constraints that can be represented efficiently using graph-based data
structures, and to investigate the combination of this data
structures with other constraint systems used in verification like
OBDDs and SAT (see e.g. [McM02]).
Furthermore, since static analysis can be used to
improve the efficiency of symbolic model checking algorithms (see
[DRV01,DRV02]), we will also study the combination of the techniques
developed in this subtasks with the techniques studied in the substask (T1).

Interaction with the other tasks
The selection of the case studies and the design of the adequate
constraint systems for their analysis will be carried over in strict
collaboration with the units involved in the Task 2 and 3 of CoVer.
As a starting point, we plan to isolate specification formalisms
(possibly involving type annotations) general enough to model in a
natural way the different kinds of examples that have been analyzed
via constraint-based technology in the last years like the
parameterized systems studied in [BD02,Del00,DB01] and the systems
with unbounded data studied in [DP99].

The activity of the unit is also strictly related to the activity of
the task 3 devoted to the investigation of abstract interpretation.
As witnessed by several case studies [BD02,Del00,DB01], it is often
necessary to apply abstractions (either at the level of system
description or during the analysis) in order for constraint-based
technology to be effective in practice. The theory of abstract
interpretation provides a set of techniques to
systematically design and apply abstractions. Recent developments
have also shown the advantages of using this theory in combination
with model checking [GQ01,Ran01].
Thus, in collaboration with the units involved in task 3, we plan in
fact to investigate the possible extension of the constraint-based
symbolic model checking paradigm towards abstract model checking with
refinement.

Obj 5: Final results and interaction with Task 5
As results of this research we expect to obtain a set of tools that
will allow us to perform an experimental combination and evaluation of
these techniques on the practical cases selected in the course of the
project (the selection of the case studies will be carried over as a
specific task of CoVer). We also plan to embed the resulting
protoptypes on a software platform we will develop for the integration
of the different technologies developed in the scope of CoVer.

The technology underlying constraint-based symbolic model checking is
still at a very preliminary development stage. Most of the existing constraint-based verification tools make use, in fact, of `services' provided by general purpose constraint solvers. For instance, Polka [HPR94] and HyTech [HHW97], two infinite-state
model checkers for hybrid systems, are based on a polyhedra library developed by Halbwachs for the static analysis of sequential programs [CH78]. The infinite-state model checker of Bultan, Gerber and Pugh [BGP99] is based instead on the Omega library, a constraint solver for integer linear arithmetic (Presburger arithmetics). Recently, Bultan
extended his tool with composite constraints, i.e., constraints that
combine boolean and Presburger formulas [Bul00,DB01,YTB01].
Finally, McMillan is currently experimenting the use of SAT as an engine for
symbolic model checking [McM02].

Unfortunately, as experimentally proved in [DR00,DRV01], such a loose
integration of model checking and of constraint programming suffers
from the `symbolic state explosion' problem when applied to large specifications. In the approaches inspired to BDDs-like data structures for Symbolic Model Checking this problem has been considered only in very specific domains by introducing dedicated data
structures to compactly represent (subclasses of) arithmetic
constraints.
The more recent data structures proposed in this field are:

• DDDs [MLAH99], a graph-based representation of difference-constraints (used in timed-automata) that improves the matrix-based representations of the clock regions used in the analysis of time stystems [AD94].
•  CSTs [DR00], a representation of upward-closed sets of Petri Nets markings via special graphs called sharing trees;
• NDDs [WB00] an automata-based package for handling Presburger arithmetics.
  

A comparison between the performance of tools based on these data
structures has not been done, yet. Furthermore, a lot of work remain
to be done in order to extend these structures to larger fragments of
numerical constraints, and to find general purpose heuristics that
could be use to make feasible the verification of large classes of
practical examples.

Applications of Constraint-based Verification

In recent years there have been several application of
constraint-based verification techniques to verification of protocols
and, more in general, of reactive systems. Specifically, we can
isolate two classes of applications: verification of systems with a
finite number of components but unbounded data paths, and verification
of systems with a finite but non fixed a priori number of components
(parameterized verification).

Within the first class, in [BGP99,DP99] mutual-exclusion algorithms
(e.g. Bakery and Ticket) have been automatically verified using the
Omega library and using CLP(R). Other examples are the verification of
the Fisher protocol, and of the Bounded Retransmission Protocol
[HHW97,LPY97], and of the Alternating Bit Protocol [ACJT96] (the
latter carried over using a symbolic domain based on strings over
finite alphabets).

Within the second class of applications, there have been several
efforts for automated verification of safety properties of Unbounded
Petri Nets [ACJT96,DRV01,FS01], Unbounded Timed Petri Nets with aged tokens
[AJ99], verification of safaety properties for skeletons of concurrent programs
[BD02], and verification of safety properties of consistency and coherence
protocols for multiprocessor systems for any number of processors
[Del00,Del00b,DB01], and verification of abstractions of multithreaded
Java programs [DRV02].
Interestingly, in several applications constraint-based techniques are
combined with abstractions defined either over the system model (as in
[Del00,DB01,DRV02]) or over the constraint representation of the
system states (as in [BD02]). The study of systematic methods to
design and apply abtraction is thus a fundamental tool for making
model checking useful in practice.

Verification as Constraint Satisfiability

There has been a dramatic speed-up for SAT procedures in the last
decade: since 1991 the problems solvable by SAT solvers have grown
from 100 to 10,000 variables. Moreover, in the last few years, a
variety of new algorithms, techniques, and heuristics improving on
previous state-of-the-art SAT technology have been put forward. On
the basis of these results, researchers from various communities have
started encoding real-world problems into SAT. The results have been
success stories. In the last decade there has been a dramatic speed-up
of SAT solvers: problems with thousands of variables are now solved
routinely in milliseconds. This has lead to breakthroughs in planning
and model-checking of hardware circuits. In particular SAT-based
Bounded Model Checking [BCCZ99] has been proposed as a complementary
approach to Model Checking based on OBDDs. Experimental results
clearly indicate that SAT-based Bounded Model Checkers can
significantly outperform OBDD-based Model Checkers in the verification
of hardware circuits.

There are several others interesting approaches to formulate a
verification problem as a single constraint solving problem and to
establish a property by invoking the corresponding solver. As an
example, this is the approched followed in the so called static
analysis of protocols modeled via Petri Net like models [STC98]. In
this setting the transition system and interesting classes of safety
properties (e.g. mutual exclusion) can be expressed via a system of
inequalities defined over integer values [EM97,EM00]. The encoding is
defined in such a way that the emptyness of the set of solutions
implies the validity of the property. The last problem can thus be
attacked by integer linear programming, or, via a relaxation from
integer to reals, by linear programming [EM00]. This kind of static
analysis can also be useful to compute information (e.g.
overapproximations of the reachabilty set of a protocol) to be used in
symbolic model checking (e.g. to prune the search space as suggested
in [DRV01,DRV02]).

Central to the success of the constraint-based approach to
verification are the development of solvers for the decidable
fragments of interest, their combination, and their extension to wider
fragments. While the development of solvers is generally carried out
in an ad hoc fashion (with proofs of correctness based on difficult
model-theoretic arguments), a uniform approach to the synthesis of
decision procedures in given in [ARR01,ARR02] which is based on
considerably simpler proof-theoretic arguments. The problem of
satisfiability procedures out of simpler ones is a long standing
problem in automated reasoning for which two solutions are available
due to Nelson and Oppen [NO78] and to Shostak [Sh84].
[AR01] presents an approach to extending a decision procedure for Presburger
Arithmetics to deal with non-linear constraints, thereby enlarging the
reange of applicability.

References

---

Relazione Primo Anno Progetto

Obj 1 - "Bounded Symbolic Model-Checking basato su SAT"

In [ACG03,AC03] e' stata studiata l'applicazione di SAT bounded model checking e di euristiche basate su tecniche di planning al debugging di protocolli crittografici. La tecnica proposta risulta essere molto efficace per il debugging di tali protocolli.

Obj 2 - "Analisi Statica di Sistemi Concorrenti Parametrici basata su IP"

In [DRV03] abbiamo studiato la combinazione della teoria strutturale delle reti di Petri (basata su Integer Programming) con le strutture dati CST (usate per rappresentare constraint lineari e analizzare in modo simbolico lo spazio degli stati di una rete di Petri).

Obj 5: "Strutture Dati Efficienti per Constraint-based Model Checking"

In [AD03,DG04] sono state definite delle nuove strutture dati (basate su una combinazione di vincoli lineari e formule del I ordine) per la verifica della correttezza di protocolli crittografici (vedi survey [DG03]). In [Del03] e' stata studiata l'applicazione di tali strutture dati all'analisi di specifiche di programmi concorrenti date in pi-calcolo (estendendo un lavoro del Prof. Amadio di Marsiglia).

Task 2.3: "Soft Constraints for verification"

In [BF03a,BF03b] proponiamo una tecnica quantitativa e scalabile che usa constraint solving per modellare e analizzare l'efficacita' di una policy di sicurezza e della sua applicazione.

In [BFO04,BFO03] consideriamo come i vincoli soft possano fornire un aiuto nell'individuare "cascade vulnerability" in una rete. Alcune volte, infatti le interconnessioni tra sistemi e le loro comunicazioni possono portare a connessioni non previste e ad incrementare il rischio di violazione della sicurezza multilivello dei sistemi in rete.

Task 1.3 "Integrazione di paradigmi diversi"

In [BCLM03a,BCLM03b] abbiamo studiato la relazione tra due frameworks di verifica: il multiset rewriting (MSR) e le process algebra (PA) ispirate al ccs e al Pi-calcolo. In [AMMR03,JMMS03,MMS03,MM03] abbiamo studiato l'integrazione di diversi linguaggi logici (alcuni che supportano vincoli tipo CLP) per la specifica e, in prospettiva, la validazione di sistemi multiagente).

OBIETTIVI II ANNO

Nel secondo anno di attivita' la nostra unita' si propone di:

NuovoObj1 -SAT-

Estendere l'uso di SAT ad altri domini applicativi quali la verifica di protocolli utilizzati su internet e programmi multithreaded

NuovoObj2 -Strutture Dati-

Studiare l'applicazione dei CST e delle strutture dati basate su logica del I ordine e vincoli al'analisi di protocolli per internet e programmi multithreaded.

NuovoObj3 -Integrazione linguaggi e tecniche e loro applicazione-

Studiare l'integrazione delle tecniche e dei linguaggi sviluppate all'interno dell'unita' (SAT, CST, ecc). Studiare la combinazione con strumenti di interpretazione astratta sviluppati in altri task del progetto CoVer. Estendere l'applicabilita delle tecniche risultanti a nuovi domini applicativi (ad es. sistemi ad agenti)

---

Publications and Technical Reports

[AC03] A. Armando and L. Compagna. "Abstraction-driven SAT-based Analysis of Security Protocols".` Proc. of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), May 5-8 2003, S.Margherita Ligure, Italy. LNCS 2919.

[AMMR03] E. Astesiano, M. Martelli, V. Mascardi and G. Reggio From Requirement Specification to Prototype Execution: a Combination of a Multiview Use-Case Driven Method and Agent-Oriented Techniques In Proceedings of the Fifteenth International Conference on Software Engineering and Knowledge Engineering (SEKE), San Francisco, 2003. [ACG03] Alessandro Armando, Luca Compagna, Pierre Ganty. SAT-based Model Checking of Security Protocols using Planning Graph Analysis Proc. FME 2003 International Symposium of Formal Methods Europe. LNCS 2805. Pisa, Italy, September 2003. Also accepted at MoChArt, Workshop on Model Checking and Artificial Intelligence, Acapulco, Mexico, 2003.

[AD03] Pierluigi Ammirati, Giorgio Delzanno Constraint-based Automatic Verification of Time Dependent Security Properties. Proc. of SPV 2003, a Satellite workshop of Concur 03.

BFO04] S. Bistarelli, S.N.Foley, B. O'Sullivan, Modelling and Detecting the Cascade Vulnerabiliy Problem using Soft Constraints, in Proc. ACM Symposium on Applied Computing (SAC 2004), Cyprus. ACM Press New York, NY, USA

[BFO03] S. Bistarelli, S.N.Foley, B. O'Sullivan, A Constraint-based Framework for the Cascade Vulnerability Problem, in Proc. ICLP2003 Workshop on Constraint and Logic Programming in Security (COLOPS2003), 9 December, Tata Institute of Fundamental Research (TIFR), Mumbay, India.

[BCLM03a] S. Bistarelli, I. cervesato, G. Lenzini, F. martinelli, Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols, Proc. Second International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security - MMM'03, St. Petersburg, Russia, 20-24 September 2003, LNAI 2776, pp. 88-101.

[BF03a] Stefano Bistarelli and Simon N. Foley, A Constraint Based Framework for Dependability Goals: Integrity, In Proc. SAFECOMP 03, 2003

[BF03b] Stefano Bistarelli and Simon N Foley, Analysis of Integrity Policies using Soft Constraints, Proc. IEEE 4th International Workshop on Policies for Distributed Systems and Networks (POLICY2003), Como, June 4-6, 2003.

[BCLM03b] S. Bistarelli, I. Cervesato, G. Lenzini, F. Martinelli, Relating Process Algebras and Multiset Rewriting for Security Protocol Analysis, Proc. Workshop on Issues in the Theory of Security (WITS'03), April 5 - 6, 2003, Warsaw, Poland, 2003.

[Del03] Giorgio Delzanno A Symbolic Procedure for Control Reachability in the Asynchronous Pi-calculus Proc. of Infinity 2003, a Satellite workshop of Concur 03, ENTCS.

[DRV03] Giorgio Delzanno, Jean-Francois Raskin, Laurent Van Begin Covering Sharing Trees: Compact Data Structures for Parameterized Verification Accepted for publication on the International Journal on Software Tools for Technology Transfer (STTT), September 2003.

[DG03] Giorgio Delzanno, Pierre Ganty. Symbolic Methods for Automatically Proving Secrecy and Authentication in Infinite-state Models of Cryptographic Protocols Proceedings of WISP, Workshop on Issues in Security and Petri Nets, Eindhoven, The Netherlands, 2003.

[DG04] Giorgio Delzanno, Pierre Ganty. Automatic Verification of Time Sensitive Cryptographic Protocols Proceedings of TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain, 2004.

[JMVS03] T. Juan, M. Martelli, V. Mascardi and L. Sterling Customizing AOSE Methodologies by Reusing AOSE Features In Proceedings of the 2nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS'03), Melbourne, 2003.

[MM03] M. Martelli and V. Mascardi From UML Diagrams to Jess Rules: Integrating OO and Rule-Based Languages to Specify, Implement and Execute Agents In Proceedings of the 8th APPIA-GULP-PRODE Joint Conference on Declarative Programming (AGP'03), Reggio Calabria, 2003

[MM03] V. Mascardi, M. Martelli and L. Sterling Logic-Based Specification Languages for Intelligent Software Agents Accepted for publication by the Theory and Practice of Logic Programming Journal

[Van03] Laurent Van Begin. Efficient Verification of Counting Abstractions for Parametric systems. PhD Thesis- Université Libre de Bruxelles, Belgium, December 2003.