Se ha anunciado la finalización exitosa de la iniciativa para reemplazar las implementaciones de algoritmos criptográficos en Python, ofrecidas en los módulos hashlib y hmac, por opciones con pruebas matemáticas de fiabilidad, preparadas por el proyecto «HACL*». El trabajo para la transición a funciones con pruebas matemáticas de fiabilidad se llevó a cabo desde 2022 y fue iniciado tras la detección de un desbordamiento de búfer en la implementación del algoritmo SHA3, utilizado en el módulo hashlib de Python.
Se ha aceptado en el repositorio principal del proyecto CPython el código con las nuevas implementaciones de funciones hash criptográficas y algoritmos HMAC (mecanismo de autenticación de mensajes). Todas las funciones hash y HMAC proporcionadas por defecto en Python han sido reemplazadas por variantes verificadas. Entre otras cosas, se ha añadido la implementación HMAC-BLAKE2, que utiliza instrucciones SIMD AVX2 para acelerar los cálculos. Se espera que el código verificado forme parte de la versión de otoño de Python 3.14.
Las nuevas implementaciones de funciones criptográficas se han trasladado desde la biblioteca HACL*, desarrollada por investigadores del Instituto Nacional de Investigación en Informática y Automática (INRIA) de Francia, una división de Microsoft Research y la Universidad Carnegie Mellon. La biblioteca HACL* soporta funciones criptográficas estándar suficientes para el funcionamiento de TLS 1.3 y el soporte completo de la API NaCl (Networking and Cryptography library), tales como Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC y HKDF. En términos de rendimiento, la biblioteca HACL* es comparable a OpenSSL, pero a diferencia de esta última, ofrece garantías adicionales de fiabilidad y seguridad.
El código de HACL* está escrito en un subconjunto del lenguaje funcional F*, que ofrece un sistema de tipos dependientes y refinamientos que permiten especificar especificaciones precisas (modelo matemático) y garantizar la ausencia de errores en la implementación mediante fórmulas SMT y herramientas auxiliares de prueba. El código de referencia en F* se traduce a código en lenguaje C mediante el compilador KaRaMeL y está disponible para su integración con otros proyectos.
La verificación implica la definición de especificaciones detalladas que describen todos los posibles comportamientos del programa y la formación de una prueba matemática que demuestre que el código escrito cumple completamente con las especificaciones preparadas. La verificación garantiza que el programa se ejecutará solo como lo pensaron los desarrolladores y que no contiene ciertas clases de errores, como desbordamiento de búfer, desreferenciación de punteros, acceso a áreas de memoria ya liberadas o liberación doble de bloques de memoria. Durante el proceso de compilación, se asegura una verificación estricta de tipos y valores: un componente nunca pasará a otro componente parámetros que no cumplan con la especificación ni accederá a los estados internos de otros componentes.
El proceso de transición al código verificado tomó dos años y medio y requirió la modificación de la biblioteca HACL*, cuya funcionalidad se amplió con capacidades necesarias para la sustitución transparente de la funcionalidad existente de hashlib. Por ejemplo, en HACL* se agregó soporte para el modo de operación de flujo de HMAC, se proporcionaron modos adicionales para los algoritmos Blake2, se implementó una nueva API para SHA3 que abarca todas las variaciones de los algoritmos de la familia Keccak, y se proporcionaron los medios necesarios para la notificación de errores (por ejemplo, en caso de problemas de asignación de memoria), se desarrollaron scripts para automatizar la transferencia de nuevas versiones de HACL* al repositorio de Python.
Fuente: opennet.ru
