L4 es una familia de micronúcleos de segunda generación , que se utiliza para implementar una variedad de tipos de sistemas operativos (SO), aunque principalmente para tipos compatibles con la interfaz de sistema operativo portátil ( POSIX ) tipo Unix .
L4, al igual que su predecesor, el microkernel L3, fue creado por el informático alemán Jochen Liedtke como respuesta al bajo rendimiento de los anteriores sistemas operativos basados en microkernel. Liedtke consideró que un sistema diseñado desde el principio para un alto rendimiento, en lugar de otros objetivos, podría producir un micronúcleo de uso práctico. Su implementación original en código de lenguaje ensamblador específico de Intel i386 codificado a mano en 1993 llamó la atención por ser 20 veces más rápido que Mach . [1] La publicación de seguimiento dos años después [2] se consideró tan influyente que ganó el Premio del Salón de la Fama ACM SIGOPS 2015. Desde su introducción, L4 se ha desarrollado para ser multiplataforma y mejorar la seguridad , el aislamiento y la solidez .
Ha habido varias reimplementaciones de la interfaz binaria de aplicación del kernel (ABI) L4 original y sus sucesores, incluido L4Ka::Pistachio (implementado por Liedtke y sus estudiantes en el Instituto de Tecnología de Karlsruhe ), L4/MIPS ( Universidad de Nueva Gales del Sur). (UNSW)), Fiasco ( Universidad Tecnológica de Dresde (TU Dresden)). Por esta razón, 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 , incluida la interfaz del kernel L4 y sus diferentes versiones.
L4 está ampliamente implementado. Una variante, OKL4 de Open Kernel Labs , se envió en miles de millones de dispositivos móviles. [3] [4]
Precisando la idea general de micronúcleo , Liedtke afirma:
Un concepto se tolera dentro del micronúcleo sólo si moverlo fuera del núcleo, es decir, permitir implementaciones competitivas, impediría la implementación de la funcionalidad requerida del sistema. [2]
En este espíritu, el micronúcleo L4 proporciona algunos mecanismos básicos: espacios de direcciones (que abstraen tablas de páginas y brindan protección de memoria), subprocesos y programación (que abstraen la ejecución y brindan protección temporal) y comunicación entre procesos (para una comunicación controlada a través de límites de aislamiento).
Un sistema operativo basado en un microkernel como L4 proporciona servicios como servidores en el espacio del usuario que los kernels monolíticos como Linux o los microkernels de generaciones anteriores incluyen internamente. Por ejemplo, para implementar un sistema seguro tipo Unix , los servidores deben proporcionar la gestión de derechos que Mach incluye dentro del kernel.
El bajo rendimiento de los microkernels de primera generación, como Mach , llevó a varios desarrolladores a reexaminar todo el concepto de microkernel a mediados de los años 1990. El concepto de comunicación de proceso asíncrono con almacenamiento en búfer interno utilizado en Mach resultó ser una de las principales razones de su bajo rendimiento. Esto indujo a los desarrolladores de sistemas operativos basados en Mach a mover algunos componentes críticos, como sistemas de archivos o controladores, nuevamente dentro del kernel. [ cita necesaria ] Si bien esto mejoró un poco los problemas de rendimiento, viola claramente el concepto de minimalidad de un verdadero micronúcleo (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 errores de caché , de los cuales la mayoría se producen en el kernel. [2] Este análisis dio lugar al principio de que un microkernel eficiente debe ser lo suficientemente pequeño como para que la mayoría del código crítico para el rendimiento quepa en el caché (de primer nivel) (preferiblemente una pequeña fracción de dicho caché).
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 (en contraste con el software multiplataforma ) podría generar grandes mejoras de rendimiento en el mundo real. En lugar del complejo sistema IPC de Mach, su micronúcleo L3 simplemente transmitía el mensaje sin gastos adicionales. Definir e implementar las políticas de seguridad requeridas se consideró responsabilidad de los servidores del espacio de usuario . La función del kernel era únicamente proporcionar el mecanismo necesario para permitir que los servidores de nivel de usuario hicieran cumplir las 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). [ cita necesaria ]
Después de algunas experiencias con L3, Liedtke llegó a la conclusión de que otros conceptos de Mach también estaban fuera de lugar. Simplificando aún más los conceptos del microkernel, desarrolló el primer kernel L4 que fue diseñado principalmente para un alto rendimiento. Para maximizar el rendimiento, todo el núcleo se escribió en lenguaje ensamblador y su IPC era 20 veces más rápido que el de Mach. [1] Estos aumentos dramáticos en el rendimiento son un evento poco común en los sistemas operativos, y el trabajo de Liedtke desencadenó nuevas implementaciones L4 y trabajo en sistemas basados en L4 en varias universidades e institutos de investigación, incluido IBM , donde Liedtke comenzó a trabajar en 1996, TU. Dresde y UNSW. En el Centro de Investigación Thomas J. Watson de IBM, Liedtke y sus colegas continuaron investigando sobre L4 y sistemas basados en microkernel en general, especialmente Sawmill OS. [5]
En 1999, Liedtke se hizo cargo del Grupo de Arquitectura de Sistemas de la Universidad de Karlsruhe , donde continuó la investigación en sistemas microkernel. Como prueba de concepto de que un microkernel de alto rendimiento también podría construirse en un lenguaje de nivel superior, el grupo desarrolló L4Ka::Hazelnut , una versión C++ del kernel que se ejecutaba en máquinas basadas en IA-32 y ARM . El esfuerzo fue un éxito, el rendimiento aún era aceptable y, con su lanzamiento, las versiones puras de los núcleos en lenguaje ensamblador fueron efectivamente descontinuadas.
Paralelamente al desarrollo de L4Ka::Hazelnut, en 1998 el grupo de sistemas operativos TUD:OS de la Universidad Técnica de Dresde comenzó a desarrollar su propia implementación en C++ de la interfaz del kernel L4, denominada L4/Fiasco. A diferencia de L4Ka::Hazelnut, que no permite concurrencia en el kernel, y su sucesor L4Ka::Pistachio, que permite interrupciones en el kernel sólo en puntos de preferencia específicos, L4/Fiasco era totalmente preferible (con la excepción de atómicos extremadamente cortos). operaciones) para lograr una baja latencia de interrupción . Esto se consideró necesario porque L4/Fiasco se utiliza como base de DROPS, [6] un sistema operativo con capacidad de computación en tiempo real , también desarrollado en la TU Dresden. Sin embargo, las complejidades de un diseño totalmente interrumpible llevaron a versiones posteriores de Fiasco a volver al enfoque tradicional L4 de ejecutar el kernel con las interrupciones deshabilitadas, excepto por un número limitado de puntos de preferencia.
Hasta el lanzamiento de L4Ka::Pistachio y las versiones más recientes de Fiasco, todos los microkernels L4 estaban inherentemente ligados a la arquitectura de CPU subyacente. El siguiente gran cambio en el desarrollo de L4 fue el desarrollo de una interfaz de programación de aplicaciones ( API ) multiplataforma (independiente de la plataforma ) que aún conservaba las características de alto rendimiento a pesar de su mayor nivel de portabilidad. Aunque los conceptos subyacentes del kernel eran los mismos, la nueva API proporcionó muchos cambios significativos en relación con las versiones L4 anteriores, incluido un mejor soporte para sistemas multiprocesador, vínculos más flexibles entre subprocesos y espacios de direcciones, y la introducción de control de subprocesos a nivel de usuario. bloques (UTCB) y registros virtuales. Después de lanzar la nueva API L4 (versión X.2 también conocida como versión 4) a principios de 2001, el Grupo de Arquitectura de Sistemas de la Universidad de Karlsruhe implementó un nuevo kernel, L4Ka::Pistachio , completamente desde cero, ahora enfocado tanto en el alto rendimiento como en el rendimiento. portabilidad. Fue lanzado bajo la licencia BSD de dos cláusulas . [7]
El micronúcleo L4/Fiasco también se ha mejorado ampliamente a lo largo de los años. Ahora admite varias plataformas de hardware que van desde x86 hasta AMD64 y varias plataformas ARM. En particular, una versión de Fiasco (Fiasco-UX) se puede ejecutar como una aplicación a nivel de usuario en Linux.
L4/Fiasco implementa varias extensiones de la API L4v2. Exception IPC permite que el kernel envíe excepciones de CPU a aplicaciones de manejo de nivel de usuario. Con la ayuda de subprocesos alienígenas , es posible realizar un control detallado sobre las llamadas al sistema. Se han agregado UTCB de estilo X.2. Además, Fiasco contiene mecanismos para controlar los derechos de comunicación y el uso de recursos a nivel del kernel. En Fiasco, se desarrolla una colección de servicios básicos a nivel de usuario (llamados L4Env) que, entre otros, se utilizan para paravirtualizar la versión actual de Linux (4.19 a partir de mayo de 2019 [actualizar]) (llamada L 4 Linux ).
El desarrollo también se produjo en la Universidad de Nueva Gales del Sur (UNSW), donde los desarrolladores implementaron L4 en varias plataformas de 64 bits. Su trabajo dio como resultado L4/MIPS y L4/Alpha , lo que dio como resultado que la versión original de Liedtke fuera nombrada retrospectivamente L4/x86 . Al igual que los núcleos originales de Liedtke, los núcleos UNSW (escritos en una combinación de ensamblador y C) no eran portátiles y cada uno se implementaba desde cero. Con el lanzamiento del L4Ka::Pistachio altamente portátil, el grupo de la UNSW abandonó sus propios núcleos a favor de producir puertos altamente optimizados de L4Ka::Pistachio, incluida la implementación de paso de mensajes más rápida jamás reportada (36 ciclos en la arquitectura Itanium ). . [8] El grupo también ha demostrado que los controladores de dispositivos pueden funcionar igual de bien a nivel de usuario que en el kernel, [9] y desarrolló Wombat , una versión altamente portátil de Linux en L4 que se ejecuta en procesadores x86 , ARM y MIPS . En los procesadores XScale , los costos de cambio de contexto de Wombat son hasta 50 veces menores que en Linux nativo. [10]
Más tarde, el grupo UNSW, en su nuevo hogar en NICTA (anteriormente National ICT Australia, Ltd. ), bifurcó L4Ka::Pistachio en una nueva versión L4 llamada NICTA::L4-embedded . Como su nombre lo indica, era para uso en sistemas integrados comerciales y, en consecuencia, las compensaciones de implementación favorecieron un tamaño de memoria pequeño y una complejidad reducida. La API se modificó para mantener casi todas las llamadas al sistema lo suficientemente breves como para que no necesiten puntos de preferencia para garantizar una alta capacidad de respuesta en tiempo real. [11]
En noviembre de 2005, NICTA anunció [12] que Qualcomm estaba implementando la versión L4 de NICTA en sus conjuntos de chips Mobile Station Modem . 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 la UNSW, Gernot Heiser, creó una empresa llamada Open Kernel Labs (OK Labs) para apoyar 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, lanzada en abril de 2008, fue la primera versión disponible de forma generalizada de L4 que presentaba seguridad basada en capacidades . OKL4 μKernel 3.0, lanzado 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 admitir una variante de hipervisor nativo denominada OKL4 Microvisor . OK Labs también distribuyó un Linux paravirtualizado llamado OK:Linux, un descendiente de Wombat, y versiones paravirtualizadas de SymbianOS y Android . OK Labs también adquirió los derechos de seL4 de NICTA.
Los envíos de OKL4 superaron los 1.500 millones a principios de 2012, [4] principalmente en chips de módem inalámbrico de Qualcomm. Otras implementaciones incluyen sistemas de información y entretenimiento para automóviles . [13]
Los procesadores Apple de la serie A que comienzan con el A7 contienen un coprocesador Secure Enclave que ejecuta un sistema operativo L4 [14] llamado sepOS (Secure Enclave Processor OS) basado en el kernel integrado L4 desarrollado en NICTA en 2006. [15] Como resultado, L4 Se envía en todos los dispositivos Apple modernos, incluidos los Mac con silicio Apple . Sólo en 2015, los envíos totales de iPhone se estimaron en 310 millones. [dieciséis]
En 2006, el grupo NICTA comenzó a diseñar desde cero un microkernel de tercera generación , denominado seL4, con el objetivo de proporcionar una base para sistemas altamente seguros y fiables, adecuados para satisfacer requisitos de seguridad como los de Common Criteria y más allá. Desde el principio, el desarrollo apuntó a la verificación formal del núcleo. Para facilitar el cumplimiento de los requisitos, a veces contradictorios, de rendimiento y verificación, el equipo utilizó un proceso de software intermedio a partir de una especificación ejecutable escrita en el lenguaje Haskell . [17] seL4 utiliza control de acceso de seguridad basado en capacidades para permitir el razonamiento formal sobre la accesibilidad de objetos.
En 2009 se completó una prueba formal de corrección funcional . [18] La prueba proporciona una garantía de que la implementación del kernel es correcta según su especificación e implica que está libre de errores de implementación como interbloqueos , bloqueos activos , desbordamientos de búfer , excepciones aritméticas o uso de variables no inicializadas . Se afirma que seL4 es el primer kernel de sistema operativo de propósito general que ha sido verificado. [18] El trabajo en seL4 ganó el Premio del Salón de la Fama ACM SIGOPS 2019.
seL4 adopta un enfoque novedoso para la gestión de recursos del kernel, [19] exportando la gestión de los recursos del kernel al nivel de usuario y los somete al mismo control de acceso basado en capacidades que los recursos del usuario. Este modelo, que también fue adoptado por Barrelfish , simplifica el razonamiento sobre las propiedades de aislamiento y permitió pruebas posteriores de que seL4 aplica las propiedades de seguridad básicas de integridad y confidencialidad. [20] El equipo de NICTA también demostró la exactitud de la traducción del lenguaje de programación C al código de máquina ejecutable , sacando al compilador de la base informática confiable de seL4. [21] Esto implica que las pruebas de seguridad de alto nivel son válidas para el ejecutable del núcleo. 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 . [20]
El 29 de julio de 2014, NICTA y General Dynamics C4 Systems anunciaron que seL4, con pruebas de extremo a extremo, ahora se lanzó bajo licencias de código abierto . [22] El código fuente del kernel y las pruebas tienen la licencia GNU General Public License versión 2 (GPLv2), y la mayoría de las bibliotecas y herramientas están bajo la cláusula BSD 2 . En abril de 2020, se anunció que se creó la Fundación seL4 bajo el paraguas de la Fundación Linux para acelerar el desarrollo y la implementación de seL4. [23]
Los investigadores afirman que el costo de la verificación formal del software es menor que el costo de diseñar software tradicional de "alta seguridad" a pesar de proporcionar resultados mucho más confiables. [24] Específicamente, el costo de una línea de código durante el desarrollo de seL4 se estimó en alrededor de 400 dólares estadounidenses , en comparación con los 1.000 dólares estadounidenses de los sistemas tradicionales de alta seguridad. [25]
En el marco del programa HACMS (Sistemas cibermilitares de alta seguridad) 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 otros herramientas y software de aseguramiento, con una 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, VA, en abril de 2017. [26] DARPA también financió varios contratos de Investigación Innovadora para Pequeñas Empresas (SBIR) relacionados con seL4 bajo un programa iniciado por el Dr. John Launchbury . Las pequeñas empresas que recibieron un SBIR relacionado con seL4 incluyeron: DornerWorks, Techshot, Wearable Inc, Real Time Innovations y Critical Technologies. [27]
En octubre de 2023, Nio Inc. anunció que sus sistemas operativos SkyOS basados en seL4 se incluirán en automóviles eléctricos producidos en masa a partir de 2024.
En 2023, seL4 ganó el premio ACM Software System Award .
Osker, un sistema operativo escrito en Haskell , apuntaba a 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 microkernel. [28]
CodeZero [29] es un microkernel L4 para sistemas integrados centrado en la virtualización y la implementación de servicios de sistema operativo nativo. Hay una versión con licencia GPL , [30] y una versión con licencia de B Labs Ltd., adquirida por Nvidia , como código cerrado y bifurcada en 2010. [31] [32]
El micronúcleo F9, [33] una implementación L4 con licencia BSD, está dedicado a procesadores ARM Cortex-M para dispositivos profundamente integrados con protección de memoria.
La arquitectura de virtualización NOVA OS [34] es un proyecto de investigación centrado en la construcción de un entorno de virtualización seguro y eficiente [35] [36] con una pequeña base informática confiable. NOVA consta de un microhipervisor, un hipervisor a nivel de usuario ( monitor de máquina virtual ) y un entorno de usuario multiservidor con componentes sin privilegios que se ejecuta en él llamado NUL. NOVA se ejecuta en sistemas multinúcleo basados en ARMv8-A y x86.
WrmOS [37] es un sistema operativo en tiempo real basado en microkernel L4. Tiene implementaciones propias de kernel, bibliotecas estándar y pila de red, y admite arquitecturas ARM, SPARC, x86 y x86-64. Existe el kernel de Linux paravirtualizado (w4linux [38] ) funcionando en WrmOS.
Helios es un microkernel inspirado en seL4. [39] Es parte del sistema operativo Ares, es compatible con x86-64 y aarch64 y todavía está en desarrollo activo en febrero de 2023. [40]