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

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

  • Par Orange
  • Thèse
  • Paris (Paris)

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 (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 la vulnérabilité découverte récemment par le Project Zero de Google, Spectre/Meltdown (9), 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)), voire 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/).

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);
·  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. Why Software Is Eating The World. Andreessen, Marc. 2011, The Wall Street Journal.

2. 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.

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. From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. Chlipala, Adam. s.l. : ACM, 2015. POPL'15.

7. Mathy Vanhoef, F. P. (2017). Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2. CCS'17, October 30-November 3, 2017, Dallas, TX, USA. Dallas: ACM.

8. Changhua He, M. S. (2005). A Modular Correctness Proof of IEEE 802.11i and TLS. CCS'05, November 7-11, 2005, Alexandria, Virginia, USA. Alexandria: ACM

contract

Thesis
Reçois les offres qui te correspondent par email !
Des milliers de jobs sont disponibles pour toi sur Wizbii :)

À propos de Orange

Orange est le leader de la télécommunication en France en couvrant les services de communication résidentiels, personnels et d'entreprise. En Europe, Afrique et Moyen Orient, Orange est présent dans 34 pays à travers le monde.

Animé par près de 155 000 personnes, le groupe Orange sert plus de 247 millions de clients à travers le monde. Tous ces collaborateurs ont chacun une responsabilité particulière qui est d'accompagner au mieux les clients face à leurs habitudes numériques. Que vous soyez un homme ou une femme, Orange se bat pour rendre accessible à tous des opportunités de carrière et même au plus jeunes pour leur offrir une première expérience significative.

La société offre une pléiades de métiers autour de la télécommunication et en particulier dans les pôles vente, système et réseaux de communication, recherche et développement et marketing. Parmi les offres à pourvoir, Orange recherche des commerciaux et responsables en boutique ainsi que de nombreux conseillers clientèle. Mais aussi des consultants, ingénieurs commerciaux, architectes réseaux, chefs de produit, spécialistes big data et bien d'autres !

Si vous êtes à la recherche d'une alternance (plus de 3000 rien qu'en France), Orange met en place un système de suivi grâce à un tuteur qui accompagnera vos missions au quotidien. Orange, certifié Top Employeur Europe 2015, saura vous offrir une place de choix au sein de l'entreprise, en France et à l'étranger en fonction de vos projets professionnels pour exercer tous vos talents.

Rejoignez-nous et soyez au coeur d'une nouvelle expérience client.

1391 jobs disponibles chez Orange

Trouve ton futur job sur Wizbii,
la 1ère plateforme professionnelle pour l’emploi des jeunes

Offres d'emploi

Ton job dans la poche
Télécharger