Investigadores del Instituto Estatal de Investigación en Informática y Automática (INRIA), Microsoft Research y Carnegie Mellon University presentaron la primera edición de prueba de la biblioteca criptográfica EverCrypt desarrollada en el marco del proyecto Everest y utilizando métodos matemáticos de verificación formal de confiabilidad.
Por sus capacidades y rendimiento, EverCrypt está muy cerca de las bibliotecas criptográficas existentes (OpenSSL) pero que, a diferencia de ellas, ofrece garantías adicionales de confiabilidad y seguridad.
Por ejemplo, el proceso de verificación se reduce a la definición de especificaciones detalladas que describen todos los comportamientos del programa y a la prueba matemática de que el código escrito cumple con las especificaciones preparadas.
A diferencia de los métodos de control de calidad basados en pruebas, la verificación proporciona garantías confiables de que el programa se ejecutará solo como lo concibieron los desarrolladores y no hay clases específicas de errores.
Por ejemplo, el cumplimiento de la especificación garantiza un trabajo seguro con la memoria y la ausencia de errores que conduzcan al desbordamiento del búfer, a los punteros de anulación de la referencia, al acceso a áreas de memoria ya liberadas o a la doble liberación de bloques de memoria.
¿Qué es EverCrypt?
EverCrypt proporciona una comprobación de tipo y valor sólida: un componente nunca pasará parámetros al otro componente que no cumpla con las especificaciones y no obtendrá acceso a los estados internos de los otros componentes.
El comportamiento de entrada/salida se ajusta completamente a las acciones de funciones matemáticas simples, que se definen en estándares criptográficos.
Para protegerse contra ataques en canales de terceros, el comportamiento durante los cálculos (por ejemplo, la duración de la ejecución o la presencia de accesos a cierta memoria) no depende de los datos secretos que se procesan.
El código del proyecto está escrito en el lenguaje funcional F* (F star) , que proporciona un sistema de tipos y refinamientos dependientes, que permiten establecer especificaciones exactas (modelo matemático) para los programas y garantizar la corrección y la ausencia de errores en la implementación mediante fórmulas SMT y herramientas de prueba auxiliares.
El código en F * se distribuye bajo la licencia Apache 2.0, y los módulos finales en C y el ensamblador bajo la licencia MIT.
Sobre la base del código de referencia F *, se genera el ensamblador, C, OCaml, JavaScript y el código de ensamblaje web.
Algunas partes del código preparado por el proyecto ya se utilizan en Firefox, el kernel de Windows , la cadena de bloques de Tezos y VPN Wireguard .
Componentes de EverCrypt
En esencia, EverCrypt combina dos proyectos anteriormente dispares de HACL * y Vale, proporcionando una API unificada basada en ellos y haciéndolos adecuados para su uso en proyectos reales.
HACL * está escrito en Low* y su objetivo es proporcionar primitivos criptográficos para usar en programas C que utilizan las API de estilo de libsodium y NaCL.
El proyecto Vale desarrolló un lenguaje específico de dominio para crear verificaciones en el ensamblador.
Cerca de 110 mil líneas de código HACL * en lenguaje Low * y 25 mil líneas de código para Vale se combinan y se reescriben en alrededor de 70 mil líneas de código en lenguaje universal F *, que también se está desarrollando como parte del proyecto Everest.
La primera versión de la biblioteca EverCrypt presenta implementaciones verificadas de los siguientes algoritmos criptográficos que se proponen en versiones de C o de ensamblador (cuando se usa la biblioteca.
De estos, en la pagina del proyecto se destacan:
- Algoritmos de hash: todas las variantes de SHA2, SHA3, SHA1 y MD5
- Códigos de autenticación: HMAC sobre SHA1, SHA2-256, SHA2-384 y SHA2-512 para la autenticación de la fuente de datos
- Algoritmo de generación de claves HKDF (función de derivación de clave de extracción y expansión basada en HMAC)
- Cifrado de flujo ChaCha20 (versión C no optimizada disponible)
- Algoritmo de autenticación de mensajes (MAC) Poly1305 (C y versión de ensamblador)
- Protocolo Diffie-Hellman en curvas elípticas Curve25519 (versiones en C y ensamblador con optimizaciones basadas en las instrucciones de BMI2 y ADX)
- Modo de cifrado de bloque AEAD (cifrado autenticado) ChachaPoly (versión C no optimizada)
- AEAD AES-GCM bloque modo de encriptación (versión de ensamblador con optimizaciones AES-NI).
En la primera versión alfa, la verificación del código ya se ha completado en gran medida, pero todavía hay algunas áreas sin cubrir.
Además, la API aún no está estabilizada, que se ampliará en las siguientes versiones alfa (está planificada para unificar estructuras para todas las API.
Entre las fallas, también se destaca la compatibilidad con la arquitectura x86_64 (en la primera etapa, el objetivo principal es la confiabilidad, mientras que la optimización y las plataformas se implementarán en el segundo lugar).
Fuente: https://jonathan.protzenko.fr