L4 es una familia de microkernels de segunda generación , que generalmente se usa para implementar sistemas operativos similares a Unix , pero también se usa en una variedad de otros sistemas.
L4, como su predecesor , el microkernel L3 , fue creado por el 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 el código de lenguaje ensamblador específico de Intel i386 codificado a mano en 1993 despertó un gran interés en la industria de la computación. [ cita requerida ] Desde su introducción, L4 se ha desarrollado para la independencia de la plataforma y también para mejorar la seguridad , el aislamiento yrobustez .
Ha habido varias reimplementaciones de la interfaz del kernel L4 binaria original ( ABI ) y sus sucesores, incluidos L4Ka :: Pistachio ( Uni Karlsruhe ), L4 / MIPS ( UNSW ), Fiasco ( TU Dresden ). Por esta razón, el nombre L4 se ha generalizado y ya no solo se refiere 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 envía en miles de millones de dispositivos móviles. [1] [2]
Paradigma de diseño
Al especificar la idea general de un micronúcleo , Liedtke afirma:
Un concepto es tolerado dentro del microkernel solo si moverlo fuera del kernel, es decir, permitir implementaciones competitivas, evitaría la implementación de la funcionalidad requerida del sistema. [3]
Con este espíritu, el microkernel L4 proporciona algunos mecanismos básicos: espacios de direcciones (abstracción de tablas de página y protección de memoria), hilos y programación (abstracción de ejecución y protección temporal) y comunicación entre procesos (para comunicación controlada a través de fronteras 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 similar a Unix , los servidores deben proporcionar la administración de derechos que Mach incluyó dentro del kernel.
Historia
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 la década de 1990. El concepto de comunicación del proceso de almacenamiento en búfer asíncrono en el 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 sistemas de archivos o controladores, de regreso al kernel. [ cita requerida ] Si bien esto mejoró un poco los problemas de rendimiento, claramente viola el concepto de minimidad 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 pobre; es decir, da como resultado demasiados fallos de caché , de los cuales la mayoría son en el kernel. [3] Este análisis dio lugar al principio de que un microkernel eficiente debería 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 IPC más delgada y bien diseñada , con una cuidadosa atención al rendimiento y al diseño específico de la máquina (en contraposición al diseño independiente de la plataforma) podría producir mejoras masivas en el rendimiento en el mundo real. En lugar del complejo sistema IPC de Mach, su microkernel L3 simplemente transmitió el mensaje sin gastos generales adicionales. Se consideró que la definición e implementación de las políticas de seguridad requeridas eran deberes de los servidores de espacio de usuario . La función del kernel era solo 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 TÜV SÜD [ cita requerida ] .
L4
Después de un poco de experiencia en el uso de L3, Liedtke llegó a la conclusión de que varios 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 con un alto rendimiento en mente. Con el fin de exprimir 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. [4] Estos aumentos de rendimiento tan dramáticos son un evento poco común en los sistemas operativos, y el trabajo de Liedtke provocó nuevas implementaciones de L4 y el trabajo en sistemas basados en L4 en varias universidades e institutos de investigación, incluida 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 sistemas basados en L4 y microkernel en general, especialmente el sistema operativo Sawmill. [5]
L4Ka :: Avellana
En 1999, Liedtke se hizo cargo del Grupo de Arquitectura de Sistemas en la Universidad de Karlsruhe , donde continuó la investigación sobre sistemas de 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 en lenguaje ensamblador puro de los núcleos fueron efectivamente descontinuadas.
L4 / Fiasco
Paralelamente al desarrollo de L4Ka :: Hazelnut, en 1998 el Grupo de Sistemas Operativos TUD: OS de TU Dresden (Universidad Tecnológica de Dresde) comenzó a desarrollar su propia implementación C ++ de la interfaz del kernel L4, llamada L4 / Fiasco. A diferencia de L4Ka :: Hazelnut, que no permite la concurrencia en el kernel en absoluto y su sucesor L4Ka :: Pistachio, que permite interrupciones en el kernel solo en puntos de preferencia específicos, L4 / Fiasco era completamente interrumpible (con la excepción de extremadamente operaciones atómicas cortas) para lograr una latencia de interrupción baja . Esto se consideró necesario porque L4 / Fiasco se utiliza como base de DROPS, [6] un sistema operativo duro con capacidad en tiempo real, también desarrollado en TU Dresden . Sin embargo, las complejidades de un diseño totalmente interrumpible hicieron que las versiones posteriores de Fiasco volvieran al enfoque tradicional L4 de ejecutar el kernel con las interrupciones desactivadas, excepto por un número limitado de puntos de preferencia.
Independencia de la plataforma
L4Ka :: Pistacho
Hasta el lanzamiento de L4Ka :: Pistachio y las versiones más recientes de Fiasco, todos los microkernels L4 habían estado inherentemente ligados a la arquitectura de la CPU subyacente. El siguiente gran cambio en el desarrollo de L4 fue el desarrollo de una API 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 hilos y espacios de direcciones, y la introducción del control de hilos 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 con enfoque tanto en el alto rendimiento como en así como portabilidad. Fue lanzado bajo la licencia BSD de dos cláusulas .
Nuevas versiones de Fiasco
El micronúcleo L4 / Fiasco también se ha mejorado mucho a lo largo de los años. Ahora es compatible con varias plataformas de hardware que van desde x86 a AMD64 hasta varias plataformas ARM. En particular, una versión de Fiasco (Fiasco-UX) puede ejecutarse como una aplicación a nivel de usuario sobre Linux.
L4 / Fiasco implementa varias extensiones a la API L4v2. Exception IPC permite que el kernel envíe excepciones de CPU a aplicaciones de controlador a nivel de usuario. Con la ayuda de subprocesos alienígenas , es posible realizar un control detallado sobre las llamadas al sistema. Se han añadido UTCB de estilo X.2. Además, Fiasco contiene mecanismos para controlar los derechos de comunicación, así como el consumo de recursos a nivel de kernel. Además de 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) (llamada L 4 Linux ).
Universidad de Nueva Gales del Sur y NICTA
El desarrollo también tuvo lugar 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 mezcla de ensamblador y C) eran importables y cada uno se implementó desde cero. Con el lanzamiento del altamente portátil L4Ka :: Pistachio, el grupo UNSW abandonó sus propios kernels a favor de producir puertos altamente ajustados de L4Ka :: Pistachio, incluida la implementación de transmisión de mensajes más rápida jamás reportada (36 ciclos en la arquitectura Itanium ) . [7] El grupo también ha demostrado que los controladores de dispositivos a nivel de usuario pueden funcionar tan bien como los controladores del kernel, [8] 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 , Wombat demuestra costos de cambio de contexto que son hasta 50 veces más bajos que en Linux nativo. [9]
Más tarde, el grupo UNSW, en su nuevo hogar en NICTA , bifurcó L4Ka :: Pistachio en una nueva versión L4 llamada NICTA :: L4-embedded . Como su nombre lo indica, esto tenía como objetivo su uso en sistemas integrados comerciales y, en consecuencia, las compensaciones de implementación favorecieron las huellas de memoria pequeñas y apuntaron a reducir la complejidad. 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. [10]
Despliegue comercial
En noviembre de 2005, NICTA anunció [11] 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 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. OKL4 Versión 2.1, lanzada en abril de 2008, fue la primera versión de L4 disponible de forma generalizada 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 nativa llamada OKL4 Microvisor. OK Labs también distribuyó un Linux paravirtualizado llamado OK: Linux, un descendiente de Wombat, así como 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, [2] principalmente en chips de módem inalámbricos de Qualcomm. Otras implementaciones incluyen sistemas de información y entretenimiento para automóviles . [12]
Los procesadores de la serie A de Apple que comienzan con el A7 contienen un coprocesador Secure Enclave que ejecuta un sistema operativo L4 [13] basado en el kernel integrado en L4 desarrollado en NICTA en 2006. [14] Esto implica que L4 ahora se envía a todos los dispositivos iOS, el envío total de los cuales se estima en 310 millones para el año 2015. [15]
Alta seguridad: seL4
En 2006, el grupo NICTA inició 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. Desde el principio, el desarrollo tuvo como objetivo 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 Haskell . [16] seL4 utiliza el control de acceso basado en capacidades para permitir un razonamiento formal sobre la accesibilidad de los objetos.
Una prueba formal de corrección funcional se completó en 2009. [17] La prueba proporciona una garantía de que la implementación del kernel es correcta contra su especificación, e implica que está libre de errores de implementación como interbloqueos, livelocks , desbordamientos de búfer, excepciones aritméticas o uso de variables no inicializadas. seL4 se afirma que es el primer kernel de sistema operativo de propósito general que se ha verificado. [17]
seL4 adopta un enfoque novedoso para la gestión de recursos del kernel, [18] exportando la gestión de los recursos del kernel a nivel de usuario y los somete 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 habilitador para pruebas posteriores de que seL4 refuerza las propiedades de seguridad básicas de integridad y confidencialidad. [19] El equipo de NICTA también demostró la exactitud de la traducción de C a código de máquina ejecutable, sacando al compilador de la base de computación confiable de seL4. [20] 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 SO en modo protegido publicado con un análisis completo y sólido del tiempo de ejecución del peor de los casos (WCET), un requisito previo para su uso en sistemas duros en tiempo real . [19]
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 . [21] El código fuente del kernel y las pruebas están bajo 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ó que la Fundación seL4 se creó bajo el paraguas de la Fundación Linux para acelerar el desarrollo y la implementación de seL4. [22]
Los investigadores afirman que el costo de la verificación formal del software es más bajo que el costo de diseñar el software tradicional de "alta seguridad" a pesar de proporcionar resultados mucho más confiables. [23] Específicamente, el costo de una línea de código durante el desarrollo de SEL4 se estimó en alrededor de 400 dólares EE.UU. , en comparación con 1.000 dólares EE.UU. para los sistemas tradicionales de alta seguridad. [24]
Bajo el programa DARPA High-Assurance Cyber Military Systems (HACMS), NICTA junto con los socios del proyecto Rockwell Collins , Galois Inc, la Universidad de Minnesota y Boeing desarrollaron un dron de alta seguridad basado en seL4, junto con otras herramientas y software de aseguramiento, con transferencia de tecnología planificada al helicóptero Little Bird autónomo, opcionalmente pilotado , que está desarrollando Boeing. La demostración final de la tecnología HACMS tuvo lugar en Sterling, VA en abril de 2017. [25] DARPA también financió varios contratos de Small Business Innovative Research (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. [26]
Otra investigación y desarrollo
Osker, un sistema operativo escrito en Haskell , apuntó a la especificación L4; aunque este proyecto se centró en el uso de un lenguaje de programación funcional para el desarrollo de sistemas operativos, no en la investigación de microkernel per se. [27]
CodeZero [28] es un microkernel L4 dirigido a sistemas embebidos con un enfoque en la virtualización e implementación de servicios de SO nativos. Hay una versión con licencia GPL , [29] y una versión que fue licenciada nuevamente por B Labs Ltd., adquirida por Nvidia , como código cerrado y bifurcada en 2010. [30] [31]
El microkernel F9, [32] una implementación L4 con licencia BSD, está dedicada a los procesadores ARM Cortex-M para dispositivos profundamente integrados con protección de memoria.
La arquitectura de virtualización de NOVA OS [33] es un proyecto de investigación que se centra en la construcción de un entorno de virtualización seguro y eficiente [34] [35] con una pequeña base informática confiable. NOVA consta de un microhipervisor, un monitor de máquina virtual a nivel de usuario y un entorno de usuario multiservidor con componentes sin privilegios que se ejecuta encima de él llamado NUL. NOVA se ejecuta en sistemas multinúcleo basados en ARMv8-A y x86.
WrmOS [36] es un sistema operativo en tiempo real basado en microkernel L4. Tiene implementaciones propias de kernel, bibliotecas estándar y pila de red, soportando arquitecturas SPARC, ARM, x86 y x86_64. Existe el kernel de Linux paravirtualizado (w4linux [37] ) trabajando sobre WrmOS.
Ver también
- PikeOS
Referencias
- ^ "Productos de hipervisor - sistemas de misión de dinámica general" . gdmissionsystems.com . Archivado desde el original el 15 de noviembre de 2017 . Consultado el 26 de abril de 2018 .
- ^ a b "El software Open Kernel Labs supera el hito de 1.500 millones de envíos de dispositivos móviles" (Comunicado de prensa). Abra Kernel Labs . 19 de enero de 2012. Archivado desde el original el 11 de febrero de 2012.
- ^ a b Liedtke, Jochen (diciembre de 1995). "Sobre la construcción de µ-Kernel" . Proc. 15º Simposio de ACM sobre principios de sistemas operativos (SOSP) . págs. 237-250. Archivado desde el original el 25 de octubre de 2015.
- ^ Liedtke, Jochen (diciembre de 1993). "Mejora de IPC por diseño de kernel" . 14º Simposio de ACM sobre principios de sistemas operativos . Asheville, Carolina del Norte, Estados Unidos. págs. 175–88.
- ^ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen ; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars (2000). "El enfoque multiservidor Aserradero" . Taller europeo ACM SIGOPS . Kolding, Dinamarca. págs. 109-114.
- ^ "Copia archivada" . Archivado desde el original el 7 de agosto de 2011 . Consultado el 10 de agosto de 2011 .CS1 maint: copia archivada como título ( enlace )
- ^ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (abril de 2005). "Itanium: el cuento de un implementador de sistemas" . Conferencia Técnica Anual de USENIX . Annaheim, CA, Estados Unidos. págs. 264-278. Archivado desde el original el 17 de febrero de 2007.
- ^ Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot (septiembre de 2005). "Controladores de dispositivos a nivel de usuario: rendimiento logrado". Revista de Ciencias y Tecnología de la Computación . 20 (5): 654–664. CiteSeerX 10.1.1.59.6766 . doi : 10.1007 / s11390-005-0654-4 . S2CID 1121537 .
- ^ van Schaik, Carl; Heiser, Gernot (enero de 2007). "Microkernels de alto rendimiento y virtualización sobre ARM y arquitecturas segmentadas" . 1er Taller Internacional de Microkernels para Sistemas Embebidos . Sídney, Australia: NICTA. págs. 11-21. Archivado desde el original el 1 de marzo de 2015 . Consultado el 25 de octubre de 2015 .
- ^ Ruocco, Sergio (octubre de 2008). "Tour de un programador en tiempo real de microkernels L4 de uso general". Revista EURASIP sobre sistemas integrados . 2008 : 1–14. doi : 10.1155 / 2008/234710 . S2CID 7430332 .
- ^ "NICTA L4 Microkernel to be used in Select QUALCOMM Chipset Solutions" (Comunicado de prensa). NICTA. 24 de noviembre de 2005. Archivado desde el original el 25 de agosto de 2006.
- ^ "Virtualización automotriz de Open Kernel Labs seleccionada por Bosch para sistemas de infoentretenimiento" (Comunicado de prensa). Abra Kernel Labs . 27 de marzo de 2012. Archivado desde el original el 2 de julio de 2012.
- ^ "Seguridad de iOS, iOS 12.3" (PDF) . Apple Inc. Mayo de 2019.
- ^ Mandt, Tarjei; Solnik, Mathew; Wang, David (31 de julio de 2016). "Desmitificando el procesador Secure Enclave" (PDF) . BlackHat USA . Las Vegas, NV, Estados Unidos. Archivado (PDF) desde el original el 21 de octubre de 2016.
- ^ Elmer-DeWitt, Philip (28 de octubre de 2014). "Pronóstico: Apple enviará 310 millones de dispositivos iOS en 2015" . Fortuna . Archivado desde el original el 27 de septiembre de 2015 . Consultado el 25 de octubre de 2015 .
- ^ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Polla; David; Chakravarty, Manuel MT (septiembre de 2006). "Ejecución del manual: un enfoque para el desarrollo de microkernel de alta seguridad" . Taller ACM SIGPLAN Haskell . Portland, Oregon . págs. 60–71.
- ^ a b Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot ; Andronick, junio; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (octubre de 2009). "seL4: verificación formal de un kernel del sistema operativo" (PDF) . 22º Simposio de ACM sobre principios de sistemas operativos . Big Sky, MT, Estados Unidos. Archivado (PDF) desde el original el 28 de julio de 2011.
- ^ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (abril de 2008). Diseño de kernel para aislamiento y aseguramiento de la memoria física . 1er Taller de Aislamiento e Integración en Sistemas Embebidos. Glasgow, Reino Unido. doi : 10.1145 / 1435458 . Consultado el 22 de febrero de 2020 .
- ^ a b Klein, Gerwin; Andronick, junio; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (febrero de 2014). "Verificación formal integral de un microkernel del sistema operativo". Transacciones ACM en sistemas informáticos . 32 (1): 2: 1–2: 70. CiteSeerX 10.1.1.431.9140 . doi : 10.1145 / 2560537 . S2CID 4474342 .
- ^ Sewell, Thomas; Myreen, Magnus; Klein, Gerwin (junio de 2013). "Validación de traducción para un kernel de sistema operativo verificado" . Conferencia ACM SIGPLAN sobre Diseño e Implementación de Lenguajes de Programación . Seattle, WA, Estados Unidos. doi : 10.1145 / 2491956.2462183 .
- ^ "El sistema operativo seguro desarrollado por NICTA se convierte en código abierto" (Comunicado de prensa). NICTA . 29 de julio de 2014. Archivado desde el original el 15 de marzo de 2016.
- ^ "Security Gets Support of Linux Foundation" (Comunicado de prensa). Fundación Linux . 7 de abril de 2020. Archivado desde el original el 15 de marzo de 2016.
- ^ Klein, Gerwin; Andronick, junio; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Verificación formal integral de un microkernel de SO" (PDF) . Transacciones ACM en sistemas informáticos . 32 : 64. CiteSeerX 10.1.1.431.9140 . doi : 10.1145 / 2560537 . S2CID 4474342 . Archivado (PDF) desde el original el 3 de agosto de 2014.
- ^ seL4 es gratis - ¿Qué significa esto para usted? en YouTube
- ^ "DARPA selecciona a Rockwell Collins para aplicar la tecnología de ciberseguridad a nuevas plataformas" (Comunicado de prensa). Rockwell Collins . 24 de abril de 2017. Archivado desde el original el 11 de mayo de 2017.
- ^ "Patrocinador de la agencia DARPA Dr. John Launchbury" . SBIRSource . 2017. Archivado desde el original el 29 de septiembre de 2017 . Consultado el 16 de mayo de 2017 .
- ^ Hallgren, T .; Jones, diputado; Leslie, R .; Tolmach, A. (2005). "Un enfoque basado en principios para la construcción de sistemas operativos en Haskell" (PDF) . Actas de la Décima Conferencia Internacional ACM SIGPLAN sobre Programación Funcional . 40 (9): 116-128. doi : 10.1145 / 1090189.1086380 . ISSN 0362-1340 . Archivado (PDF) desde el original el 15 de junio de 2010 . Consultado el 24 de junio de 2010 .
- ^ ANUNCIO - Presentamos Codezero
- ^ "jserv / codezero: Codezero Microkernel" . Archivado desde el original el 15 de agosto de 2015 . Consultado el 20 de octubre de 2020 .
- ^ "Código cero: hipervisor y sistema operativo integrados" . Archivado desde el original el 11 de enero de 2016 . Consultado el 25 de enero de 2016 .
- ^ "Copia archivada" . Archivado desde el original el 2 de febrero de 2014 . Consultado el 2 de febrero de 2014 .CS1 maint: copia archivada como título ( enlace )
- ^ "F9 Microkernel" . Consultado el 20 de octubre de 2020 .
- ^ "Sitio web de NOVA Microhypervisor" . Consultado el 9 de enero de 2021 .
- ^ Steinberg, Udo; Kauer, Bernhard (abril de 2010). "NOVA: una arquitectura de virtualización segura basada en microhypervisor". EuroSys '10: Actas de la 5ª Conferencia Europea de Sistemas Informáticos . París, Francia .
- ^ Steinberg, Udo; Kauer, Bernhard (abril de 2010). "Hacia un entorno de nivel de usuario multiprocesador escalable". IIDS'10: Taller de Aislamiento e Integración de Sistemas Confiables . París, Francia .
- ^ "WrmOS" . Consultado el 20 de octubre de 2020 .
- ^ "w4linux es un kernel de Linux paravirtualizado que funciona sobre WrmOS" . Consultado el 20 de octubre de 2020 .
Otras lecturas
- Jochen Liedtke, Ulrich Bartling, Uwe Beyer, Dietmar Heinrichs, Rudolf Ruland, Gyula Szalay. Dos años de experiencia con un sistema operativo basado en μ-Kernel , ACM Press 1991
- Liedtke, Jochen ; Haeberlen, Andreas; Park, Yoonho; Reuther, Lars; Uhlig, Volkmar (22 de octubre de 2000). "El rendimiento del código stub se está volviendo importante" . En Actas del 1er Taller sobre Experiencias Industriales con Software de Sistemas (WIESS), San Diego, CA, octubre de 2000 . Archivado desde el original (PDF) el 2006-09-05 . Consultado el 5 de septiembre de 2006 . (en el kernel y el compilador L4)
- Cheng Guanghui, Nicholas Mc Guire. L4 / Fiasco / L4Linux Kickstart , laboratorio de sistemas integrados y distribuidos - Universidad de Lanzhou
- Elphinstone, Kevin; Heiser, Gernot (noviembre de 2013). "De L3 a seL4: ¿Qué hemos aprendido en 20 años de microkernels L4?" . 24º Simposio ACM SIGOPS sobre principios de sistemas operativos . Farmington, PA, Estados Unidos. págs. 133–150. Evolución de los enfoques de diseño e implementación de L4
enlaces externos
- L4Hq: sede de L4, sitio comunitario para proyectos de L4 Archivado el 25 de octubre de 2019 en Wayback Machine
- página de inicio de seL4
- La familia de microkernel L4 : descripción general de las implementaciones, la documentación y los proyectos de L4
- TUD oficial: OS Wiki
- L4Ka : Implementaciones L4Ka :: Pistacho y L4Ka :: Avellana
- UNSW : Implementaciones para la arquitectura DEC Alpha y MIPS
- OKL4 Archivado 2008-08-20 en Wayback Machine : Versión comercial L4 de Open Kernel Labs Archivado 2009-03-19 en Wayback Machine
- NICTA L4 : Resumen de la investigación y publicaciones archivadas] 2014-07-17 en Wayback Machine
- Trustworthy Systems Group en CSIRO's Data61 : actual hogar del antiguo grupo NICTA que desarrolló seL4
- Marco del sistema operativo Genode : un vástago de la comunidad L4