Smartboxing: policy-dependent defensive code generation using verified static analysis and program transformations

CONTEXTE
Au centre Inria de Rennes, les équipes-projets Inria TEA et Celtique participent au Inria Challenge RIOT-fp, coordonné par Infine et en partenariat avec Inria Eva, Grace, Prosecco, Freie Universität Berlin et Fujitsu. L'un des objectifs de RIOT-fp est de créer une bibliothèque de systèmes d'exploitation vérifiée pour les appareils IoT à l'aide de composites de modules de sécurité certifiés, développés en F*, en les interfaçant avec des bibliothèques de fonctions système C existantes.

OBJECTIFS
Notre approche combine l'analyse statique, appliquée à la sécurité mémoire et au contrôle de flot d’informations (IFC), et l'isolement de pannes logicielles (SFI ou sandboxing), une technique de transformation de programme vérifiée visant à la co-exécution de bibliothèques de fonctions C existantes avec une base de confiance (TCB) générée à l'aide du langage de programmation vérifié F*.

Notre objectif est d'assurer la sécurité de tels composites par la génération automatique de code défensif combinant une politique d’IFC paramétrable avec une stratégie de SFI intelligente fondée sur l’analyse statique de programmes. La conception conjointe et la vérification des bibliothèques système avec la TCB sera réalisée en paramétrant la transformation de programmes systèmes par rapport à des exigences de sécurité de haut niveau, exprimées au moyen de types dépendants, et à refléter les garanties obtenues par cet outil au moyen de types dépendant, également.

CANDIDATURES
La thèse sera réalisée en collaboration avec les équipes Inria Tea et Celtique à Rennes, Prosecco et Infine à Paris. Le domaine du projet de doctorat porte sur la preuve et la programmation et exigera donc des résultats théoriques importants ainsi que le développement de prototypes validant ces résultats et assurant leur reproductibilité. Le travail à réaliser demande enthousiasme et motivation avec une solide expérience, un intérêt et des compétences en compilation, analyse statique, théories des types, de la preuve, des langages de programmation. La thèse sera effectuée avec l'équipe TEA au centre Inria de Rennes, en collaboration étroite avec l’équipe Celtique, et démarrera au plus tard au quatrième trimestre 2020, pour une durée de trois ans et un salaire mensuel de ~2k€, subventions et sécurité sociale.