“Formal verifiziert” wird zu einem Beschaffungskriterium für Post-Quanten-Kryptographie. Es bedeutet, dass der Code durch automatisierte Werkzeuge mathematisch als korrekt bewiesen wurde, nicht nur getestet. Für ML-KEM- und ML-DSA-Implementierungen, die in Produktionsumgebungen eingesetzt werden, ist es ein bedeutendes Unterscheidungsmerkmal. Es ist auch ein Ausdruck, der weniger abdecken kann, als er klingt.
Eine neue Arbeit des Kryptographen Nadim Kobeissi untersucht die Verifikations-Pipeline hinter Cryspens libcrux, einer der am weitesten verbreiteten PQ-Bibliotheken der Welt. Libcrux liefert die ML-KEM-Implementierung in Signals Post-Quanten-Ratchet. Google arbeitet mit Cryspen an FIPS-standardisiertem PQ-Code zusammen. Mozilla liefert es in Firefox aus. Das PQ Code Package der Linux Foundation enthält es.
Kobeissi fand strukturelle Lücken im Verifikationswerkzeug selbst. Code durchläuft den vollständigen Verifikationsprozess, erzeugt gültige Beweisartefakte und trägt dennoch Sicherheitseigenschaften, die die Beweise nie geprüft haben. Er nennt dies eine “Verifikationsfassade.” Die Verifikation fand statt. Sie deckte weniger ab, als man erwarten würde.
Was die Arbeit ergab
ML-KEM und ML-DSA basieren auf Rejection Sampling: Einen Kandidaten generieren, gegen eine Sicherheitsanforderung prüfen, wiederholen bis einer besteht. Diese Schleife macht ML-DSA-Signaturen zero-knowledge und die ML-KEM-Schlüsselgenerierung korrekt. Funktioniert sie nicht, werden private Schlüssel offengelegt.
Das Verifikationswerkzeug kann derzeit nichts über diese Schleifen beweisen. Eine fehlende Annotation bewirkt, dass die Pipeline stillschweigend einen Standardwert erzeugt, der die Schleife unprüfbar macht. Die Beweis-Engine meldet keinen Fehler. Sie meldet Erfolg, weil sie keinen Verstoß gefunden hat, aber nur weil sie nie tatsächlich geprüft hat. Die Beweisartefakte sehen gültig aus. Die Extraktion gelingt ohne Warnungen. Aber nichts hinter der Ausgabe deckt ab, was die Schleife erzeugt.
Kobeissi demonstrierte dies mit fünf Proof-of-Concept-Exploits gegen ML-KEM (FIPS 203), ML-DSA (FIPS 204), Ed25519 und ChaCha20. Jeder kompiliert, besteht Tests und erzeugt gültig aussehende Verifikationsausgabe, während er eine Sicherheitslücke trägt, die die Verifikation nicht erkennen kann. Er identifizierte auch zwei weitere Lückenklassen: Operationen, die die Beweis-Engine ungeprüft akzeptiert, und einen Annotationsmechanismus, der alle nachgelagerten Beweise bei Missbrauch vakuos wahr machen kann.
Was der Produktionscode zeigt
Die Arbeit verwendet vereinfachte Modelle. Wir haben das Produktions-Repository von libcrux untersucht, um zu prüfen, ob diese Lücken auf den ausgelieferten Code zutreffen. Das tun sie.
Die Annotation, die Rejection-Sampling-Schleifen verifizierbar machen würde, taucht nirgends in der libcrux-Codebasis auf. Sechs While-Schleifen in ML-KEM und ML-DSA, die alle Rejection Sampling oder Koeffizientengenerierung für FIPS 203 und FIPS 204 implementieren, werden ohne sie extrahiert.
Das Build-System geht weiter. Das Sampling-Modul von ML-KEM und sein IND-CPA-Verschlüsselungskern sind so konfiguriert, dass die Beweis-Prüfung komplett übersprungen wird. ML-DSA verwendet eine Whitelist von 28 verifizierten Modulen; das Signaturmodul, das die Rejection-Sampling-Schleife enthält, steht nicht darauf. Fünfundvierzig Module in der Codebasis haben ihre Beweise deaktiviert. Das gesamte ARM64-Backend (jedes iOS- und Android-Gerät) hat null geprüfte Beweise. Optimierten SIMD-Code zu verifizieren ist tatsächlich schwieriger als portable Implementierungen zu verifizieren, und die Branchenpraxis setzt oft auf das Testen optimierter Pfade gegen eine verifizierte Referenz. Aber die öffentlichen Aussagen unterschieden nicht zwischen Backends.
Als Cryspen im August 2024 ihre Google-Partnerschaft ankündigte, beschrieben sie die Implementierungen als “verifiziert als panic-frei, funktional korrekt und secret-independent.” Als Signal libcrux für SPQR im Oktober 2025 übernahm, zitierten sie die Verifikation als “hohen Grad an Sicherheit” bietend. Eine sorgfältigere Beschreibung dessen, was die Verifikation abdeckt, erschien vom Mitgründer von Cryspen im Februar 2026, in derselben Woche, in der Kobeissi dreizehn Bugs in der Bibliothek in einer Begleitarbeit offenlegte. Das waren keine abstrakten Verifikationslücken. Sie umfassten einen Endianness-Bug, der reale Entschlüsselungsfehler in Signals Post-Quanten-Ratchet verursachte, fehlende X25519-Validierung und FIPS-204-Spezifikationsverstöße. Vier der dreizehn lagen innerhalb der formal verifizierten Grenze.
Was das für PQ-Deployment bedeutet
Der Rust-Code ist korrekt. Die Rejection-Schleifen erzeugen richtige Ergebnisse. Die Arithmetik ist solide. Kobeissi ist diesbezüglich sorgfältig. Das Problem ist die Distanz zwischen dem, was “formal verifiziert” jemandem kommuniziert, der Implementierungen evaluiert, und dem, was die Verifikation tatsächlich nachweist.
Jedes Verifikationswerkzeug hat Grenzen. CompCert verifiziert nicht den Linker. seL4 verifiziert nicht die Hardware. Die Frage ist nicht, ob Grenzen existieren. Die Frage ist, ob sie für die Entscheidungsträger beim Deployment sichtbar sind.
Organisationen, die ihre eigene PQ-Aufstellung mit [PQ]probe scannen, fragen bereits, was ihre Infrastruktur tatsächlich aushandelt im Vergleich zu dem, was Anbieter behaupten. Dieselbe Disziplin gilt für Implementierungssicherheit. “Formal verifiziert” ist eine Aussage über ein Modell. Wie viel des eingesetzten Codes dieses Modell abdeckt, ist eine beantwortbare Frage.
Wenn die Antwort das Lesen eines Makefiles erfordert, liest sich die Sicherheitsaussage eher wie aspiratives Marketing als tatsächliche Ingenieursarbeit.