Familia de microkernels L4

L4 es una familia de microkernels de segunda generación , utilizados para implementar diversos tipos de sistemas operativos (SO), aunque principalmente para tipos similares a Unix y compatibles con la interfaz de sistema operativo portátil ( POSIX ).

L4, al igual que su predecesor, el microkernel L3 , fue creado por el científico informático alemán Jochen Liedtke como respuesta al bajo rendimiento de los sistemas operativos basados ​​en microkernels anteriores. Liedtke creía que un sistema diseñado desde el principio para un alto rendimiento, en lugar de otros objetivos, podría producir un microkernel de utilidad práctica. Su implementación original en código ensamblador específico para Intel i386, escrito a mano en 1993, llamó la atención por ser 20 veces más rápido que Mach . ^{[ 2 ]} La publicación posterior, dos años después ^{[ 3 ],} fue considerada tan influyente que ganó el premio ACM SIGOPS Hall of Fame de 2015. Desde su introducción, L4 se ha desarrollado para ser multiplataforma y para mejorar la seguridad , el aislamiento y la robustez .

Se han realizado diversas reimplementaciones de la interfaz binaria de aplicación (ABI) del kernel L4 original y sus sucesoras, entre las que se incluyen L4Ka::Pistachio (implementada por Liedtke y sus estudiantes en el Instituto Tecnológico de Karlsruhe ), L4/MIPS ( Universidad de Nueva Gales del Sur (UNSW)) y Fiasco ( Universidad Tecnológica de Dresde (TU Dresden)). Por este motivo, el nombre L4 se ha generalizado y ya no se refiere únicamente a la implementación original de Liedtke. Ahora se aplica a toda la familia de microkernels, incluyendo la interfaz del kernel L4 y sus diferentes versiones.

L4 está ampliamente implementado. Una variante, OKL4 de Open Kernel Labs, se incluyó en miles de millones de dispositivos móviles. ^{[ 4 ] [ 5 ]}

Al especificar la idea general de un microkernel , Liedtke afirma:

Un concepto se tolera dentro del microkernel solo si trasladarlo fuera del kernel, es decir, permitir implementaciones competitivas, impediría la implementación de la funcionalidad requerida del sistema. ^{[ 3 ]}

En este sentido, el microkernel L4 proporciona algunos mecanismos básicos: espacios de direcciones (que abstraen las tablas de páginas y proporcionan protección de memoria), subprocesos y planificación (que abstraen la ejecución y proporcionan protección temporal) y comunicación entre procesos (para una comunicación controlada a través de los límites de aislamiento).

Un sistema operativo basado en un microkernel como L4 proporciona servicios de servidor en el espacio de usuario que los kernels monolíticos como Linux o los microkernels de generaciones anteriores incluyen internamente. Por ejemplo, para implementar un sistema seguro similar a Unix , los servidores deben proporcionar la gestión de derechos que Mach incluyó dentro del kernel.

El bajo rendimiento de los microkernels de primera generación, como Mach , llevó a varios desarrolladores a reconsiderar el concepto de microkernel a mediados de la década de 1990. El concepto de comunicación asíncrona entre procesos con almacenamiento en búfer dentro del kernel , utilizado en Mach, resultó ser una de las principales causas de su bajo rendimiento. Esto impulsó a los desarrolladores de sistemas operativos basados ​​en Mach a trasladar algunos componentes críticos en tiempo real, como los sistemas de archivos o los controladores, de nuevo al interior del kernel. Si bien esto mejoró en cierta medida los problemas de rendimiento, viola claramente el concepto de minimalidad de un verdadero microkernel (y desperdicia sus principales ventajas).

El análisis detallado del cuello de botella de Mach indicó que, entre otras cosas, su conjunto de trabajo es demasiado grande: el código IPC expresa una localidad espacial deficiente; es decir, produce demasiados fallos de caché , la mayoría de los cuales ocurren dentro del núcleo. ^{[ 3 ]} Este análisis dio origen al principio de que un micronúcleo eficiente debería ser lo suficientemente pequeño como para que la mayor parte del código crítico para el rendimiento quepa en la caché (de primer nivel) (preferiblemente una pequeña fracción de dicha caché).

L3

Jochen Liedtke se propuso demostrar que una capa de comunicación entre procesos (IPC) más delgada y bien diseñada, con especial atención al rendimiento y al diseño específico de la máquina (a diferencia del software multiplataforma ), podría generar grandes mejoras de rendimiento en el mundo real. En lugar del complejo sistema IPC de Mach, su microkernel L3 simplemente transmitía el mensaje sin sobrecarga adicional. La definición e implementación de las políticas de seguridad requeridas se consideraban responsabilidades de los servidores del espacio de usuario . El papel del kernel era únicamente proporcionar el mecanismo necesario para que los servidores de nivel de usuario pudieran aplicar dichas políticas. L3, desarrollado en 1988, demostró ser un sistema operativo seguro y robusto , utilizado durante muchos años, por ejemplo, por Technischer Überwachungsverein (Asociación de Inspección Técnica).

En noviembre de 2005, NICTA anunció ^{[ 13 ]} que Qualcomm estaba implementando la versión L4 de NICTA en sus chipsets de módem de estación móvil . Esto llevó al uso de L4 en teléfonos móviles a la venta desde finales de 2006. En agosto de 2006, el líder de ERTOS y profesor de UNSW, Gernot Heiser, creó una empresa llamada Open Kernel Labs (OK Labs) para dar soporte a los usuarios comerciales de L4 y seguir desarrollando L4 para uso comercial bajo la marca OKL4 , en estrecha colaboración con NICTA. OKL4 μKernel Versión 2.1, publicada en abril de 2008, fue la primera versión de L4 disponible para el público general que presentaba seguridad basada en capacidades . OKL4 μKernel 3.0, publicada en octubre de 2008, fue la última versión de código abierto de OKL4 μKernel. Las versiones más recientes son de código cerrado y se basan en una reescritura para dar soporte a una variante de hipervisor nativo llamada OKL4 Microvisor . OK Labs también distribuyó una versión paravirtualizada de Linux llamada OK:Linux, descendiente de Wombat, y versiones paravirtualizadas de SymbianOS y Android . Además, OK Labs adquirió los derechos de seL4 de NICTA.

Los envíos de OKL4 superaron los 1.500 millones a principios de 2012, ^{[ 5 ]} principalmente en chips de módem inalámbrico de Qualcomm. Otras implementaciones incluyen sistemas de infoentretenimiento para automóviles . ^{[ 14 ]}

Los procesadores de la serie A de Apple , a partir del A7 , contienen un coprocesador Secure Enclave que ejecuta un sistema operativo L4 ^{[ 15 ]} llamado sepOS (Secure Enclave Processor OS), basado en el kernel integrado en L4 desarrollado en NICTA en 2006. ^{[ 16 ]} Como resultado, L4 viene incluido en todos los dispositivos Apple modernos, incluyendo las Mac con Apple Silicon . Solo en 2015, se estimó que los envíos totales de iPhone alcanzaron los 310 millones. ^{[ 17 ]}

En 2006, el grupo NICTA comenzó el diseño desde cero de un microkernel de tercera generación , llamado seL4, con el objetivo de proporcionar una base para sistemas altamente seguros y confiables, adecuados para satisfacer requisitos de seguridad como los de Common Criteria y más allá. Desde el principio, el desarrollo se centró en la verificación formal del kernel. Para facilitar el cumplimiento de los requisitos, a veces contradictorios, de rendimiento y verificación, el equipo utilizó un proceso de software intermedio que partía de una especificación ejecutable escrita en el lenguaje Haskell . ^{[ 18 ]} seL4 utiliza un control de acceso de seguridad basado en capacidades para permitir el razonamiento formal sobre la accesibilidad de los objetos.

En 2009 se completó una prueba formal de corrección funcional. ^{[ 19 ]} La prueba garantiza que la implementación del núcleo es correcta según su especificación e implica que está libre de errores de implementación como interbloqueos , bloqueos permanentes , desbordamientos de búfer , excepciones aritméticas o el uso de variables no inicializadas . Se afirma que seL4 es el primer núcleo de sistema operativo de propósito general que ha sido verificado. ^{[ 19 ]} El trabajo en seL4 ganó el premio ACM SIGOPS Hall of Fame de 2019.

seL4 adopta un enfoque novedoso para la gestión de recursos del kernel, ^{[ 20 ]} exportando la gestión de los recursos del kernel al nivel de usuario y sometiéndolos al mismo control de acceso basado en capacidades que los recursos de usuario. Este modelo, que también fue adoptado por Barrelfish , simplifica el razonamiento sobre las propiedades de aislamiento y fue un facilitador para las pruebas posteriores de que seL4 impone las propiedades de seguridad centrales de integridad y confidencialidad. ^{[ 21 ]} El equipo de NICTA también demostró la corrección de la traducción del lenguaje de programación C a código máquina ejecutable , eliminando el compilador de la base de computación confiable de seL4. ^{[ 22 ]} Esto implica que las pruebas de seguridad de alto nivel son válidas para el ejecutable del kernel. seL4 es también el primer kernel de sistema operativo en modo protegido publicado con un análisis completo y sólido del tiempo de ejecución en el peor de los casos (WCET), un requisito previo para su uso en computación en tiempo real estricto . ^{[ 21 ]}

El 29 de julio de 2014, NICTA y General Dynamics C4 Systems anunciaron que seL4, con pruebas de extremo a extremo, se había publicado bajo licencias de código abierto . ^{[ 23 ]} El código fuente del kernel y las pruebas están licenciados bajo la Licencia Pública General GNU versión 2 (GPLv2), y la mayoría de las bibliotecas y herramientas están bajo la licencia BSD de 2 cláusulas . En abril de 2020, se anunció la creación de la Fundación seL4 bajo el paraguas de la Fundación Linux para acelerar el desarrollo y la implementación de seL4. ^{[ 24 ]}

Los investigadores afirman que el costo de la verificación formal de software es menor que el costo de ingeniería de software tradicional de "alta seguridad", a pesar de proporcionar resultados mucho más fiables. ^{[ 25 ]} Específicamente, el costo de una línea de código durante el desarrollo de seL4 se estimó en alrededor de US$400 , en comparación con US$1,000 para los sistemas tradicionales de alta seguridad. ^{[ 26 ]}

Bajo el programa de Sistemas Militares Cibernéticos de Alta Seguridad (HACMS) de la Agencia de Proyectos de Investigación Avanzada de Defensa ( DARPA ), NICTA, junto con los socios del proyecto Rockwell Collins , Galois Inc., la Universidad de Minnesota y Boeing, desarrollaron un dron de alta seguridad utilizando seL4, junto con otras herramientas y software de seguridad, con la transferencia de tecnología planificada al helicóptero autónomo Boeing AH-6 Unmanned Little Bird, pilotado opcionalmente, que está desarrollando Boeing. La demostración final de la tecnología HACMS tuvo lugar en Sterling, Virginia, en abril de 2017. ^{[ 27 ]} DARPA también financió varios contratos de Investigación Innovadora para Pequeñas Empresas (SBIR) relacionados con seL4 bajo un programa iniciado por John Launchbury . Las pequeñas empresas que recibieron un SBIR relacionado con seL4 fueron: DornerWorks, Techshot, Wearable Inc., Real Time Innovations y Critical Technologies. ^{[ 28 ]}

En octubre de 2023, Nio Inc. anunció que sus sistemas operativos SkyOS basados ​​en seL4 estarán presentes en los coches eléctricos de producción en masa a partir de 2024. ^{[ 29 ]}

En 2023, seL4 ganó el premio ACM Software System Award .

Osker, un sistema operativo escrito en Haskell , tenía como objetivo la especificación L4; aunque este proyecto se centró principalmente en el uso de un lenguaje de programación funcional para el desarrollo de sistemas operativos, no en la investigación de microkernels. ^{[ 30 ]}

RedoxOS ^{[ 31 ]} es un sistema operativo basado en Rust, que también está inspirado en seL4 y utiliza un diseño de microkernel.

CodeZero ^{[ 32 ]} es un microkernel L4 para sistemas embebidos centrado en la virtualización y la implementación de servicios nativos del sistema operativo. Existe una versión con licencia GPL ^{[ 33 ]} y otra versión que fue re-licenciada por B Labs Ltd., adquirida por Nvidia , como código cerrado y bifurcada en 2010. ^{[ 34 ] [ 35 ]}

El microkernel F9, ^{[ 36 ]} una implementación L4 con licencia BSD, está dedicado a los procesadores ARM Cortex-M para dispositivos profundamente integrados con protección de memoria.

La arquitectura de virtualización NOVA OS ^{[ 37 ]} es un proyecto de investigación centrado en la construcción de un entorno de virtualización seguro y eficiente ^{[ 38 ] [ 39 ]} con una pequeña base de computación confiable. NOVA consta de un microhipervisor, un hipervisor a nivel de usuario ( monitor de máquina virtual ) y un entorno de usuario multiservidor modularizado sin privilegios que se ejecuta sobre él, denominado NUL. NOVA se ejecuta en sistemas multinúcleo basados ​​en ARMv8-A y x86.

WrmOS ^{[ 40 ]} es un sistema operativo en tiempo real basado en el microkernel L4. Cuenta con implementaciones propias del kernel, bibliotecas estándar y pila de red, y admite las arquitecturas ARM, SPARC, x86 y x86-64. Existe un kernel Linux paravirtualizado (w4linux ^{[ 41 ]} ) que funciona en WrmOS.

Helios es un microkernel inspirado en seL4. ^{[ 42 ]} Forma parte del sistema operativo Ares, es compatible con x86-64 y aarch64 y sigue en desarrollo activo a fecha de febrero de 2023. ^{[ 43 ]}

• PikeOS

• Liedtke, Jochen ; Bartling, Ulrich; Beyer, Uwe; Heinrichs, Dietmar; Ruland, Rudolf; Szalay, Gyula (abril de 1991). "Dos años de experiencia con un sistema operativo basado en μ-Kernel" . Revisión de los sistemas operativos ACM SIGOPS . 25 (2): 51– 62. doi : 10.1145/122120.122124 . S2CID 17602151 . 
• Liedtke, Jochen ; Haeberlen, Andreas; Park, Yoonho; Reuther, Lars; Uhlig, Volkmar (22 de octubre de 2000). "El rendimiento del código auxiliar se está volviendo importante" . Actas del 1er Taller sobre Experiencias Industriales con Software de Sistemas (WIESS), San Diego, CA, octubre de 2000. Archivado del original (PDF) el 5 de septiembre de 2006. Recuperado el 5 de septiembre de 2006 .(en el núcleo y compilador L4)
• Cheng, Guanghui; McGuire, Nicholas. L4/Fiasco/L4Linux Kickstart (PDF) . Laboratorio de Sistemas Distribuidos y Embebidos (Informe). Universidad de Lanzhou. Archivado del original (PDF) el 27 de marzo de 2012.
• Elphinstone, Kevin; Heiser, Gernot (noviembre de 2013). «De L3 a seL4: ¿Qué hemos aprendido en 20 años de microkernels L4?» (PDF) . 24.º Simposio ACM SIGOPS sobre Principios de Sistemas Operativos . Farmington, PA, EE. UU. pp. 133–150 . CiteSeerX 10.1.1.636.9410 . doi : 10.1145/2517349.2522720 . ISBN   978-1-4503-2388-8.Evolución de los enfoques de diseño e implementación de L4

• L4Hq: Sede de L4, sitio comunitario para proyectos de L4. Archivado el 25/10/2019 en Wayback Machine.
• La familia de micro-kernels L4 , descripción general de las implementaciones de L4, documentación, proyectos
• Wiki oficial de TUD:OS
• L4Ka : Implementaciones L4Ka::Pistacho y L4Ka::Hazelnut
• Sitio web oficial , seL4
• UNSW : Implementaciones para la arquitectura DEC Alpha y MIPS
• OKL4 archivado el 20/08/2008 en Wayback Machine : versión comercial L4 de Open Kernel Labs archivada el 19/03/2009 en Wayback Machine
• NICTA L4 : Resumen de investigación y publicaciones archivadas] 17/07/2014 en Wayback Machine
• Trustworthy Systems Group en Data61 de CSIRO : sede actual del antiguo grupo NICTA que desarrolló seL4.
• Marco de sistema operativo Genode : Un descendiente de la comunidad L4.