- seL4 es un microkernel de SO orientado a sistemas embebidos y ciberfísicos donde la seguridad y la confiabilidad son críticas; aísla y multiplexa recursos de hardware, pero no es un SO de propósito general completo
- Reduce el código en modo kernel a unos 10 kSLOC para disminuir la TCB y la superficie de ataque, y desplaza servicios del SO como sistema de archivos, red y drivers al modo usuario
- Es el primer kernel de SO del mundo con verificación formal a nivel de código, y en sistemas configurados correctamente el kernel incluso garantiza propiedades de seguridad como confidencialidad, integridad y disponibilidad
- Combina control de acceso basado en capabilities, análisis WCET, soporte para sistemas de tiempo real de criticidad mixta y funciones de hipervisor para ofrecer aislamiento fino junto con tiempo real
- La API de seL4 es de muy bajo nivel, por lo que no es fácil construir sistemas complejos directamente; cuando encaja una arquitectura estática, usar frameworks como Microkit es una opción más realista
Alcance de seL4
- seL4 es un microkernel, es decir, la parte central de bajo nivel de un sistema operativo
- El SO controla el hardware y los recursos en modo kernel, un modo de ejecución con privilegios más altos del procesador
- Las aplicaciones se ejecutan en modo usuario y solo acceden al hardware de las maneras permitidas por el SO
- Un microkernel es el núcleo del SO que minimiza el código que se ejecuta con altos privilegios
- seL4 pertenece a la familia de microkernels L4, cuya historia se remonta a mediados de los años 90
- seL4 no tiene relación con seLinux
- seL4 no es un SO completo, sino un kernel de bajo nivel que multiplexa y aísla recursos de hardware de forma segura
- Servicios comunes del SO, como el sistema de archivos, el stack de red y los drivers de dispositivos, no están dentro del kernel
- Esos servicios deben proporcionarse como programas en modo usuario
Estructura de microkernel y reducción de la superficie de ataque
- Los kernels monolíticos como Linux ofrecen servicios del SO, como almacenamiento de archivos y redes, como código en modo kernel
- El código en modo kernel puede acceder sin restricciones a los recursos del sistema, por lo que si un bug deriva en escalación de privilegios o ejecución arbitraria de código, todo el sistema puede verse comprometido
- Se estima que el kernel de Linux tiene alrededor de 20 MSLOC y podría contener decenas de miles de bugs
- Un microkernel bien diseñado como seL4 reduce el código en modo kernel a alrededor de 10 kSLOC
- Eso lo hace varios órdenes de magnitud más pequeño que el kernel de Linux
- Al reducir la TCB, también se reduce la superficie de ataque
- La mayoría de los servicios del SO salen del kernel, y el microkernel actúa como una capa delgada alrededor del hardware
- Las funciones principales que ofrece son el aislamiento entre programas y un mecanismo seguro de llamadas
- Los servicios ya no viven dentro del kernel, sino que pasan a ser programas en modo usuario que se ejecutan en sandboxes separados
- Un estudio que analizó casos conocidos de compromisos graves en Linux concluyó que un diseño de microkernel podía eliminar por completo 29% de ellos y mitigar otro 55% hasta el punto de que dejaran de clasificarse como críticos
PPC, capabilities y control fino de permisos
- seL4 ofrece un mecanismo de PPC (protected procedure call)
- Por razones históricas todavía se usa el término IPC, pero esa expresión puede inducir a error y llevar a malos diseños
- PPC permite que un programa llame de forma segura a una función de otro programa ubicado en otro sandbox
- El microkernel transporta entradas y salidas en el PPC y hace cumplir la interfaz
- Las funciones remotas solo pueden invocarse mediante puntos de entrada exportados
- Solo pueden llamarlas clientes explícitamente autorizados que hayan recibido la capability adecuada
- Una capability es un token de acceso que permite usar un recurso específico del sistema
- Permite controlar con mucho detalle qué entidad puede acceder a qué recurso
- Da soporte al principio de mínimo privilegio o POLA
- Los mecanismos de control de acceso de sistemas dominantes como Linux o Windows no permiten alcanzar este nivel de mínimo privilegio
- seL4 es el único SO del mundo que combina un modelo basado en capabilities con verificación formal, y se considera que esta combinación permite sostener de forma defendible la afirmación de que es el SO más seguro del mundo
Verificación formal y garantías de seguridad
- seL4 ofrece pruebas formales, matemáticas y verificadas por máquina sobre la corrección de su implementación
- Estas pruebas significan, en un sentido muy fuerte respecto de la especificación, que el kernel está “libre de bugs”
- seL4 es el primer kernel de SO del mundo con este tipo de prueba a nivel de código
- Además de la corrección de implementación, seL4 ofrece pruebas adicionales sobre la imposición de seguridad
- En un sistema basado en seL4 configurado correctamente, el kernel garantiza confidencialidad, integridad y disponibilidad
- La cadena de verificación es el principal diferenciador de seL4
- Para que el kernel sea una base confiable en sistemas críticos de seguridad y confiabilidad, se necesitan garantías sólidas tanto sobre la implementación como sobre las propiedades de seguridad
Tiempo real y sistemas de criticidad mixta
- seL4 es un kernel de SO sometido a un análisis completo y sólido del WCET (worst-case execution time)
- Si el kernel está configurado adecuadamente, todas las operaciones del kernel tienen un límite temporal
- Y ese límite además es conocido
- Estas características son un requisito previo para construir sistemas de tiempo real estricto
- Se orientan a sistemas donde no reaccionar a un evento dentro de un tiempo estrictamente acotado puede ser catastrófico
- seL4 también soporta sistemas de tiempo real de criticidad mixta (MCS)
- Está pensado para entornos donde debe garantizarse la temporalidad de actividades importantes incluso si se ejecuta en la misma plataforma código menos confiable
- A diferencia de los SO MCS tradicionales, que usan particionamiento rígido e inflexible de tiempo y espacio, seL4 ofrece un modelo flexible que mantiene el aprovechamiento de recursos
seL4 como hipervisor
- seL4 es tanto un microkernel como un hipervisor
- Puede ejecutar máquinas virtuales sobre seL4
- Dentro de esas máquinas virtuales puede correr un SO invitado general como Linux
- Los invitados y las aplicaciones pueden comunicarse entre sí según los canales de comunicación impuestos por seL4
- También pueden comunicarse con aplicaciones nativas
- Es posible usar una VM de Linux como medio para proporcionar servicios del sistema
- En una configuración de ejemplo, servicios como red y almacenamiento se obtienen de varias instancias de Linux que se ejecutan en VMs separadas
Cómo construir sistemas sobre seL4
- La API de seL4 es de muy bajo nivel, incluso comparada con la de otros microkernels
- Solo proporciona las abstracciones mínimas necesarias para gestionar el hardware de forma segura
- seL4 ha sido descrito como el “lenguaje ensamblador de los sistemas operativos”
- No es adecuado construir sistemas complejos directamente sobre seL4
- Hace falta un framework de más alto nivel que permita concentrarse en el código de implementación de servicios y automatice la complejidad del hardware y la integración del sistema
- seL4 cuenta con tres frameworks principales de componentes open source
- Microkit: simplifica la API de seL4 con unas pocas abstracciones centradas en protection domains, y ofrece un SDK que integra módulos compilados por separado y el binario del kernel para crear una imagen arrancable
- CAmkES: es el predecesor de Microkit y un framework de componentes para sistemas de arquitectura estática, pero al no tener SDK el proceso de build es más incómodo y tiene más overhead
- Genode: soporta varios microkernels y ofrece abundantes servicios y drivers para plataformas x86; no impone una arquitectura estática, pero no aprovecha todas las funciones de seguridad y confiabilidad de seL4 ni tiene una historia de garantías
- Siempre que una arquitectura estática se ajuste a los requisitos, se recomienda Microkit para construir sistemas basados en seL4
- Una arquitectura estática es un modelo donde el conjunto de módulos y la estructura de comunicación se definen al momento de configurar el sistema
- Se considera que este modelo encaja con los requisitos de la mayoría de los sistemas embebidos, incluidos sistemas ciberfísicos complejos como los de automoción y aeronáutica
1 comentarios
Comentarios en Hacker News
seL4 en sí ya es tema viejo, pero me pregunto si además del microkernel se han añadido nuevas capas o componentes verificados formalmente
También parece que hay personas que, al ver la palabra “prueba”, se saturan emocionalmente y se les bloquea el pensamiento. La verificación formal no es una panacea que resuelva el problema infinito de la seguridad en TI, ni un método para producir software perfecto
Según entiendo, se trata de una prueba de que se satisfacen ciertos requisitos bajo ciertas condiciones, y esos requisitos y condiciones pueden ser bastante estrechos, lo que significa que no dice nada sobre funciones y condiciones fuera de la especificación; me pregunto si esa idea es más o menos correcta
A nivel práctico, también me pregunto qué espera un especialista en seguridad cuando ve “software verificado formalmente”. Siento que aquí la información clave es cuál es la especificación que cumple seL4
https://github.com/seL4/seL4/pull/243
https://github.com/seL4/l4v/pull/453
También hay varios bugs relacionados con memoria en el rastreador de issues
https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
Curiosamente, el PR que corrigió el “register clobbering” de memoria no tiene la etiqueta bug, así que no aparece si filtras por “bug”. Antes pensaba que, gracias a las pruebas, seL4 era inmune a este tipo de problemas, pero después de ver esto empecé a pensar que las pruebas no son tan abarcadoras como la comunidad llegó a creer. Aun así, seL4 sigue siendo software muy impresionante
Para responder a la pregunta, la especificación que cumple seL4 está publicada en GitHub
https://github.com/seL4/l4v
La planificación de criticidad mixta ofrece acceso basado en capabilities al tiempo de CPU, límites máximos de ejecución por hilo, garantía de prioridad y acceso a recursos para tareas de alta criticidad, y “passive servers” que corren con tiempo de planificación donado por el llamador
Microkit es una capa de abstracción verificada que facilita mucho construir sistemas reales sobre seL4, y Device Driver Framework es un conjunto de plantillas de controladores, implementaciones de plano de control/plano de datos y herramientas para escribir drivers y virtualizar dispositivos de alto rendimiento en seL4
La verificación formal puede garantizar que ciertos requisitos se cumplen bajo ciertas condiciones. En general es cierto que esos requisitos y condiciones pueden ser estrechos, pero en el caso de seL4 hay muchas pruebas que cubren un rango amplio de propiedades esperables en un kernel, y esas garantías se sostienen incluso bajo supuestos muy débiles. Ni siquiera se asume la corrección del compilador de C: existe una herramienta aparte que examina la salida del compilador y prueba que el binario compilado se comporta conforme a la semántica de C requerida
Entre los requisitos que cumple seL4 está que el código binario del kernel implementa exactamente el comportamiento descrito en la especificación abstracta y no hace nada más. No hay buffer overflows, memory leaks, errores de punteros, dereferencias de punteros nulos, comportamiento indefinido del código C, ni terminaciones del kernel fuera de los métodos explícitos enumerados en la especificación
La especificación y el binario de seL4 también satisfacen propiedades de seguridad de integridad y confidencialidad. Integridad significa que no existe ninguna forma de que un proceso modifique datos para los que no tiene permiso explícito, y confidencialidad significa que no puede leer datos no autorizados de ninguna manera. Incluso se demuestra que no puede inferirse indirectamente información por ciertos canales laterales. Además de seguridad, también se cumplen garantías de peor tiempo de ejecución esperado y propiedades de planificación
El trabajo actual apunta a una adopción más amplia con LionsOS: https://lionsos.org/
https://docs.sel4.systems/projects/sel4/frequently-asked-que...
Usa bastante programación a nivel de tipos para rastrear recursos, acceso a hardware y capabilities en tiempo de compilación. Como descubrir problemas en runtime y depurarlos es de lo peor, es un intento de llevar parte de las garantías del kernel base hacia el compilador
Me gustan los hosts con microkernel sobre los que se levantan kernels monolíticos invitados; en los servidores están corriendo seL4 como capa de seguridad y respaldo para VMs de FreeBSD, y dentro usan renderfarms, clústeres de BEAM y jails para Jenkins
Lo malo es que no existe un port a ARM para el threading y el kernel intra-proceso de DragonflyBSD, es decir, para ese diseño de kernel híbrido. El sueño es correr OpenMoonRay de forma más eficiente sobre un Ampere Altra de 128 núcleos
Parece que el debate a favor o en contra de los microkernels ya no tiene mucho sentido. La única forma de acceder a servicios privilegiados de manera rápida, eficiente y segura son las mitigaciones por hardware, y hay límites para lo que el software puede hacer
Es parecido a la diferencia entre el 80286 y el 80386. Este último agregó soporte de hardware real para multitarea, algo que el primero no tenía. Después de eso siguieron aumentando los mecanismos de protección a nivel de hardware, como los que hicieron posibles a los hipervisores
Apple, en particular, está metiendo muchas funciones en el SoC para proteger a nivel de chip el kernel, los drivers y los componentes, y para hacer cumplir privilegios al usar hilos y punteros en ejecución. https://support.apple.com/guide/security/operating-system-in...
Eso no significa que el OS sea imposible de vulnerar, pero es mucho más efectivo que una estrategia de administrar privilegios solo con software. Si se usan este tipo de funciones o similares, da la impresión de que la estructura del kernel ya no es tan importante; me pregunto si estoy equivocado
También hay mucho que aprender de sistemas micro/híbridos más componibles. Por ejemplo, Plan 9 es un excelente sistema híbrido que expone todos los objetos del sistema en espacio de usuario mediante un único protocolo: 9P. Es híbrido porque algunas partes están dentro del kernel para evitar la sobrecarga de llamadas al sistema, como ocurre con IP o TLS
Otro aspecto interesante del diseño es que los drivers dentro del kernel son mínimos y en general solo sirven como una interfaz 9P para la lógica del hardware. Así, objetos de máquina como punteros o registros pueden convertirse en archivos navegables, protegerse con permisos estándar de Unix y distribuir fácilmente componentes entre varias máquinas a través de la red. Como resultado, la lógica del driver puede empujarse de forma segura a programas en espacio de usuario
9P es transparente a la red y a la arquitectura, así que permite trabajar de inmediato entre distintas máquinas como Arm, x86 o mips. Volver de Plan 9 a Linux/Unix o Windows da tristeza y frustración. La flexibilidad es casi de roca ígnea, y las funciones se han ido agregando de forma incompatible entre sí mediante muchísimos protocolos que hacen lo mismo: exponer archivos/objetos
Desde una perspectiva práctica de ingeniería, los kernels monolíticos eran más rápidos, más fáciles y tenían más recursos, mientras que la seguridad era lo que se podía lograr con C: el mejor esfuerzo y una enorme cantidad de bugs. Se introdujo mucho hardware para mitigar ese caos. Pero con seL4, en teoría podría no hacer falta un coprocesador de seguridad, porque hay un nivel muy alto de confianza en el aislamiento entre procesos y en la ausencia de exploits a nivel root. Así que el codesarrollo hardware/software sí importa
Aun así, el equipo de seL4 también tuvo que gastar muchos recursos de ingeniería en eliminar canales laterales del hardware. El mundo real tampoco se preocupa por la simulación física, así que el hardware también tiene defectos
La ventaja del microkernel aquí es que es lo bastante pequeño como para que la verificación formal pueda abarcarlo. La prueba en sí mide 10 veces el tamaño del kernel. El cambio de contexto de seL4 es un múltiplo de un solo dígito más rápido que el de Linux, así que el impacto en rendimiento debería ser despreciable. Pero si mágicamente se pudiera verificar un kernel monolítico de varios millones de líneas, seguiría siendo más rápido no hacer cambios de contexto. De hecho, el equipo de seL4 intentó mover el scheduler al espacio de usuario, pero el costo de rendimiento era demasiado alto, así que lo dejaron dentro del kernel y asumieron esa carga extra en la prueba
Más bien, la función principal del hardware es mejorar la eficiencia. Por ejemplo, los microkernels actuales ya aprovechan bien hardware como la MMU, así que son bastante robustos. Luego, la pequeña base de cómputo confiable del microkernel le da confiabilidad al kernel, y kernel y hardware juntos forman una base sólida
Al final, es cuestión de hasta qué punto se quiere hacer “trampa” con el hardware, pero en general los microkernels aprovechan mejor las funciones de protección. O también puedes mirar los exokernels
https://genode.org/index
Es un sistema operativo con soporte para seL4
He dado una presentación sobre seL4 en un capítulo local de OWASP. No sé si todavía se podrá encontrar el material.
Este proyecto está realmente muy bien hecho, pero especialmente en computación de propósito general cuesta verlo como un reemplazo de Linux. Eso no significa que los microkernels sean malos para uso general en términos generales. RedoxOS parece haber avanzado algo recientemente y usa un microkernel escrito en Rust
Aun así, si Redox tiene éxito, eso por sí solo ya sería un buen avance. En seL4 estas características son todavía más extremas. Sus ventajas técnicas son sobresalientes, pero hasta ahora, y probablemente también en el futuro, no parece tener algo para convertirse en “la próxima gran tendencia”. Dejando de lado las consideraciones políticas, los microkernels tendrán éxito, y así debería ser
Para que seL4 sea realmente útil, hace falta mucho encima de él. Por suerte, también ha habido bastante trabajo open source en esa parte, y está en una posición mucho mejor que hace unos años.
Para escenarios estáticos está LionsOS[0], y ya es bastante utilizable.
Para escenarios dinámicos está Provably Secure, General-Purpose Operating System[1], aunque todavía está en una etapa temprana.
Ambos se pueden encontrar en la página Projects[2] de trustworthy systems enlazada desde el sitio web de seL4.
[0] https://trustworthy.systems/projects/LionsOS/
[1] https://trustworthy.systems/projects/smos/
[2] https://trustworthy.systems/projects/
Me pregunto si el sistema operativo que corre sobre este kernel también tendría que estar verificado formalmente para que se mantengan las garantías de seguridad
Claro, el kernel por sí solo no es muy útil, así que el diseño de los drivers, servidores de sistema de archivos y otros servicios que se ejecutan sobre él sigue siendo importante.
También es importante que, aunque la mayoría de los demás sistemas, incluido Linux, tienen fallas a nivel fundamental, seL4 sí permite construir sistemas seguros y confiables
Por eso puedes ejecutar el kernel de Linux junto a un proceso de alta seguridad y aun así tener la garantía de que están aislados entre sí, salvo por el IPC permitido
Pero hay límites. Hay que desactivar DMA, y también usar solo drivers verificados formalmente.
También es importante que el kernel multinúcleo de seL4 todavía no está verificado
También vale la pena ver el Helios Microkernel de Drew DeVault. Dice que está basado en seL4.
https://ares-os.org/docs/helios/
En la Universidad de Karlsruhe, L4 era popular. Nunca lo examiné en detalle, pero parecía más un proyecto interesado en probar ideas teóricas que en crear algo útil en la práctica
Eso fue hace 20 años y, por lo que veo, no ha cambiado mucho hasta ahora. Buscando rápido, parece que ha habido intentos de construir sistemas operativos encima de él, pero se ven más como pruebas de concepto que como algo de uso real
“Los envíos de OKL4 superaron los 1.500 millones a principios de 2012, en su mayoría en chips de módems inalámbricos de Qualcomm. Otras implementaciones incluyen sistemas de infoentretenimiento automotriz”
“Los procesadores de la serie Apple A, a partir del A7, incluyen un coprocesador Secure Enclave que ejecuta un sistema operativo L4, sepOS, basado en el kernel L4-embedded desarrollado por NICTA en 2006. Como resultado, L4 está presente en todos los dispositivos Apple modernos, incluidas las Mac con Apple silicon”
Rittinghaus, exalumno de Bellosa, participa en Unikraft[0], que también ha aparecido varias veces en HN, y usa tecnología de unikernel
[0] https://unikraft.org/
“El Secure Enclave Processor ejecuta una versión personalizada por Apple del microkernel L4”
https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
Por lo que veo, el kernel de L4Re también forma parte de Elektrobit Safe Linux
Hice un sistema operativo basado en Pistachio como tesis de graduación. Siempre he pensado que, si hubiera estudiado en Karlsruhe, probablemente habría terminado investigando sistemas operativos
Yo también tenía ideas sobre diseño de sistemas operativos, y la capability que consideré usaba funciones de intermediación y delegación como seL4. Además de lo que dice ahí, tiene otras ventajas. Por ejemplo, se podría usar una capability proxy para aplicar filtros al audio o para implementar transparencia de red
Pensaba que las capacidades de tiempo real podían permitirse como una implementación opcional. Mi idea se parecía más a una especificación que a una implementación única
Otra característica que quería era que todos los programas, salvo por la entrada/salida, funcionaran de forma determinista. Sin E/S, no podrían conocer la fecha/hora ni cuánto tiempo ha estado ejecutándose el programa, y tampoco podrían inspeccionar las funciones del procesador. Si usaban una función no soportada por el hardware, el sistema operativo podría emularla
Para implementar esto, pensaba combinar soporte de hardware y de software. El documento tiene una nota sobre ataques contra capabilities implementadas en hardware, pero no tengo las referencias y no sé si ese ataque también aplicaría a la forma en que yo lo imaginaba
Desde la perspectiva de seguridad, parece mostrar fallas similares a KVM del kernel de Linux. Si el hipervisor está en ring 0, existe el riesgo de escapar de una VM hacia otra VM o incluso hacia el propio host
Me pregunto cómo se mitiga ese riesgo
El VMM no tiene más capabilities que la propia VM, así que, salvo en el sentido académico, escapar de la VM no tiene valor
Se puede ver en las páginas 8–10 del PDF original