ETD

Archivio digitale delle tesi discusse presso l'Università di Pisa

Tesi etd-05292006-113319


Tipo di tesi
Tesi di dottorato di ricerca
Autore
Troina, Angelo
URN
etd-05292006-113319
Titolo
Probabilistic Timed Automata for Security Analysis and Design
Settore scientifico disciplinare
INF/01
Corso di studi
INFORMATICA
Relatori
relatore Prof. Maggiolo Schettini, Andrea
Parole chiave
  • Concurrency
  • Real-time Systems
  • Probabilistic Systems
  • Model Checking
  • Automata Theory
  • Security
Data inizio appello
26/06/2006
Consultabilità
Non consultabile
Data di rilascio
26/06/2046
Riassunto
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