Inicio Intelectualidad Criptografía inabordable por los piratas

Criptografía inabordable por los piratas

Las bibliotecas criptográficas posibilitan las comunicaciones seguras. EverCript es la primera demostrablemente segura contra los formas conocidas de ataque de los piratas informáticos [Eric Nyquist para Quanta Magazine, fragmento].

También te puede interesar

La información La información Abr/Jun 2004 Nº 36

¿Qué es la información? ¿Cómo puede cuantificarse? ¿Cómo operan los distintos dispositivos que nos permiten almacenarla? ¿Y los mecanismos e infraestructuras que la transmiten? Este monográfico ofrece una visión transversal de las principales cuestiones que plantea este concepto tan fundamental para la ciencia.

Más información

Los programadores son humanos, pero las matemáticas son inmortales. Al hacer que la programación sea más matemática, un grupo de científicos de la computación espera eliminar los fallos de programación que les abren las puertas a los piratas informáticos, que permiten que se difundan secretos digitales y que son,en general, una lacra de la sociedad moderna.

Ahora, un conjunto de científicos de la computación ha dado un gran paso hacia esa meta al publicar el 2 de abril EverCrypt, un conjunto de herramientas criptográficas digitales. Han podido probar (en el mismo sentido de la palabra que cuando se dice que se prueba el teorema de Pitágoras) que su forma de abordar la seguridad en Internet es completamente invulnerable ante los tipos principales de pirateos que han minado otros programas en el pasado. «Cuando decimos ‘prueba’, queremos decir que probamos que nuestro programa no puede sufrir esos tipos de ataques», dice Khartik Bhargavan, científico de la computación del Inria de París que ha trabajado en la creación de EverCrypt.

EverCript no se ha escrito como se escribe la mayoría de los programas. Por lo común, un equipo de programadores crea programas de los que piensa que satisfarán ciertos objetivos. Una vez que han acabado, los someten a ensayos. Si logran los objetivos sin mostrar ningún comportamiento indeseado, concluirán que los programas hacen lo que se supone que han de hacer.

Sin embargo, los errores de programación se manifiestan a menudo solo en algunos «casos de encerrona» (corner cases) extremos: tormentas perfectas de sucesos improbables que revelan una vulnerabilidad crítica. Muchos de los ataques piratas más dañinos de los últimos años han aprovechado precisamente encerronas.

«Un fallo en cascada, digamos, puede costar encontrarlo sistemáticamente porque ([los sucesos que conducen a él] son todos, individualmente, muy improbables», dice Bryan Parno, científico de la computación de la Universidad Carnegie Mellon que trabajó en el EverCrypt.

Por el contrario, Parno y sus colaboradores han especificado exactamente lo que se supone que tiene que hacer su programa y luego han probado que hace eso y solo eso, descartando la posibilidad de que pueda desviarse de maneras inesperadas en circunstancias inusuales. La estrategia general recibe le nombre de «verficación formal».

«Se puede reducir el problema de cómo se comporta el programa a una fórmula matemática, y entonces se puede comprobar si la fórmula se cumple. Si lo hace, sabrás que tu programa tiene esa propiedad».

Como es a todos los efectos imposible especificar formalmente la función de un programa complejo, un navegador de la Red, por ejemplo, los investigadores se centraron en unos programas que tienen una importancia crítica pero a los que se puede formalizar matemáticamente. EverCrypt es una biblioteca de programas de criptografía, la codificación y decodificación de la información privada. Estas bibliotecas criptográficas son intrínsecamente matemáticas. Se encargan de operaciones aritméticas con números primos y operaciones con objetos geométricos canónicos, como las curvas elípticas. Definir lo que las bibliotecas criptográficas hacen en términos formales no es desorbitado.

Se empezó a trabajar en EverCrypt en 2016, dentro del proyecto Everest, una iniciativa encabezada por Microsoft Research. Por entonces, y todavía hoy, las bibliotecas criptográficas eran un punto débil de muchas aplicaciones informáticas. Ejecutarlas era lento, lo que lastraba el rendimiento final de las aplicaciones de las que formaban parte, y estaban plagadas de errores. «Creo que los creadores de aplicaciones han caído ya un poco en la cuenta de que es un desastre en puertas», dice Jonathan Protzenko, científico de la computación de Microsoft Research que ha trabajado en EverCrypt. «El mundo de los programas informáticos está maduro para algo nuevo que ofrezca garantías [como las que ofrece EverCrypt]».

La mayor dificultad en la creación de EverCrypt fue la elaboración de una sola plataforma de programación que expresase todas las características diferentes que los investigadores querían para una biblioteca criptográfica verificada. La plataforma necesitaba la capacidad de un lenguaje de programación tradicional, como el C++, y la sintáxis lógica y la estructura de los programas de ayuda a la prueba, como Isabelle y Coq, que los matemáticos llevan utilizando desde hace años. No había ninguna plataforma «todo en uno» cuando los investigadores se pusieron a trabajar en EverCrypt, así que produjeron una: un lenguaje de programación llamado F*. Puso las matemáticas y la programación en pie de igualdad.

«Unificamos estas cosas en un solo marco coherente de modo que la distinción entre escribir programas y hacer pruebas se redujese de verdad», dice Bhargavan. «Se puede escribir un programa como si uno fuese un programador, pero al mismo tiempo se puede escribir una prueba como si se fuese un teórico».

La nueva biblioteca criptográfica ofrece una serie de garantías de seguridad. Los investigadores probaron que EverCrypt está libre de errores de programación, como el desbordamiento de búferes, que pueden posibilitar los ataques de los piratas; en realidad, descarta de manera probada la susceptibilidad de todos los posibles casos de «encerron. Probaron también que EverCrypt siempre hace bien las matemáticas criptográficas: nunca realiza el cálculo equivocado.

Pero la más notable de las garantías que ofrece EverCrypt tiene que ver con una clase enteramente diferente de debilidades de la seguridad. Estas se producen cuando un interviniente malintencionado infiere el contenido de un mensaje encriptado con observar cómo está operando un programa.

Un ejemplo: un observador podría saber que un algoritmo de encriptación se ejecuta un poco más deprisa cuando añade un 0 a un valor y un poco más despacio cuando añade un 1. Midiendo el tiempo que un algorimo tarda en encriptar un mensaje, un observador podría empezar haciéndose una idea de si la representación binaria de un mensaje tiene más ceros o más unos, y al final inferiría el mensaje completo. «En alguna parte de los entresijos del algoritmo o de la manera en que se implementa se está filtrando información que puede acabar por completo con el propósito de la encriptación», dice Bhargavan. Esos «ataques de canal lateral», como se los llama, fueron el fundamento de algunos de los pirateos más famoso de los últimos años, entre ellos el conocido como ataque de Lucky Thirteen. Los investigadores han probado que EverCrypt nunca filtra información de maneras que puedan ser aprovechadas por ataques de temporización de ese tipo.

Sin embargo, si bien EverCrypt es probadamente inmune a muchos tipos de ataques, no anuncia una era de programas perfectamente seguros. Protzenko señala que siempre habrá formas de ataque en las que nadie había pensado antes. No se puede probar que EverCrypt será seguro contra ellas, aunque solo sea por la sencilla razón de que no se sabe cómo serán.

Además, hasta una biblioteca criptográfica verificada tiene que trabajar concertadamente con un montón de otros programas (un sistema operativo, muchas aplicaciones de escritorio corrientes) que de ordinario no están verificados y que seguramente no lo van a estar en el futuro previsible. «No vamos a tomar como objetivo algo tan complejo como un procesador de textos o un cliente de Skipe», afirma Protzenko, ya que no es evidente cómo se podría captar en un lenguaje formal lo que se suponen que hacen. «Resulta dificil pensar en el comportamiento pretendido de cosas así».

Como las vulnerabilidades de programas adyacentes no verificados pueden socavar una biblioteca criptográfica, el proyecto Everest quiere rodear a EverCrypt de tantos programas verificados como se pueda. La finalidad más general de la iniciativa es completar una implementación totalmente verificada del protocolo seguro de transferencia de hipertexto seguro, el HTTPS, que es el programa que se encarga de la seguridad de la mayor parte de las comunicaciones en red. Esto abarcará media docena de elementos individuales, como EverCrypt, cada uno de los cuales está verificado formalmente para que funcione por su cuenta y todos los cuales están verificados formalmente para que trabajen juntos.

«El proyecto Everest intenta construir un conjunto mayor de programas verificados y verificados para trabajar juntos. Esperamos que con el tiempo la frontera [de los prgramas verificados] siga creciendo», dice Parno.

Kevin Harnett / Quanta Magazine

Artículo traducido por Investigación y Ciencia con permiso de QuantaMagazine.org, una publicación independiente promovida por la Fundación Simons para potenciar la comprensión de la ciencia.

Más información en Microsoft Research Blog.