En verano de 2015 la Agencia de Proyectos de Investigación Avanzada de Defensa (en adelante DARPA) inició una serie de pruebas en las que un equipo de hackers debía intentar tomar el control de un helicóptero militar no tripulado conocido como Little Bird. Después de seis semanas, el Red Team fue incapaz de hackear el dron incluso contando más facilidades de las que podría soñar cualquier atacante externo...

El proyecto High-Assurance Cyber Military Systems (HACMS) de DARPA pone en marcha un nuevo viejo tipo de mecanismo de seguridad - un sistema de software que no puede ser comprometido. Las partes fundamentales del sistema informático del Little Bird eran impenetrables con la tecnología existente, y su código tan confiable como una prueba matemática.

La verificación formal

La tecnología que "repele" a los hackers es un estilo de programación de software conocido como verificación formal. A diferencia de la mayoría del código que está escrito de manera informal y cuya evaluación se basa principalmente en ver si funciona o no, el software verificado formalmente se lee como una prueba matemática: cada declaración es consecuencia lógica de la anterior. Un programa completo se puede probar con la misma seguridad que los matemáticos demuestran teoremas.

La aspiración de crear un software verificado formalmente ha existido casi desde la creación de la informática. Durante mucho tiempo parecía inalcanzable pero los avances en la última década en los llamados "métodos formales" están empezando a posibilitar su aplicación práctica. Hoy en día la verificación del software formal está siendo estudiada mediante colaboraciones académicas bien financiados, empresas militares y de tecnología de Estados Unidos, tales como Microsoft y Amazon.

Una especificación formal es una manera de definir qué, exactamente, hace un programa de ordenador. Y una verificación formal es una manera de probar más allá de toda duda que el código de un programa logra perfectamente esa especificación.

Por poner un ejemplo, piensa en un programa para ordenar una lista de números. Un programador tratando de formalizar una especificación para un programa tipo podría llegar a algo como esto:

    Por cada elemento j en una lista, asegúrese de que el elemento j ≤ j + 1

Sin embargo, esta especificación formal - garantizar que todos los elementos de una lista es menor que o igual al elemento que le sigue - contiene un error: El programador asume que la salida será una permutación de la entrada. Es decir, dada la lista [7, 3, 5], se espera que el programa volverá [3, 5, 7] y así satisfacer la definición. Sin embargo, la lista [1, 2] también satisface la definición ya que "es una lista ordenada, pero no la lista ordenada probable que esperábamos", comenta Brian Parno de Investigación de Microsoft.

En otras palabras, es difícil de traducir una idea que tiene para lo que debe hacer un programa en una especificación formal que excluye toda posible (pero incorrecta) interpretación de lo que desea que el programa debe hacer.

Y el ejemplo anterior es para algo tan simple como un programa de clasificación. Ahora imagina tomando algo mucho más abstracto que la clasificación, tales como la protección de una contraseña. "¿Qué significa eso matemáticamente? Definiéndola puede implicar escribir una descripción matemática de lo que significa guardar un secreto, o lo que significa para un algoritmo de cifrado ser seguro" comenta Parno. "Todas estas son preguntas que nosotros, y muchos otros, han estudiado y realizado progresos, pero puede ser muy sutil hacerlo bien".

Retomando la técnica

Un programa que incluye la información de verificación formal puede ser cinco veces más largo que un programa tradicional que fue escrito para lograr el mismo fin. Además del esfuerzo que suponer readaptar en cada paso el software a la lógica de verificación formal, todo ello han hecho que esta técnica se haya ido estancando a lo largo de los años.

Sin embargo, ahora se ha visto relanzada por la preocupación por la seguridad informática en el mundo cada vez más interconectado y la Internet de las Cosas (IoT) y los avances en la tecnología que subyace en métodos formales: las mejoras en los programas de prueba-asistente como Coq e Isabelle que soportan los métodos formales; el desarrollo de nuevos sistemas lógicos (llamado teorías de tipo dependiente) que proporcionan un framework; y las mejoras en lo que se llama "semántica operacional" - en esencia, un lenguaje que tiene las palabras adecuadas para expresar lo que se supone que un programa tiene que hacer.

El proyecto HACMS

El proyecto HACMS ilustra cómo es posible generar grandes garantías de seguridad mediante la especificación de una pequeña parte de un sistema informático. El primer objetivo del proyecto era crear un quadcopter recreativo no hackeable. El software off-the-shelf que dirigía el quadcopter era monolítico, lo que significa que si un atacante rompía una sola pieza de la misma tenía acceso a todo. Por lo tanto y durante dos años, el equipo dividió el código del ordenador de control de la misión del quadcopter en particiones.

El equipo también volvió a escribir la arquitectura de software utilizando lo que Fisher, el director del proyecto fundación HACMS, llama "bloques de construcción de alta seguridad" - herramientas que permiten a los programadores probar la fidelidad de su código. Uno de esos bloques de construcción verificados viene con una prueba que garantiza que alguien con acceso dentro de una partición no será capaz de escalar sus privilegios y conseguir acceso a otras particiones.

Más tarde, los programadores de HACMS instalaron este software particionado en Little Bird. En la prueba contra los hackers del Red Team, les proporcionaron acceso a una partición que controla ciertos aspectos del helicóptero teledirigido, como la cámara, pero no a las funciones esenciales. Y los hackers fueron matemáticamente bloqueados.

Un año después de las pruebas con Little Bird, DARPA ha estado aplicando las herramientas y técnicas del proyecto HACMS a otras áreas de la tecnología militar, como los satélites y los camiones auto-conducidos.

Más proyectos en liza

Los ingenieros de software de Microsoft Research tienen en curso dos ambiciosos proyectos de verificación formal. El primero, llamado Everest, es crear una versión verificada de HTTPS, y la segunda es la creación de especificaciones verificadas para los sistemas ciber-físicos complejos, tales como aviones no tripulados. Así que esto es sólo el principio... ¿del fin del hacking? No lo creo...

Fuente: Hacker-Proof Code Confirmed