- Die standardmäßigen Hash- und HMAC-Algorithmen von Python wurden nun durch verifizierten Kryptografie-Code aus HACL* ersetzt
- Rund 15.000 Zeilen C-Code wurden automatisch aus HACL* in die Python-Codebasis integriert
- Eine Streaming-API wurde allgemein entworfen und verifiziert, damit sich verschiedene Blockalgorithmen verarbeiten lassen
- Aufwändige Engineering-Themen wie Behandlung fehlgeschlagener Speicherallokation, Lösung von AVX2-Kompilierungsproblemen und Optimierung der CI-Umgebung wurden adressiert
- Durch die Zusammenarbeit der Python- und Kryptografie-Community wurden praktische Sicherheit und Wartbarkeit zugleich erreicht
Einführung vollständig verifizierten Codes für Kryptografie-Algorithmen in Python
- Nach CVE-2022-37454 im Zusammenhang mit der SHA3-Implementierung aus dem Jahr 2022 kam die Frage auf, die Hash-Infrastruktur von Python auf verifizierten Code umzustellen
- In den folgenden zweieinhalb Jahren ersetzte Python die eingebauten Hash- und HMAC-Algorithmen vollständig durch verifizierte Implementierungen auf Basis von HACL*
- Dieser Austausch erfolgte vollständig transparent für die Nutzer, ohne Funktionsverluste
- HACL* implementierte zusätzlich Funktionen für Python: verschiedene Blake2-Modi, eine API zur Unterstützung von Keccak-Varianten bei SHA3 und Streaming-Optimierungen für HMAC
- Die Übernahme neuer Versionen ist über Skripte automatisiert und dadurch leicht wartbar
Die Streaming-API verstehen
- Die meisten Kryptografie-Algorithmen sind Blockalgorithmen, bei denen Eingaben blockweise verarbeitet werden müssen
- In realen Einsatzumgebungen ist eine blockweise Eingabe oft unpraktisch, daher wird eine Streaming-API benötigt
- Eine Streaming-API arbeitet unabhängig von der Eingabelänge und erlaubt auch das Auslesen von Zwischenergebnissen
- Streaming-Implementierungen erfordern komplexes Zustandsmanagement; in der früheren SHA3-Implementierung gab es dazu einen schwerwiegenden Sicherheitsfehler
- Jeder Hash-Algorithmus verarbeitet Daten anders, was die Komplexität erhöht: z. B. erlaubt Blake2 keine leeren Blöcke, HMAC kann Schlüssel nach der Initialisierung löschen usw.
Verifizierung eines allgemeinen Streaming-Algorithmus
- Ein in einer 2021 veröffentlichten Arbeit vorgestellter Ansatz abstrahiert Blockalgorithmen und definiert darauf einen allgemeinen Streaming-Algorithmus
- Anschließend lässt sich dieser wie ein Template auf einzelne Algorithmen anwenden und wiederverwenden
- Er wurde so verallgemeinert, dass alle Sonderfälle abgedeckt sind:
- Ob sich die Ausgabelänge festlegen lässt (SHA3 vs. Shake)
- Ob vor der Verarbeitung eine Eingabe erforderlich ist (z. B. der Schlüsselblock bei Blake2)
- Unterschiede bei der Verarbeitung des letzten Blocks
- Zusätzliche Informationen, die im internen Zustand erhalten bleiben müssen
- Wie Zustände für das Auslesen von Zwischenergebnissen kopiert werden (stack vs. heap)
- Strategie zwischen individueller API pro Algorithmus und einer Family-API
Build-Stabilität für die Python-Integration sicherstellen
- Die CI von Python prüft gegen mehr als 50 Toolchains und Architekturen, wodurch selbst kleine Probleme sichtbar werden
- Bei der HMAC-Implementierung trat ein Problem mit der Unterstützung von AVX2-Instruktionen auf:
- Einige Compiler können den Header
immintrin.h ohne AVX2 nicht verarbeiten
- Dies wurde durch Nutzung des Musters abstrakter Strukturen in C gelöst
- Wegen des Unterschieds zwischen dem Abstraktionskonzept in von F* erzeugtem C-Code und C-Strukturen musste dem Compiler
krml eine präzise Sichtbarkeitsanalyse hinzugefügt werden
Umgang mit fehlgeschlagener Speicherallokation
- Das bisherige F*-Modell konnte Speicherfehler theoretisch modellieren, praktisch eingesetzt wurde das jedoch erstmals hier
- Entsprechend den Anforderungen von Python wurden Zustandsstrukturen, Algorithmusdefinitionen und Streaming-Strukturen so verbessert, dass sie Allokationsfehler propagieren können
- In F* wird dafür der Typ
option verwendet, der in C als tagged union kompiliert wird
- Künftig könnte dies zur Verringerung der Komplexität auf einen Runtime-Fehler-Flag-Ansatz umgestellt werden
Automatisierung von HACL*-Code-Updates
- Der anfängliche Python-PR nutzte
sed, um unnötige Header-Definitionen zu entfernen und Pfade anzupassen
- Nachdem sich die Stabilität des HACL*-Codes bestätigt hatte, wurde das komplexe
sed entfernt und durch ein einfaches Skript ersetzt
- Mit diesem Skript kann jeder den HACL*-Code im Python-Quellbaum einfach auf die neueste Version aktualisieren
Fazit
- Verifizierter Kryptografie-Code wurde erfolgreich in Python als repräsentative Produktionsumgebung integriert
- Das ist ein Beleg dafür, dass diese Technologie nicht nur über das akademische Forschungsstadium hinaus ist, sondern auch in realer Software praktisch und wartbar eingesetzt werden kann
- Es ist ein gutes Beispiel für die Zusammenarbeit zwischen der Python-Community und den HACL*-Entwicklern und könnte künftig auch andere Projekte beeinflussen
2 Kommentare
Wie auch in den Hacker-News-Kommentaren erwähnt wurde, ist schwer zu verstehen, was genau das Python-Ökosystem erreicht haben soll, das „über die Phase akademischer Forschung hinaus auch in echter Software praktisch und wartbar“ sei.
Wenn eigentlich gemeint war, dass daran gearbeitet wurde, Streaming-Algorithmen über eine bestehende, nicht verifizierte Hash-Infrastruktur zu abstrahieren, dann ist das wohl nur ein weiteres „pythonic“ Wortspiel.
Hacker-News-Kommentare
Die Python-Version ist nicht angegeben. Nach Recherche soll diese Funktion in Version 3.14 enthalten sein. Vor Oktober wird man sie wohl nicht sehen.
Sie haben die verifizierte C-Bibliothek, die in Microsofts F* erzeugt wurde, in CPython aufgenommen und eine C-Erweiterung geschrieben.
Ich frage mich, ob Unterstützung für „Streaming“-Ausgabe von SHAKE übernommen wird.
Moderne, weit verbreitete Kryptografie ist praktisch nicht zu brechen, und die Crypto Wars der 90er wirken inzwischen etwas überholt. Ich frage mich, welche Gedanken es zu den gesellschaftlichen Auswirkungen davon gibt.
Ich frage mich, wie gut ein allgemeines Streaming-Verifikations-Framework über kryptografische Hashes hinaus wiederverwendbar ist.
Ich frage mich, ob alles, was das Krypto-Modul importiert, G++ oder etwas Ähnliches mitbringen muss, oder ob es direkt in CPython selbst kompiliert wird.
Ich kenne mich mit Kryptografie nicht gut aus. Ich frage mich, was das für Python bedeutet.
Ich frage mich, welcher Anteil der Entwicklung verifiziert wurde und was genau das umfasst.
Codezeilen sind ein sehr ungeeignetes Maß. Besonders im Kontext von Kryptografie-Code gilt das umso mehr, wenn mit großen Zahlen geprahlt wird.