Soutenance de thèse de Pierre Jacob

Titre de la thèse

High-Order Statistics for Image Representations using Metric Learning

Date et lieu de soutenance

Mardi 8 septembre 2020, 14h.

ENSEA Cergy, salle à préciser.

Abstract

An important challenge in artificial intelligence is the learning of useful data representations, or features, on which recognition algorithms can be used in order to solve a specific task (object or scene recognition, video annotation, etc.). By learning rich representations, that is, which encode the relevant information with respect to the given task, performances of the majority of recognition algorithms can be highly improved. The major difficulty in learning such representations rests on the high dimensionality of the input data, and the lack of prior knowledge about the relevant patterns that should be encoded.

In this thesis, we particularly focus on image representation for the task of content-based image retrieval using the deep metric learning framework. These representations must be low-dimensional in order to reduce the memory storage, the computation cost, and to speed-up the search. Also, they should encode useful information in order to be able to retrieve the most relevant images from the database.

We make the following contributions to alleviate the aforementioned issues: First, we present three image representations that leverage dictionary learning in order to produce richer representation along with covariance matrices or attention mechanisms. Second, we propose two improvements during the training: a method that generates hard examples to resume the training, and a regularization that improves the robustness of the local features for a variety of representations. We empirically show that the proposed strategies significantly improve baseline methods and provide stronger results than most of the state-of-the-art methods.

Composition du jury

  • Mme LARLUS Diane, Senior Research Scientist, Navers Labs Europe, Examinatrice
  • Mme VINCENT Nicole, Professeure des Universités, Université de Paris, Examinatrice
  • M. JEGOU Hervé, Senior Research Scientist, Facebook AI, Examinateur
  • M. CHUM Ondrej, Associate Professor, Czech Technical University in Prague, Rapporteur
  • M.CORD Matthieu, Professeur des Universités, Sorbonne Université, Rapporteur
  • M. KLEIN Edouard, Capitaine, Pôle Judiciaire de la Gendarmerie Nationale, Co-encadrant de thèse
  • M. PICARD David, Senior Research Scientist, Ecole des Ponts ParisTech, Co-encadrant de thèse
  • M. HISTACE Aymeric, Professeur des Universités, ENSEA, Directeur de thèse

Soutenance de HdR de Nga Nguyen

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