Soutenance de thèse de HAMADA Khalid
Titre de thèse
Séquences de synchronisation sous contraintes dans les réseaux de Petri synchronisés avec sorties : application aux systèmes cyber-physiques attaqués
Synchronizing sequences under constraints in output synchronized Petri nets: application to attacked cyber physical systems
Résumé de la thèse
Les systèmes cyber-physiques (CPS) intègrent des composants logiciels, matériels et de communication, dont l'interconnexion en réseau les expose à de nouvelles formes de menaces. Les cyberattaques visant les capteurs ou les actionneurs peuvent altérer la perception et le comportement du système, provoquant des conditions opérationnelles indésirables et critiques. Dans ce contexte, la capacité de ramener un CPS attaqué vers un état connu et sûr constitue un mécanisme de défense contre ces cyberattaques.
Inscrits dans la théorie des systèmes à événements discrets, les réseaux de Petri synchronisés avec sorties (OutSynPN) constituent un formalisme adapté à la modélisation conjointe des interactions entre commandes (entrées) et observations (sorties). Dans ce formalisme, une séquence de synchronisation (SS) désigne une séquence d'événements d'entrée permettant de conduire le système, quel que soit son état courant, vers un état cible connu. L'objectif de cette thèse est d'utiliser les SS pour ramener le CPS — modélisé par un OutSynPN — vers un état connu en présence d'une attaque compromettant l'estimation de l'état courant. Les méthodologies développées reposent sur l'OutSynPN et sur un automate fini étiqueté par les entrées (LFAI), à partir duquel un graphe auxiliaire intégrant les sorties est dérivé afin de permettre le calcul des SS via un algorithme greedy. Trois types de contraintes sont pris en compte : (i) les états de blocage, traités par un LFAI restreint fusionnant ces états en un état puits ; (ii) les événements d'entrée interdits, gérés par un LFAI modifié par élagage des transitions concernées ; et (iii) les événements de sortie interdits, exclus par une extension de l'algorithme greedy intégrant une recherche en profondeur. Lorsqu'il existe plusieurs SS menant à un même état cible, une sélection est effectuée selon un critère fondé sur le nombre total d'événements sollicités (entrées et sorties), afin d'identifier celles mobilisant le moins d'événements.
Un cas d'étude basé sur des robots mobiles illustre l'application des approches de calcul de SS sous contraintes, l'ensemble formé par les robots, le contrôleur et le réseau de communication constituant un CPS. Dans ce système, modélisé par un OutSynPN, une attaque compromet la capacité d'estimation de l'état et rend les positions des robots inconnues. Dans un premier scénario, les SS sont exploitées pour assurer la conduite automatique des robots vers les postes d'évacuation. Dans un second scénario, les SS permettent de repositionner les robots à un état connu, sans recourir à des entrées compromises ni produire de sorties susceptibles de divulguer des informations sensibles à l'attaquant. Dans un troisième scénario, les SS sont exploitées pour assurer la conduite automatique des robots vers les postes d'évacuation, sans recourir aux entrées compromises ni produire les sorties susceptibles de divulguer des informations. Des évaluations de performances ont été réalisées pour chaque scénario. Une implémentation sous MATLAB a été développée afin de calculer les SS sous les différentes contraintes. Ces travaux démontrent ainsi l'intérêt du calcul de séquences de synchronisation sous contraintes dans les OutSynPN, appliquées aux CPS attaqués.
Thesis resume
Cyber physical systems (CPS) integrate software, hardware and communication components, whose interconnection exposes them to various malicious actions. Cyberattacks targeting sensors or actuators may alter the system's perception and behaviour, leading to undesirable and critical operating conditions. In this context, the ability to bring an attacked CPS back to a known and safe state constitutes a defence mechanism against such cyberattacks.
Within the theory of discrete event systems, Output synchronized Petri nets (OutSynPN) provide a suitable formalism for jointly modelling the interactions between commands (inputs) and observations (outputs). In this framework, a synchronizing sequence (SS) is an input event sequence that drives the system, regardless of its current state, toward a known target state. The objective of this thesis is to use SS to bring the CPS — modelled by an OutSynPN — back to a known state in the presence of an attack compromising the estimation of the current state. The developed methodologies rely on the OutSynPN and on an input-labeled finite automaton (LFAI), from which an auxiliary graph integrating outputs is derived to compute SS by means of a greedy algorithm. Three types of constraints are addressed: (i) deadlock states, handled by a restricted LFAI merging these states into a sink state; (ii) forbidden input events, managed by modifying the LFAI through pruning of the corresponding transitions; and (iii) forbidden output events, excluded through an extended greedy algorithm incorporating a depth-first search. When several SS reach the same target state, a selection is made according to a criterion based on the total number of events (inputs and outputs), in order to identify those involving the smallest number of events.
A case study involving mobile robots illustrates the application of the constrained SS computation approaches, where the robots, the controller and the communication network form a CPS. In this system, modelled by an OutSynPN, an attack compromises the state estimation capability and makes the robot positions unknown. In a first scenario, SS are used to automatically drive the robots to evacuation stations. In a second scenario, SS bring the system back to a known state without using compromised inputs or producing outputs that could reveal sensitive information to the attacker. In a third scenario, SS are used again to drive the robots to evacuation stations without resorting to compromised inputs or producing the outputs that could reveal information. Performance evaluations were carried out for each scenario. A MATLAB implementation was developed to compute SS under the various constraints. These results demonstrate the relevance of constrained synchronizing sequence computation in OutSynPN when applied to attacked CPS.