Existe código ininterrumpido
Los informáticos pueden demostrar que no hay errores en el programa con la misma certeza que los matemáticos pueden probar los teoremas. Estos avances se utilizan para mejorar la seguridad en una variedad de áreas, desde drones hasta Internet.
En la primavera de 2015, un equipo de hackers intentó ingresar a un helicóptero militar no tripulado llamado Little Bird ("Bird"). El helicóptero, similar a la versión tripulada del avión favorito de las fuerzas especiales de EE. UU., Estaba ubicado en Boeing, Arizona. Los piratas informáticos tenían una ventaja: al comienzo de su trabajo, tenían acceso a uno de los subsistemas de la computadora de control. Solo podían piratear la computadora principal de vuelo a bordo y obtener el control del UAV.Al comienzo del proyecto, el equipo de piratas informáticos del Equipo Rojo podría descifrar un sistema de helicóptero casi tan fácilmente como el WiFi de su hogar. En los meses siguientes, los ingenieros de DARPA implementaron un nuevo mecanismo de seguridad, un sistema de software no sujeto a expropiación forzada. Los parámetros clave del sistema Little Bird no se pueden descifrar utilizando las tecnologías existentes, y se puede confiar en su código como evidencia matemática. Y aunque el equipo tuvo seis semanas de acceso al UAV, y el acceso al sistema informático excedió las capacidades de acceso de un verdadero equipo de hackers, no pudieron romper la defensa del Bird."No pudieron descifrar o interrumpir la operación", dice Kathleen Fisher, profesor de ciencias de la computación en la Universidad de Tufts y gerente de proyectos de sistemas cibermilitares de alta seguridad (HACMS). "Como resultado, los representantes de DARPA se levantaron y dijeron, oh Dios mío, en realidad puedes usar esta tecnología en sistemas importantes".La tecnología que se opone a los hackers es un estilo de programación llamado confirmación formal . A diferencia del código ordinario escrito informalmente y generalmente evaluado solo por su rendimiento, el software formalmente verificado parece una prueba matemática: cada enunciado se sigue lógicamente del anterior. Todo el programa se puede verificar con la misma certeza que un teorema matemático."Usted escribe una fórmula matemática que describe el comportamiento de un programa y utiliza una herramienta de prueba de concepto que prueba la validez de esta declaración", dice Brian Parno , investigador de confirmación formal y seguridad en Microsoft Research.El deseo de crear programas formalmente confirmados existió casi tanto como el campo de la informática en sí. Y durante mucho tiempo esto permaneció imposible, pero los logros de los últimos diez años en el campo de los "métodos formales" han acercado este enfoque a la práctica convencional. Hoy, la confirmación formal del software se está estudiando en grupos académicos financiados, en proyectos militares de EE. UU. Y en empresas de tecnología como Microsoft y Amazon.El interés está creciendo junto con un aumento en el número de tareas vitales que se realizan en línea. Cuando las computadoras existían aisladas en hogares y oficinas, los errores de programación eran solo una molestia. Ahora, abren agujeros de seguridad en las máquinas en la red, permitiendo que cualquier persona con conocimientos penetre en los sistemas informáticos."En el siglo XX, cuando un programa tenía un error, era malo, podía caer, bueno, que Dios la bendiga", dijo Andrew Appel , profesor de informática en la Universidad de Princeton y líder en validación de programas. Pero en el siglo XXI, un error puede abrir un camino para que los piratas informáticos obtengan el control del programa y roben sus datos. De un error tolerable, se ha convertido en una vulnerabilidad, que es mucho peor ", dice.
Kathleen FisherSueños de programas perfectos
En octubre de 1973, a Edsger Dijkstra se le ocurrió la idea de crear código sin errores. Por la noche, mientras estaba en un hotel en una conferencia, de repente pensó en cómo hacer que la programación sea más matemática. Explicando la idea más tarde, dijo: "Con una mente emocionada, me levanté de la cama a las 2:30 de la mañana y escribí durante más de una hora". Este material fue el comienzo de su fructífero libro de 1976, La disciplina de la programación, que, junto con el trabajo de Charles Hoare (como Dijkstra, quien recibió el Premio Turing ), definió puntos de vista sobre el uso de la prueba de corrección en los programas de escritura.Pero la informática no siguió esta idea, principalmente porque durante muchos años pareció poco práctico, o incluso imposible, determinar la función de un programa utilizando las reglas de la lógica formal.Una definición formal es una forma de determinar qué hace un programa específicamente. La confirmación formal es una forma de demostrar sin lugar a dudas que el código del programa se ajusta perfectamente a esta definición. Imagine que está escribiendo un programa para un robot que lo lleva a una tienda de comestibles. A nivel de operaciones, usted determina los movimientos que tiene el robot robótico para alcanzar el objetivo: puede girar, reducir la velocidad o acelerar, encender o apagar al principio y al final del camino. Su programa consistirá en estas operaciones básicas, organizadas en el orden correcto para que al final usted venga a la tienda y no al aeropuerto.La forma tradicional de evaluar la salud de un programa es a través de pruebas. Los programadores le dan al programa muchos datos de entrada (pruebas unitarias) para asegurarse de que se comporta como debería. Si su programa define un algoritmo para el movimiento de un robot robótico, puede probar sus viajes entre muchos puntos diferentes. Dichas pruebas aseguran el correcto funcionamiento de los programas en la mayoría de los casos, lo cual es suficiente para la mayoría de las aplicaciones. Pero las pruebas unitarias no garantizan que el software siempre funcione correctamente; no puede verificar el programa con todos los datos de entrada posibles. Incluso si el algoritmo funciona para todos los destinos, siempre existe la posibilidad de que se comporte de manera diferente en condiciones excepcionales, o, como dicen, en "condiciones límite", y abra un agujero de seguridad. En programas reales, tales errores pueden ser simples, por ejemplo, desbordamientos de búfer,en el que el programa copia un poco más de datos de los necesarios y sobrescribe parte de la memoria de la computadora. Este error aparentemente inofensivo es difícil de eliminar, y proporciona un agujero para un ataque de piratas informáticos: una bisagra de puerta débil que abre el camino al castillo.“Un agujero en alguna parte del software, y esto es una vulnerabilidad. Es muy difícil verificar todas las rutas para todas las entradas posibles ", dice Parno.Estas especificaciones son más complicadas que un viaje a la tienda. Los programadores, por ejemplo, pueden necesitar un programa de notarización y fijación de la fecha de recepción de los documentos en el orden en que fueron recibidos. En este caso, la especificación debería indicar que el contador siempre está aumentando, y que el programa nunca debe permitir que la clave utilizada para firmar se filtre.En lenguaje humano, esto es fácil de describir. Convertir una especificación en un lenguaje formal que una computadora entienda es mucho más difícil, lo que explica el problema principal de escribir programas."Construir una especificación formal que sea comprensible para una computadora es difícil en esencia", dice Parno. "Es fácil en el nivel superior decir" no permita que se filtre la contraseña ", pero debe pensar en cómo convertir esto en una definición matemática".Otro ejemplo es un programa que ordena una lista de números. Un programador al tratar de formalizar una especificación para ella puede llegar a esto:Para cada elemento j de la lista, asegúrese de que j ≤ j + 1
Pero incluso en esta especificación formal, para asegurarse de que cada elemento de la lista sea menor o igual que el siguiente, hay un error. El programador supone que la salida contendrá la entrada modificada. Si la lista es [7, 3, 5], espera que el programa regrese [3, 5, 7]. Pero la salida del programa [1, 2] satisfará las especificaciones, porque "también es una lista ordenada, pero no la lista que probablemente esperaba", dice Parno.En otras palabras, es difícil convertir la idea de lo que debe hacer un programa en una especificación formal que excluya cualquier interpretación incorrecta de lo que desea del programa. Y el ejemplo dado describe el programa de clasificación más simple. Ahora imagine una descripción de algo mucho más abstracto, como la protección con contraseña. “¿Qué significa esto matemáticamente? Para tal definición, puede ser necesario escribir una descripción matemática de lo que significa "mantener un secreto", o lo que significa que el algoritmo de cifrado sea seguro ", dice Parno. "Consideramos todos estos problemas y avanzamos en su estudio, pero pueden ser extremadamente difíciles de implementar".Bloque de seguridad
De hecho, es necesario escribir especificaciones y comentarios adicionales necesarios para que el software saque conclusiones sobre el código. Un programa, incluida su confirmación formal, puede ser cinco veces más grande que un programa regular escrito con el mismo propósito.Esta carga se puede aliviar un poco con las herramientas adecuadas: lenguajes de programación y programas auxiliares que ayudan a los programadores a crear programas a prueba de balas. Pero en la década de 1970 no existían. "Muchos aspectos de la ciencia y la tecnología no crecieron lo suficiente en ese entonces, por lo que en la década de 1980 muchas áreas de la informática habían perdido interés en esto", dice Appel, investigador principal de DeepSpec, un grupo de desarrolladores de sistemas informáticos formalmente validados.A pesar de la mejora de las herramientas, surgió otra barrera en la forma de confirmar los programas: no había certeza de que fuera necesaria. Aunque los entusiastas del método dijeron que los pequeños errores pueden conducir a grandes problemas, el resto llamó la atención sobre el hecho de que básicamente los programas de computadora funcionan bastante bien. A veces se bloquean, sí, pero perder un poco de datos no guardados o, a veces, reiniciar el sistema parece un pequeño precio a pagar por no tener que traducir minuciosamente cada parte del programa al lenguaje de la lógica formal. Con el tiempo, incluso aquellos que estaban en los orígenes de la confirmación del programa comenzaron a dudar de sus beneficios. En la década de 1990, incluso Hoar reconoció que las especificaciones podrían ser una solución que lleva mucho tiempo a un problema inexistente. En 1995, escribió:( ) , … , , .
Luego llegó Internet, que hizo lo mismo con los errores en el código que los viajes aéreos hicieron para las infecciones: cuando todas las computadoras están conectadas entre sí, los errores incómodos pero tolerantes pueden conducir a problemas de seguridad cada vez mayores."No lo entendimos completamente", dice Appel. "Hay programas abiertos a todos los piratas informáticos de Internet, y si hay un error en dicho programa, puede convertirse en una vulnerabilidad".Para cuando los investigadores comenzaron a comprender la gravedad de las amenazas a la seguridad planteadas por Internet, la confirmación del programa estaba a punto de regresar. Para empezar, los investigadores han progresado en las partes fundamentales de los métodos formales. Esta es una mejora en programas auxiliares como Coq e Isabelle; desarrollo de sistemas lógicos ( teoría de tipos dependientes) proporcionar una plataforma de desarrollo que ayude a las computadoras a evaluar el código; La “semántica operacional” es un lenguaje que tiene las palabras correctas para expresar lo que se requiere del programa."Comenzando con la especificación en lenguaje humano, te has encontrado con ambigüedades", dice Janette Wing , vicepresidenta de Microsoft Research. - Cualquier lenguaje natural contiene ambigüedades. En la especificación formal, usted escribe una descripción exacta basada en las matemáticas para explicar lo que quiere del programa ".
Janette Wing de Microsoft ResearchAdemás, los investigadores del método formal han redefinido sus objetivos. En las décadas de 1970 y 1980, querían crear sistemas informáticos totalmente probados, desde circuitos electrónicos hasta programas. Hoy, la mayoría de los investigadores trabajan en partes pequeñas, pero más críticas o vulnerables de los sistemas, por ejemplo, sistemas operativos o protocolos criptográficos."No estamos diciendo que demostraremos que todo el sistema es 100% correcto, hasta los circuitos electrónicos", dice Wing. - Tales declaraciones son ridículas. Somos precisos en lo que podemos o no podemos hacer ”.El proyecto HACMS muestra cómo puede lograr grandes garantías de seguridad al describir una pequeña parte de un sistema informático. El primer objetivo del proyecto era crear un quadrocopter irrompible para el entretenimiento. El software que vino con el cuádruple era monolítico, es decir, al obtener acceso a una parte de él, el pirata informático obtuvo acceso a todos los demás. Durante dos años, el equipo de HACMS ha estado dividiendo el código en la computadora de control en partes.El equipo reescribió la arquitectura del software utilizando lo que Fisher llama "bloques de construcción de alta confianza", herramientas que permiten a un programador demostrar la pureza del código. Uno de ellos proporciona evidencia de que, habiendo obtenido acceso a una de las unidades, no es posible escalar los privilegios para llegar a los demás.Más tarde, los programadores instalaron dicho software en el "Bird". En la prueba con el Equipo Rojo, se le dio acceso a una de las partes del sistema que controlaba alguna parte del helicóptero, por ejemplo, la cámara, pero no las funciones principales. El fracaso de los hackers estaba matemáticamente garantizado. "Probaron de forma verificable por máquina que los piratas informáticos no podrán ir más allá de la partición del sistema, por lo que esto no es sorprendente", dice Fisher. "Esto es consistente con el teorema, pero siempre es útil realizar una prueba".En el año siguiente a la auditoría, DARPA aplicó las herramientas y tecnologías del proyecto a otras áreas de tecnología militar, por ejemplo, satélites y camiones automáticos. Las nuevas iniciativas coinciden con la forma en que la confirmación formal se ha extendido en los últimos diez años: cada proyecto exitoso alienta al siguiente. "Las excusas sobre la complejidad de este principio ya no funcionan", dice Fisher.Comprobar internet
La seguridad y la fiabilidad son dos de los objetivos principales que inspiran los métodos formales. Cada día, la necesidad de mejoras es cada vez más evidente. En 2014, un pequeño error de software, que una descripción formal detectaría, abrió el camino para un error de Heartbleed que amenazaba con romper Internet. Un año después, un par de piratas informáticos "legales" confirmaron los peores temores sobre los automóviles conectados a Internet y obtuvieron el control remoto del Jeep Cherokee .Con tasas más altas, los investigadores de métodos formales establecen objetivos cada vez más ambiciosos. El equipo de DeepSpec, dirigido por Appel (que también trabaja en HACMS), está tratando de construir un sistema tan complejo y completamente probado como un servidor web. Si tiene éxito, el proyecto, que recibió una subvención de la Fundación de Ciencias del Estado de $ 10 millones, reunirá muchos proyectos exitosos más pequeños de la última década. Los investigadores han creado varios componentes seguros probados, como el núcleo del sistema operativo. "Lo que no se ha hecho hasta ahora es la integración de estos componentes en interfaces específicas de la especificación", dice Appel.En Microsoft Research, los programadores tienen dos proyectos ambiciosos. El primero, Everest, tiene como objetivo crear una versión validada de HTTPS, un protocolo para proteger los navegadores web que Wing llama el "talón de Aquiles de Internet".El segundo es la creación de especificaciones confirmadas para sistemas ciberfísicos complejos, como los UAV. El proyecto tiene dificultades significativas. Mientras que los programas convencionales funcionan con pasos separados e inequívocos, los programas de control de drones utilizan el aprendizaje automático para tomar decisiones probabilísticas basadas en un flujo continuo de datos ambientales. Está lejos de ser obvio cómo se pueden tomar decisiones lógicas con tal grado de inexactitud, o describirlas como una especificación formal. Pero solo en los últimos diez años, los métodos formales han avanzado bastante, y Wing, al administrar el proyecto, cree de manera optimista que los investigadores podrán resolver todos estos problemas. Source: https://habr.com/ru/post/es398825/
All Articles