Probabilistic Timed Automata for Security Analysis and Design

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.