Après huit ans de développement, le projet Muen 1.0, qui développe un noyau de séparation (Separation kernel), a vu le jour. L'absence d'erreurs dans le code source a été vérifiée à l'aide de méthodes mathématiques de vérification formelle de fiabilité. Le noyau est disponible pour l'architecture x86_64 et peut être utilisé dans des systèmes critiques nécessitant un niveau de fiabilité élevé et des garanties sur l'absence de pannes. Les codes sources du projet sont écrits en Ada et son dialecte vérifiable SPARK 2014. Le code est distribué sous la licence GPLv3.
Le noyau de séparation est un micro-noyau qui offre un environnement d'exécution pour des composants isolés les uns des autres, dont les interactions sont strictement régulées par des règles définies. L'isolation repose sur l'utilisation des extensions de virtualisation Intel VT-x et inclut des mécanismes de protection pour bloquer l'organisation de canaux de communication cachés. Le noyau de séparation est plus minimaliste et statique par rapport à d'autres micro-noyaux, ce qui permet de réduire le nombre de situations susceptibles de provoquer des pannes.
Le noyau s'exécute en mode racine VMX, à l'instar d'un hyperviseur, tandis que tous les autres composants s'exécutent en mode non racine VMX, comparativement aux systèmes invités. L'accès au matériel se fait en utilisant les extensions Intel VT-d DMA et le remappage des interruptions, ce qui permet de réaliser un couplage sécurisé des dispositifs PCI avec les composants gérés par Muen.
Parmi les fonctionnalités de Muen, on note le support des systèmes multi-cœurs, des pages de mémoire imbriquées (EPT, Extended Page Tables), des MSI (Message Signaled Interrupts), et des tables d'attributs de pages mémoire (PAT, Page Attribute Table). Muen fournit également un planificateur cyclique fixe basé sur le timer préemptif Intel VMX, un runtime compact qui n'impacte pas la performance, un système d'audit des pannes, un mécanisme d'attribution statique des ressources basé sur des règles, un système de traitement des événements et des canaux de mémoire partagée pour l'interaction entre les composants exécutés.
Le démarrage des composants Muen avec du code machine de 64 bits, 32 ou 64 bits est pris en charge. machines virtuelles, des applications de 64 bits en Ada et SPARK 2014, des machines virtuelles avec Linux et des « unikernel » autonomes basés sur MirageOS.
Les principales nouveautés proposées dans la version Muen 1.0 :
- Des documents contenant les spécifications du noyau (disposition et architecture), du système (politiques système, Tau0 et outils) et des composants, dans lesquels tous les aspects du projet sont documentés, ont été publiés.
- L'outil Tau0 (Muen System Composer) a été ajouté, comprenant un ensemble de composants vérifiés prêts à l'emploi pour l'assemblage d'images système et le développement de services standard exécutés sur Muen. Parmi les composants fournis figurent le pilote AHCI (SATA), le gestionnaire de périphériques (DM), le chargeur de démarrage, le gestionnaire système, un terminal virtuel, etc.
- Le pilote Linux muenblock (implémentation d'un dispositif de bloc fonctionnant sur la mémoire partagée Muen) a été adapté pour utiliser l'API blockdev 2.0.
- Des outils ont été réalisés pour gérer le cycle de vie des composants natifs.
- Les images système ont été adaptées pour utiliser SBS (Signed Block Stream) et CSL (Command Stream Loader) pour protéger l'intégrité.
- Un pilote AHCI-DRV vérifié, écrit en SPARK 2014, a été développé pour permettre la connexion de dispositifs prenant en charge l'interface ATA, ou de partitions de disque séparées, aux composants.
- Le support de unikernel des projets MirageOS et Solo5 a été amélioré.
- L'outil pour le langage Ada a été mis à jour à la version GNAT Community 2021.
- Le système d'intégration continue a été transféré de l'émulateur Bochs aux environnements imbriqués QEMU/KVM.
- Les images des composants avec Linux utilisent le noyau Linux 5.4.66.
Source : opennet.ru
