Thèse Conception d'un noyau sécurisé pour les processeurs avec MPU pour l'IOT et composition de preuves et d'évaluations de sécurité

Description de l'offre

about the role

Votre rôle est d'effectuer un travail de thèse autour de la conception d'un noyau sécurisé pour les processeurs avec MPU (Memory Protection Unit) pour les objets connectés (IOT) et de la composition de preuves formelles pour atteindre cet objectif.

La sécurité des objets connectés est un sujet récurrent mais qui n'est, à ce jour, que partiellement implémenté. En effet, les objets connectés sont de natures diverses et conçus à partir de solutions matérielles variées possédant des puissances de calcul également variées et pour lesquelles les calculs cryptographiques complexes sont plus ou moins possibles et suffisants. Aussi l'objet connecté, en fonction de ses capacités de calculs, peut devenir la cible d'attaques multiples.

La sécurité des objets connectés impose de s'intéresser non seulement à la sécurité intrinsèque de l'objet mais aussi à la propagation de cette sécurité de bout-en-bout. Ainsi, l'objet est intégré dans un écosystème plus général et pensé à l'origine comme sûr (security by design).

Sur ce thème, le projet européen Celtic-Plus ODSI (On Demand Secure Isolation) a démontré que la réalisation d'un micro noyau TCB (Trusted Computing Base) minimal basé sur de l'isolation mémoire formellement prouvée était possible en garantissant à la fois sa robustesse et son absence de bugs. La solution proposée repose sur une architecture Intel de type x86 et sur une MMU (Memory Management Unit) qui n'adresse que partiellement le domaine de l'IOT.

Dans le cadre de l'internet des objets, l'isolation permettra soit à plusieurs entités avec des systèmes d'information différents de partager les fonctionnalités d'un objet (de grande ou moyenne capacité) soit de décomposer cet équipement en plusieurs fonctionnalités et d'isoler celles qui sont critiques.

Aujourd'hui, il existe plusieurs résultats scientifiques concernant la preuve d'isolation sur les OS et hyperviseurs basés sur les MMU (Memory Management Unit) (Sel4 [3] et CertikOS [4] par exemple) qui équipent les objets et systèmes embarqués de capacités plus importantes (routeur, téléphone par exemple) mais aucun concernant les MPU (Memory Protection Unit), qui par leur faible coût seront clés dans le monde de l'IOT. Le seul noyau qui adresse cette problématique à notre connaissance est mbed uvisor [1], qui n'est pas prouvé formellement.

L'objectif principal de la thèse sera de concevoir un noyau pour l'isolation dans les objets les plus petits en adaptant un noyau formellement prouvé (par exemple Pip, le noyau développé au sein du projet ODSI). Pour réaliser cet objectif, vous vous intéresserez à la composition de preuves, et à la mise en oeuvre d'une stratégie pour combler un écart entre un objectif sur un nouveau système et une preuve sur un système existant. Cette stratégie pourra s'appuyer sur l'expression de nouvelles preuves à réaliser ou le choix d'une architecture ou d'un matériel permettant de combler cet écart.

Les informations détaillées concernant la mission scientifique et les principales activités associées à la thèse se trouvent en section 3.

about you

Vous avez préparé une formation de niveau Bac +4/5 dans le domaine de l'informatique ou de la sécurité des systèmes d'information et suivi un cursus approfondi en électronique et systèmes et vous maitrisez l'outil informatique.

Vous avez un très bon relationnel,

Vous maitrisez un ou plusieurs langages de programmation tels que C/C++, Java, Python,

Vous avez un bon niveau d'anglais,

Vous maîtrisez les systèmes embarqués et la programmation sur ses systèmes,

Vous avez des notions sur le fonctionnement des réseaux de télécommunications,

Vous avez des notions ou maîtrisez les preuves formelles.

Vous avez déjà réalisé des stages mettant en oeuvre vos compétences en systèmes ou preuve formelle.

additional information

·  Objectif scientifique - verrous à lever

L'objectif de la thèse est de voir comment adapter le mécanisme de security by design proposé par Pip, noyau formellement prouvé au coeur du projet ODSI, à l'environnement des microcontrôleurs sans MPU.

Verrous scientifiques :

1)Peut-on / comment produire une preuve d'isolation dans un contexte MPU (Memory Protection Unit) plutôt que MMU (Memory Management Unit). Il y a des résultats scientifiques et des OS, hyperviseurs prouvés pour les MMU mais rien pour les MPU, qui, par leur faible coût seront clés dans le monde de l'IOT.

2)Peut-on / comment utiliser les travaux de formalisation du fonctionnement du microprocesseur ARM [2] pour faire le lien entre la preuve formelle d'isolation et les pré-requis matériels indispensables à cette preuve de sécurité. ARM est en train de créer une spécification formelle du matériel. Cela ouvre peut-être une porte pour obtenir une preuve de sécurité par design du logiciel jusqu'au matériel. C'est une opportunité accessible pour la première fois et que nous pouvons saisir dans cette thèse.

Durant le workshop Entropy (https://entropy2018.sciencesconf.org/), nous avons pu voir que cette question était cruciale dans la communauté. En effet, toutes les preuves d'OS existantes sont bousculées par les attaques Spectre et Meltdown car celles-ci touchent les hypothèses matérielles sur lesquelles elles se basent.

3)Peut-on / comment composer des éléments de preuve pour atteindre un certain objectif de sécurité ou une certaine architecture. Comment mettre en oeuvre une telle stratégie?

·  Approche méthodologique-planning

Première année de thèse :

Comprendre les objectifs et les résultats du projet européen ODSI,

Comprendre la solution développée par l'Université de Lille sur l'architecture x86 et participer/ suivre son portage vers une architecture ARM

Etudier en détails l'architecture ARM cible et en particulier les mécanismes de MPU et les spécifications fournies par ARM

Comparer et synthétiser ces 2 approches.

Réaliser un état de l'art de mécanismes de secure boot et d'attestation à distance (remote attestation) et identifier des axes d'amélioration pour améliorer la confiance dans le système.

Deuxième année de thèse:

Modéliser les mécanismes d'isolation sécurisée sur cette architecture,

Faire évoluer ou Participer à l'élaboration de la preuve formelle basée sur ces mécanismes et sur les spécifications ARM

Proposer une méthodologie pour évaluer les écarts entre une preuve formelle existante et un objectif (de sécurtié ou fonctionnel)

Débuter l'implémentation d'une solution au travers d'un démonstrateur (architecture ARM cible + FreeRTOS par exemple) en montrant le rôle et les mécanismes mis en oeuvre dans cette nouvelle approche

Troisième année de thèse :

Continuer et terminer cette implémentation,

Rédaction du mémoire et soutenance de la thèse

department

Au service de plus de 200 millions de clients sur les cinq continents, le Groupe Orange est l'un des principaux opérateurs de télécommunications dans le monde. Les Orange Labs constituent le réseau mondial d'innovation du Groupe Orange. Ils regroupent des chercheurs répartis au sein de 18 laboratoires sur 4 continents, à proximité des écosystèmes innovants, pour tirer parti des compétences locales, et être proches des nouveaux marchés.

Le département SESAME d'Orange Labs Services regroupe une cinquantaine de collaborateurs aux compétences reconnues dans les domaines des éléments de sécurité (carte SIM, NFC, services sans contacts.

Qu'est ce qui fait la valeur ajoutée de cette offre ?

Travailler sur la sécurité de l'IOT, sujet d'avenir.

Approfondir ses connaissances sur les architectures et les preuves formelles.

Travailler sur un sujet stratégique qui nécessite une composante en modélisation importante.

Travailler dans un environnement multiculturel, au sein d'une entité à la pointe de l'innovation. Travailler au sein d'un département de Recherche et en collaboration avec des laboratoires.

Acquérir une expérience de recherche dans un groupe possédant un spectre large de compétences.

Références :

[1]https://www.mbed.com/en/technologies/security/uvisor/

[2]Who guards the guards ? Formal verification of the Arm v8-M Architecture specification, Alastair Red, Proceedigns of the ACM on Programming Language, Vol.1, Octobre 2017

[3]sel4 : Formal verification of an OS kernel, Klein et.al. , Proceedings of the ACM SIGOPS 22nd Symposium on Operating systems principles

[4]CertikOS: An extensible architecture for Building Certified Concurrent OS Kernels, Gu et.al. OSDI, vol.16

[5]Fusing hybrid remote attestation with a formally verified microkernel: lessons learned, Eldefrawy et.al., WiSec17, proceedings of the 10th ACM Conference on Security and Privacy in Wireless and Mobile Networks.

contract

Thesis