Ironclad – kernel tipo Unix con capacidad de respuesta en tiempo real

• Ironclad es un kernel tipo Unix con capacidad de respuesta en tiempo real y basado en verificación formal para entornos de uso general y embebidos
  • Verificación formal: serie de procesos y comprobaciones por los que pasa el código del kernel para garantizar la ausencia de errores en tiempo de ejecución (AoRTE, Absence of Runtime Errors) y la corrección de sus componentes
• Está escrito en SPARK y Ada y está compuesto en un 100% por software libre
• Ofrece interfaz compatible con POSIX, multitarea preventiva, control de acceso obligatorio (MAC) y planificación de tiempo real duro
• Se distribuye bajo licencia GPLv3 y mantiene una arquitectura completamente de código abierto sin blobs de firmware
• Puede portarse a múltiples plataformas y sigue ampliando su ecosistema mediante distribuciones como Gloire

---

Resumen del kernel del sistema operativo Ironclad

• Ironclad es un kernel tipo UNIX con capacidad de respuesta en tiempo real que aplica verificación formal de manera parcial
  • Está diseñado tanto para sistemas de propósito general como embebidos
  • Verificación formal: serie de procesos y comprobaciones por los que pasa el código del kernel para garantizar la ausencia de errores en tiempo de ejecución (AoRTE, Absence of Runtime Errors) y la corrección de sus componentes
  • Para ello utiliza SPARK, un subconjunto de Ada
  • Todo el código está compuesto por software libre
• El kernel ofrece una interfaz compatible con POSIX y soporta multitarea preventiva, control de acceso obligatorio (MAC) y planificación de tiempo real duro
  • Proporciona una experiencia de desarrollo similar a la de un entorno UNIX tradicional
  • Tiene una arquitectura adecuada para sistemas que requieren control en tiempo real

Características como software libre

• Ironclad se distribuye como un proyecto completamente de código abierto bajo licencia GPLv3
  • El kernel no incluye blobs de firmware
  • Todos los componentes del stack se ofrecen en formato de código abierto

Verificación formal

• Aprovecha las funciones de verificación formal del lenguaje SPARK para garantizar la ausencia de errores y la corrección de componentes clave
• SPARK verifica matemáticamente la consistencia lógica del código al declarar en código Ada precondiciones (Pre), postcondiciones (Post) y dependencias (Depends), entre otros elementos
  • Entre los objetivos de verificación se incluyen módulos criptográficos, el sistema MAC y funciones relacionadas con la interfaz de usuario

Portabilidad y entorno de desarrollo

• Ironclad ha sido portado a varias plataformas y placas y está diseñado para facilitar nuevos ports
  • Depende únicamente de la toolchain de GNU, lo que permite una compilación cruzada sencilla
  • Gracias a su compatibilidad con POSIX, facilita el portado de software y el desarrollo

Distribuciones y ecosistema

• El proyecto Ironclad ofrece distribuciones para diversas arquitecturas y placas
  • Una de las principales distribuciones libres y de código abierto es Gloire
  • También ofrece imágenes de distribución descargables en formato tarball

Soporte del proyecto y sostenibilidad

• Ironclad se mantiene como un proyecto de uso, investigación y modificación libre
  • La operación del proyecto depende de donaciones y subvenciones
  • Toda contribución impacta directamente en la expansión y el desarrollo del proyecto

[GN⁺]

Comentarios de Hacker News

• Es un proyecto interesante. Me pregunto cuáles son los límites de la verificación formal del peor tiempo de ejecución (WCET)
  También existen otros kernels verificados como seL4 y atmosphere, y se puede montar una capa de compatibilidad POSIX como en genode
  También hay kernels completamente compatibles y maduros como QNX o VxWorks, así que la verificación completa quizá no aporte tanto valor adicional
  Pero casi no he visto casos que reúnan WCET + verificación formal + compatibilidad POSIX al mismo tiempo
  En su estado actual, no parece tener la madurez suficiente como para usarse de inmediato en los casos de tiempo real que menciona la documentación

  • Hoy en día, cualquier gobierno puede conseguir RCE sobre un OS. Por eso la verificación formal del aislamiento entre procesos es realmente importante
    seL4 es mucho más rápido que Linux, pero esto parece que sería más lento. POSIX tiene fallas de fondo, y MAC es demasiado complejo para usarlo en la práctica
  • Todavía está al nivel de stone, pero parece posible que en el futuro hasta consiga certificación oficial. Un OS verificado formalmente es un gran avance para mejorar la seguridad

• Ada pertenece a la familia de lenguajes de Wirth (la familia de Pascal). Hasta ahora, el único kernel tipo Unix en un lenguaje de la familia Wirth que conocía era TUNIS
  TUNIS fue implementado en Concurrent Euclid

  • También estaba SPIN, desarrollado en la Universidad de Washington en los 90. Era un sistema basado en microkernel escrito en Modula-3 que soportaba la interfaz de llamadas al sistema de Digital UNIX
    Además, en los 80, Sol de INRIA fue implementado en un dialecto de Pascal y ofrecía un entorno compatible con Unix; más adelante derivó en Chorus

• También existe una empresa relacionada con NDA llamada Ironclad. Deberían tener cuidado con el tema de la marca registrada
  Aun así, da gusto ver intentos así. Pero en la práctica, el eslabón más débil de la seguridad suele ser la capa de firmware
  Mi sueño es que hardware como las computadoras de Framework tenga firmware EFI verificado y firmware auditado por componente

  • Ironclad también es el nombre de una importante biblioteca criptográfica de Common Lisp (ironclad GitHub)
  • También vale la pena mirar MNT Research. Fabrican laptops reparables y publican tanto el hardware como el software como open source (mnt.re)
  • Para verificar firmware se necesita un kernel aparte. Ya estamos en un punto en que estas cosas deberían gestionarse a nivel de regulación
  • Las marcas no son problema si pertenecen a sectores industriales distintos aunque tengan el mismo nombre. Como Apple Computer y Apple Music de los Beatles, por ejemplo (xkcd 386)

• Crear un OS nuevo es algo realmente ambicioso. Hace poco también apareció Radiant Computer; me pregunto si habrá otros proyectos parecidos e interesantes

  • Asterinas (kernel compatible con Linux) y Redox OS prometen bastante
  • También está SerenityOS
  • Aunque es una alternativa vieja, Haiku OS sigue siendo interesante
  • Yo también tengo una idea para un OS. Estoy pensando en varios componentes, desde el hardware y el kernel hasta los programas de usuario
  • ReactOS también sigue avanzando. No es un OS completamente nuevo, pero aun así me parece algo novedoso

• Ojalá algún día los kernels completamente verificados formalmente se vuelvan algo común
  Verificar Linux completo será imposible, pero seL4 quizá podría encontrar una oportunidad en mercados como el de los smartphones

  • seL4 ya se usa en cosas como Secure Enclave OS (L4 microkernel family)
  • seL4 ya se usa en varios lugares, y viendo los casos de uso y la lista de miembros, parece que podría expandirse aún más

• Viendo su hoja de ruta de verificación, llamarlo “verificación formal” parece exagerado
  No hay pruebas de propiedades centrales del kernel, y no llega al nivel de kernels como seL4 o Tock

• CuBit es otro OS escrito en SPARK/Ada
  El código fuente puede verse en GitHub

• Desde la perspectiva de un usuario común, el kernel por sí solo no sirve de mucho
  Un ejemplo de OS que usa el kernel Ironclad es Gloire

• La documentación sobre MAC está bien organizada (Mandatory Access Control)

• Al ver la frase “consultar precio” de SPARK, da la impresión de que aquí ‘free’ significa otra cosa y no precisamente ‘software libre’

  • La mayoría de los enlaces de GitHub de arriba también cobran por el soporte comercial. Consultar precio es un procedimiento normal, así que no tiene nada de raro
  • Al final, los desarrolladores también tienen que ganarse la vida, y eso es completamente razonable