seL4

seL4 utiliza un modelo basado en capacidades para controlar todo el acceso a la memoria y los recursos del kernel. Esto permite razonar y gestionar los recursos y el flujo de información de forma programática (en contraposición a las políticas de seguridad y arquitectura que no se adaptan a todos los casos). En este modelo, una capacidad es un token infalsificable que nombra un objeto del kernel y codifica las operaciones que se pueden realizar sobre él. Las capacidades se almacenan en tablas gestionadas por el kernel llamadas nodos de capacidad (CNodes), que forman un espacio de nombres jerárquico análogo a la estructura de directorios de un sistema de archivos. Un CNode contiene ranuras de capacidad y es en sí mismo un objeto del kernel al que solo se accede mediante una capacidad, lo que permite delegar, subdividir o revocar explícitamente la autoridad sobre los recursos. ^{[ 15 ]}

En seL4, la memoria física se representa inicialmente como capacidades de memoria sin tipo , que otorgan autoridad sobre regiones sin procesar de la RAM, pero no corresponden a objetos utilizables. La memoria sin tipo se convierte en objetos del kernel con tipo mediante una operación de reescritura . El kernel registra las relaciones entre la memoria sin tipo y los objetos derivados en un árbol de derivación de capacidades (CDT), lo que permite al sistema garantizar la reutilización segura de la memoria: todas las capacidades derivadas de una región sin tipo deben eliminarse antes de que dicha región pueda reasignarse. Este mecanismo reemplaza los asignadores implícitos del kernel con un ciclo de vida de memoria explícito y auditable bajo el control de la aplicación. ^{[ 15 ]}

La gestión de la memoria virtual también se rige por capacidades. Una capacidad asignada a un marco de memoria confiere la autoridad para asignar dicho marco a un espacio de direcciones, sujeto a los derechos de acceso codificados en la capacidad. Los espacios de direcciones se construyen a partir de objetos de tabla de páginas que, a su vez, se crean a partir de memoria sin tipar y se referencian mediante capacidades. Además de la memoria de propósito general, seL4 distingue la memoria sin tipar del dispositivo , la cual está sujeta a restricciones adicionales para evitar la reescritura o reutilización inseguras. ^{[ 16 ]}

seL4 IPC no está diseñado como un mecanismo de paso de mensajes de propósito general, sino como una forma de implementar la invocación entre dominios de funciones o servicios a través de límites de protección. Los diseñadores de seL4 lo conciben como una llamada a procedimiento protegido (PPC), que transporta solo pequeños argumentos y valores de retorno (similar a una llamada a función entre dominios de protección) en lugar de un transporte de almacenamiento en búfer para datos arbitrarios. Los diseñadores de seL4 desaconsejan explícitamente el uso de IPC para el envío de grandes volúmenes de datos o para la sincronización, y recomiendan utilizar IPC principalmente para la invocación de servicios mediante solicitud-respuesta y la transferencia de capacidades . ^{[ 17 ]}

La comunicación entre procesos en seL4 se basa en objetos del núcleo controlados por capacidades y está diseñada para minimizar el estado del núcleo al tiempo que explicita la autoridad. El objeto IPC principal es el punto final , que representa tanto el derecho a comunicarse como el punto de encuentro para la comunicación: un hilo puede enviar o recibir desde un punto final solo si posee la capacidad adecuada. ^{[ 15 ]}

La comunicación entre procesos (IPC) a través de puntos finales es síncrona y bloqueante (con otras convenciones superpuestas). Una operación de envío espera hasta que un receptor esté listo, y una operación de recepción espera hasta que llegue un remitente. A diferencia de muchos sistemas de paso de mensajes tradicionales, los puntos finales de seL4 no proporcionan colas de mensajes ni buzones gestionados por el kernel. El kernel solo mantiene colas de hilos en espera, y los datos de los mensajes se transfieren directamente entre los hilos que se comunican mediante una carga útil pequeña y de tamaño fijo. Esto evita la asignación implícita de memoria del kernel durante la comunicación y es coherente con el modelo de gestión de recursos explícito de seL4. ^{[ 15 ] [ 7 ]} Los mensajes pueden incluir tanto datos como capacidades seleccionadas, lo que permite que la IPC sirva no solo como mecanismo de comunicación, sino también como medio para delegar autoridad explícitamente. Transferir una capacidad durante la IPC transfiere directamente el derecho a acceder a un objeto del kernel, integrando estrechamente la comunicación y el control de acceso. ^{[ 15 ]}

Al igual que otros sistemas formalmente verificados, las garantías de seL4 son relativas a su especificación y supuestos subyacentes. Si bien esto significa que la verificación no aborda todas las fallas posibles, mejora sustancialmente la seguridad general del sistema al eliminar clases de defectos de implementación y hacer explícitos los supuestos restantes (y, por lo tanto, comprobables). ^{[ 27 ] [ 25 ]}

• seL4 es solo un microkernel sobre el cual se construyen sistemas operativos completos . Sin embargo, un estudio de caso de CVE críticos del kernel de Linux muestra que el aislamiento de sus subsistemas no verificados habría disminuido la gravedad de cada CVE muestreado que no estaba vinculado al entorno de prearranque. ^{[ 28 ]}
• Las pruebas no cubren todos los aspectos de un ordenador en funcionamiento que ejecuta seL4 y no se extienden a todas las plataformas y configuraciones compatibles. ^{[ 7 ]} Las pruebas iniciales (por ejemplo) solo se referían al código base C, pero trabajos posteriores extendieron las pruebas a los binarios compilados (la verificación binaria no es compatible con todas las plataformas).
• Aunque seL4 puede vincular sus especificaciones con las especificaciones de hardware , puede haber errores en las especificaciones o en el hardware físico. Sin embargo, no se han reportado públicamente errores en las partes verificadas del kernel en más de 15 años. ^{[ 29 ]} Si bien el hardware defectuoso afecta a todos los sistemas operativos y seL4 cuenta con medidas de mitigación para algunos errores de hardware conocidos, el proyecto actualmente no tiene los recursos para implementar tantas medidas de mitigación como los sistemas operativos comerciales más maduros. ^{[ 30 ]} Sin embargo, esta no es una limitación fundamental de seL4.

El microkit seL4 es un marco de sistema operativo construido sobre seL4 que proporciona un pequeño conjunto de abstracciones destinadas a reducir la barrera para construir sistemas estructurados estáticamente, al tiempo que se preservan los objetivos de rendimiento y eficiencia de memoria. ^{[ 43 ] [ 44 ]}

El marco de controlador de dispositivo seL4 (sDDF) es una arquitectura de controlador para sistemas basados ​​en seL4 que se discutió en varias cumbres; los materiales de las cumbres describen un diseño que enfatiza la separación de responsabilidades y la comunicación asíncrona/basada en eventos con rutas de datos de memoria compartida. ^{[ 45 ]}

LionsOS está siendo desarrollado actualmente por Trustworthy Systems en la Universidad de Nueva Gales del Sur (UNSW) ^{[ 46 ]} y tiene como objetivo proporcionar servicios de sistema operativo orientados a aplicaciones, como redes, sistemas de archivos y otras operaciones de entrada/salida. Si bien está dirigido principalmente a arquitecturas estáticas con recursos asignados al arrancar (por ejemplo, sistemas embebidos), se planea brindar soporte para sistemas operativos más dinámicos. ^{[ 47 ] [ 48 ]}

Los objetivos principales de LionsOS son competir con Linux mediante el uso del microkernel seL4, que mantiene el rendimiento del sistema y, al mismo tiempo, proporciona una implementación correcta del hardware seL4 mediante herramientas de verificación de Satisfacibilidad Módulo Teorías (SMT). ^{[ 49 ]} Los principales componentes del sistema propuesto son el microkit seL4 y el marco de controladores de dispositivos seL4 (sDDF). Actualmente, la versión 0.3.0 se lanzó el 25 de marzo de 2025. ^{[ 50 ] [ 51 ]}