Stage Exploration de la résilience de la preuve de l'OS seL4 aux modifications de son code et de son architecture (F/H)

Description de l'offre

about the role

Sous la responsabilité d'un ingénieur de recherche, le stagiaire mènera l'analyse, l'exploration et la prise en main concrète de la preuve de l'OS seL4, dans le cadre d'un projet de recherche sur l'exploration des interrelations entre Trusted Computing Base et preuves de systèmes (étude des Systèmes Logiciels prouvés à la frontière Matériel/Logiciel).

Le stagiaire prendra en main la preuve de l'OS seL4

[1,2] pour essayer d'infirmer ou de confirmer les dires du chercheur Adam Chlipala quant à la fragilité et la non résilience de celle-ci, en cas de modification de seL4: « The most recent impressive system verifications are not modular. The L4.verified and Verve projects have both verified operating-system kernels with different semi-automated proof tools. Their proofs are structured around global invariants relating all states of all system components, both in the kernel and in relevant parts of applications. When one part of a kernel changes, the global invariant must often be modified, and the proofs of all other components must be reconsidered.”

[3] Après l'avoir assimilée, le stagiaire procédera à l'évaluation des modifications nécessaires de la preuve actuelle, suite à des modifications consistantes et localisées du code de seL4. Au terme de cette exploration il tentera de les rapprocher des commentaires d'Adam Chlipala ci-dessus. S'il lui reste du temps il pourra se concentrer sur le modèle hardware dans Isabelle, sa fidélité au hardware réel et sur les modifications du code non-prouvé de seL4

[4,5]. Mots clés : seL4, OS (Système d'exploitation), micro-noyau, Preuve, Isabelle, TCB, Hardware model.

Références bibliographiques :

[1] Preuve de seL4 sur github, https://github.com/seL4/l4v

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

[4] David Cock. Leakage in Trustworthy Systems. Phd thesis, Computer Science and Engineering, Sydney, Australia, August 2014.

[5] seL4 Proof statistics, https://ts.data61.csiro.au/projects/TS/l4.verified/numbers.pml

about you

Master 2 Recherche en Informatique ou équivalent.
Le stagiaire a acquis des connaissances d'architecture des systèmes d'exploitation et des outils et principes de la preuve de systèmes logiciels. Une première connaissance du micro-noyau seL4, d'Isabelle et les autres outils utilisés dans sa preuve seront appréciées.

department

Le département Sécurité (SEC) d'Orange Labs Services propose des solutions innovantes pour protéger les réseaux et services du Groupe Orange, ainsi que les données de ses clients ; il accompagne les projets du Groupe dans leur démarche de gestion des risques de sécurité. Il développe et maintient pour cela une expertise de référence sur toutes les technologies utilisées par l'opérateur : réseau, cloud, systèmes, cryptographie, etc. à travers des activités de Recherche et de Développement.

contract

Internship

Duration : 6 months

Level : Master 2