Titre original :

Conception et réalisation d’un écosystème basé sur des propriétés formelles d’isolation mémoire pour l’Internet des objets

Titre traduit :

Design and implementation of an ecosystem for the Internet of Things based on a formally proven memory isolation

Mots-clés en français :
  • Sûreté
  • Écosystème IoT
  • Système embarqué
  • Internet des objets
  • Sécurité
  • Isolation mémoire

  • Systèmes embarqués (informatique)
  • Internet des objets
  • Méthodes formelles (informatique)
Mots-clés en anglais :
  • Security
  • Internet of Things
  • Embedded system
  • Safety
  • IoT ecosystem

  • Langue : Français
  • Discipline : Informatique et applications
  • Identifiant : 2019LILUI124
  • Type de thèse : Doctorat
  • Date de soutenance : 19/12/2019

Résumé en langue originale

Depuis leur apparition durant la conquête spatiale, à leur arrivée dans nos maisons, les systèmes embarqués ont énormément évolué dans leur composition, leur fonctionnement et leurs méthodes de développement. De plus, avec l'apparition de réseaux comme Internet, on a vu émerger une nouvelle forme de systèmes embarqués, dit l'Internet des Objets (ang, Internet of Things, IoT). Ces systèmes sont très diversifiés. Ils sont utilisés dans les transports, la télécommunication ou encore la domotique et la médecine. De plus, on voit aussi apparaître des objets connectés fonctionnant en groupe, permettant de fournir des fonctionnalités encore plus complexes à des utilisateurs. Ces utilisateurs peuvent être des êtres humains ou d'autres machines.Cette diversification a vu apparaître de nombreux acteurs, avec des compétences variées, proposant des composants logiciels ou matériels pour ces systèmes embarqués. Malheureusement, la multiplication des acteurs et des méthodes de développement et de collaboration peut nuire aux mécanismes de sécurité ou de sûreté de fonctionnement des systèmes. Lorsqu'une défaillance survient, il peut être difficile dans certaines situations de déterminer le responsable, en dépit des contraintes contractuelles et légales. De plus, si des acteurs économiques distincts et concurrents sont amenés à fournir des services simultanément pour ces objets, il est possible que l'un d'eux cherche à nuire à ses rivaux.Pour répondre à ces problématiques de sécurité et sûreté, des solutions logicielles ou matérielles sont développées. L'isolation mémoire ou la virtualisation garantissent notamment l'intégrité et la confidentialité au sein de l'objet. L'utilisation de méthodes formelles permet la vérification de propriétés en amont de la période de fonctionnement du système. En plus des liens contractuels, les acteurs sont parfois dans l'obligation de respecter des normes ou des standards de développement destinés à fournir des garanties légales sur les objets.Dans cette thèse, j'étudie d'abord l'écosystème dans lequel les systèmes embarqués et les objets connectés sont développés, afin d'y identifier de la manière la plus exhaustive possible les acteurs de cet écosystème. Cette étude m'a mené à constater la dilution des responsabilités de chaque acteur au sein du système embarqué en cas de défaillance de sécurité ou de sûreté ainsi que le manque de confiance entre eux. Ainsi, après cette analyse, j'ai conçu une hiérarchie et des droits entre ces acteurs et leur relation. Pour construire cette architecture, je me base sur des travaux d'un noyau formellement prouvé, fournissant des propriétés d'isolation mémoire et des garanties fortes de sécurité et de sûreté. Avec ces briques de base, je montre comment on peut construire l'architecture et y propager ces garanties afin de maintenir la confiance entre les acteurs, le confinement de défaillances et la responsabilité de chacun. Avec le mécanisme de sécurisation des échanges mis en place, je montre qu'il est possible d'étendre cette architecture afin de construire un groupement d'objets tout en maintenant les propriétés de sécurité et de sûreté définies au sein des objets.

Résumé traduit

Since their advent during the space conquest, to their arrival in our homes, embedded systems have evolved enormously in their composition, their functioning and their development methods. In addition, with the emergence of networks such as the Internet, a new form of embedded systems has emerged, known as the Internet of Things (IoT). These systems are very diverse. They are used in transport, telecommunications, home automation and medicine. In addition, connected objects operating in groups are also emerging, allowing even more complex functionalities to be provided to users. These users can be human beings or other machines.This diversification has seen the emergence of many stakeholders, with various skills, offering software or hardware components for these embedded systems. Unfortunately, the proliferation of actors and development methods and collaboration can have a negative impact on the security or operational safety mechanisms of systems. When a default occurs, it may be difficult in some situations to determine who is responsible, despite contractual and legal constraints. In addition, if separate and competing economic actors are required to provide services simultaneously for these objects, it is possible that one of them may attempt to harm its rivals.To address these security and safety issues, software or hardware solutions are developed. In particular, memory isolation or virtualization guarantees integrity and confidentiality within the object. The use of formal methods allows the verification of properties before the system's operating period. In addition to contractual relationships, actors are sometimes required to comply with development norms or standards designed to provide legal guarantees on objects.In this thesis, I first study the ecosystem in which embedded systems and connected objects are developed, in order to identify in the most exhaustive way possible the actors of this ecosystem. This study led me to observe the dilution of the responsibilities of each actor within the embedded system in the event of a safety or security failure as well as the lack of trust between them. So, after this analysis, I designed a hierarchy and rights between these actors and their relationship. To build this architecture, I rely on the work of a formally proven core, providing memory isolation properties and strong guarantees of security and safety. With these basic building blocks, I show how the architecture can be built and propagated in order to maintain trust between the actors, the containment of failures and the responsibility of each party. With the communication security mechanism in place, I show that it is possible to extend this architecture to build a group of objects and still maintain the security and safety properties defined within the objects.

  • Directeur(s) de thèse : Grimaud, Gilles - Cartigny, Julien
  • Président de jury : Haese-Rolland, Nathalie
  • Membre(s) de jury : Marquet, Kevin
  • Rapporteur(s) : Donsez, Didier - Bouzefrane, Samia
  • Laboratoire : Centre de Recherche en Informatique, Signal et Automatique de Lille
  • École doctorale : École doctorale Sciences pour l'ingénieur (Lille ; 1992-2021)

AUTEUR

  • Yaker, Mahieddine
Droits d'auteur : Ce document est protégé en vertu du Code de la Propriété Intellectuelle.
Accès libre