Suchergebnisse

Information systems have become ubiquitous and are used to handle each day more and more data. This data is increasingly confidential: strategic military or financial information, or private data. Any leakage of this data can be harmful in many different ways, such that human casualties, money loss, privacy breaching or identity theft. 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. ; Les systèmes informatiques sont devenus omniprésents et sont utilisés au quotidien pour gérer toujours plus d'information. Ces informations sont de plus en plus souvent confidentielles: informations stratégiques militaires ou financières, données personnelles. La fuite de ces informations peut ainsi avoir des conséquences graves telles que des pertes humaines, financières, des violations de la vie privée ou de l'usurpation d'identité. Les contributions de cette thèse se découpent en trois parties. Tout d'abord, nous étudions le problème de synthèse d'un ...

Information systems have become ubiquitous and are used to handle each day more and more data. This data is increasingly confidential: strategic military or financial information, or private data. Any leakage of this data can be harmful in many different ways, such that human casualties, money loss, privacy breaching or identity theft. 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. ; Les systèmes informatiques sont devenus omniprésents et sont utilisés au quotidien pour gérer toujours plus d'information. Ces informations sont de plus en plus souvent confidentielles: informations stratégiques militaires ou financières, données personnelles. La fuite de ces informations peut ainsi avoir des conséquences graves telles que des pertes humaines, financières, des violations de la vie privée ou de l'usurpation d'identité. Les contributions de cette thèse se découpent en trois parties. Tout d'abord, nous étudions le problème de synthèse d'un ...

We propose to study concurrent games on a new extension of Vector Addition Systems with States, where inhibition conditions are added for modeling purposes. Games are a well-suited framework to solve control problems, and concurrent semantics reflect realistic situationswhere the environment can always produce a move before the controller, although it is never required to do so. This is in contrast with previous works, which focused mainly on turn-based semantics. Moreover, we consider asymmetric games, where environment and controller do not have the same capabilities, although they both have restricted power. In this setting, we investigate reachability and safety objectives, which are not dual to each other anymore, and we prove that (i) reachability games are undecidable for finite targets, (ii) they are 2-EXPTIME-complete forupward-closed targets and (iii) safety games are co-NP-complete for finite, upward-closed and semi-linear targets. Moreover, for the decidable cases, we build a finite representation of the corresponding controllers. ; Supported by ERC Starting Grant n°279499 "inVEST" ; Supported by project CoChaT ; Supported by project ImpRo (ANR-2010-BLAN-0317) ; info:eu-repo/semantics/published ; Supported by the European Union Seventh Framework Programme [FP7/2007-2013] under grant agreement 257462 HYCON2 NOE