Thèse de Mahieddine Yaker

Conception et implémentation d'un écosystème pour l'Internet des objets basé sur une isolation mémoire formellement prouvée

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.

Jury

M. Didier DONSEZ Laboratoire LIG Universite Joseph Fourier - Grenoble 1 Rapporteur Mme Samia BOUZEFRANE Centre d'études et de recherche en informatique et communications Rapporteur M. Kevin MARQUET INSA Lyon Examinateur Mme Nathalie HAESE ROLLAND Université de Lille Examinateur M. Gilles GRIMAUD Université de Lille Directeur de thèse M. Julien CARTIGNY Université de Lille Co-directeur de thèse Mme Chrystel GABER Orange Labs Invitée

Thèse de l'équipe 2XS soutenue le 19/12/2019