{"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\/nl\/blog\/news\/vypusk-muen-1-0-otkrytogo-mikroyadra-dlya-sozdaniya-vysokonadyozhnyh-sistem","title":{"rendered":"De release van Muen 1.0, een open microkernel voor het cre\u00ebren van hoog betrouwbare systemen","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"

Na acht jaar ontwikkeling is de release van het Muen 1.0-project een feit, dat de core separation (scheidingkernel) ontwikkelt, waarvan de afwezigheid van fouten in de bronbestanden is bevestigd met behulp van mathematische methoden voor formele verificatie van betrouwbaarheid. De kernel is beschikbaar voor de x86_64-architectuur en kan worden toegepast in kritieke systemen die een verhoogd niveau van betrouwbaarheid vereisen en garanties bieden voor het ontbreken van storingen. De bronbestanden van het project zijn geschreven in de Ada-taal en zijn verifieerbare dialect SPARK 2014. De code wordt verspreid onder de GPLv3-licentie. <\/p>\n

De scheidingkernel is een microkernel die een omgeving biedt voor de uitvoering van van elkaar ge\u00efsoleerde componenten, waarvan de interactie streng wordt gereguleerd door vastgestelde regels. De isolatie is gebaseerd op het gebruik van Intel VT-x virtualisatie-extensies en omvat ook mechanismen voor bescherming tegen het cre\u00ebren van verborgen communicatiekanalen. De scheidingkernel is minimalistisch en statisch in vergelijking met andere microkernels, wat het aantal situaties dat tot een storing kan leiden vermindert. <\/p>\n

De kernel draait in VMX-rootmodus, vergelijkbaar met een hypervisor, en alle andere componenten in non-root VMX-modus, vergelijkbaar met gastsystemen. Toegang tot de hardware wordt verkregen met behulp van Intel VT-d DMA-extensies en interrupt-remapping, wat veilige binding van PCI-apparaten aan componenten die onder Muen draaien mogelijk maakt.

\"De<\/center> <\/p>\n

Onder de mogelijkheden van Muen wordt de ondersteuning voor multicore-systemen, geneste paginatabellen (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), en paginattributentabellen (PAT, Page Attribute Table) benadrukt. Muen biedt ook een vaste cyclusplaner op basis van de preemptive timer van Intel VMX, een compacte runtime die de prestaties niet be\u00efnvloedt, een crashaudit-systeem, een mechanisme voor statische toewijzing van middelen op basis van regels, een gebeurtenisverwerkingsysteem en kanalen voor gedeeld geheugen voor interactie binnen de draaiende componenten. <\/p>\n

Het is mogelijk om Muen-componenten te draaien met 64-bits machinecode, 32- of 64-bits virtuele machines<\/a>, 64-bits applicaties in de talen Ada en SPARK 2014, virtuele machines met Linux en zelfvoorzienende \u00abunikernel\u00bb op basis van MirageOS. <\/p>\n

De belangrijkste vernieuwingen die in de release van Muen 1.0 zijn voorgesteld: <\/p>\n