Es wurde bekannt gegeben, dass die Initiative zur Ersetzung der in Python verwendeten Implementierungen kryptografischer Algorithmen in den Modulen hashlib und hmac durch Varianten mit mathematischem Sicherheitsnachweis, die vom Projekt âHACL*â vorbereitet wurden, erfolgreich abgeschlossen wurde. Die Umstellung auf Funktionen mit mathematischem Sicherheitsnachweis wurde 2022 initiiert und folgte der Entdeckung eines Buffer Overflows in der Implementierung des SHA3-Algorithmus, der im Python-Modul hashlib verwendet wird.
Der Hauptrepository des CPython-Projekts hat Code mit neuen Implementierungen kryptografischer Hash-Funktionen und HMAC-Algorithmen (Mechanismus zur Nachrichtenauthentifizierung) angenommen. Alle standardmĂ€Ăig in Python bereitgestellten Hash-Funktionen und HMACs wurden durch verifiziert Varianten ersetzt. Unter anderem wurde eine Implementierung von HMAC-BLAKE2 hinzugefĂŒgt, die SIMD-Befehle AVX2 zur Beschleunigung der Berechnungen nutzt. Es wird erwartet, dass der verifizierte Code Teil des Herbst-Release von Python 3.14 wird.
Die neuen Implementierungen der kryptografischen Funktionen wurden aus der HACL*-Bibliothek ĂŒbertragen, die von Forschern des französischen Nationalen Instituts fĂŒr Informatik und Automatik (INRIA), einer Abteilung von Microsoft Research, und der Carnegie Mellon University entwickelt wird. Die HACL*-Bibliothek unterstĂŒtzt gĂ€ngige kryptografische Funktionen, die fĂŒr den Betrieb von TLS 1.3 und die vollstĂ€ndige UnterstĂŒtzung der NaCl-API (Networking and Cryptography library) erforderlich sind, wie Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC und HKDF. In Bezug auf die Leistung liegt die HACL*-Bibliothek nahe bei OpenSSL, bietet jedoch im Gegensatz zu letzterem zusĂ€tzliche Garantien fĂŒr ZuverlĂ€ssigkeit und Sicherheit.
Der HACL*-Code ist in einer Teilmenge der funktionalen Sprache F* geschrieben, die ein System abhĂ€ngiger Typen und Verfeinerungen bietet, um prĂ€zise Spezifikationen (mathematische Modelle) zu definieren und die Fehlerfreiheit der Implementierung mithilfe von SMT-Formeln und unterstĂŒtzenden Beweiswerkzeugen zu garantieren. Der Referenzcode in F* wird mit dem Compiler KaRaMeL in C-Code ĂŒbersetzt und ist fĂŒr die Integration in andere Projekte verfĂŒgbar.
Die DurchfĂŒhrung der Verifizierung umfasst die Festlegung detaillierter Spezifikationen, die alle Verhaltensweisen des Programms beschreiben, sowie die Erstellung eines mathematischen Nachweises, dass der geschriebene Code vollstĂ€ndig mit den erstellten Spezifikationen ĂŒbereinstimmt. Die Verifizierung garantiert, dass das Programm nur so ausgefĂŒhrt wird, wie es die Entwickler vorgesehen haben, und dass bestimmte Klassen von Fehlern, wie PufferĂŒberlĂ€ufe, Dereferenzierung von Zeigern, der Zugriff auf bereits freigegebene Speicherbereiche oder die doppelte Freigabe von Speicherblöcken, nicht vorkommen. WĂ€hrend des Kompilierungsprozesses wird eine strenge Typ- und WerteĂŒberprĂŒfung sichergestellt â ein Komponent wird niemals einem anderen Komponent Parameter ĂŒbergeben, die nicht den Spezifikationen entsprechen, und erhĂ€lt keinen Zugriff auf interne ZustĂ€nde anderer Komponenten.
Der Prozess der Umstellung auf den verifiziertem Code dauerte zweieinhalb Jahre und erforderte Anpassungen der HACL*-Bibliothek, deren FunktionalitĂ€t um die notwendigen Möglichkeiten fĂŒr den nahtlosen Ersatz der bestehenden FunktionalitĂ€t von hashlib erweitert wurde. Beispielsweise wurde in HACL* die UnterstĂŒtzung fĂŒr den Streaming-Modus von HMAC hinzugefĂŒgt, zusĂ€tzliche Betriebsmodi der Blake2-Algorithmen bereitgestellt, eine neue API fĂŒr SHA3 implementiert, die alle Varianten der Keccak-Familie abdeckt, und die nötigen Mittel zur Fehlerbenachrichtigung (z. B. bei Problemen mit der Speicherzuweisung) sichergestellt sowie Skripte zur Automatisierung der Ăbertragung neuer Versionen von HACL* in das Python-Repository entwickelt.
Quelle: opennet.ru
