Timed Automata for Security of Real-Time Systems

Ensuring information security is a fundamental problem in computing environments of modern society. Information flow theory provides key techniques for guaranteeing that certain information security goals are met by a computing system. However, the focus of the researchers has been mainly around the security of programming languages, whereas, little effort has been put in the security analysis of cyber-physical systems (CPS) and internet of things (IoT) devices. CPS and IoT involve computations which have unstructured control flow and can be both data- and continuous time-dependent, making the programming language approaches inadequate. This thesis makes a breakthrough to the problem of information security in such systems. To this end, we model systems using timed automata, a formalism that has established itself for analyzing safety properties of CPS and IoT devices. We then leverage approaches from the theory of information flow, and we develop novel techniques for both the qualitative, and the quantitative security analysis of our models. Our main contributions include • the development of a language, whose semantics is given using timed automata, and a sound type system, which enforces a non-interference security condition on programs written in our language.
• a sound algorithm which traverses a timed automaton and enforces a non-interference condition, which permits locality-based information release.
• a logic for the specification of time- and data-dependent access control policies for networks of timed automata, and techniques for translating policies in our logic to a logic which can be handled by standard model-checkers for timed automata such as UPPAAL. We also provide an implementation of our translation.
• the first principled information-flow analysis of information leakage on systems that implement the countermeasure clocks with reduced resolution. Our analysis
relies on a novel translation of timed automata to information-theoretic channels, which we then use to derive insights into the effectiveness of this countermeasure
and the existing attacks that can bypass it.