PhD graduated
Team : MoVe
Departure date : 12/31/2011

Supervision : Béatrice BÉRARD

Noninterférence et canaux cachés dans les systèmes temporisés

Information systems have become ubiquitous and are used to handle each day more and more data. This data is increasingly confidential: it may be strategic military or financial information, or private information. Any leakage of this data can be harmful in many different ways, such that human casualties, money loss, privacy breaching or identity theft. The use of formal methods and especially formal verification of such systems has become necessary to ensure both the safety of the behavior of the system and the security of the information it handles. These techniques are applied on models of the system where some parameters ? especially quantitative parameters ? may have been abstracted. These omitted parameters have sometimes been used in order to breach the security of supposedly secure systems. Nowadays, models tend to include more of this information, which is often relative to the (continuous) elapsing of time or to the probability distributions that rule the system's behavior. Models also include the architecture of the systems as several processes, who may have different, or even contradictory, goals: one may want to keep a secret while the other tries to discover it. When the behavior of all processes is partially or completely unknown, formal methods have to consider all possible cases, which is in general impossible (if there exist an infinite number of choice) or intractable (if there exist too many possibilities to consider them all). The contributions of this thesis are threefold. First, we study the problem of synthesis of a communication channel inside a system given as a transducer. Even though the model of transducers is syntactically limiting, we show that this synthesis problem is undecidable in general. However, when the system is functional, meaning that its behavior from an external point of view is always the same, the problem becomes decidable. We then generalize the concept of opacity to probabilistic systems, by giving measures separated in two groups. When the system is opaque, we evaluate the robustness of this opacity with respect to the bias induced by the probability distributions in the system. When the system is not opaque, we evaluate the size of the security hole opened by this non-opacity. Finally, we study the model of Interrupt Timed Automata (ITA) where information about time elapsing is organized along levels, which therefore resemble accreditation levels. We study properties of regularity and closure of the time languages accepted by these automata and give some model-checking algorithms for fragments of timed temporal logics. These results allow to verify formulas such as ?the system is (in state) ready before 7 time units have elapsed since the beginning of the system's execution?.

Defence : 11/28/2011 - 10h - Site Jussieu 25-26/105

Jury members :

PALAMIDESSI Catuscia (LIX, INRIA et École Polytechnique) [Rapporteur]
RASKIN Jean-François (Université Libre de Bruxelles) [Rapporteur]
HADDAD Serge (LSV, ENS Cachan)
KORDON Fabrice (LIP6, Université Pierre et Marie Curie)
BÉRARD Béatrice (LIP6, Université Pierre et Marie Curie)

2009-2021 Publications