Il a été annoncé que l'initiative visant à remplacer les implémentations des algorithmes cryptographiques offerts dans les modules hashlib et hmac par des variantes avec preuve mathématique de fiabilité, développées par le projet « HACL* », a été couronnée de succès. Les travaux sur la migration vers des fonctions avec preuve mathématique de fiabilité ont commencé en 2022 et ont été initiés après la découverte d'un débordement de tampon dans l'implémentation de l'algorithme SHA3 utilisé dans le module hashlib de Python.
Le code contenant de nouvelles implémentations des fonctions de hachage cryptographique et des algorithmes HMAC (mécanisme d'authentification des messages) a été intégré dans le dépôt principal du projet CPython. Toutes les fonctions de hachage et HMAC fournies par défaut dans Python ont été remplacées par des variantes vérifiées. Parmi les nouveautés, une implémentation d'HMAC-BLAKE2 a été ajoutée, utilisant les instructions SIMD AVX2 pour accélérer les calculs. Il est prévu que le code vérifié sera inclus dans la prochaine version de Python 3.14, prévue pour l'automne.
Les nouvelles implémentations des fonctions cryptographiques ont été transférées de la bibliothèque HACL*, développée par des chercheurs de l'Institut national de recherche en informatique et en automatique (INRIA) en France, de Microsoft Research et de l'Université Carnegie Mellon. La bibliothèque HACL* prend en charge les fonctions cryptographiques standards suffisantes pour le fonctionnement de TLS 1.3 et le soutien complet de l'API NaCl (Networking and Cryptography library), telles que Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC et HKDF. En termes de performances, la bibliothèque HACL* est proche d'OpenSSL, mais contrairement à la dernière, elle offre des garanties supplémentaires de fiabilité et de sécurité.
Le code HACL* est écrit dans un sous-ensemble du langage fonctionnel F*, qui propose un système de types dépendants et de précisions permettant de spécifier des spécifications exactes (modèle mathématique) et de garantir l'absence d'erreurs dans l'implémentation à l'aide de formules SMT et d'outils d'assistance à la preuve. Le code de référence en F* est traduit en code C à l'aide du compilateur KaRaMeL et est disponible pour une intégration avec d'autres projets.
La vérification implique la définition de spécifications détaillées décrivant tous les comportements possibles du programme, ainsi que la création d'une preuve mathématique que le code écrit correspond parfaitement aux spécifications préparées. La vérification garantit que le programme s'exécutera uniquement comme l'ont prévu les développeurs et qu'il ne contient pas certaines classes d'erreurs, telles que le débordement de tampon, le déréférencement de pointeurs, l'accès à des zones mémoire déjà libérées ou la libération double de blocs mémoire. Lors de la compilation, une vérification stricte des types et des valeurs est effectuée : un composant ne transmet jamais à un autre composant des paramètres qui ne correspondent pas aux spécifications et n'accède pas aux états internes d'autres composants.
Le processus de transition vers le code vérifié a duré deux ans et demi et a nécessité des améliorations de la bibliothèque HACL*, dont la fonctionnalité a été élargie avec les capacités nécessaires pour remplacer de manière transparente les fonctionnalités existantes de hashlib. Par exemple, le mode de fonctionnement HMAC en streaming a été ajouté à HACL*, ainsi que des modes supplémentaires pour les algorithmes Blake2, un nouvel API pour SHA3 couvrant toutes les variantes des algorithmes de la famille Keccak a été mis en œuvre, des mécanismes nécessaires pour notifier des erreurs (par exemple, en cas de problèmes d'allocation de mémoire) ont été fournis, et des scripts pour automatiser le transfert des nouvelles versions de HACL* vers le dépôt Python ont été développés.
Source : opennet.ru
