Après huit années de développement, le projet Muen 1.0 est sorti, développant le noyau Separation, dont l'absence d'erreurs dans le code source a été confirmée à l'aide de méthodes mathématiques de vérification formelle de la fiabilité. Le noyau est disponible pour l'architecture x86_64 et peut être utilisé dans des systèmes critiques qui nécessitent un niveau de fiabilité accru et une garantie d'absence de panne. Le code source du projet est écrit dans le langage Ada et son dialecte vérifiable SPARK 2014. Le code est distribué sous licence GPLv3.
Le noyau de séparation est un micro-noyau qui fournit un environnement d'exécution de composants isolés les uns des autres, dont l'interaction est strictement réglementée par des règles données. L'isolation est basée sur l'utilisation des extensions de virtualisation Intel VT-x et comprend des mécanismes de sécurité pour bloquer l'organisation des canaux de communication secrets. Le noyau de partitionnement est plus minimaliste et statique que les autres micro-noyaux, ce qui réduit le nombre de situations pouvant provoquer des échecs.
Le noyau s'exécute en mode racine VMX, similaire à un hyperviseur, et tous les autres composants s'exécutent en mode VMX non root, similaire aux systèmes invités. L'accès à l'équipement se fait à l'aide des extensions Intel VT-d DMA et du remappage des interruptions, ce qui permet de mettre en œuvre une liaison sécurisée des périphériques PCI aux composants fonctionnant sous Muen.
Les capacités de Muen incluent la prise en charge des systèmes multicœurs, des pages de mémoire imbriquées (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) et des tables d'attributs de pages de mémoire (PAT, Page Attribute Table). Muen fournit également un planificateur circulaire fixe basé sur le minuteur préemptif Intel VMX, un environnement d'exécution compact qui n'a pas d'impact sur les performances, un système d'audit des pannes, un mécanisme d'affectation de ressources statiques basé sur des règles, un système de gestion des événements et des canaux de mémoire partagée pour communication au sein des composants en cours d’exécution.
Il prend en charge l'exécution de composants avec du code machine 64 bits, des machines virtuelles 32 ou 64 bits, des applications 64 bits dans les langages Ada et SPARK 2014, des machines virtuelles Linux et des « unikernels » autonomes basés sur MirageOS au-dessus de Muen.
Les principales innovations proposées dans la sortie de Muen 1.0 :
- Des documents ont été publiés avec des spécifications pour le noyau (périphérique et architecture), le système (politiques système, Tau0 et boîte à outils) et les composants, qui documentent tous les aspects du projet.
- La boîte à outils Tau0 (Muen System Composer) a été ajoutée, qui comprend un ensemble de composants vérifiés prêts à l'emploi pour composer des images système et développer des services standard qui s'exécutent sur Muen. Les composants fournis incluent le pilote AHCI (SATA), le gestionnaire de périphériques (DM), le chargeur de démarrage, le gestionnaire système, le terminal virtuel, etc.
- Le pilote Linux muenblock (une implémentation d'un périphérique bloc fonctionnant au-dessus de la mémoire partagée Muen) a été converti pour utiliser l'API blockdev 2.0.
- Implémentation d'outils de gestion du cycle de vie des composants natifs.
- Les images système ont été converties pour utiliser SBS (Signed Block Stream) et CSL (Command Stream Loader) pour protéger l'intégrité.
- Un pilote AHCI-DRV vérifié a été implémenté, écrit dans le langage SPARK 2014 et vous permettant de connecter des lecteurs prenant en charge l'interface ATA ou des partitions de disque individuelles aux composants.
- Prise en charge unikernel améliorée des projets MirageOS et Solo5.
- La boîte à outils du langage Ada a été mise à jour pour la version GNAT Community 2021.
- Le système d'intégration continue a été transféré de l'émulateur Bochs vers les environnements imbriqués QEMU/KVM.
- Les images de composants Linux utilisent le noyau Linux 5.4.66.
Source: opennet.ru