Familia de micronúcleos L4

L4 es una familia de micronúcleos de segunda generación, utilizados para implementar una variedad de tipos de sistemas operativos (SO), aunque principalmente para la interfaz de sistema operativo portátil similar a Unix. i> (POSIX) tipos compatibles.

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 sintió 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 despertó un gran interés en la industria informática. Desde su introducción, L4 se ha desarrollado para ser multiplataforma y mejorar la seguridad, el aislamiento y la robustez.

Ha habido varias reimplementaciones de la interfaz binaria (ABI) de la aplicación del kernel binario 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 Dresden (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 kernel L4 y sus diferentes versiones.

L4 está ampliamente implementado. Una variante, OKL4 de Open Kernel Labs, se distribuyó en miles de millones de dispositivos móviles.

Paradigma de diseño

Al especificar la idea general de un micronúcleo, Liedtke afirma:

Un concepto se tolera dentro del microcarril solo si lo mueve fuera del núcleo, es decir, permitiendo implementaciones competitivas, evitaría la implementación de la funcionalidad requerida del sistema.

Con este espíritu, el microkernel L4 proporciona pocos mecanismos básicos: espacios de direcciones (abstracción de tablas de páginas y protección de la memoria), subprocesos y programación (abstracción de la ejecución y protección temporal) y comunicación entre procesos (para una comunicación controlada a través del aislamiento). límites).

Un sistema operativo basado en un microkernel como L4 proporciona servicios como servidores en el espacio del usuario que kernels monolíticos como Linux o 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.

Historia

El bajo rendimiento de los micronúcleos de primera generación, como Mach, llevó a varios desarrolladores a reexaminar todo el concepto de micronúcleo a mediados de la década de 1990. El concepto de comunicación asíncrona del proceso de búfer en el kernel 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 de tiempo crítico, como sistemas de archivos o controladores, de regreso al kernel. Si bien esto mejoró un poco los problemas de rendimiento, claramente viola 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, da como resultado demasiadas fallas de caché, de las cuales la mayoría están en el kernel. 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 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 (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 microkernel L3 simplemente pasó el mensaje sin sobrecarga adicional. Se consideró que la definición e implementación de las políticas de seguridad requeridas eran deberes de los servidores del espacio de usuario. La función 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).

L4 árbol familiar

L4

Después de cierta experiencia con 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 extraer todo el rendimiento, todo el kernel se escribió en lenguaje ensamblador y su IPC era 20 veces más rápido que el de Mach. Estos aumentos drásticos en el rendimiento 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, incluido IBM, donde Liedtke comenzó a trabajar en 1996. Universidad Técnica de 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 el sistema operativo Sawmill.

L4Ka::Avellana

En 1999, Liedtke se hizo cargo del Grupo de Arquitectura de Sistemas de la Universidad de Karlsruhe, donde continuó la investigación de los sistemas de micronúcleo. 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 IA-32- y ARM. -máquinas basadas. El esfuerzo fue un éxito, el rendimiento seguía siendo aceptable y, con su lanzamiento, las versiones en lenguaje ensamblador puro de los núcleos se descontinuaron efectivamente.

L4/Fiasco

Paralelamente al desarrollo de L4Ka::Hazelnut, en 1998 el grupo de sistemas operativos TUD:OS de TU Dresden comenzó a desarrollar su propia implementación en C++ de la interfaz del kernel L4, llamada L4/Fiasco. A diferencia de L4Ka::Hazelnut, que no permite la concurrencia en el kernel, y su sucesor L4Ka::Pistachio, que permite interrupciones en el kernel solo en puntos de preferencia específicos, L4/Fiasco era completamente preventivo (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, un sistema operativo con capacidad de computación dura en tiempo real, también desarrollado en la TU Dresden. Sin embargo, las complejidades de un diseño totalmente preventivo provocaron que las versiones posteriores de Fiasco volvieran al enfoque tradicional L4 de ejecutar el núcleo con las interrupciones deshabilitadas, excepto por un número limitado de puntos preventivos.

Multiplataforma

L4Ka::Pistacho

Hasta el lanzamiento de L4Ka::Pistachio y las versiones más recientes de Fiasco, todos los micronúcleos L4 habían estado inherentemente vinculados a la arquitectura de la 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 anteriores de L4, incluida una mejor compatibilidad con 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 (UTCBs) 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 centrándose tanto en el alto rendimiento como en la portabilidad. Fue lanzado bajo la licencia BSD de dos cláusulas.

Versiones más recientes de Fiasco

El micronúcleo L4/Fiasco también se ha mejorado considerablemente a lo largo de los años. Ahora es compatible con varias plataformas de hardware que van desde x86 hasta AMD64 y varias plataformas ARM. En particular, 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 que el kernel envíe excepciones de CPU a aplicaciones de manejo a nivel de usuario. Con la ayuda de subprocesos extraños, 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 de kernel. En Fiasco, se desarrolla una colección de servicios básicos de nivel de usuario (llamado L4Env) que, entre otros, se utilizan para virtualizar la versión actual de Linux (4.19 a partir de mayo de 2019) (llamado L4Linux).

Universidad de Nueva Gales del Sur y NICTA

El desarrollo también ocurrió 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 se llamara 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 implementó desde cero. Con el lanzamiento del altamente portátil L4Ka::Pistachio, el grupo UNSW abandonó sus propios núcleos en favor de producir puertos altamente optimizados de L4Ka::Pistachio, incluida la implementación más rápida jamás informada de paso de mensajes (36 ciclos en la arquitectura Itanium). El grupo también ha demostrado que los controladores de dispositivos pueden funcionar igual de bien a nivel de usuario que en el kernel, 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 más bajos que en Linux nativo.

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- incrustado. Como su nombre lo indica, era para uso en sistemas integrados comerciales y, en consecuencia, las ventajas y desventajas de la 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 al sistema lo suficientemente cortas como para que no necesiten puntos de preferencia para garantizar una alta capacidad de respuesta en tiempo real.

Despliegue comercial

En noviembre de 2005, NICTA anunció que Qualcomm estaba implementando la versión L4 de NICTA en sus conjuntos de chips Mobile Station Modem. Esto condujo 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 desarrollar aún más L4 para uso comercial bajo la marca OKL4, en estrecha colaboración con NICTA. La versión 2.1 de OKL4, lanzada en abril de 2008, fue la primera versión de L4 generalmente disponible que incluía seguridad basada en capacidades. OKL4 3.0, lanzado en octubre de 2008, fue la última versión de código abierto de OKL4. 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 1500 millones a principios de 2012, principalmente en chips de módem inalámbrico Qualcomm. Otros despliegues incluyen sistemas de información y entretenimiento para automóviles.

Los procesadores de la serie A de Apple que comienzan con A7 contienen un coprocesador Secure Enclave que ejecuta un sistema operativo L4 basado en el kernel integrado L4 desarrollado en NICTA en 2006. Esto implica que L4 ahora se distribuye en todos los dispositivos iOS, cuyo envío total se estima en 310 millones para el año 2015.

Alta seguridad: seL4

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 contradictorios, de rendimiento y verificación, el equipo utilizó un proceso de software intermedio a partir de una especificación ejecutable escrita en Haskell. seL4 utiliza el control de acceso de seguridad basado en la capacidad para permitir el razonamiento formal sobre la accesibilidad de los objetos.

En 2009 se completó una prueba formal de corrección funcional. La prueba proporciona una garantía de que la implementación del kernel es correcta en comparación con su especificación e implica que está libre de errores de implementación, como interbloqueos, bloqueos dinámicos, 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 se ha verificado.

seL4 adopta un enfoque novedoso para la gestión de recursos del kernel, exportando la gestión de los recursos del kernel al nivel del usuario y sometiéndolos al mismo control de acceso basado en la capacidad 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 hace cumplir las propiedades de seguridad básicas de integridad y confidencialidad. 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. 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 dura en tiempo real.

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. El código fuente y las pruebas del kernel tienen 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.

Los investigadores afirman que el costo de la verificación formal del software es más bajo que el costo de la ingeniería tradicional de "alta seguridad" software a pesar de proporcionar resultados mucho más fiables. 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 sistemas tradicionales de alta seguridad.

En el marco del programa HACMS (High-Assurance Cyber Military Systems) 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 aseguramiento, 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, VA, en abril de 2017. 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 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.

Otra investigación y desarrollo

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 del sistema operativo, no en la investigación de microkernel.

CodeZero es un microkernel L4 para sistemas integrados que se centra en la virtualización y la implementación de servicios de SO nativos. Hay una versión con licencia GPL y una versión que fue relicenciada por B Labs Ltd., adquirida por Nvidia, como código cerrado y bifurcada en 2010.

El microkernel F9, 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 de NOVA OS es un proyecto de investigación centrado en la construcción de un entorno de virtualización seguro y eficiente. 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 sin privilegios que se ejecuta en él denominado NUL. NOVA se ejecuta en sistemas multinúcleo basados en ARMv8-A y x86.

WrmOS es un sistema operativo en tiempo real basado en microkernel L4. Tiene implementaciones propias de kernel, bibliotecas estándar y pila de red, compatible con arquitecturas ARM, SPARC, x86 y x86-64. Existe el kernel de Linux paravirtualizado (w4linux) que funciona en WrmOS.

Helios es un microkernel inspirado en seL4. Es parte del sistema operativo Ares, admite x86-64 y aarch64 y todavía está en desarrollo activo a partir de febrero de 2023.