Séminaires
Séminaire du 20 janvier 2017
Lieu
LTCI, amphithéatre Grenat (Telecom Paris Tech, campus Barrault): comment y aller
Programme
14h00-15h00: Jean Leneutre (Telecom ParisTech), "Towards a strategic approach to security based on game theory"
Abstract : 
In the recent years, a large number of works have proposed to use game theory as a decision support framework for security. Problems tackled in these works include:
- how to optimize the allocation of security resources?
- how to configure in an optimal way protection or monitoring resources?
- how to select the best security response to an incident?
Along this line of research, we will present in this talk a recent contribution related to the integrity and availability of outsourced data. A Service Level Agreement (SLA) is usually signed between the Coud Provider and the customer. For redundancy purposes, it is important to verify the Cloud Provider’s compliance with data backup requirements in the SLA. There exists a number of security mechanisms to check the integrity and availability of outsourced data. This task can be performed by the customer or be delegated to an independent entity that we will refer to as the Verifier. However, checking the availability of data introduces extra costs, which can discourage the customer of performing data verification too often. The interaction between the Verifier and the Cloud provider can be captured using game theory in order to find an optimal data verification strategy. We formulate this problem as a two player non-cooperative one-shot game. We consider the case in which each type of data is replicated a number of times that can depend on a set of parameters including, among others, its size and sensitivity. We analyze the strategies of the cloud provider and the verifier at the Nash Equilibrium and derive the expected behavior of both players. We also consider a second formulation of the problem as a Stackelberg game in which there are a leader and a follower. While, providing some valuable insights for decision making in security, these models based on game theory are not without limitations, in particular regarding the high level of abstraction that it implies.
In a second part of the talk, we will discuss these limitations, and propose future research directions to improve the applicability of game theoretic approaches to security..
15h00-15h30 : Hoang Gia NGuyen (LIPN), "Parametric model checking timed automata under non-Zenoness assumption"
Abstract : Real-time systems often involve hard timing constraints and concurrency, and are notoriously hard to design or verify. Given a model of a real-time system and a property, parametric model-checking aims at synthesizing timing valuations such that the model satisfies the property. However, the counter-example returned by such a procedure may be Zeno (an infinite number of discrete actions in a finite time), which is unrealistic. On the one hand, we show that synthesizing parameter valuations such that at least one counter-example run is non-Zeno is undecidable for Parametric Timed Automata (PTA). On the other hand, we propose a procedure based on a transformation of PTA into Clock Upper Bound PTA to derive such valuations.