Fairness is a desirable and crucial property of many protocols that handle, for instance, exchanges of message. It states that if at least one agent engaging in the protocol is honest, then either the protocol will unfold correctly and fulfill its intended goal for all participants, or it will fail for everyone. In this work, we present a game-based framework for the study of fairness protocols, that does not define a priori an attacker model. It is based on the notion of strong secure equilibria, and leverages the conceptual and algorithmic toolbox of game theory. In the case of finite games, we provide decision procedures with tight complexity bounds for determining whether a protocol is immune to nefarious attacks from a coalition of participants, and whether such a protocol could exist based on the underlying graph structure and objectives.

Interrupt Timed Automata (ITA ) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (PolITA ). We prove that reachability is decidable in 2EXPTIME on PolITA, using an adaptation of the cylindrical algebraic decomposition algorithm for the first-order theory of reals. We also obtain decidability for the model checking of a timed version of CTL and for reachability in several extensions of PolITA. In particular, compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also study expressiveness questions for PolITA and show that PolITA are incomparable with stopwatch automata.

On a partially observed system, a secret φ is opaque if an observer cannot ascertain that its trace belongs to φ. We consider specifications given as Constraint Markov Chains (CMC), which are underspecified Markov chains where probabilities on edges are required to belong to some set. The nondeterminism is resolved by a scheduler, and opacity on this model is defined as a worst case measure over all implementations obtained by scheduling. This measures the information obtained by a passive observer when the system is controlled by the smartest scheduler in coalition with the observer. When restricting to the subclass of Linear CMC, we compute (or approximate) this measure and prove that refinement of a specification can only improve opacity.

Security of computer systems is central in our digitalized world. Security of businesses, persons, and even governments is facing a growing threat from a wide variety of attackers. Eliminating vulnerabilities from application's code is necessary to prevent attacks. The first step toward eliminating security vulnerabilities is their detection, which can be an arduous task in large size programs. Static analysis of the code helps to automate this process, by guiding the programmer toward the potential vulnerabilities before they are discovered by an adversary. We investigate in this paper vulnerabilities that arise in C code through the calling of library functions. We define criteria to detect dangerous use of these functions, and show that the evaluation of a static analyzer implementing the proposed detection model yields a low false‐positive rate.

In this article, we propose to use game theory to model our WSN network. In this setting, the goal of the compromised node is to keep disrupting the network while remaining alive. The game studied is a two-player quantitative infinite game on a finite graph, where each transition can change some energy levels and some reward. The goal of the compromised node is hence to maximize its reward while maintaining a positive energy level. On the theoretical side, we show that solving these games is not algorithmically possible if the objective is too complex. We can however provide solutions in some restricted cases. The ultimate purpose is to demonstrate that, with the presented detection solution, a compromised node cannot "win the game", and hence either gets detected, dies, or behaves as an normal (sane) node would.

Given a probabilistic transition system (PTS) A partially observed by an attacker, and an ω-regular predicate φ over the traces of A, measuring the disclosure of the secret φ in A means computing the probability that an attacker who observes a run of A can ascertain that its trace belongs to φ. We consider specifications given as Interval Markov Chains (IMCs), which are underspecified Markov chains where probabilities on edges are only required to belong to intervals. Scheduling an IMC S produces a concrete implementation as a PTS and we define the worst case disclosure of secret φ in S as the maximal disclosure of φ over all PTSs thus produced. We compute this value for a subclass of IMCs and we prove that simulation between specifications can only improve the opacity of implementations.

In this invited contribution, we summarize new solution concepts useful for the synthesis of reactive systems that we have introduced in several recent publications. These solution concepts are developed in the context of non-zero sum games played on graphs. They are part of the contributions obtained in the inVEST project funded by the European Research Council.

Covert channels represent a security problem for information systems, since they permit illegal flows and sometimes leaks of classified data. Although numerous descriptions have been given at a concrete level, relatively few work has been carried out at a more abstract level. In this paper, we propose a definition for covert channels based on encoding and decoding binary messages with transducers, in a finite transition system, and we explain why this definition is different from a similar notion of so called iterated interference. We also show that covert channels can be detected using a restricted class of transducers.

Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (PolITA). We prove the decidability of the reachability and model checking of a timed version of CTL by an adaptation of the cylindrical decomposition method for the first-order theory of reals. Compared to previous approaches, our procedure handles parameters and clocks in a unified way. Moreover, we show that PolITA are incomparable with stopwatch automata. Finally additional features are introduced while preserving decidability.

Given a probabilistic transition system (PTS) A partially observed by an attacker, and an ω-regular predicate ϕ over the traces of A, measuring the disclosure of the secret ϕ in A means computing the probability that an attacker who observes a run of A can ascertain that its trace belongs to ϕ. In the context of refinement, we consider specifications given as Interval-valued Discrete Time Markov Chains (IDTMCs), which are underspecified Markov chains where probabilities on edges are only required to belong to intervals. Scheduling an IDTMC S produces a concrete implementation as a PTS and we define the worst case disclosure of secret ϕ in S as the maximal disclosure of ϕ over all PTSs thus produced. We compute this value for a subclass of IDTMCs and we prove that refinement can only improve the opacity of implementations.

Opacity is a general language-theoretic framework in which several security properties of a system can be expressed. Its parameters are a predicate, given as a subset of runs of the system, and an observation function, from the set of runs into a set of observables. The predicate describes secret information in the system and, in the possibilistic setting, it is opaque if its membership cannot be inferred from observation. In this paper, we propose several notions of quantitative opacity for probabilistic systems, where the predicate and the observation function are seen as random variables. Our aim is to measure (i) the probability of opacity leakage relative to these random variables and (ii) the level of uncertainty about membership of the predicate inferred from observation. We show how these measures extend possibilistic opacity, we give algorithms to compute them for regular secrets and observations, and we apply these computations on several classical examples. We finally partially investigate the non-deterministic setting.

This document present two works realized in the framework of the ImpRo project and in relation with the task Quantifying robustness and implementabil-ity. One of the goal of this task is to propose methods to qualify in which manner a system is robust to some properties. The first work presented in this document studies the opacity of purely probabilistic systems. i.e. systems in which the non-deterministic choices have been replaced by probabilistic distribution over the set of states. The notion of opacity has been previously studied in the case of non-deterministic transition systems to determine whether a system respects some security properties. The idea is the following: an external passive attacker tries to gain information on a secret property through observation of the system executions and the system is considered opaque if secret and non secret executions cannot be distinguished by the attacker. Hence, by instantiating the secret predicate and the observation function, one is able to show several interesting security properties on the modeled systems like for instance anonymity or non-interference. In this work, the authors propose two probabilistic definitions of opacity with the aim to (1) measure the security breach, instead of simply giving a yes/no answer and (2) measure the opacity robustness, when the system is opaque. Indeed, even when a system is opaque, the distribution of runs in some observation classes can be unbalanced and hence give information to an observer, thus weakening the system. For instance, if a bip is emitted after reception of an incoming message in 99% of cases, then an observer clearly gains information from hearing the bip. These definitions are illustrated on several examples given by probabilistic 1 models. The authors also show how to compute these measures for restricted types of observation, in the special case where the secret predicate is regular. The joint document is a preliminary version of an article to appear in Mathematical Structures in Computer Science. The second work studies the concept of robustness and implementability, i.e. whether a system is robust to some perturbation and whether it can be "really" implemented, for systems with real-time behavior considering the model of timed automata. One interesting question, given a model for a real-time system, is to determine whether there exists a robust or implementable model for such a system which respects the same properties. In fact, imagine that given a timed automaton respecting some properties, one want …

Iterated admissibility is a well-known and important concept in classical game theory, e.g. to determine rational behaviors in multi-player matrix games. As recently shown by Berwanger, this concept can be soundly extended to infinite games played on graphs with omega-regular objectives. In this paper, we study the algorithmic properties of this concept for such games. We settle the exact complexity of natural decision problems on the set of strategies that survive iterated elimination of dominated strategies. As a byproduct of our construction, we obtain automata which recognize all the possible outcomes of such strategies.

We introduce the class of Interrupt Timed Automata (ITA), a subclass of hybrid automata well suited to the description of timed multi-task systems with interruptions in a single processor environment.While the reachability problem is undecidable for hybrid automata we show that it is decidable for ITA. More precisely we prove that the untimed language of an ITA is regular, by building a finite automaton as a generalized class graph. We then establish that the reachability problem for ITA is in NEXPTIME and in PTIME when the number of clocks is fixed. To prove the first result, we define a subclass ITA of ITA, and show that (1) any ITA can be reduced to a language-equivalent automaton in ITA and (2) the reachability problem in this subclass is in NEXPTIME (without any class graph).In the next step, we investigate the verification of real time properties over ITA. We prove that model checking SCL, a fragment of a timed linear time logic, is undecidable. On the other hand, we give model checking procedures for two fragments of timed branching time logic.We also compare the expressive power of classical timed automata and ITA and prove that the corresponding families of accepted languages are incomparable. The result also holds for languages accepted by controlled real-time automata (CRTA), that extend timed automata. We finally combine ITA with CRTA, in a model which encompasses both classes and show that the reachability problem is still decidable. Additionally we show that the languages of ITA are neither closed under complementation nor under intersection.

We investigate how two agents can communicate through a noisy medium modeled as a finite non deterministic transducer. The sender and the receiver are also described by finite transducers which can respectively encode and decode binary messages. When the communication is reliable, we call the encoder/decoder pair a channel. We study the channel synthesis problem which, given a transducer, asks whether or not such sender and receiver exist and builds them if the answer is positive. To that effect we introduce the structural notion of encoding state in a transducer which is a necessary condition for the existence of a channel. It is not, however, a sufficient condition. In fact, we prove that the problem is undecidable. Nonetheless, we obtain a synthesis procedure when the transducer is functional. We discuss these results in relation to security properties.

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 situations where 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 for upward-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.

Les systemes informatiques sont devenus omnipresents et sont utilises au quotidien pour gerer toujours plus d'information. Ces informations sont de plus en plus souvent confidentielles: informations strategiques militaires ou financieres, donnees personnelles. La fuite de ces informations peut ainsi avoir des consequences graves telles que des pertes humaines, financieres, des violations de la vie privee ou de l'usurpation d'identite. Les contributions de cette these se decoupent en trois parties. Tout d'abord, nous etudions le probleme de synthese d'un canal de communication dans un systeme decrit par un transducteur. Malgre les limites imposees par ce modele, nous montrons que le probleme de synthese est indecidable en general. Cependant, lorsque le systeme est fonctionnel, c'est-a-dire que son fonctionnement externe est toujours le meme, le probleme devient decidable. Nous generalisons ensuite le concept d'opacite aux systemes probabilistes, en donnant des mesures groupees en deux familles. Lorsque le systeme est opaque, nous evaluons la robustesse de cette opacite vis-a-vis des informations donnees par les lois de probabilites du systeme. Lorsque le systeme n'est pas opaque, nous evaluons la taille de la faille de securite induite par cette non opacite. Enfin, nous etudions le modele des automates temporises a interruptions (ITA) ou les informations sur l'ecoulement du temps sont organisees en niveaux comparables a des niveaux d'accreditation. Nous etudions les proprietes de regularite et de cloture des langages temporises generes par ces automates et proposons des algorithmes de model-checking pour des fragments de logiques temporelles temporisees.

It is commonplace to have multiple behaviour models that describe the same system but have been produced by different stakeholders or synthesized from different sources. Although in practice, such models frequently exhibit inconsistencies, there is a lack of tool support for analyzing them. There are two key difficulties in explaining why two behavioural models are inconsistent: (1) explanations often require branching structures rather than linear traces, or scenarios; and (2) there can be multiple sources of inconsistency and many different ways of explaining each one. In this paper, we present an approach that supports exploration of inconsistencies between modal transition systems, an extension to labelled transition systems. We show how to produce sound graphical explanations for inconsistencies, how to compactly represent all possible explanations in a composition of the models being compared, and how modelers can use this composition to explore the explanations encoded therein.

Given (1) an architecture defined by processes and communication channels between them or with the environment, and (2) a specification on the messages transmitted over the channels, distributed synthesis aims at deciding existence of local programs, one for each process, that together meet the specification, whatever the environment does. Recent work shows that this problem can be solved when a linear preorder sorts the agents w.r.t. the information received from the environment. In this paper we show a new decidability result in the case where this preorder is broken by the addition of noisy agents embedded in a pipeline architecture. This case cannot be captured by the classical framework. Besides, this architecture makes it possible to model particular security threats, known as covert channels, where two users (the sender and the receiver) manage to communicate via a noisy protocol, and despite incomparable views over the environment.