| | All
sessions take place in auditorium 3.08:50- | 09:50
| David
Sands, Chalmers U of Techn., Sweden Invited
talk: **Probability and timing: Challenges for secure programming** In
this talk we will provide an overview of our recent work on
the specification and verification of secure information flow in such
programs. We highlight how probabilistic considerations enter in two quite
different ways. In the first instance, probabilities are an additional
security threat. Concurrent systems might exhibit probabilistic behaviour
which an attacker could exploit to leak information. In this case we look
at the modelling and verification of secure information flow using
probabilistic bisimulations. In the second case, we look at how
probabilistic behaviour can come to our aide when trying to eliminate the
information flows which arise through the *timing behaviour*
of programs. This talk is based on joint work with Andrei Sabelfeld and
Johan Agat. |
09:50- | 10:30
| Alessandro Aldini, U Bologna, Italy Roberto
Gorrieri, U Bologna, Italy
**Security
analysis of a probabilistic non-repudiation
protocol** Non-interference
is a definition of security introduced for the
analysis of confidential information flow in computer systems. In this
paper, a probabilistic notion of non-interference is used to reveal
information leakage which derives from the probabilistic behavior of
systems. In particular, as a case study, we model and analyze a
non-repudiation protocol which employs a probabilistic algorithm to achieve
a fairness property. The analysis, conducted by resorting to a definition
of probabilistic non-interference in the context of process algebras,
confirms that a solely nondeterministic approach to the information flow
theory is not enough to study the security guarantees of cryptographic
protocols. |
11:00- | 11:40
| Michael Huth, Imperial College, UK
**Possibilistic
and probabilistic abstraction-based model
checking** We
present a framework for the specification of abstract models
whose verification results transfer to the abstracted models for a logic
with unrestricted use of negation and quantification. This framework is
novel in that its models have quantitative or probabilistic observables and
state transitions. Properties of a quantitative temporal logic have
measurable denotations in these models. For probabilistic models such
denotations approximate the probabilistic semantics of full LTL. We show
how predicate-based abstractions specify abstract quantitative and
probabilistic models with finite state space. |
11:40- | 12:20
| Marta Kwiatkowska, U Birmingham,
UK Gethin
Norman, U Birmingham, UK Antonio
Pacheco, IST Lisbon, Portugal
**Model
checking CSL until formulae with random time bounds** Continuous
Time Markov Chains (CTMCs) are widely used as the
underlying stochastic process in performance and dependability analysis.
Model checking of CTMCs against Continuous Stochastic Logic (CSL) has been
investigated previously by a number of authors. CSL contains a time-bounded
until operator that allows one to express properties such as "the probability
of 3 servers becoming faulty within 7.01 seconds is at most 0.1". In
this paper we extend CSL with a random time-bounded until operator, where
the time bound is given by a random variable instead of a fixed real-valued
time (or interval). With the help of such an operator we can state that the
probability of reaching a set of goal states within some generally
distributed delay while passing only through states that satisfy a certain
property is at most (at least) some probability threshold. In addition,
certain transient properties of systems which contain general distributions
can be expressed with the extended logic. We extend the efficient model
checking of CTMCs against the logic CSL developed in [Katoen et al. 2001]
to cater for the new operator. Our method involves precomputing a family of
coefficients for a range of random variables which includes Pareto, uniform
and gamma distributions, but otherwise carries the same computational cost
as that for ordinary time-bounded until. We implement the algorithms in
Matlab and evaluate them by means of a
queueing system example. |
14:00- | 14:20
| Richard Lassaigne, U Paris VII,
France Sylvain
Peyronnet, U Paris XI (Paris-Sud), France Short
presentation: **Approximate verification of probabilistic systems** |
14:20- | 14:40
| Olivier Bournez, LORIA Nancy, France Short
presentation: **A generalization of equational proof theory?** |
14:40- | 15:00
| Alessandra Di Pierro, U Pisa, Italy Herbert
Wiklicky, Imperial College, UK Short
presentation: **Probabilistic abstract interpretation and statistical
testing** |
15:00- | 15:20
| Mario Bravetti, U Bologna, Italy Short
presentation: **An integrated approach for the specification and analysis of
stochastic real-time systems** |
16:00- | 16:40
| Pedro D'Argenio, National U of
Córdoba, Argentina Bertrand
Jeannet, IRISA Rennes, France Henrik
Jensen, Aalborg U, Denmark Kim
Guldstrand Larsen, Aalborg U, Denmark
**Reduction
and refinement strategies for probabilistic
analysis** We
report on new strategies for model checking quantitative
reachability properties of Markov decision processes by successive
refinements. In our approach, properties are analyzed on abstractions
rather than directly on the given model. Such abstractions are expected to
be significantly smaller than the original model, and may safely refute or
accept the required property. Otherwise, the abstraction is refined and the
process repeated. As the numerical analysis involved in settling the
validity of the property is more costly than the refinement process, the
method profits from applying such numerical analysis on smaller state
spaces. The method is significantly enhanced by a number of novel
strategies: a strategy for reducing the size of the numerical problems to
be analyzed by identification of so-called *essential
states*, and heuristic strategies for guiding the refinement
process. |
| |