- Los algoritmos base de hash y HMAC de Python ahora fueron reemplazados por código criptográfico verificado de HACL*
- Cerca de 15,000 líneas de código C fueron integradas automáticamente desde HACL* al código base de Python
- Se diseñó y verificó de forma genérica una API de streaming para poder manejar diversos algoritmos por bloques
- Se abordaron problemas avanzados de ingeniería como manejo de fallas de asignación de memoria, resolución de problemas de compilación con AVX2 y optimización del entorno de CI
- Gracias a la colaboración entre Python y la comunidad criptográfica, se lograron al mismo tiempo seguridad real y mantenibilidad
Adopción de código completamente verificado para los algoritmos criptográficos de Python
- Después de CVE-2022-37454 relacionado con la implementación de SHA3 en 2022, surgió la necesidad de migrar en Python la infraestructura de hash hacia código verificado
- Tras dos años y medio, Python reemplazó por completo sus algoritmos integrados de hash y HMAC por implementaciones verificadas basadas en HACL*
- Este reemplazo se hizo de forma totalmente transparente para el usuario, sin pérdida de funcionalidad
- HACL* además implementó funciones adicionales para Python: varios modos de Blake2, una API con soporte para variantes Keccak de SHA3 y optimizaciones de streaming para HMAC
- La incorporación de nuevas versiones está automatizada mediante scripts, lo que facilita el mantenimiento
Entendiendo la API de streaming
- La mayoría de los algoritmos criptográficos son algoritmos por bloques, por lo que deben procesar la entrada en bloques
- En entornos reales de uso, ingresar datos en bloques suele ser difícil, por eso se necesita una API de streaming
- Una API de streaming funciona sin importar la longitud de la entrada y también permite extraer resultados intermedios
- Las implementaciones de streaming requieren una gestión compleja del estado, y en la implementación anterior de SHA3 hubo una falla de seguridad grave relacionada con esto
- Cada algoritmo hash tiene una forma distinta de procesar, lo que aumenta la complejidad: por ejemplo, Blake2 no permite bloques vacíos, mientras que HMAC puede inicializar la clave y luego descartarla
Verificación de un algoritmo de streaming genérico
- Un enfoque presentado en un artículo de 2021 consiste en abstraer los algoritmos por bloques y luego definir sobre esa base un algoritmo de streaming genérico
- Después, se puede aplicar como una plantilla a cada algoritmo, permitiendo su reutilización
- Se generalizó para incluir todas las condiciones especiales:
- Si la longitud de salida puede especificarse o no (SHA3 vs Shake)
- Si se necesita entrada previa al procesamiento (por ejemplo, el bloque de clave de Blake2)
- Diferencias en el procesamiento del bloque final
- Información adicional que debe conservarse en el estado interno
- Cómo copiar el estado para extraer resultados intermedios (
stack vs heap)
- Estrategia de uso de API individual por algoritmo vs API por familia
Garantizar estabilidad de compilación para la integración en Python
- El CI de Python se valida sobre más de 50 toolchains y arquitecturas, lo que hace aflorar incluso problemas menores
- Durante la implementación de HMAC surgieron problemas con el soporte de instrucciones AVX2:
- Algunos compiladores no pueden procesar el encabezado
immintrin.h sin AVX2
- Para resolverlo, se usó el patrón de estructura abstracta en C
- Debido a las diferencias entre el concepto de abstracción en el código C generado desde F* y las estructuras de C, fue necesario agregar al compilador
krml una función precisa de análisis de visibilidad
Manejo de fallas de asignación de memoria
- El modelo previo de F* en teoría podía modelar fallas de memoria, pero esta fue la primera vez que se aplicó en la práctica
- Según los requisitos de Python, se mejoraron tanto las estructuras de estado como las definiciones de algoritmos y las estructuras de streaming para que puedan propagar fallas de asignación
- En F* se usa el tipo
option, que en C se compila como una tagged union
- A futuro existe la posibilidad de cambiar a un esquema de bandera de falla en tiempo de ejecución para reducir la complejidad
Automatización de las actualizaciones de código de HACL*
- El PR inicial de Python usaba
sed para eliminar definiciones de encabezados innecesarias, ajustar rutas y otras tareas
- Luego, una vez confirmada la estabilidad del código de HACL*, ese
sed complejo se eliminó y fue reemplazado por un script simple
- Con este script, cualquiera puede actualizar fácilmente el código de HACL* a la versión más reciente dentro del árbol de código fuente de Python
Conclusión
- El código criptográfico verificado se integró con éxito en Python, un entorno de producción representativo
- Este caso demuestra que esta tecnología no se queda solo en el ámbito académico, sino que también es práctica y mantenible en software real
- Es un buen ejemplo de colaboración entre la comunidad de Python y los desarrolladores de HACL*, y podría influir en otros proyectos en el futuro
2 comentarios
Como se mencionó también en los comentarios de Hacker News, es difícil entender qué logró exactamente el ecosistema de Python que haya ido "más allá de la etapa de investigación académica para volverse algo práctico y mantenible también en software real".
Si lo que querían decir era que trabajaron en abstraer algoritmos de streaming sobre la infraestructura de hash existente no verificada, entonces esto no es más que otro juego de palabras "pythonic".
Comentarios en Hacker News
No se especificó la versión de Python. Según lo que investigué, esta función está prevista para incluirse en la versión 3.14. No la veremos hasta octubre
Incluyeron en CPython una biblioteca de C verificada generada desde F* de Microsoft y escribieron una extensión en C
Me pregunto si van a incorporar soporte para salida "streaming" de SHAKE
La criptografía moderna de uso extendido es, en la práctica, irrompible, y las guerras criptográficas de los 90 ahora parecen algo anticuadas. Me pregunto si alguien tiene ideas sobre el impacto que esto tiene en la sociedad
Me pregunto qué tanto se puede reutilizar un framework general de verificación de streaming más allá de los hashes criptográficos
Me pregunto si todo lo que importe el módulo de criptografía tendrá que incluir G++ o algo similar, o si se compilará dentro del propio CPython
No sé mucho de criptografía. Me pregunto qué significa esto para Python
Me pregunto qué parte del desarrollo fue verificada y qué es exactamente lo que eso incluye
Las líneas de código son una métrica muy inapropiada. Más aún en el contexto del código criptográfico, cuando se presume un número grande