Después de ocho años de desarrollo, se lanzó el proyecto Muen 1.0, que desarrolla el kernel Separation, cuya ausencia de errores en el código fuente se confirmó mediante métodos matemáticos de verificación formal de confiabilidad. El kernel está disponible para la arquitectura x86_64 y puede usarse en sistemas de misión crítica que requieren un mayor nivel de confiabilidad y garantía de ausencia de fallas. El código fuente del proyecto está escrito en el lenguaje Ada y su dialecto verificable SPARK 2014. El código se distribuye bajo la licencia GPLv3.
El núcleo de separación es un micronúcleo que proporciona un entorno para la ejecución de componentes aislados entre sí, cuya interacción está estrictamente regulada por reglas determinadas. El aislamiento se basa en el uso de extensiones de virtualización Intel VT-x e incluye mecanismos de seguridad para bloquear la organización de canales de comunicación encubiertos. El kernel de partición es más minimalista y estático que otros microkernels, lo que reduce la cantidad de situaciones que pueden causar fallas.
El kernel se ejecuta en modo raíz VMX, similar a un hipervisor, y todos los demás componentes se ejecutan en modo no raíz VMX, similar a los sistemas invitados. El acceso al equipo se realiza mediante extensiones Intel VT-d DMA y reasignación de interrupciones, lo que permite implementar un enlace seguro de dispositivos PCI a componentes que se ejecutan en Muen.
Las capacidades de Muen incluyen soporte para sistemas multinúcleo, páginas de memoria anidadas (EPT, tablas de páginas extendidas), MSI (interrupciones señalizadas de mensajes) y tablas de atributos de páginas de memoria (PAT, tabla de atributos de página). Muen también proporciona un programador rotativo fijo basado en el temporizador preventivo Intel VMX, 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 comunicación dentro de los componentes en ejecución.
Admite la ejecución de componentes con código de máquina 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 Linux y "unikernels" autónomos basados en MirageOS sobre Muen.
Las principales innovaciones ofrecidas en el lanzamiento de Muen 1.0:
- Se han publicado documentos con especificaciones para el kernel (dispositivo y arquitectura), el sistema (políticas del sistema, Tau0 y kit de herramientas) y componentes, que documentan todos los aspectos del proyecto.
- Se ha agregado el kit de herramientas Tau0 (Muen System Composer), que incluye un conjunto de componentes verificados listos para usar para componer imágenes del sistema y desarrollar servicios estándar que se ejecutan sobre Muen. Los componentes proporcionados incluyen el controlador AHCI (SATA), el administrador de dispositivos (DM), el cargador de arranque, el administrador del sistema, el terminal virtual, etc.
- El controlador muenblock Linux (una implementación de un dispositivo de bloque que se ejecuta sobre la memoria compartida de Muen) se ha convertido para utilizar la API blockdev 2.0.
- Herramientas implementadas para la gestión del ciclo de vida de componentes nativos.
- Las imágenes del sistema se han convertido para utilizar SBS (Signed Block Stream) y CSL (Command Stream Loader) para proteger la integridad.
- Se implementó un controlador AHCI-DRV verificado, escrito en el lenguaje SPARK 2014 y que le permite conectar unidades que admiten la interfaz ATA o particiones de disco individuales a los componentes.
- Soporte unikernel mejorado de los proyectos MirageOS y Solo5.
- El kit de herramientas del lenguaje Ada se actualizó para la versión GNAT Community 2021.
- El sistema de integración continua se ha transferido del emulador de Bochs a entornos anidados QEMU/KVM.
- Las imágenes de componentes de Linux utilizan el kernel Linux 5.4.66.
Fuente: opennet.ru