logo SBA

ETD

Digital archive of theses discussed at the University of Pisa

 

Thesis etd-05292006-113319


Thesis type
Tesi di dottorato di ricerca
Author
Troina, Angelo
URN
etd-05292006-113319
Thesis title
Probabilistic Timed Automata for Security Analysis and Design
Academic discipline
INF/01
Course of study
INFORMATICA
Supervisors
relatore Prof. Maggiolo Schettini, Andrea
Keywords
  • Automata Theory
  • Concurrency
  • Model Checking
  • Probabilistic Systems
  • Real-time Systems
  • Security
Graduation session start date
26/06/2006
Availability
Withheld
Release date
26/06/2046
Summary
The usefulness of formal methods for the description and verification of
complex systems is nowadays widely accepted. While some system properties
can be studied in a non-timed and non-probabilistic setting, others, such
as quantitative security properties, system performance and reliability
properties, require a timed and probabilistic description of the system.
This thesis focuses on methods for the formal modeling of probabilistic
timed systems, and on algorithms for the automated verification of their
properties. The models considered describe the behavior of a system in
terms of time and probability, and the formal description languages used
are based on extensions of Timed Automata, Markov Decision Processes and
combinations of them.


In multilevel systems it is important to avoid unwanted indirect
information flow from higher levels to lower levels, namely the so called
covert channels. Initial studies of information flow analysis were
performed by abstracting away from time and probability. It is already
known that systems which are considered to be secure may turn out to be
insecure when time or probability are considered. Recently, work has been
done in order to consider also aspects either of time or of probability,
but not both. In this thesis, a general framework is proposed, which is
based on Probabilistic Timed Automata, where both probabilistic and timing
covert channels can be studied. A concept of weak bisimulation for
Probabilistic Timed Automata is given, together with an algorithm to
decide it. Such an equivalence relation is necessary to define information
flow security properties. Thus, a Non Interference security property and a
Non Deducibility on Composition security property are given. They allow
expressing information flow in a timed and probabilistic setting, and they
can be compared with analogous properties defined in settings where either
time or probability or none of them are taken into account. This permits a
classification of the properties depending on their discriminating power.


Some new aspects are then explored involving the introduction of
parameters in Markov Decision Processes and the use of Timed Automata in
the study of cryptographic protocols. Finally, some real-life applications
are described through automata-based formalisms, and model checking is
used to study security issues affected by aspects of time and probability.
File