Les offres de “Orange”

Expire bientôt Orange

Thèse Mise à jour de preuves mathématiques de systèmes d'exploitation : définitions, stratégies et évaluations F/H

  • CDI
  • Cesson-Sévigné (Ille-et-Vilaine)
  • Développement informatique

Description de l'offre



about the role

Votre rôle est d'effectuer un travail de thèse sur : « Mise à jour de preuves mathématiques de systèmes d'exploitation : définitions, stratégies et évaluations».

Les approches d'assurance logicielle à base de méthodes formelles de preuve et de vérification de ces preuves, apparaissent jusqu'à aujourd'hui comme prometteuses, à la fois techniquement et économiquement. Ces méthodes formelles appliquées aux logiciels des systèmes d'exploitation se sont beaucoup développées ces dernières années en raison de la massification du nombre d'appareils numériques et les nombreuses vulnérabilités sécuritaires dues à l'obésité -et non simplicité- croissante de leurs systèmes logiciels (1) (2) (3).

Pour rappel, les vérifications formelles se fondent sur une couche logicielle à l'appellation floue, le TCB, Trusted Computing Base, comme les preuves en logique et mathématiques se basent sur une axiomatique ou une théorie. Ce TCB, non prouvé, mais que l'on considère correct, est en quelque sorte le modèle hardware/firmware, ou couche d'abstraction sur lequel se basent et se construisent les preuves, leur validité et, en fin de compte, le fonctionnement du système numérique dans son ensemble. Il est souvent qualifié aussi de ‘bas-niveau' et escamoté dans les analyses de sécurité.

Cependant le code dans ces TCB n'est pas du tout, en ce qui concerne la sécurité de l'appareil numérique, en position subalterne, en ‘bas-niveau' : bien au contraire, y résident bien souvent les parties du code les plus privilégiées de l'appareil. N'importe quelle erreur ou vulnérabilité dans le TCB peut avoir, en cas d'attaque, des conséquences négatives très importantes (voir, à titre d'illustration, les vulnérabilités Spectreou Meltdown (6), ou celle dans Knox de Samsung, le framework de sécurité pour Android (4), ou Rowhammer un bug des mémoires DRAM qui peut être exploité par des attaquants sur plateformes Intel ou ARM (5)), même totalement invalidantes, pour la stabilité et le fonctionnement du système logiciel, même prouvé, ou du moins rompre les invariants sur lesquels le bon fonctionnement de celui-ci et son éventuelle preuve se basent.

Cette non maitrise des hypothèses du TCB, couplée à la complexification croissante des processeurs (exécution spéculative, nombre de coeurs, niveaux de caches multiples, etc…) et des systèmes logiciels nous fait craindre une perte à moyen terme de la maitrise acquise aujourd'hui. Cette problématique a commencé à être explorée lors du récent workshop ENTROPY 2018 que nous avons co-organisé avec l'Université de Lille 1 (https://entropy2018.sciencesconf.org/) et se prolongera dans la prochaine édition ENTROPY 2019 (https://entropy2019.sciencesconf.org/)..

Aussi, tout changement d'architecture ou d'organisation de ce TCB, même à bon escient, pourra, de la même façon, avoir des conséquences importantes et invalidantes pour la preuve initiale ou courante de validité du système logiciel dans son ensemble qu'il s'agira donc de ‘mettre à jour' dans les plus brefs délais. Cette recherche visera donc à proposer des stratégies de ‘mise à jour' de preuves mathématiques de systèmes d'exploitation vérifiables mécaniquement et à en évaluer la praticité.

Vous vous référerez à la section 3, « Le plus de l'offre » pour des informations détaillées sur la mission scientifique et les principales activités associées à la thèse.

about you

Pour mener à bien cette exploration, vous avez une bonne connaissance de la frontière Matériel/Logiciel dans les appareils numériques. Vous vous êtes particulièrement intéressé(e) pendant votre master d'informatique à la sécurité et à la programmation de cette frontière (architecture des Systèmes d'exploitation, des Hyperviseurs, etc …). Il est par ailleurs requis que vous ayez des notions et de l'intérêt pour les méthodes de la conception, de la preuve et de la vérification formelles de systèmes logiciels. Des connaissances de seL4 et de sa preuve seront un plus.

additional information

L'objectif de cette recherche est d'explorer concrètement et pratiquement les interrelations fonctionnelles et exploitables entre l'organisation/architecture du TCB et celles de la pile logicielle, de sa programmation et de sa preuve mathématique vérifiable.

Ces maîtrises des interrelations permettraient d'asseoir une meilleure et plus rapide résilience et adaptabilité des évolutions du TCB et du système (prise en compte nécessaire aux évolutions réciproques, pour maintenir la cohérence et correction de l'ensemble).

Cette exploration visera donc en particulier les éventuelles interrelations qui seraient semi-automatisables par outils et algorithmes permettant de les adapter plus facilement, à moindre coût et/ou plus rapidement aux changements. Concrètement la recherche se concentrera sur au moins deux cas précis et prouvés représentatifs du meilleur état de l'art publié, leurs preuves et leurs correspondants TCB et matériels de référence.

En synthèse, les objectifs de cette recherche comprennent :

·  la réalisation d'un état de l'art précis mais élargi des efforts industriels et académiques comparables/proches ;
·  l'exploration sérieuse de quelques pistes prometteuses d'automatisation de l'adaptation des preuves aux divers types de changements du TCB. Ces explorations seront menées sur au moins deux exemples publiés de systèmes d'exploitation prouvés faisant partie de l'état de l'art. L'un de ces systèmes sera seL4 (2)(3);
·  en fonction du succès de cette exploration : la définition et conception de propositions méthodologiques et algorithmiques précises et évaluables sur les exemples étudiés de systèmes d'exploitation prouvés.

A moyen terme cette ligne de recherche visera à la fois :

·  à rendre réellement utiles, adaptables et résilientes en environnement industriel -de l'IoT au Cloud- les méthodes de la preuve, de la vérification et de l'assurance formelles ;

Et à en étudier les limites pour mieux les contourner ou complémenter afin d'offrir une véritable sécurité de bout en bout.

department

Vous serez intégré.e au sein d'une équipe de recherche dynamique, à la fois pragmatique et créative. Vous participerez à un projet de recherche visant à contribuer solidement à la mise en place de méthodes de conception et de développement logicielles plus fiables permettant de construire un monde numérique respectant la sécurité de chacun.

Références :

1. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems. Février 2014, Vol. 32, 1, pp. 2:1-2:70.

2. seL4 specification and proofs, https://github.com/seL4/l4v.

3. Formal proof of dynamic memory isolation based on MMU. Narjes Jomaa, David Nowak, Gilles Grimaud, and Samuel Hym. [éd.] IEEE Computer Society. Shangai : s.n., 2016. 10th International Symposium on Theoretical Aspects of Software Engineering (TASE 2016). pp. 73-80.

4. Google, Project Zero team at. Lifting the (Hyper) Visor: Bypassing Samsung's Real-Time Kernel Protection. Google Project Zero. [En ligne] https://googleprojectzero.blogspot.fr/2017/02/lifting-hyper-visor-bypassing-samsungs.html.

5. Drammer: Deterministic Rowhammer Attacks on Mobile Platforms. V. van der Veen, Y. Fratantonio, M. Lindorfer, D. Gruss, C. Maurice, G. Vigna, H. Bos, K. Razavi, C. Giuffrida. s.l. : ACM, 2016. CCS'16.

6. Google, Project Zero team at. Reading privileged memory with a side-channel. Google Project Zero. [En ligne] https://googleprojectzero.blogspot.fr/2018/01/reading-privileged-memory-with-side.html.

contract

Thesis

Faire de chaque avenir une réussite.
  • Annuaire emplois
  • Annuaire entreprises
  • Événements