You are here

Quantifying the robustness of a system under attack.

Team and supervisors
Department / Team: 
Team Web Site: 
http://www.irisa.fr/sumo/
PhD Director
Loïc Hélouët
Co-director(s), co-supervisor(s)
Contact(s)
NameEmail addressPhone Number
Loïc Hélouët
loic.helouet@inria.fr
02 99 84 75 90
Hervé Marchand
herve.marchand@inria.fr
02 99 84 75 09
PhD subject
Abstract

Computer systems are often critical systems that should guarantee some safety properties, but also some quality of service (QoS), and in many cases confidentiality properties. Examples of such systems are urban trains networks, autonomous vehicles, health systems, online websites, etc.

These systems can be studied trough several types of formal models and dedicated techniques. A standard setting is to consider variants of automata and apply model-checking techniques to guarantee that a given set of requirements is not violated. In the context of an attack of a system that has to maintain a QoS, one might consider quantitative aspects. Games theory [CDHR10,CRR14] is well adapted to consider actions performed by the attacker and their costs (where a cost should be understood in a broad sense encompassing time consumption, energy, reputation loss, some amount of money, ….)

The topic of this PhD is to consider how attacks of a system can affect its security, or its quality of service. We consider systems that are under the control of a supervisor, in charge of ensuring the qualitative and quantitative properties of the system from its estimation of the current configuration of the system and of its environment (see [DDM10]). We assume that attacker can interact with the system, and can in addition perturb the interactions between the system and the supervisor (man-in-the-middle attacks). An example of this setting can be found in [MGRKL17].

Under this setting, various kinds of problems can arise: An attacker can force a system to reveal some confidential Information, or reduce significantly the effort required for a guessing attack on a secret information. Similarly, by perturbing a system (through interaction or by forging malevolent inputs [HMM17]), and attacker can seriously degrade the quality of service. In this thesis, we will be interested in quantifying the effort needed for an attacker to be successful in such attacks.  Similarly, another direction will be to quantify the efforts needed by a supervisor to counter such attacks. We will also consider the synthesis of optimal supervisors, i.e. supervisors that can resist to attacks at the lowest possible cost, or that can reduce as much as possible the quality loss or increase the effort of an attacker up to prohibitive costs. Last, we will consider quantification of QoS loss for attacked systems.

The techniques developed during the thesis will find applications in the domain of security and of transport networks regulation [HK18].

Required skills:

Candidates should hold a Master of Science degree or equivalent in computer science or math. They should be interested by formal methods. Former work in this domain will be welcome. The working languages can be both French and English. Foreign applications are welcome. Programming skills are not mandatory but will be considered.

Working environment:

The thesis will take place in the SUMO team at IRISA/INRIA Rennes Bretagne Atlantique in Rennes (http://www.irisa.fr/sumo/index.html) and will be co-supervised by Hervé Marchand and Loïc Hélouët.

Application:

Candidates should send their CVs, references and motivation letters by mail to the supervisors.

 

Bibliography

[BMS15] Béatrice Bérard, John Mullins, Mathieu Sassolas, Quantifying opacity. Mathematical Structures in Computer Science 25(2): 361-403 (2015)

[CDHR10] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin, Generalized Mean-payoff and Energy Games. FSTTCS 2010: p505-516 (2010)

[CRR14] Krishnendu Chatterjee, Mickael Randour, Jean-François Raskin, Strategy synthesis for multi-dimensional quantitative objectives, Acta Inf. 51(3-4): 129-163 (2014)

[DDM10] Jérémy Dubreil, Philippe Darondeau, Hervé Marchand, Supervisory Control for Opacity, IEEE Trans. Automat. Contr. 55(5): 1089-1100 (2010)

[HK18] Loïc Hélouët, Karim Kecir,Realizability of schedules by stochastic time Petri nets with blocking semantics, Sci. Comput. Program. 157: 71-102 (2018)

[HMM18] Loïc Hélouët, Hervé Marchand, John Mullins, Concurrent Secrets with Quantified Suspicion, ACSD 2018: 75-84 (2018)

[MGRKL17] Romulo Meira Goes, Eunsuk Kang, Raymond Kwong, Stéphane Lafortune, Stealthy deception attacks for cyber-physical systems, CDC 2017: p 4224-4230 (2017).

Work start date: 
Dès que possible / As soon as possible
Keywords: 
Sécurité, Qos, Model-checking, Formal methods, Games Theory
Place: 
IRISA - Campus universitaire de Beaulieu, Rennes