Comprobar la seguridad de cualquier software no es un proceso sencillo, y cuando alguien dice que puede hacerlo a nivel matemático, hay que prestar atención. El microkernel seL4 cae dentro de esta categoría, y su robustez ha ayudado a proteger toda clase de sistemas integrados, incluyendo drones. Ahora, sus creadores en NICTA y General Dynamics C4 Systems anunciaron la apertura de su código.
El uso de drones es cada vez más amplio, tanto en el entorno civil como el militar. Desde el traslado de paquetes hasta un ataque furtivo contra grupos terroristas, los drones tienen un punto en común, y es que su software debe estar lo más cerca posible a la invulnerabilidad. Después de todo, nadie quiere ver a un ejército de drones desplomándose en tierra o pasando al otro bando sin razón aparente. Esto también se extiende a sistemas integrados y plataformas industriales. Imagina que la línea de producción en una fábrica se ve paralizada por culpa de un usuario malicioso. Lo ideal es que el software de control cuente con diferentes mecanismos que le permitan resistir un ataque, o en el peor de los casos, desactivar la infraestructura de forma segura.
En noviembre de 2012, la gente de la agencia australiana NICTA y la división C4 Systems de General Dynamics comenzó el desarrollo de seL4, un microkernel cuya seguridad puede ser comprobada matemáticamente. El plan original era proteger a los drones, y para ello se invirtieron unos 18 millones de dólares como parte del programa HACMS desarrollado por nuestros amigos de DARPA. Pero su potencial es gigantesco, y va mucho más allá de los drones. Hasta aquí, aplicaciones de defensa han sido la prioridad bajo su estructura de desarrollo. Ahora, el microkernel seL4 es open source, y esto abre todo un abanico de posibilidades, que van desde la protección de sistemas autónomos en plantas de producción, hasta coches inteligentes y dispositivos médicos, como por ejemplo marcapasos.
En esencia, lo que permite el microkernel seL4 a un sistema es resistir fallas en una sección específica, e impedir que esa falla se propague a otros elementos críticos. La demostración de seL4 sobre drones comerciales (el vídeo más arriba) es más que contundente. Bajo una estación maliciosa, el software convencional que controla al dron acepta comandos de interrupción en cualquier momento, provocando que el dron caiga como una piedra. En cambio, seL4 detecta el ataque, advierte visualmente al operador, y se aleja sin mayores inconvenientes. Tanto el código como todas sus pruebas ya están disponibles en GitHub.
