Forum

SafeOS: un OS entièrement safe



On sait depuis un moment que chez Microsoft l'avenir s'inscrit autour des langages managés. De nombreux articles ont déjà été publiés à propos du projet Singularity.



L'un des buts de Singularity est de créer un safe OS . Un OS est dit safe quand il est type safe et memory safe. De nombreux types de bugs comme les buffers overflow (à l'origine de nombreuses failles dans les systèmes actuels) disparaissent. C'est aussi un prérequis pour pouvoir créer un OS entièrement sécurisé. Le problème de Singularity est qu'il n'est justement pas totalement safe. Les applications et le noyau dans sa plus grande partie sont compilés depuis des langages managés en TAL (Typed assembly language) au moyen de Bartok. Le code est donc entièrement safe à l'exception d'une petite partie qui reste en code natif. C'est entre autres le cas de la HAL (Hardware Abstraction Layer), un mélange de code C et d'assembleur qui assure l'interface entre le matériel et le noyau.



SafeOS, or a similar operating system constructed using the “Automated, Static Safety Verifier”, includes a “Nucleus” that provides access to hardware and memory, a “kernel” that builds services on top of the Nucleus, and applications that run on top of the kernel. The Nucleus, written in verified assembly language, implements allocation, garbage collection, multiple stacks, interrupt handling, and device access. The kernel, written in C# (or other language) and compiled to TAL, builds higher-level services, such as preemptive threads, on top of the Nucleus. A TAL checker then verifies the safety of the kernel and applications. Finally, a Hoare-style verifier with an automated theorem prover verifies both the safety and correctness of the Nucleus.

Depuis quelques mois dans les sources de Singularity (dossier verify) on peut trouver le projet VERVE. Un brevet a également été déposé sous le nom de code SafeOS. Ce projet est mené par Jean Yang du MIT (Massachusetts Institute of Technology) et Chris Hawblitzel de MSR (Microsoft Research). Ce système est présenté comme safe de bout en bout. L'idée est de placer toutes les primitives en langage natif dans un composant baptisé nucleus et de faire reposer un noyau compilé en TAL sur ce dernier. Le code du nucleus est compilé en assembleur à partir de code BoogiePL. Boogie est un langage de vérification formel utilisant la logique de Hoare: c'est-à-dire que des outils mathématiques vérifient dans le langage formel BoogiePL que le code est safe. Cet outil ainsi que Z3 (un composant interne de BoogiePL) sont liés à plusieurs projets de formalisation de code chez MS. Ils sont par ailleurs utilisés par Spec# un language dérivé de C# servant à spécifier les communications interprocess dans Singularity. Ils sont aussi utilisés pour vérifier le code de l'hyperviseur Hyper-V. Certains outils de vérification de code des drivers utiliseraient aussi Z3. Pour le moment SafeOS est un système très minimaliste incompatible avec Singularity. Mais je pense que Microsoft pourrait l'adapter pour l'utiliser avec Singularity.

Sources: brevet safeOS Projet verve Présentation Verve Sources code Singularity et Verve

Ça me semble utopique comme concept, mais bon, s'ils y arrivent, tant mieux.