Introducción al microkernel seL4 [PDF]

• seL4 es un microkernel de sistema operativo que ejecuta el modo kernel con la mínima cantidad de código para controlar los recursos de hardware y reforzar la seguridad
• Pertenece a la familia de microkernels L4 y se desarrolla desde mediados de la década de 1990
• Puede funcionar como hipervisor, lo que permite ejecutar sistemas operativos invitados como Linux
• Es el primer kernel de sistema operativo del mundo con corrección funcional demostrada, con una prueba matemática completada a nivel de código
• Usa un modelo de seguridad basado en capabilities para un control de acceso detallado

Estructura de seL4 y funciones de hipervisor

• Kernel monolítico vs microkernel
  • Kernel monolítico (Linux, etc.): el código del kernel es enorme y tiene muchas vulnerabilidades de seguridad → aproximadamente 20 millones de líneas de código (20M SLOC)
  • Microkernel (seL4): usa la mínima cantidad de código de kernel → aproximadamente 10 mil líneas de código (10K SLOC)
  • Reducción del tamaño del kernel → mayor seguridad y menor superficie de ataque
• seL4 cumple el rol de hipervisor
  • Puede ejecutar un sistema operativo invitado completo como Linux dentro de una VM
  • Cada VM se ejecuta de forma independiente y no puede interferir con las demás → garantiza un aislamiento fuerte
  • Llamadas a procedimientos protegidos (PPC) → permiten comunicación segura entre VMs

Verificación y modelo de seguridad de seL4

• Verificación de corrección funcional
  • En seL4 se demostró matemáticamente, a nivel de código, que su funcionamiento es correcto
  • Garantiza que todo el comportamiento del kernel se ajusta a la especificación
• Validación de traducción (Translation Validation)
  • Demuestra que el código binario generado por el compilador coincide exactamente con el código C original
  • Se ejecuta mediante una cadena de herramientas automatizada
• Verificación de propiedades de seguridad
  • Confidencialidad: solo se puede acceder a los datos cuando está permitido explícitamente
  • Integridad: solo se pueden modificar los datos cuando está permitido explícitamente
  • Disponibilidad: solo se pueden usar los recursos cuando está permitido explícitamente

Modelo de seguridad basado en capabilities

• ¿Qué es una capability?
  • Un token de seguridad que otorga permisos de acceso a un objeto específico
  • Codifica en conjunto la referencia al objeto y los permisos de acceso
  • Permite un control de acceso detallado → aplica el principio de mínimo privilegio (Principle of Least Privilege, POLA)
• Ventajas de las capabilities
  • Control de acceso detallado → permite minimizar privilegios
  • Permiten delegación y revocación de permisos
  • Modelo de seguridad sólido → superior al modelo tradicional de control de acceso (ACL)
• Resolución del problema del deputy confuso
  • En los sistemas tradicionales basados en ACL, el estado de seguridad se determina según el ID de seguridad del sujeto
  • En seL4, la capability determina directamente los permisos de seguridad → permite un control claro de privilegios

Soporte para sistemas en tiempo real y sistemas de criticidad mixta

• Soporte para sistemas en tiempo real
  • seL4 admite planificación basada en prioridades
  • Ya se completó el análisis del peor tiempo de ejecución (WCET) de todas las operaciones del kernel → garantiza tiempo real estricto
• Soporte para sistemas de criticidad mixta (Mixed-Criticality System, MCS)
  • Asigna y aísla recursos de CPU con base en contextos de planificación
  • Controla que las tareas de mayor prioridad no monopolicen la CPU
  • Permite ejecutar simultáneamente tareas críticas y no críticas

Rendimiento y eficiencia

• El microkernel de mayor rendimiento
  • No reduce la seguridad incluso cuando el rendimiento es crítico
  • El costo de las llamadas al sistema y del IPC se minimiza → es más de 5 veces más rápido que sistemas competidores
• Rendimiento superior frente a sistemas competidores
  • Fiasco.OC: aproximadamente 2 veces más lento que seL4
  • Zircon: aproximadamente 9 veces más lento que seL4
  • CertiKOS: aproximadamente 5 veces más lento que seL4

Aplicación en el mundo real y ciberretroadaptación

• Casos de uso reales

  • Se aplicó con éxito en el ULB (helicóptero no tripulado) de Boeing
  • Se confirmó un refuerzo de la seguridad y un aumento en la estabilidad del sistema

• Refuerzo gradual de seguridad en sistemas existentes (Incremental Cyber Retrofit)

  • Ejecuta los sistemas existentes dentro de VMs mientras los modulariza de forma gradual
  • Refuerza la seguridad y minimiza la degradación del rendimiento

Conclusión

• seL4 es el microkernel más seguro del mundo, con corrección funcional, seguridad y rendimiento demostrados
• Gracias a su modelo de seguridad verificado y al soporte para sistemas de criticidad mixta, puede usarse de forma práctica en múltiples áreas
• Permite reforzar la seguridad y mejorar el rendimiento de sistemas existentes → un microkernel innovador que equilibra seguridad y rendimiento