{"id":101775,"date":"2021-10-25T22:22:37","date_gmt":"2021-10-25T20:22:37","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/vypusk-muen-1-0-otkrytogo-mikroyadra-dlya-sozdaniya-vysokonadyozhnyh-sistem"},"modified":"2021-10-25T22:22:37","modified_gmt":"2021-10-25T20:22:37","slug":"vypusk-muen-1-0-otkrytogo-mikroyadra-dlya-sozdaniya-vysokonadyozhnyh-sistem","status":"publish","type":"post","link":"https:\/\/prohoster.info\/fr\/blog\/news\/vypusk-muen-1-0-otkrytogo-mikroyadra-dlya-sozdaniya-vysokonadyozhnyh-sistem","title":{"rendered":"Sortie de Muen 1.0, un micro-noyau open source pour cr\u00e9er des syst\u00e8mes hautement fiables","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Apr\u00e8s huit ans de d\u00e9veloppement, le projet Muen 1.0, qui d\u00e9veloppe un noyau de s\u00e9paration (Separation kernel), a vu le jour. L'absence d'erreurs dans le code source a \u00e9t\u00e9 v\u00e9rifi\u00e9e \u00e0 l'aide de m\u00e9thodes math\u00e9matiques de v\u00e9rification formelle de fiabilit\u00e9. Le noyau est disponible pour l'architecture x86_64 et peut \u00eatre utilis\u00e9 dans des syst\u00e8mes critiques n\u00e9cessitant un niveau de fiabilit\u00e9 \u00e9lev\u00e9 et des garanties sur l'absence de pannes. Les codes sources du projet sont \u00e9crits en Ada et son dialecte v\u00e9rifiable SPARK 2014. Le code est distribu\u00e9 sous la licence GPLv3. <\/p>\n
Le noyau de s\u00e9paration est un micro-noyau qui offre un environnement d'ex\u00e9cution pour des composants isol\u00e9s les uns des autres, dont les interactions sont strictement r\u00e9gul\u00e9es par des r\u00e8gles d\u00e9finies. L'isolation repose sur l'utilisation des extensions de virtualisation Intel VT-x et inclut des m\u00e9canismes de protection pour bloquer l'organisation de canaux de communication cach\u00e9s. Le noyau de s\u00e9paration est plus minimaliste et statique par rapport \u00e0 d'autres micro-noyaux, ce qui permet de r\u00e9duire le nombre de situations susceptibles de provoquer des pannes. <\/p>\n
Le noyau s'ex\u00e9cute en mode racine VMX, \u00e0 l'instar d'un hyperviseur, tandis que tous les autres composants s'ex\u00e9cutent en mode non racine VMX, comparativement aux syst\u00e8mes invit\u00e9s. L'acc\u00e8s au mat\u00e9riel se fait en utilisant les extensions Intel VT-d DMA et le remappage des interruptions, ce qui permet de r\u00e9aliser un couplage s\u00e9curis\u00e9 des dispositifs PCI avec les composants g\u00e9r\u00e9s par Muen.
<\/center> <\/p>\n
Parmi les fonctionnalit\u00e9s de Muen, on note le support des syst\u00e8mes multi-c\u0153urs, des pages de m\u00e9moire imbriqu\u00e9es (EPT, Extended Page Tables), des MSI (Message Signaled Interrupts), et des tables d'attributs de pages m\u00e9moire (PAT, Page Attribute Table). Muen fournit \u00e9galement un planificateur cyclique fixe bas\u00e9 sur le timer pr\u00e9emptif Intel VMX, un runtime compact qui n'impacte pas la performance, un syst\u00e8me d'audit des pannes, un m\u00e9canisme d'attribution statique des ressources bas\u00e9 sur des r\u00e8gles, un syst\u00e8me de traitement des \u00e9v\u00e9nements et des canaux de m\u00e9moire partag\u00e9e pour l'interaction entre les composants ex\u00e9cut\u00e9s. <\/p>\n
![\"Sortie](\"\/wp-content\/uploads\/2021\/10\/bd30e656326f6fd3667eec5773341420.jpg\")
<\/center> <\/p>\n