seL4, un kernel que dice ser a prueba de hackers

Imaginemos el siguiente escenario, un helicóptero autónomo equipado con armamento sobrevuela una zona en modo exploración bajo la supervisión lejana de sus responsables, pero su sistema no está hecho a prueba de hackers y acaba sufriendo un ataque que deriva en una pérdida de control muy peligrosa que podría costar la vida a muchas personas.

El mismo ejemplo sería aplicable a los coches inteligentes, que han demostrado ser un blanco fácil para este tipo de ataques, y que incluso llevó a pedir la devolución de 1,4 millones de coches Jeep Cherokee.

Estos hechos han llevado a la búsuqeda de un kernel (núcleo central de un sistema operativo) que sea imposible de hackear, algo que en DARPA, la agencia estadounidense de investigación de proyectos avanzados de defensa, dicen haber conseguido con el seL4.

Las claves de este kernel radican en que ha sido construido para que sólo pueda hacer una serie de cosas limitadas y concretadas, de manera que los atacantes no pueden llevar a cabo en él funciones para las que no ha sido concebido, pero tampoco pueden modificar su código ni acceder a la memoria o realizar transferencias si permiso.

En el desarrollo también se centraron en conseguir que el kernel fuera capaz de comprobarse matemáticamente, y además consigue mantener aisladas diferentes zonas o partes en caso de ataque, de manera que en el caso de que se consiguiera acceso a una parte de un dispositivo este kernel podría aislar otras para evitar que el problema se maximice.

Lo dicho podría ser muy útil en los coches inteligentes, por ejemplo, ya que aunque los hackers lograran acceder al sistema de infoentretenimiento se aislarían otras funciones vitales como la dirección o el frenado, por ejemplo.

Sin duda un gran avance que de hecho cuenta con una versión previa conocida como OKL4 instalada en algunos dispositivos móviles, pero que ciertamente nos deja muchas preguntas y nos hacer recordar aquello de que ningún sistema es absolutamente seguro.

Más información: Newscientist.