Después de ocho años de desarrollo, se ha lanzado el proyecto Muen 1.0, que desarrolla un núcleo de separación (Separation kernel), cuya ausencia de errores en los textos fuente ha sido confirmada mediante métodos matemáticos de verificación formal de fiabilidad. El núcleo está disponible para la arquitectura x86_64 y puede ser utilizado en sistemas críticos que requieren un alto nivel de fiabilidad y garantía de ausencia de fallos. Los textos fuente del proyecto están escritos en Ada y su dialecto verificable SPARK 2014. El código se distribuye bajo la licencia GPLv3.
El núcleo de separación es un microkernel que proporciona un entorno para la ejecución de componentes aislados entre sí, cuya interacción está estrictamente regulada por reglas establecidas. La aislamiento se basa en el uso de extensiones de virtualización Intel VT-x y prevé mecanismos de protección para bloquear la creación de canales de comunicación ocultos. El núcleo de separación es más minimalista y estático en comparación con otros microkernels, lo que permite reducir la cantidad de situaciones que podrían llevar a fallos.
El núcleo se ejecuta en modo raíz VMX, al igual que un hipervisor, mientras que todos los demás componentes se ejecutan en modo no raíz VMX, similar a los sistemas invitados. El acceso al hardware se realiza utilizando extensiones Intel VT-d DMA y re-mapeo de interrupciones, lo que permite implementar un enlace seguro de dispositivos PCI a los componentes que se ejecutan bajo Muen.
Entre las capacidades de Muen se destacan el soporte para sistemas multinúcleo, páginas de memoria anidadas (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), y tablas de atributos de páginas de memoria (PAT, Page Attribute Table). Muen también proporciona un planificador cíclico fijo basado en un temporizador de reemplazo Intel VMX, un runtime compacto que no afecta el rendimiento, un sistema de auditoría de fallos, un mecanismo de asignación estática de recursos basado en reglas, un sistema de manejo de eventos y canales de memoria compartida para la interacción dentro de los componentes en ejecución.
Se admite la ejecución de componentes con código de máquina de 64 bits, 32 o 64 bits máquinas virtuales, 64 bits de aplicaciones en Ada y SPARK 2014, máquinas virtuales con Linux y "unikernels" autosuficientes basados en MirageOS.
Las principales innovaciones presentadas en la versión Muen 1.0:
- Se han publicado documentos con las especificaciones del núcleo (diseño y arquitectura), sistema (políticas del sistema, Tau0 y herramientas) y componentes, donde se documentan todos los aspectos del funcionamiento del proyecto.
- Se ha añadido la herramienta Tau0 (Muen System Composer), que incluye un conjunto de componentes verificados listos para ser utilizados en la composición de imágenes de sistema y el desarrollo de servicios estándar que se ejecutan sobre Muen. Entre los componentes ofrecidos se encuentran el controlador AHCI (SATA), el Administrador de Dispositivos (DM), el gestor de arranque, el gestor del sistema, el terminal virtual, entre otros.
- El controlador de Linux muenblock (implementación de un dispositivo de bloque que opera sobre la memoria compartida de Muen) ha sido adaptado para usar la API blockdev 2.0.
- Se han implementado herramientas para gestionar el ciclo de vida de componentes nativos.
- Las imágenes de sistema han sido adaptadas para utilizar SBS (Signed Block Stream) y CSL (Command Stream Loader) para proteger su integridad.
- Se ha implementado un controlador verificado AHCI-DRV, escrito en el lenguaje SPARK 2014 y que permite conectar dispositivos de almacenamiento que soportan la interfaz ATA o particiones de disco individuales.
- Se ha mejorado el soporte para unikernel de los proyectos MirageOS y Solo5.
- La herramienta para el lenguaje Ada se ha actualizado a la versión GNAT Community 2021.
- El sistema de integración continua ha sido trasladado de un emulador Bochs a entornos anidados QEMU/KVM.
- En las imágenes de componentes de Linux se ha utilizado el núcleo Linux 5.4.66.
Fuente: opennet.ru
