Los investigadores, más cerca de crear un código anti-hackers

El auge de la tecnología e internet ha supuesto a su vez un nuvo caldo de cultivo para el hacking y las brechas de seguridad, cada vez más sofisticadas. Hoy en día es un juego de niños colarse en sistemas informáticos avanzados, al menos si eres un hacker de primera. Solo necesitas conocer un fallo de seguridad en el código de un programa y ¡sorpresa! has sido hackeado.

Es por eso que la mayor preocupación de los investigadores en ciberseguridad se ciñe a día de hoy a los procesos utilizados para definir el código de las aplicaciones de software. Los programas, en general, están escritos de una forma informal y requieren testeo que garantice que se comportarán como se espera y ofrecen la salida deseda.

Experimento del HACMS con un Little Bird

El año pasado, una versión no desvelada de un helicóptero militar llamado Little Bird fué puesta a prueba por un grupo de hackers. Su reto era tomar el control absoluto del helicóptero. El equipo fué capaz de tomar el control de algunos de los sistemas del aparato y pronto quedó claro que no les sería imposible acceder al resto del sistema. Pero el objetivo real no era poner a prueba el software de control de helicóptero.

El alcance de la operación entraba dentro de lo que denominan HACMS o High-Assurance Cyber military Systems, un proyecto fundado por el DARPA. La organización desarrolló un sistema de seguridad completamente nuevo para el Little Bird.

Los resultados sorprendieron a todos, ya que en un nuevo intento de hacking sobre el aparato llevado a cabo de forma intensiva durante 6 meses, «no fueron capaces de penetrar ni alterar las operaciones de ninguna forma«, como los describen los propios investigadores.

Este resultado hizo que la gente del DARPA se levantara y exclamara ¡oh Dios mio! podemos utilizar esta tecnología en todos aquellos sistemas informáticos de nuestro interés.

Ahora mismo Kathleen Fisher es la directora del proyecto HACMS y ha puesto a un profesor de ciencias de la información a trabajar también en la Universidad de Tufts.

La verificación formal proporciona código anti-hackers

Este nuevo sistema anti-hackers está basado en algo denominado verificación formal, un concepto con cierta historia pero que está ganando cada vez más apoyo entre la comunidad de desarrolladores. La verificación formal es una técnica de testeo de código de software que actúa como una prueba matemática.

Cada sentencia en una prueba es derivada a nivel lógico de la anterior sentencia, de la misma forma que los matemáticos siempre han demostrado sus teoremas:

Estás básicamente escribiendo una fórmula matemática que describe el estado del programa y utilizando algún tipo de mecanismo de verificación que va a garantizar la exactitud de dicha sentencia.

El proceso incluye la comprobación cruzada del hecho de que el código del programa se adhiere a una especificación formal. Así, básicamente es una especificación formal la que define lo que el programa puede hacer.

Para ver como funciona, imagina escribir un programa de ordenador para un robot que te lleva a la pastelería. Al nivel operacional, definirás los movimientos que dispone el vehículo durante su viaje -girar a derecha o izquierda, acelerar o frenar, encender o apagar motores-. Tu software, sea como fuere, sería una compilación básica de estas operaciones individuales colocadas en un orden apropiado para que, al final, llegues a la pastelería y no acabes en el aeropuerto.

El software instalado en el ya citado Little Bird está compartimentado o divido en particiones. El sistema está diseñado de forma que si un hacker consigue controlar una partición simple, obtendrá un pié en las demás. Este fué el primer caso cuando el Red Team accedió a la cámara del aparato, pero falló al hackear el resto de sistemas.

Aplicaciones y proyecto Everest de Microsoft

DARPA tiene planes para utilizar esta verificación formal en tecnologías militares diversas, como en camiones automátas y satélites de comunicaciones. Sin embargo el uso de esta técnica no es patrimonio exclusivo de este sector y empresas como Microsoft y Amazon están invirtiendo fuerte para crear estos productos.

El equipo de la compañía de Redmond tiene su división de investigación «currando» duro en Everest, un proyecto destinado a conseguir una verificación formal para conexiones seguras mediante la creación de una versión supervisada y verficada de HTTPS.

Otro proyecto en marcha se centra en sistemas físicos complejos como pueden ser los drones.

La verificación formal puede ser usada para hacer software con código anti-hackers en tecnologías modernas como coches automáticos conectados a internet. Los ciberdelincuentes han demostrado cierta facilidad para controlar estos vehículos y hacer cosas realmente graves con ellos.

De otro lado está el internet de las cosas o IoT, un fenómeno en auge que traerá en pocos años hogares inteligentes y un montón de dispositivos interconectados, mucho más de lo que se podía imaginar hace tiempo. Este tipo de iniciativas ayudarán a mejorar la seguridad del usuario medio.

Consulta el artículo completo en Quanta Magazine.