21 septembre 2020

Soutenance de HdR de Nga Nguyen

[TheChamp-Sharing]
Soutenance d'habilitation à diriger des recherches (HdR) de Nga Nguyen. Titre : "Sûreté et sécurité des systèmes embarqués : de la modélisation à la vérification et la validation". Soutenance le lundi 21 septembre à 10h30, à l'amphi Turing, CYTECH/EISTI, avenue du parc, 95000 Cergy

Title: Safety and Security of Embedded Systems: from Modeling to Verification and Validation

Abstract:

This HDR document summarizes my research activities on the safety and security of complex embedded systems, with a model-based approach. The safety and security properties are formally modeled and verified, early from the design process of the system, which helps to reduce late errors and development time. The main contributions presented here are as follows.

First, we proposed to integrate safety analysis into the system engineering process to ensure consistency between the design models and the safety assessment. Model-to-model transformation algorithms are used to automatically generate, from system models, the safety artifacts that are Failure Modes and Effects Analysis (FMEA) and Dynamic Fault Trees (DFT). These results will allow designers to validate or not the architecture of a system and, if necessary, to add, for example, redundant components in order to guarantee the reliability of critical subsystems. For this, a Safety Profile and a Redundancy Profile have been integrated directly into the static model of the system under study. In order to complete these structural analyses, the dynamic behavior of the system with nominal and error states, as well as the propagation of these errors, all modeled in a semiformal language, i.e., SysML, is transformed into a formal language, i.e., NuSMV, to verify if the safety requirements are met by the system.

Our second contribution concerns the modeling of attacks in cyber-physical systems, where connectivity is increasingly present. Extended attack trees are modeled from atomic attacks, using temporal logic operators to describe the propagation of threats. An Extended Attack Tree Profile and a Connectivity Profile are proposed to model the attack and the system respectively. The models are then transformed into NuSMV code, and a model checker is used to check if the system is secure against attacks represented in temporal specifications.

The various analyses in this research suggest some improvements and open up new perspectives for future work on the convergence of safety and cybersecurity in embedded systems. My goal in the coming years is to approach the two analyses directly in a single high-level formal language like AltaRica. The scientific barrier to be lifted will be to find how to adapt a language initially dedicated to safety, which deals with random and unintentional events using statistical methods, to security, with intentional threats for which relevant statistics cannot generally be defined. In parallel, to exploit formal methods at the software level and provide other practical tools to address the general issue of correctness in systems, my second perspective will be to study the combination between static binary code analysis and machine learning for the detection of vulnerability in embedded systems.

Keywords: Embedded Systems, Model-Based Systems Engineering (MBSE), Model-Based Safety Assessment (MBSA), Safety, Security, Model Checking, Attack Modeling.

Titre : Sûreté et sécurité des systèmes embarqués : de la modélisation à la vérification et la validation

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.

Mots-clés : système embarqué, ingénierie système, sûreté de fonctionnement, sécurité, méthode formelle, modélisation d’attaque

Jury

  • 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, LASS, 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
21 septembre 2020, 10h3013h00
CYTECH/EISTI, avenue du parc, 95000 Cergy.
Amphi Turing.