Python intègre désormais 15000 lignes de code cryptographique ve9rifie9

• Les algorithmes de hachage de base et HMAC de Python sont de9sormais remplace9s par HACL*, un code cryptographique ve9rifie9
• Environ 15000 lignes de code C issues de HACL* ont e9te9 inte9gre9es automatiquement dans la base de code de Python
• Une API de streaming a e9te9 cone7ue et ve9rifie9e de manie8re ge9ne9rique afin de prendre en charge divers algorithmes par blocs
• Des proble8mes d'inge9nierie avance9s ont e9te9 traite9s, notamment la gestion des e9checs d'allocation me9moire, la re9solution de proble8mes de compilation AVX2 et l'optimisation de l'environnement CI
• La collaboration entre Python et la communaute9 de la cryptographie a permis d'ame9liorer concre8tement la se9curite9 et la maintenabilite9

---

Adoption dans Python de code entie8rement ve9rifie9 pour les algorithmes cryptographiques

• Apre8s CVE-2022-37454, lie9 e0 l'imple9mentation de SHA3 en 2022, la question d'une migration de l'infrastructure de hachage de Python vers du code ve9rifie9 s'est impose9e
• Au cours des deux anne9es et demie suivantes, Python a entie8rement remplace9 ses imple9mentations inte9gre9es de hachage et de HMAC par des imple9mentations ve9rifie9es base9es sur HACL*
• Ce remplacement a e9te9 effectue9 de manie8re totalement transparente pour les utilisateurs, sans perte fonctionnelle
• HACL* a imple9mente9 des fonctionnalite9s supple9mentaires 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'inte9gration des nouvelles versions est automatise9e 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 entre9es bloc par bloc
• Dans les conditions d'utilisation re9elles, il est difficile de fournir les entre9es directement par blocs, d'of9 le besoin d'une API de streaming
• Une API de streaming fonctionne quelle que soit la longueur de l'entre9e et permet aussi d'extraire des re9sultats interme9diaires
• Les imple9mentations de streaming exigent une gestion d'e9tat complexe, et l'ancienne imple9mentation de SHA3 pre9sentait e0 ce sujet une grave faille de se9curite9
• La complexite9 augmente car chaque algorithme de hachage traite les donne9es diffe9remment : par exemple, Blake2 n'autorise pas les blocs vides, et HMAC peut supprimer la cle9 apre8s initialisation

Ve9rification d'un algorithme de streaming ge9ne9rique

• Une me9thode pre9sente9e dans un article publie9 en 2021 consiste e0 abstraire les algorithmes par blocs, puis e0 de9finir par-dessus un algorithme de streaming ge9ne9rique
• Elle peut ensuite eatre applique9e comme un mode8le e0 chaque algorithme, ce qui la rend re9utilisable
• La ge9ne9ralisation couvre tous les cas particuliers, notamment :
  • la possibilite9 ou non de spe9cifier une longueur de sortie (SHA3 vs Shake)
  • l'existence d'une entre9e pre9alable ne9cessaire au traitement (par exemple le bloc de cle9 de Blake2)
  • les diffe9rences de traitement du bloc final
  • les informations supple9mentaires e0 conserver dans l'e9tat interne
  • la manie8re de copier l'e9tat pour extraire des re9sultats interme9diaires (stack vs heap)
  • la strate9gie consistant e0 utiliser une API propre e0 chaque algorithme ou une API de famille

Assurer la stabilite9 du build pour l'inte9gration e0 Python

• La CI de Python valide le code sur plus de 50 toolchains et architectures, ce qui fait remonter meame les proble8mes mineurs
• Lors de l'imple9mentation de HMAC, un proble8me de prise en charge des instructions AVX2 est apparu :
  • certains compilateurs ne peuvent pas traiter l'en-teate immintrin.h sans AVX2
  • le proble8me a e9te9 re9solu en utilisant le pattern de structure abstraite en C
  • en raison de la diffe9rence entre le concept d'abstraction dans le code C ge9ne9re9 par F* et les structures C, il a fallu ajouter au compilateur krml une fonction fine d'analyse de visibilite9

Re9ponse aux e9checs d'allocation me9moire

• Le mode8le F* existant permettait en the9orie de mode9liser les pannes me9moire, mais c'est la premie8re fois qu'il e9tait applique9 en pratique
• Pour re9pondre aux exigences de Python, les structures d'e9tat, les de9finitions d'algorithmes et les structures de streaming ont tous e9te9 ame9liore9s afin de propager les e9checs d'allocation
• Dans F*, cela passe par le type option, compile9 en C sous forme de union e9tiquete9e
• c0 l'avenir, il pourrait eatre remplace9 par un me9canisme de drapeau d'e9chec e0 l'exe9cution afin de re9duire la complexite9

Automatisation des mises e0 jour du code HACL*

• La PR Python initiale utilisait sed pour supprimer des de9finitions d'en-teate inutiles, corriger des chemins, etc.
• Une fois la stabilite9 du code HACL* confirme9e, les traitements sed complexes ont e9te9 supprime9s et remplace9s par un script simple
• Ce script permet e0 n'importe qui de mettre facilement e0 jour le code HACL* vers la dernie8re version dans l'arborescence des sources de Python

Conclusion

• Du code cryptographique ve9rifie9 a e9te9 inte9gre9 avec succe8s dans Python, un environnement de production majeur
• Cela montre que cette technologie ne rele8ve plus seulement de la recherche acade9mique, mais qu'elle est aussi pratique et maintenable dans des logiciels re9els
• C'est un bon exemple de collaboration entre la communaute9 Python et les de9veloppeurs de HACL*, qui pourrait inspirer d'autres projets e0 l'avenir

[sonnet]

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 ».

[GN⁺]

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

  • On peut soutenir qu’il s’agit d’un correctif de sécurité et qu’elle devrait être incluse dans toutes les versions actuellement prises en charge de Python (>=3.9)

• 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

  • Au cours du processus, ils ont découvert que la bibliothèque d’origine ne gérait pas les échecs d’allocation
  • Je me demande quel est le véritable enjeu pour Python. Ce n’est finalement qu’une autre bibliothèque C encapsulée

• Je me demande s’ils vont ajouter la prise en charge de la sortie « streaming » de SHAKE

  • Il y a un ticket récemment fermé sur cette fonctionnalité dans pyca/cryptography. Je ne trouve pas de ticket équivalent pour la bibliothèque standard Python
  • J’ai trouvé le ticket correspondant, et il a été fermé comme « non prévu »

• 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 mot « vérifiée » m’inquiète un peu quand je le lis

• 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