Fiat Cryptography, el sistema del MIT para generar código criptográfico optimizado para todo tipo de hardware

Fiat Cryptography es el nombre que recibe un sistema desarrollado por investigadores del MIT para generar automáticamente y verificar simultáneamente algoritmos criptográficos optimizados en todas las plataformas de hardware. De esta manera, se evitan los errores de implementarlos a mano y resultan mucho más eficientes. Google usa implementaciones de esa biblioteca en BoringSSL para reemplazar el código especializado existente en Chrome, Android y CloudFlare.

¿Qué tiene de especial este sistema y por qué es tan importante?

Toda conexión TLS comienza con un apretón de manos

La criptografía está por todas partes. Por ejemplo, cada vez que te conectas con el navegador a una página a través del protocolo HTTPS, tu dispositivo y el servidor web ejecutan un establecimiento de comunicación (handshake) para negociar una sesión de TLS:

1. Intercambian los algoritmos de cifrado soportados junto con sus fortalezas y acuerdan los parámetros de conexión deseados.
2. Validan los certificados presentados o se autentican utilizando otros medios. Hoy RSA sigue siendo el algoritmo de clave pública más utilizado, aunque perdiendo terreno rápidamente ante ECC, debido a que ECC utiliza claves mucho más cortas y previene algunos problemas de RSA.
3. Acuerdan una clave secreta compartida para cifrar con un algoritmo simétrico tipo AES los datos intercambiados durante la sesión.
4. Comprueban que los mensajes anteriores no han sido modificados por un tercero.

A partir de este momento, todos los datos viajarán cifrados. Todas estas operaciones consumen muchos recursos, especialmente el uso de algoritmos de clave asimétrica, y en particular el uso de RSA. De ahí la importancia de codificar los algoritmos de forma totalmente correcta, para evitar brechas de seguridad, y de forma tan optimizada como sea posible, para agilizar las transacciones con potencialmente miles de clientes.

En pos de la máxima eficiencia, los algoritmos criptográficos se codifican por lo general en lenguajes de bajo nivel, como C a pelo e incluso ensamblador, independientemente para cada tipo de hardware. Hay que tener en cuenta que la criptografía de clave pública como ECC o RSA opera con enteros muy grandes. La mayoría de los chips no pueden almacenar números tan grandes en un solo registro, por lo que los dividen en números más pequeños que puedan almacenarse en un registro. Pero el número de registros y su tamaño varían de un chip a otro con consecuencias de rendimiento diferentes. Y, para colmo, si se cambia el tamaño del módulo primo bajo el que se realizan las operaciones matemáticas al cifrar y descifrar, entonces ¡hay que recodificar a mano todo el algoritmo!

¿Buscas codificar criptografía? ¡Pues vas a sufrir!

¿Por qué codificar algoritmos criptográficos es fuente de tanto sufrimiento? La mala programación vuelve insegura la mejor criptografía. La implementación a mano de bajo nivel ha sido la única manera de lograr un buen rendimiento, asegurar que el tiempo de ejecución no filtre información secreta y permitir que el código sea llamado desde cualquier lenguaje de programación.

Para que te hagas una idea de la complejidad de esta tarea, aquí tienes el código en C solamente para la operación elevar un número al cuadrado módulo un primo en una arquitectura de 64 bits.

Recapitulando: cada algoritmo criptográfico debe programarse cuidadosamente para cada longitud de módulo para cada arquitectura y para cada longitud de palabra. Y todo ello a mano. Cambia cualquiera de esos elementos y ¡vuelta a empezar desde cero!

Como puedes imaginar, surgen muchas oportunidades para cometer errores por el camino. Y así ha sido, como listan con paciencia los autores del trabajo Fiat Cryptography en su apéndice.

¡Hágase la criptografía! Y los algoritmos fueron creados. Y los criptógrafos vieron que eran buenos

Los autores de Fiat Cryptography muestran que su compilador automático puede producir este código especializado en aritmética modular, a través de versiones formalizadas de las optimizaciones basadas en teoría de números que antes sólo se aplicaban a mano. En su trabajo, presentan experimentos para una amplia gama de longitudes de módulo, compilados para procesadores x86 de 64 bits y ARM de 32 bits, demostrando velocidades desde cinco hasta diez veces superiores en comparación con bibliotecas tradicionales de grandes enteros.

Además, al implementar su compilador en el asistente de pruebas Coq, genera pruebas de corrección funcional. Estas ventajas combinadas con las garantías rigurosas de corrección/seguridad y ahorro de mano de obra bastaron para convencer a Google de que adoptara el compilador para partes de su implementación de TLS en su biblioteca de código abierto BoringSSL, utilizada para generar claves y certificados para Chrome, apps de Android y otros programas.

Al automatizar la escritura de algoritmos criptográficos, la Fiat Cryptography puede eliminar errores, producir código más seguro y aumentar el rendimiento. Tras el éxito obtenido en BoringSSL, muy pronto la veremos en otras bibliotecas criptográficas.