seL4, el kernel imposible de hackear

seL4, el kernel imposible de hackear

Hace unas semanas, la agencia militar DARPA, la mismísima creadora de Internet, le entregó un helicóptero militar Boeing Little Bird a los hackers.

"Ahí lo tenéis, hackeadlo".

Los hackers consiguieron controlar todos los sistemas menos el kernel, el núcleo del sistema operativo que controla las funciones críticas del software. Sin el control del kernel, la capacidad de hacer daño está muy limitada.

Dicho helicóptero estaba utilizando el nuevo kernel seL4 desarrollado por la agencia australiana de seguridad nacional, Data 61. Según afirman, es imposible de hackear. Demasiadas veces hemos escuchado esta frase pero al parecer, es matemáticamente cierto. En efecto, sus creadores han demostrado matemáticamente que seL4 no se puede hackear.

Los 5 hackers más buscados del FBI

Para que el kernel seL4 sea imposible de hackear, implementa funciones de seguridad extremas. Hace exactamente lo que tiene que hacer, y cualquier mínima alteración es detectada. No se puede alterar el código sin un permiso, y no se puede leer la memoria y los datos sin un permiso. Los datos están completamente aislados del propio kernel, y es capaz de ejecutar dos sistemas operativos al mismo tiempo, así que si uno es hackeado podría usarse el otro para detenerlo.

Según uno de sus creadores, Gernot Geiser: "espero que en 10 años cualquier dispositivo que requiera seguridad crítica utilice nuestro kernel o una variante de sus principios".

El kernel seL4 se utilizará en equipo médico, automóviles sin conductor, satélites, centrales nucleares, dispositivos del Internet de las cosas, y otro hardware en donde la seguridad sea un elemento crítico. Una primera versión llamada OKL4 ya se emplea en muchos smartphones.

Según afirm Data61 las medidas extraordinarias de seguridad no interfieren en su rendimiento.

seL4 es un proyecto de código abierto en el que todo el mundo puede participar. Puedes obtener más información en la web de seL4.

[Fuente: fossbytes]