- Les algorithmes de hachage de base et HMAC de Python sont d�e9sormais remplac�e9s par HACL*, un code cryptographique v�e9rifi�e9
- Environ 15�000 lignes de code C issues de HACL* ont �e9t�e9 int�e9gr�e9es automatiquement dans la base de code de Python
- Une API de streaming a �e9t�e9 con�e7ue et v�e9rifi�e9e de mani�e8re g�e9n�e9rique afin de prendre en charge divers algorithmes par blocs
- Des probl�e8mes d'ing�e9nierie avanc�e9s ont �e9t�e9 trait�e9s, notamment la gestion des �e9checs d'allocation m�e9moire, la r�e9solution de probl�e8mes de compilation AVX2 et l'optimisation de l'environnement CI
- La collaboration entre Python et la communaut�e9 de la cryptographie a permis d'am�e9liorer concr�e8tement la s�e9curit�e9 et la maintenabilit�e9
Adoption dans Python de code enti�e8rement v�e9rifi�e9 pour les algorithmes cryptographiques
- Apr�e8s CVE-2022-37454, li�e9 �e0 l'impl�e9mentation de SHA3 en 2022, la question d'une migration de l'infrastructure de hachage de Python vers du code v�e9rifi�e9 s'est impos�e9e
- Au cours des deux ann�e9es et demie suivantes, Python a enti�e8rement remplac�e9 ses impl�e9mentations int�e9gr�e9es de hachage et de HMAC par des impl�e9mentations v�e9rifi�e9es bas�e9es sur HACL*
- Ce remplacement a �e9t�e9 effectu�e9 de mani�e8re totalement transparente pour les utilisateurs, sans perte fonctionnelle
- HACL* a impl�e9ment�e9 des fonctionnalit�e9s suppl�e9mentaires pour Python : divers modes de Blake2, une API prenant en charge les variantes Keccak de SHA3, ainsi que des optimisations de streaming pour HMAC
- L'int�e9gration des nouvelles versions est automatis�e9e par script, ce qui facilite la maintenance
Comprendre l'API de streaming
- La plupart des algorithmes cryptographiques sont des algorithmes par blocs, qui doivent traiter les entr�e9es bloc par bloc
- Dans les conditions d'utilisation r�e9elles, il est difficile de fournir les entr�e9es directement par blocs, d'o�f9 le besoin d'une API de streaming
- Une API de streaming fonctionne quelle que soit la longueur de l'entr�e9e et permet aussi d'extraire des r�e9sultats interm�e9diaires
- Les impl�e9mentations de streaming exigent une gestion d'�e9tat complexe, et l'ancienne impl�e9mentation de SHA3 pr�e9sentait �e0 ce sujet une grave faille de s�e9curit�e9
- La complexit�e9 augmente car chaque algorithme de hachage traite les donn�e9es diff�e9remment : par exemple, Blake2 n'autorise pas les blocs vides, et HMAC peut supprimer la cl�e9 apr�e8s initialisation
V�e9rification d'un algorithme de streaming g�e9n�e9rique
- Une m�e9thode pr�e9sent�e9e dans un article publi�e9 en 2021 consiste �e0 abstraire les algorithmes par blocs, puis �e0 d�e9finir par-dessus un algorithme de streaming g�e9n�e9rique
- Elle peut ensuite �eatre appliqu�e9e comme un mod�e8le �e0 chaque algorithme, ce qui la rend r�e9utilisable
- La g�e9n�e9ralisation couvre tous les cas particuliers, notamment :
- la possibilit�e9 ou non de sp�e9cifier une longueur de sortie (SHA3 vs Shake)
- l'existence d'une entr�e9e pr�e9alable n�e9cessaire au traitement (par exemple le bloc de cl�e9 de Blake2)
- les diff�e9rences de traitement du bloc final
- les informations suppl�e9mentaires �e0 conserver dans l'�e9tat interne
- la mani�e8re de copier l'�e9tat pour extraire des r�e9sultats interm�e9diaires (
stack vs heap)
- la strat�e9gie consistant �e0 utiliser une API propre �e0 chaque algorithme ou une API de famille
Assurer la stabilit�e9 du build pour l'int�e9gration �e0 Python
- La CI de Python valide le code sur plus de 50 toolchains et architectures, ce qui fait remonter m�eame les probl�e8mes mineurs
- Lors de l'impl�e9mentation de HMAC, un probl�e8me de prise en charge des instructions AVX2 est apparu :
- certains compilateurs ne peuvent pas traiter l'en-t�eate
immintrin.h sans AVX2
- le probl�e8me a �e9t�e9 r�e9solu en utilisant le pattern de structure abstraite en C
- en raison de la diff�e9rence entre le concept d'abstraction dans le code C g�e9n�e9r�e9 par F* et les structures C, il a fallu ajouter au compilateur
krml une fonction fine d'analyse de visibilit�e9
R�e9ponse aux �e9checs d'allocation m�e9moire
- Le mod�e8le F* existant permettait en th�e9orie de mod�e9liser les pannes m�e9moire, mais c'est la premi�e8re fois qu'il �e9tait appliqu�e9 en pratique
- Pour r�e9pondre aux exigences de Python, les structures d'�e9tat, les d�e9finitions d'algorithmes et les structures de streaming ont tous �e9t�e9 am�e9lior�e9s afin de propager les �e9checs d'allocation
- Dans F*, cela passe par le type
option, compil�e9 en C sous forme de union �e9tiquet�e9e
- �c0 l'avenir, il pourrait �eatre remplac�e9 par un m�e9canisme de drapeau d'�e9chec �e0 l'ex�e9cution afin de r�e9duire la complexit�e9
Automatisation des mises �e0 jour du code HACL*
- La PR Python initiale utilisait
sed pour supprimer des d�e9finitions d'en-t�eate inutiles, corriger des chemins, etc.
- Une fois la stabilit�e9 du code HACL* confirm�e9e, les traitements
sed complexes ont �e9t�e9 supprim�e9s et remplac�e9s par un script simple
- Ce script permet �e0 n'importe qui de mettre facilement �e0 jour le code HACL* vers la derni�e8re version dans l'arborescence des sources de Python
Conclusion
- Du code cryptographique v�e9rifi�e9 a �e9t�e9 int�e9gr�e9 avec succ�e8s dans Python, un environnement de production majeur
- Cela montre que cette technologie ne rel�e8ve plus seulement de la recherche acad�e9mique, mais qu'elle est aussi pratique et maintenable dans des logiciels r�e9els
- C'est un bon exemple de collaboration entre la communaut�e9 Python et les d�e9veloppeurs de HACL*, qui pourrait inspirer d'autres projets �e0 l'avenir
2 commentaires
Comme cela a été mentionné dans les commentaires sur Hacker News, il est difficile de comprendre ce que cela signifie de dire que l’écosystème Python a accompli quelque chose qui « dépasse le stade de la recherche académique pour devenir réellement pratique et maintenable dans des logiciels concrets ».
Si l’on voulait dire qu’un travail a été mené pour abstraire des algorithmes de streaming par-dessus l’infrastructure de hachage existante non vérifiée, alors ce n’est encore qu’un autre jeu de mots « pythonique ».
Commentaires Hacker News
La version de Python n’est pas précisée. Après vérification, cette fonctionnalité devrait être incluse dans la version 3.14. On ne la verra probablement pas avant octobre
Ils ont intégré à CPython une bibliothèque C vérifiée générée à partir de F* de Microsoft et ont écrit une extension C
Je me demande s’ils vont ajouter la prise en charge de la sortie « streaming » de SHAKE
La cryptographie moderne largement utilisée est en pratique incassable, et les guerres de la crypto des années 90 paraissent désormais un peu datées. Je me demande s’il y a une réflexion sur l’impact que cela a sur la société
Je me demande dans quelle mesure un framework général de vérification en streaming est réutilisable au-delà des fonctions de hachage cryptographique
Je me demande si tout ce qui importe le module crypto doit inclure G++ ou autre chose, ou si cela est compilé directement dans CPython
Je ne connais pas bien la cryptographie. Je me demande ce que cela signifie concrètement pour Python
Je me demande quelle part du développement a été vérifiée, et ce que cela recouvre exactement
Le nombre de lignes de code est une très mauvaise métrique. C’est encore plus vrai quand on se vante de gros chiffres, surtout dans le contexte du code cryptographique