Python intègre la bibliothèque cryptographique formellement vérifiée HACL*

Après 2,5 ans de travail, Python a intégré avec succès la bibliothèque cryptographique formellement vérifiée HACL* dans ses implémentations de hachage et HMAC. Cette mise à jour remplace l'implémentation précédente de SHA3, qui contenait une vulnérabilité CVE, et couvre plusieurs algorithmes, notamment Blake2, SHA3 et HMAC, améliorant ainsi considérablement la sécurité de Python. Le projet a surmonté les défis liés à la mise en œuvre des API de streaming et à la construction du système, et a également implémenté la gestion des échecs d'allocation de mémoire. Cela démontre le potentiel de la vérification formelle dans les projets du monde réel à grande échelle.