Soutenance de thèse de Dimitri ANTAKLY (équipes DUKe / AeLoS)

Dimitri Antakly, doctorant au sein des équipes DUKe et AeLoS, soutiendra sa thèse intitulée « Apprentissage et Vérification Statistique pour la Sécurité » / « Machine Learning and Statistical Verification for Security »

jeudi 2 juillet 2020 à 10h, sur le site de la FST au bâtiment 34 et en visio.

Jury :
– Directeur thèse : Leray Philippe
– Co-encadrant : Delahaye Benoit
– Rapporteurs : Schiex Thomas (INRAE Toulouse), Tabia Karim (Université d’Artois)
– Autres membres : Rouveirol Céline (Université Paris 13), Bertrand Nathalie (Inria Rennes)

Résumé : Les principaux objectifs poursuivis au cours de cette thèse sont en premier lieu de pouvoir combiner les avantages de l’apprentissage graphique probabiliste de modèles et de la vérification formelle afin de pouvoir construire une nouvelle stratégie pour les évaluations de sécurité. D’autre part, il s’agit d’évaluer la sécurité d’un système réel donné. Par conséquent, nous proposons une approche où un « Recursive Timescale Graphical Event Model (RTGEM) » appris d’après un flux d’évènements est considéré comme représentatif du système sous-jacent. Ce modèle est ensuite utilisé pour vérifier une propriété de sécurité. Si la propriété n’est pas vérifiée, nous proposons une méthodologie de
recherche afin de trouver un autre modèle qui la vérifiera. Nous analysons et justifions les différentes techniques utilisées dans notre approche et nous adaptons une mesure de distance entre Graphical Event Models. La mesure de distance entre le modèle appris et le proximal secure model trouvé nous donne un aperçu d’à quel point notre système réel est loin de vérifier la propriété donnée. Dans un souci d’exhaustivité, nous proposons des séries d’expériences sur des données de synthèse nous permettant de fournir des preuves
expérimentales que nous pouvons atteindre les objectifs visés.

Mots-clés : Apprentissage de modèles, Vérification formelle, Statistical Model Checking, Recursive Timescale Graphical Event Models, Flux d’événements, Evaluation de sécurité.

*****************

Abstract: The main objective of this thesis is to combine the advantages of probabilistic graphical model learning and formal verification in order to build a novel strategy for security assessments. The second objective is to assess the security of a given system by verifying whether it satisfies given properties and, if not, how far is it from satisfying them. We are interested in performing formal verification of this system based on event sequences collected from its execution. Consequently, we propose a model-based approach where a Recursive Timescale Graphical Event Model (RTGEM), learned from the event streams, is considered to be representative of the underlying system. This model is then used to check a security property. If the property is not verified, we propose a search methodology to find another close model that satisfies it. We discuss and justify the different techniques we use in our approach and we adapt a distance measure between Graphical Event Models. The distance measure between the learned « fittest » model and the found proximal secure model gives an insight on how far our real system is from verifying the given property. For the sake of completeness, we propose series of experiments on synthetic data allowing to provide experimental evidence that we can attain the goals.

Keywords: Model-based learning, Formal verification, Statistical Model Checking, Recursive Timescale Graphical Event Models (RTGEMs), Event streams, Security assessments.