Python integriert die formal verifizierte Kryptografie-Bibliothek HACL*

Nach 2,5 Jahren Arbeit hat Python erfolgreich die formal verifizierte kryptografische Bibliothek HACL* in seine Hash- und HMAC-Implementierungen integriert. Dieses Update ersetzt die vorherige SHA3-Implementierung, die eine CVE-Schwachstelle enthielt, und umfasst verschiedene Algorithmen wie Blake2, SHA3 und HMAC, wodurch die Sicherheit von Python deutlich verbessert wird. Das Projekt meisterte die Herausforderungen bei der Implementierung von Streaming-APIs und dem Build-System und implementierte auch die Behandlung von Speicherzuweisungfehlern. Dies zeigt das Potenzial der formalen Verifikation in großen realen Projekten.