Soutenance de Nga NGUYEN

Enseignante-chercheur en informatique et Responsable de l'option Informatique Embarquée (INEM), Nga NGUYEN, a présenté sa soutenance HDR "Sûreté et sécurité des systèmes embarqués : de la modélisation à la vérification et la validation".

La soutenance s'est déroulée le lundi 21 septembre 2020 à 10h30, l'amphi Turing de CY Tech, avenue du Parc, à Cergy, devant le jury composé de :

- M. GERARD Sébastien, Directeur de Recherche, CEA LIST, Rapporteur
- M. JOUVELOT Pierre, Directeur de Recherche, Mines ParisTech, Rapporteur
- M. RAUZY Antoine, Professeur, Norwegian University of Science Technology, Rapporteur
- M. APVRILLE Ludovic , Professeur, Télécom Paris, LabSoC, Examinateur
- Mme. BARON Claude, Professeur, INSA Toulouse, LAAS, Examinateur
- Mme. DUBOIS Catherine, Professeur, ENSIIE,  Samovar, Examinateur
- Mme MUNIER Alix, Professeur, Université Sorbonne, LIP6, Examinateur
- M. ROMAIN Olivier, Professeur, CY Cergy Paris Univeristé, ETIS, Garant

L'équipe enseignante et administrative de CY Tech lui adresse toutes ses félicitations.

Résumé

Ce mémoire HDR résume mes activités de recherche  autour de la sûreté et de la sécurité des systèmes embarqués complexes, avec une approche fondée sur les modèles. Les propriétés de sûreté et de sécurité sont modélisées et vérifiées formellement dès la conception d'un système, ce qui permet de réduire les erreurs tardives et le temps de développement.  Les contributions principales présentées ici sont les suivantes.

D’abord, nous avons proposé d’intégrer l’analyse de sûreté de fonctionnement au processus d'ingénierie système pour assurer la cohérence entre les modèles de conception et l'analyse de sûreté. Des transformations modèle-à-modèle permettent de générer automatiquement, à partir de modèles de système, des analyses des modes de défaillance, de leurs effets et de leur criticité et des arbres de défaillances dynamiques. Ces résultats permettront aux concepteurs de valider ou pas l'architecture d’un système et, le cas échéant, d'ajouter, par exemple, des composants redondants afin de garantir la fiabilité des sous-systèmes critiques. Pour cela, des profils de sûreté et de redondance ont été intégrés directement dans le modèle statique des systèmes.  Afin de compléter ces analyses structurelles, le comportement dynamique d'un système avec des états nominaux et des états d’erreur, ainsi que la propagation de ces erreurs, le tout modélisé dans un langage semi-formel comme SysML, est transformé dans un langage formel comme NuSMV pour vérifier si les exigences de sûreté sont satisfaites par le système.

Notre deuxième contribution concerne la modélisation des attaques dans les systèmes cyber-physiques où la connectivité est de plus en plus présente. Des arbres d’attaque étendus sont modélisés à partir des attaques atomiques, en utilisant des opérateurs de la logique temporelle pour décrire la propagation de menaces. Un profil de l’arbre d’attaque étendu et un profil de connectivité sont proposés afin de modéliser l’attaque et le système respectivement. Les modèles sont ensuite transformés en code NuSMV, et un model checker est utilisé pour vérifier si le système est sécurisé contre les attaques sous forme de spécifications temporelles.

Les diverses analyses dans le cours de cette recherche suggèrent quelques améliorations et ouvrent de nouvelles perspectives pour les travaux futurs sur la  convergence de la sûreté  et de la cybersécurité dans les systèmes embarqués.  Ma proposition consiste à aborder les deux analyses directement dans un unique langage formel de haut niveau comme AltaRica. Le verrou scientifique à lever sera de voir comment adapter un langage initialement dédié à la sûreté, qui traite d'événements aléatoires et non-intentionnels en utilisant des méthodes statistiques, à la sécurité, avec des menaces intentionnelles pour lesquelles des statistiques pertinentes ne peuvent généralement pas être définies. En parallèle, pour utiliser des méthodes formelles au niveau logiciel et fournir d'autres outils pratiques visant à améliorer la correction des systèmes, une deuxième perspective sera d’étudier la combinaison entre analyse statique de code binaire et apprentissage automatique pour la détection de vulnérabilités dans les systèmes embarqués.