Casi cada vez que abre un navegador seguro de Google Chrome, un nuevo sistema criptográfico desarrollado por el MIT ayuda a proteger mejor sus datos.

En un artículo presentado en el reciente Simposio de IEEE sobre seguridad y privacidad, Los investigadores del MIT detallan un sistema que, por primera vez, genera automáticamente un código de criptografía optimizado que generalmente se escribe a mano. Implementado a principios de 2018, Google y otras firmas tecnológicas ahora utilizan ampliamente el sistema.

El documento ahora demuestra a otros investigadores en el campo cómo se pueden implementar métodos automatizados para evitar errores humanos al generar criptocódigo. y cómo los ajustes clave a los componentes del sistema pueden ayudar a lograr un mayor rendimiento.

Para proteger las comunicaciones en línea, Los protocolos criptográficos ejecutan algoritmos matemáticos complejos que realizan operaciones aritméticas complejas con números grandes. Entre bastidores, sin embargo, un pequeño grupo de expertos escribe y reescribe esos algoritmos a mano. Para cada algoritmo, deben sopesar varias técnicas matemáticas y arquitecturas de chips para optimizar el rendimiento. Cuando cambian las matemáticas o la arquitectura subyacentes, en esencia, comienzan de cero. Aparte de ser un trabajo intensivo, este proceso manual puede producir algoritmos no óptimos y, a menudo, introduce errores que luego se detectan y se corrigen.

En cambio, los investigadores del Laboratorio de Ciencias de la Computación e Inteligencia Artificial (CSAIL) diseñaron "Criptografía Fiat, "un sistema que genera automáticamente, y verifica simultáneamente, algoritmos criptográficos optimizados para todas las plataformas de hardware. En las pruebas, los investigadores encontraron que su sistema puede generar algoritmos que coinciden con el rendimiento del mejor código escrito a mano, pero mucho más rápido.

El código generado automáticamente por los investigadores ha poblado el BoringSSL de Google, una biblioteca criptográfica de código abierto. Google Chrome, Aplicaciones de Android, y otros programas utilizan BoringSSL para generar las diversas claves y certificados que se utilizan para cifrar y descifrar datos. Según los investigadores, aproximadamente el 90 por ciento de las comunicaciones seguras de Chrome ejecutan actualmente su código.

"La criptografía se implementa haciendo aritmética en números grandes. [Fiat Cryptography] hace que sea más sencillo implementar los algoritmos matemáticos ... porque automatizamos la construcción del código y proporcionamos pruebas de que el código es correcto, "dice el coautor del artículo Adam Chlipala, investigador de CSAIL y profesor asociado de ingeniería eléctrica e informática y jefe del grupo de Lenguajes de Programación y Verificación. "Es básicamente como tomar un proceso que se ejecuta en el cerebro humano y comprenderlo lo suficientemente bien como para escribir un código que imite ese proceso".

Jonathan Protzenko de Microsoft Research, un experto en criptografía que no participó en esta investigación, considera que el trabajo representa un cambio en el pensamiento de la industria.

"La criptografía Fiat que se utiliza en BoringSSL beneficia a toda la comunidad [criptográfica], ", dice." [Es] una señal de que los tiempos están cambiando y que los grandes proyectos de software se están dando cuenta de que la criptografía insegura es una desventaja, [y muestra] que el software verificado es lo suficientemente maduro para entrar en la corriente principal. Tengo la esperanza de que cada vez más proyectos de software establecidos hagan el cambio a la criptografía verificada. Quizás en los próximos años, El software verificado será utilizable no solo para algoritmos criptográficos, sino también para otros dominios de aplicaciones ".

Junto a Chlipala en el artículo están:el primer autor Andres Erbsen y los coautores Jade Philipoom y Jason Gross, que son todos estudiantes graduados de CSAIL; así como Robert Sloan MEng '17.

Dividiendo los bits

Los protocolos de criptografía utilizan algoritmos matemáticos para generar claves públicas y privadas, que son básicamente una larga cadena de bits. Los algoritmos utilizan estas claves para proporcionar canales de comunicación seguros entre un navegador y un servidor. Una de las familias de algoritmos criptográficos eficientes y seguras más populares se llama criptografía de curva elíptica (ECC). Básicamente, genera claves de varios tamaños para los usuarios eligiendo puntos numéricos al azar a lo largo de una línea curva numerada en un gráfico.

La mayoría de los chips no pueden almacenar cantidades tan grandes en un solo lugar, por lo que los dividen brevemente en dígitos más pequeños que se almacenan en unidades llamadas registros. Pero la cantidad de registros y la cantidad de almacenamiento que proporcionan varía de un chip a otro. "Tienes que dividir los bits en un montón de lugares diferentes, pero resulta que la forma de dividir los bits tiene diferentes consecuencias en el rendimiento, "Dice Chlipala.

Tradicionalmente, los expertos que escriben algoritmos ECC implementan manualmente esas decisiones de división de bits en su código. En su trabajo, Los investigadores del MIT aprovecharon esas decisiones humanas para generar automáticamente una biblioteca de algoritmos ECC optimizados para cualquier hardware.

Sus investigadores exploraron primero las implementaciones existentes de algoritmos ECC escritos a mano, en los lenguajes ensambladores y de programación C, y transfirió esas técnicas a su biblioteca de códigos. Esto genera una lista de los algoritmos de mejor rendimiento para cada arquitectura. Luego, utiliza un compilador, un programa que convierte los lenguajes de programación en códigos que las computadoras entienden, que ha demostrado ser correcto con una herramienta de revisión, llamado Coq. Básicamente, todo el código producido por ese compilador siempre será verificado matemáticamente. Luego simula cada algoritmo y selecciona el de mejor rendimiento para cada arquitectura de chip.

Próximo, los investigadores están trabajando en formas de hacer que su compilador se ejecute aún más rápido en la búsqueda de algoritmos optimizados.

Compilación optimizada

Existe una innovación adicional que garantiza que el sistema seleccione rápidamente las mejores implementaciones de división de bits. Los investigadores equiparon su compilador basado en Coq con una técnica de optimización, llamada "evaluación parcial, "que básicamente calcula previamente ciertas variables para acelerar las cosas durante el cálculo.

En el sistema de los investigadores, precalcula todos los métodos de división de bits. Al combinarlos con una arquitectura de chip determinada, inmediatamente descarta todos los algoritmos que simplemente no funcionarán para esa arquitectura. Esto reduce drásticamente el tiempo que lleva buscar en la biblioteca. Una vez que el sistema se concentra en el algoritmo óptimo, finaliza la compilación del código.

A partir de ese, Luego, los investigadores acumularon una biblioteca de las mejores formas de dividir los algoritmos ECC para una variedad de arquitecturas de chips. Ahora está implementado en BoringSSL, por lo que los usuarios se basan principalmente en el código de los investigadores. La biblioteca se puede actualizar automáticamente de manera similar para nuevas arquitecturas y nuevos tipos de matemáticas.

"Básicamente, hemos escrito una biblioteca que, de una vez por todas, es correcto para todas las formas en que posiblemente pueda dividir números, ", Dice Chlipala." Puede explorar automáticamente el espacio de posibles representaciones de los grandes números, compilar cada representación para medir el desempeño, y elija el que corra más rápido para un escenario determinado ".

Esta historia se vuelve a publicar por cortesía de MIT News (web.mit.edu/newsoffice/), un sitio popular que cubre noticias sobre la investigación del MIT, innovación y docencia.