Después de ocho años de desarrollo Muen 1.0 El proyecto fue Aprobado, Desarrollo de Núcleo de separacióncuya corrección en el código fuente ha sido confirmada utilizando métodos matemáticos para la verificación formal de la confiabilidad. El kernel está disponible para la arquitectura x86_64 y puede usarse en sistemas críticos para el negocio que requieren un mayor nivel de confiabilidad y garantizan la ausencia de fallas. Los textos fuente del proyecto están escritos en lengua Ada y su dialecto verificable. CHISPA 2014 . El codigo es repartido bajo la licencia GPLv3.
El núcleo de partición es un microkernel que proporciona un entorno para la ejecución de componentes mutuamente aislados, cuya interacción está estrictamente regulada por reglas definidas. El aislamiento se basa en el uso de Intel VT-x La virtualización amplía y contiene mecanismos de protección para bloquear la organización de canales de comunicación ocultos. El kernel de partición es más minimalista y estático que otros microkernels, lo que reduce la cantidad de situaciones que pueden conducir a fallas.
El kernel se ejecuta en Modo raíz VMX , similar a un hipervisor, y todos los demás componentes en modo VMX no root, similar a los sistemas invitados. El acceso al hardware se realiza a través de expansiones Intel VT-d DMA y reasignación de interrupciones, mediante el cual se puede implementar una conexión segura de dispositivos PCI a componentes que se ejecutan bajo el control de Muen.
Muen proporciona soporte para sistemas multinúcleo, páginas de memoria anidadas ( EPT , Tablas de páginas extendidas), MSI (interrupciones señalizadas por mensaje), tablas de atributos de páginas de memoria ( DERROTAR , Tabla de atributos de página). Muen también ofrece un programador de bucle fijo basado en Intel VMX Preemptive Timer, un tiempo de ejecución compacto que no afecta el rendimiento, un sistema de auditoría de fallas, un mecanismo de asignación de recursos estáticos basado en reglas, un sistema de manejo de eventos y canales de memoria compartida para la comunicación durante el inicio. Componentes.
MX Linux 21 se carga en Debian 11 para ofrecer su versión más pulida hasta el momento
Admite la ejecución en componentes Muen con código nativo de 64 bits, máquinas virtuales de 32 o 64 bits, aplicaciones de 64 bits en los lenguajes Ada y SPARK 2014, máquinas virtuales con Linux y «Unikernel» independiente basado en MirageOS .
Las principales innovaciones propuestas en la versión de Muen 1.0 son:
- Documentos con las especificaciones del. liberado Núcleo (Dispositivo y arquitectura), Sistemas (Pautas del sistema, Tau0 y Toolkit) y Componentes documentar todos los aspectos del proyecto.
- los Año0 (Muen System Composer) Se creó el kit de herramientas adicional que contiene una serie de componentes verificados prediseñados para crear imágenes del sistema y desarrollar servicios típicos que se ejecutan en Muen. Los componentes proporcionados incluyen controlador AHCI (SATA), administrador de dispositivos (DM), cargador de arranque, administrador del sistema, terminal virtual, etc.
- los Muenblock El controlador de Linux (una implementación de un dispositivo de bloque que se ejecuta en la memoria compartida de Muen) se ha movido para usar la API blockdev 2.0.
- Implementamos herramientas para gestionar el ciclo de vida de los componentes nativos.
- Las imágenes del sistema se han convertido para su uso SBS (Signed Block Stream) y CSL (Command Stream Loader) para la protección de la integridad.
- Se implementó un controlador AHCI-DRV verificado escrito en SPARK 2014, que permite que las unidades que admiten la interfaz ATA o particiones de disco duro separadas se conecten a los componentes.
- Mejorado unikernel Soporte de MirageOS y Proyectos Solo5.
- Hell Language Toolkit se ha actualizado para la versión GNAT Community 2021.
- El sistema de integración continua se transfirió del emulador de Bochs a los entornos anidados QEMU / KVM.
- Las imágenes de los componentes de Linux utilizan el kernel de Linux 5.4.66.
