In Python wurden kryptografische Funktionen mit mathematischer Zuverlässigkeitsnachweis implementiert.

Die erfolgreiche Beendigung der Initiative zur Ersetzung der Implementierungen kryptografischer Algorithmen in Python, die in den Modulen hashlib und hmac angeboten werden, durch Varianten mit mathematischer Sicherheitsgarantie, die vom Projekt „HACL*“ bereitgestellt wurden, wurde angekündigt. Die Arbeit an der Umstellung auf Funktionen mit mathematischer Sicherheitsgarantie begann im Jahr 2022 und wurde nach der Feststellung einer Buffer-Overflow-Schwachstelle in der Implementierung des SHA3-Algorithmus, der im Python-Modul hashlib verwendet wird, initiiert.

In das Hauptrepository des CPython-Projekts wurde der Code mit neuen Implementierungen kryptografischer Hash-Funktionen und HMAC-Algorithmen (Mechanismus zur Überprüfung der Nachrichtenintegrität) aufgenommen. Alle standardmäßig in Python bereitgestellten Hash-Funktionen und HMACs wurden durch verifizierte 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 Bestandteil der Herbstversion von Python 3.14 sein wird.

Neue Implementierungen kryptografischer Funktionen wurden aus der HACL*-Bibliothek übernommen, die von Forschern des französischen Nationalen Instituts für Informatik und Automatisierung (INRIA), dem Microsoft Research-Unternehmen und der Carnegie Mellon University entwickelt wird. Die HACL*-Bibliothek unterstützt alle erforderlichen kryptografischen Funktionen für die Arbeit mit TLS 1.3 und eine vollständige Unterstützung der NaCl API (Networking and Cryptography library), wie Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC und HKDF. In Bezug auf die Leistung liegt die HACL*-Bibliothek nahe an OpenSSL, bietet jedoch im Gegensatz zu letzterem zusätzliche Sicherheits- und Zuverlässigkeitsgarantien.

Der HACL*-Code ist in einer Teilmenge der funktionalen Sprache F* geschrieben, die ein System abhängiger Typen und Spezifikationen bietet, das es ermöglicht, präzise Spezifikationen (mathematische Modelle) zu definieren und das Fehlen von Fehlern in der Implementierung durch SMT-Formeln und unterstützende Nachweiswerkzeuge zu garantieren. Der Referenzcode in F* wird mithilfe des Compilers KaRaMeL in C-Code übersetzt und steht zur Integration in andere Projekte zur Verfügung.

Die Durchführung der Verifizierung umfasst die Festlegung detaillierter Spezifikationen, die alle Verhaltensvarianten 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 beabsichtigt haben, und dass bestimmte Klassen von Fehlern, wie Pufferüberlauf, Dereferenzierung von Zeigern, Zugriff auf bereits freigegebene Speicherbereiche oder doppelte Freigabe von Speicherblöcken, nicht auftreten. Während des Kompilierungsprozesses wird eine strenge Überprüfung von Typen und Werten sichergestellt – eine Komponente wird niemals einer anderen Komponente Parameter übergeben, die nicht der Spezifikation entsprechen, und erhält keinen Zugriff auf die internen Zustände anderer Komponenten.

Der Prozess der Migration zu verifiziertem Code dauerte zweieinhalb Jahre und erforderte Anpassungen der HACL*-Bibliothek, deren Funktionalität durch die erforderlichen Funktionen für den nahtlosen Austausch der bestehenden hashlib-Funktionalität erweitert wurde. Beispielsweise wurde in HACL* die Unterstützung für den Stream-Modus von HMAC hinzugefügt, zusätzliche Betriebsmodi für die Blake2-Algorithmen bereitgestellt, eine neue API für SHA3 entwickelt, die alle Varianten der Keccak-Familie abdeckt, notwendige Mittel zur Fehlerbenachrichtigung (z. B. bei Speicherproblemen) bereitgestellt und Skripte zur Automatisierung der Übertragung neuer Versionen von HACL* in das Python-Repository entwickelt.

Quelle: opennet.ru