Probabilistic Timed Automata for Security Analysis and Design

Doctoral Thesis / Dissertation from the year 2006 in the subject Computer Science - IT-Security, University of Pisa (Dipartimento di Informatica), course: Computer Science, language: English, abstract: 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 nonprobabilistic 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 behaviour 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