L4 es una familia de microkernels de segunda generación , utilizados para implementar una variedad de 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 anteriores 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 microkernel de uso práctico. Su implementación original en código de lenguaje ensamblador específico para Intel i386 codificado a mano en 1993 llamó la atención al 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 robustez .
Se han realizado varias reimplementaciones de la interfaz binaria de aplicación (ABI) del núcleo L4 original y sus sucesores, incluyendo L4Ka::Pistachio (implementada por Liedtke y sus estudiantes en el Instituto de Tecnología de Karlsruhe ), L4/MIPS ( Universidad de Nueva Gales del Sur (UNSW)), Fiasco ( Universidad de Tecnología 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 microkernel , incluida la interfaz del núcleo L4 y sus diferentes versiones.
L4 se ha implementado ampliamente. Una variante, OKL4 de Open Kernel Labs , se distribuye en miles de millones de dispositivos móviles. [3] [4]
Al especificar la idea general de un micronúcleo , Liedtke afirma:
Un concepto se tolera dentro del microkernel sólo si moverlo fuera del kernel, es decir, permitir implementaciones competitivas, impediría la implementación de la funcionalidad requerida del sistema. [2]
En este espíritu, el microkernel L4 proporciona algunos mecanismos básicos: espacios de direcciones (abstrayendo las tablas de páginas y proporcionando protección de memoria), subprocesos y programación (abstrayendo la ejecución y proporcionando 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 de usuario que los núcleos monolíticos como Linux o 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 incluyó dentro del núcleo.
El pobre desempeño de los microkernels de primera generación, como Mach , llevó a varios desarrolladores a reexaminar todo el concepto de microkernel a mediados de la década de 1990. El concepto de comunicación asincrónica del proceso de almacenamiento en búfer dentro del núcleo 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 en el tiempo, como los sistemas de archivos o los controladores, nuevamente dentro del núcleo. [ cita requerida ] Si bien esto mejoró un poco los problemas de rendimiento, viola claramente el concepto de minimalidad de un verdadero microkernel (y desperdicia sus principales ventajas).
Un 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 pobre; es decir, da como resultado demasiados errores de caché , de los cuales la mayoría son dentro del núcleo. [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 una atención cuidadosa al rendimiento y al diseño específico de la máquina (en contraste con el software multiplataforma ), podría producir grandes mejoras de rendimiento en el mundo real. En lugar del complejo sistema IPC de Mach, su microkernel L3 simplemente pasaba el mensaje sin sobrecarga adicional. Se consideró que definir e implementar las políticas de seguridad requeridas eran tareas de los servidores del espacio de usuario . El papel del kernel era solo proporcionar el mecanismo necesario para permitir que los servidores de nivel de usuario aplicaran 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 requerida ]
Después de cierta experiencia con el uso de L3, Liedtke llegó a la conclusión de que varios otros conceptos de Mach también estaban fuera de lugar. Al simplificar aún más los conceptos de microkernel, desarrolló el primer kernel L4 que fue diseñado principalmente para un alto rendimiento. Para maximizar el rendimiento, todo el kernel fue escrito en lenguaje ensamblador , y su IPC era 20 veces más rápido que el de Mach. [1] Estos aumentos de rendimiento tan dramáticos son un evento raro en los sistemas operativos, y el trabajo de Liedtke desencadenó nuevas implementaciones de L4 y trabajo en sistemas basados en L4 en varias universidades e institutos de investigación, incluyendo IBM , donde Liedtke comenzó a trabajar en 1996, TU Dresden y UNSW. En el Centro de Investigación Thomas J. Watson de IBM , Liedtke y sus colegas continuaron la investigación sobre L4 y sistemas basados en microkernel en general, especialmente el sistema operativo Sawmill. [5]
En 1999, Liedtke se hizo cargo del Grupo de Arquitectura de Sistemas de la Universidad de Karlsruhe , donde continuó la investigación sobre sistemas de micronúcleos. Como prueba de concepto de que un micronúcleo de alto rendimiento también se podía construir en un lenguaje de nivel superior, el grupo desarrolló L4Ka::Hazelnut , una versión del núcleo en C++ que se ejecutaba en máquinas basadas en IA-32 y ARM . El esfuerzo fue un éxito, el rendimiento seguía siendo aceptable y, con su lanzamiento, las versiones de los núcleos en lenguaje ensamblador puro se dejaron de fabricar.
En paralelo al desarrollo de L4Ka::Hazelnut, en 1998 el Grupo de Sistemas Operativos TUD:OS de la TU Dresden comenzó a desarrollar su propia implementación en C++ de la interfaz del núcleo L4, llamada L4/Fiasco. A diferencia de L4Ka::Hazelnut, que no permite concurrencia en el núcleo, y su sucesor L4Ka::Pistachio, que permite interrupciones en el núcleo solo en puntos de preempción específicos, L4/Fiasco era completamente preemptible (con la excepción de operaciones atómicas extremadamente cortas) para lograr una baja latencia de interrupción . Esto se consideró necesario porque L4/Fiasco se usa como base de DROPS, [6] un sistema operativo capaz de computación en tiempo real , también desarrollado en la TU Dresden. Sin embargo, las complejidades de un diseño completamente preemptible impulsaron a versiones posteriores de Fiasco a volver al enfoque tradicional L4 de ejecutar el núcleo con las interrupciones deshabilitadas, excepto por un número limitado de puntos de preempción.
Hasta el lanzamiento de L4Ka::Pistachio y versiones más nuevas de Fiasco, todos los microkernels L4 habían estado 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 núcleo 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 hilos y espacios de direcciones y la introducción de bloques de control de hilos a nivel de usuario (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 núcleo, L4Ka::Pistachio , completamente desde cero, ahora con el foco puesto tanto en el alto rendimiento como en la portabilidad. Fue lanzado bajo la licencia BSD de dos cláusulas . [7]
El microkernel L4/Fiasco también ha sido mejorado ampliamente a lo largo de los años. Ahora es compatible con varias plataformas de hardware, desde x86 hasta AMD64 y varias plataformas ARM. Cabe destacar que una versión de Fiasco (Fiasco-UX) puede ejecutarse como una aplicación a nivel de usuario en Linux.
L4/Fiasco implementa varias extensiones a la API L4v2. Exception IPC permite al núcleo enviar excepciones de CPU a aplicaciones de manejo de nivel de usuario. Con la ayuda de hilos ajenos , es posible realizar un control detallado sobre las llamadas del 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 de núcleo. 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 provocó que la versión original de Liedtke se llamara retrospectivamente L4/x86 . Al igual que los núcleos originales de Liedtke, los núcleos de la UNSW (escritos en una mezcla de ensamblaje y C) no eran portables y cada uno se implementó desde cero. Con el lanzamiento del altamente portable L4Ka::Pistachio, el grupo de la UNSW abandonó sus propios núcleos a favor de producir puertos altamente ajustados de L4Ka::Pistachio, incluida la implementación más rápida jamás reportada de paso de mensajes (36 ciclos en la arquitectura Itanium ). [8] El grupo también ha demostrado que los controladores de dispositivos pueden funcionar igualmente bien a nivel de usuario como en el núcleo, [9] y desarrolló Wombat , una versión altamente portable 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 más bajos que en Linux nativo. [10]
Más tarde, el grupo de la UNSW, ahora en NICTA (anteriormente National ICT Australia, Ltd. ), bifurcó L4Ka::Pistachio en una nueva versión L4 llamada NICTA::L4-embedded . Estaba destinada a utilizarse en sistemas embebidos comerciales y, en consecuencia, las ventajas de implementación favorecían un tamaño de memoria pequeño y una complejidad reducida. La API se modificó para mantener casi todas las llamadas del sistema lo suficientemente cortas como para que no necesitaran puntos de preempción a fin de 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 chipsets Mobile Station Modem . Esto condujo al uso de L4 en teléfonos móviles a la venta desde fines 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 brindar soporte a los usuarios comerciales de L4 y desarrollar aún más 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 generalmente disponible 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 llamada OKL4 Microvisor . OK Labs también distribuyó un Linux paravirtualizado llamado OK:Linux, 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 de la serie A de Apple , comenzando con el A7, contienen un coprocesador Secure Enclave que ejecuta un sistema operativo L4 [14] llamado sepOS (Secure Enclave Processor OS) basado en el núcleo L4 integrado desarrollado en NICTA en 2006. [15] Como resultado, L4 se entrega en todos los dispositivos Apple modernos, incluidos los Mac con silicio de Apple . Solo en 2015, se estimó que los envíos totales de iPhone fueron de 310 millones. [16]
En 2006, el grupo NICTA comenzó un 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 apuntó a la verificación formal del kernel. Para facilitar el cumplimiento de los requisitos a veces conflictivos 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 los 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 núcleo es correcta frente a su especificación e implica que está libre de errores de implementación como bloqueos , bloqueos activos , desbordamientos de búfer , excepciones aritméticas o 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. [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 núcleo, [19] exportando la gestión de los recursos del núcleo al nivel de usuario y sometiéndolos 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 fue un facilitador para pruebas posteriores de que seL4 hace cumplir las propiedades de seguridad básicas de integridad y confidencialidad. [20] El equipo de NICTA también demostró la corrección 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 núcleo de SO 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 prerrequisito para su uso en computación en tiempo real estricta . [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 núcleo 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 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 coste de la verificación formal del software es menor que el coste de la ingeniería de software tradicional de "alta seguridad" a pesar de proporcionar resultados mucho más fiables. [24] En concreto, el coste de una línea de código durante el desarrollo de seL4 se estimó en unos 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 High-Assurance Cyber Military Systems (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 una transferencia de tecnología planificada al helicóptero autónomo opcionalmente pilotado Boeing AH-6 Unmanned Little Bird que está desarrollando Boeing. La demostración final de la tecnología HACMS tuvo lugar en Sterling, Virginia, en abril de 2017. [26] DARPA también financió varios contratos de Investigación Innovadora para Pequeñas Empresas (SBIR) relacionados con seL4 en el marco de un programa iniciado por 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 estarán presentes en automóviles eléctricos producidos en masa a partir de 2024. [28]
En 2023, seL4 ganó el premio ACM Software System Award .
Osker, un sistema operativo escrito en Haskell , apuntó 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 microkernels. [29]
RedoxOS [30] es un sistema operativo basado en Rust, que también está inspirado en seL4 y utiliza un diseño de micro kernel.
CodeZero [31] es un microkernel L4 para sistemas embebidos enfocado en la virtualización y la implementación de servicios nativos del SO. Existe una versión con licencia GPL [32] y una versión que fue relicenciada por B Labs Ltd., adquirida por Nvidia , como código cerrado y bifurcada en 2010. [33] [34]
El microkernel F9, [35] 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 [36] es un proyecto de investigación que se centra en la construcción de un entorno de virtualización seguro y eficiente [37] [38] con una pequeña base informática de confianza. NOVA consta de un microhipervisor, un hipervisor de nivel de usuario ( monitor de máquina virtual ) y un entorno de usuario multiservidor componentizado sin privilegios que se ejecuta en él llamado NUL. NOVA se ejecuta en sistemas multinúcleo basados en ARMv8-A y x86.
WrmOS [39] es un sistema operativo en tiempo real basado en un microkernel L4. Tiene sus propias implementaciones de kernel, bibliotecas estándar y pila de red, y soporta arquitecturas ARM, SPARC, x86 y x86-64. Existe un kernel Linux paravirtualizado (w4linux [40] ) que funciona sobre WrmOS.
Helios es un microkernel inspirado en seL4. [41] Es parte del sistema operativo Ares, soporta x86-64 y aarch64 y todavía se encuentra en desarrollo activo a febrero de 2023. [42]
{{cite journal}}: CS1 maint: DOI inactivo a partir de noviembre de 2024 ( enlace )