Vous êtes ici

Compilation sécurisée de services sous forme d’unikernels au moyen d’un langage système et de preuve automatique

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
team.inria.fr/tea
Directeur de thèse
Jean-Pierre Talpin
Co-directeur(s), co-encadrant(s)
Contact(s)
NomAdresse e-mailTéléphone
Jean-Pierre Talpin
talpin@irisa.fr
0299847436
Sujet de thèse
Descriptif


To minimize resource usage, energy consumption and exposure of services, system design in distribution grids, sensor networks, connected objects, employs methods to specialize a system library with the program that specifies its designated service on the target networked architecture or hypervisor: system programming.

The goal of our project is to explore, define and prototype, fundamental aspects toward the construction of safe and secure system programs in a possibly certified runtime environment:

• System stealth and security – services implemented using system programs boot fast and respond quickly (booting the service in parallel of the client's request). Minimized exposure paired with layered verification of inferred data and information flow properties of system programs make them ideal to device stealth and resilient network services.

• Architecture analysis and integration – Just as the AADL was initially designed to integrate ADA programs on embedded architecture, we seek the definition of a framework to structure the architecture system programs are integrated with, to define functional and non-functional characteristics relevant to that architecture, to check and optimize the allocation of the system program on the target architecture using contracts, interfaces.
 
• Type-based program analysis – we seek the use of value-dependent types subject to logical properties, e.g. liquid types or refinement types, to express functional properties (invariants about program values) as well as non-functional properties or effects, pertaining to the usage of resources (memory, system calls, communication, devices, hypervisor) to verify security policies, architecture integration, functional behavior.
 
Implementation of prototypes will be conducted using high-level programming languages such as Haskell or Ocaml. It will possibly reuse existing, open-source, implementations of refinement types, as well as powerful SAT/SMT solvers, such as Z3, to gain scalability.
 
A Master in Theoretical Computer Science with demonstrated experience in type theory, logic and verification, programming languages, operating systems, is a prerequisite for application. Good spoken and written scientific English will be beneficial, as well as demonstrated teamwork skills.

Bibliographie

Bibliographie

Sur le concept d’uni-kernels, l’excellent site http://unikernel.org liste les projets en lien avec cette approche. Le plus avancé est sans doute Mirage OS https://mirage.io, qui  permet de spécifier des scripts de service en Ocaml puis de les compiler sous la forme de systèmes bootables (voir l’exemple de “hello world” en 10 lignes: https://mirage.io/wiki/hello-world).  D’autres projets utilisent Javascript, des langages dédiés comme Go et sa variante temps-réel The Go Programming Language, ou bien encore le langage système Rust https://www.rust-lang.org.  

Il existe également d’importants projets apparentés : SeL4, CertiKOS, Cogent, Pip ; visant à certifier des noyaux système, et par rapport auxquels définir les contributions de la thèse. Dans le cadre du projet, nous nous attacherons avant tout à utiliser les outils de programmation (Liquid Haskell, Rust) et les librairies système (Mirage OS, Rump) les mieux adaptées aux objectifs de recherche envisagés.

Début des travaux: 
Dès que possible/ As soon as possible
Mots clés: 
systèmes en librairie, théorie des types par rafinnement, analyse, vérification automatique et preuve de programme
Lieu: 
IRISA - Campus universitaire de Beaulieu, Rennes