{"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\/en\/blog\/news\/vypusk-muen-1-0-otkrytogo-mikroyadra-dlya-sozdaniya-vysokonadyozhnyh-sistem","title":{"rendered":"Release of Muen 1.0, an open microkernel for creating highly reliable systems","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"

After eight years of development, the Muen 1.0 project, which advances the separation kernel, has been released. The absence of errors in the source texts has been confirmed using mathematical methods of formal verification of reliability. The kernel is available for the x86_64 architecture and can be used in mission-critical systems that require a high level of reliability and guaranteed faultlessness. The project's source texts are written in Ada and its verifiable dialect SPARK 2014. The code is distributed under the GPLv3 license. <\/p>\n

The separation kernel is a microkernel that provides an environment for executing isolated components, whose interactions are strictly governed by specified rules. The isolation relies on Intel VT-x virtualization extensions and includes mechanisms to block the organization of covert communication channels. The separation kernel is more minimalist and static compared to other microkernels, which helps reduce the number of situations that could lead to failures. <\/p>\n

The kernel operates in VMX root mode similar to a hypervisor, while all other components run in VMX non-root mode akin to guest systems. Access to hardware is achieved using Intel VT-d DMA extensions and interrupt remapping, allowing for secure binding of PCI devices to components running under Muen.

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

Muen supports multicore systems, nested page tables (EPT), Message Signaled Interrupts (MSI), and Page Attribute Tables (PAT). Muen also features a fixed cyclic scheduler based on the preemptive timer from Intel VMX, a compact runtime that does not affect performance, a crash auditing system, a rule-based static resource allocation mechanism, an event handling system, and shared memory channels for interaction within the running components. <\/p>\n

It supports running components with 64-bit machine code, 32- or 64-bit applications in Ada and SPARK 2014, Linux virtual machines, and self-contained unikernels based on MirageOS. of virtual machines<\/a>, 64-bit applications in Ada and SPARK 2014, virtual machines with Linux, and self-sufficient 'unikernel' based on MirageOS. <\/p>\n

The main innovations introduced in the Muen 1.0 release: <\/p>\n