Ein fünfköpfiges Team und KI bewiesen den Code von Signal in vier Wochen

Vier Wochen. So lange brauchte ein fünfköpfiges Team von Google DeepMind, unterstützt von KI-Agenten, um maschinell geprüfte Beweise für wichtige Sicherheitseigenschaften im kompilierten Code der Signal-Chatbibliothek zu erstellen. Die Beweise umfassen rund 6,5 Millionen Zeilen. Frühere bahnbrechende Arbeiten an anderen Systemen erforderten jahrelange Spezialistenarbeit und meist neu geschriebenen Code, dessen Sicherheit bewiesen werden musste.

Der Forschungsbeitrag vom 10. November 2026 erläutert die Methode und ihre Grenzen. Die dazugehörige technische Abhandlung enthält detailliertere Angaben zu den Zahlen. Die vorliegende Arbeit ist kein Beweis für die Signal-App als Ganzes und auch kein Beweis für andere Apps mit einem ähnlichen Design. Sie beweist vielmehr spezifische Eigenschaften der Referenzbibliothek libsignal für Eins-zu-Eins-Sitzungen, bis hin zum kompilierten Maschinencode, der tatsächlich ausgeführt wird.

Was bewiesen wurde

libsignal ist die Bibliothek, die das Verschlüsselungsdesign von Signal implementiert. Vereinfacht ausgedrückt, soll dieses Design sicherstellen, dass eine Nachricht auch dann vertraulich bleibt, wenn der Schlüssel später gestohlen wird, und dass die Daten wiederhergestellt werden können, nachdem ein Gerät kurzzeitig kompromittiert wurde. Diese beiden Konzepte werden üblicherweise als Forward Secrecy und Post-Compromise Security bezeichnet.

Das Team kompilierte die unveränderte Bibliothek (Version 0.105.4) sowie die zugehörige SPQR-Crate (Version 1.6.0) mit dem Standard-Rust-Compiler zu einem kleinen Kommandozeilenprogramm für 64-Bit-Arm-Linux. Die Beweise beziehen sich auf diese ausführbare Datei, nicht auf eine überarbeitete Version. Die verifizierte Bibliothek ist etwa 560 KB groß, was ungefähr 140.000 Maschinenbefehlen entspricht.

Sie beschreiben den PQXDH-Handshake, mit dem zwei Personen eine private Sitzung starten. Dieser beinhaltet einen Post-Quanten-Schritt, der zukünftigen Quantencomputern standhalten soll, sowie die Triple-Ratchet-Verschlüsselung, die für jede Nachricht einen neuen Schlüssel generiert. Im “symbolischen” Modell, das die zugrundeliegende Kryptographie als ideal betrachtet, behauptet die Arbeit außerdem, dass der Handshake auch gegenüber einem späteren Angreifer mit einem Quantencomputer geheim bleibt. Gruppenchats, der versiegelte Absender und das serverseitige Protokoll werden in zukünftigen Arbeiten behandelt.

Wie die Arbeit erledigt wurde

Formale Verifikation bedeutet, eine präzise mathematische Aussage darüber zu formulieren, was der Code leisten muss, und anschließend zu beweisen, dass er diese Aussage erfüllt. Eine einzige fehlende Annahme kann das Ergebnis schwächen, daher müssen weiterhin die zu beweisenden Aspekte ausgewählt und die Aussage bestätigt werden.

Die Arbeit beschreibt die Aufteilung unmissverständlich. Menschen wählten die Eigenschaften aus, beseitigten Unklarheiten und gaben die Spezifikation frei. Anschließend erstellten Agenten die Beweise. Diese Beweise werden nur akzeptiert, wenn Lean, ein System zur Beweisprüfung, sie bestätigt. Die Zuverlässigkeit des Ergebnisses, so die Autoren, hängt nicht von der Zuverlässigkeit der beweisenden Agenten ab, da der Kern von Lean die Logik überprüft.

Der Forschungsbeitrag besagt, dass die Beweisagenten auf Gemini Carbon basierten. Die Beweisarbeit selbst wurde von fünf Forschern über vier Wochen hinweg durchgeführt, wobei jeder Agenten auf seiner eigenen Workstation ausführte. Für die Verhältnisse in diesem Bereich ist dies eine kurze Projektlaufzeit. Der Beitrag merkt an, dass der seL4-Mikrokernel, eine bekannte frühere Verifikationsmethode, zwanzig Personenjahre und der CompCert-C-Compiler sechs Personenjahre in Anspruch nahm. Beide Codebasen wurden mit Blick auf den Beweis entwickelt. libsignal hingegen nicht.

Wollen Sie, dass KI Ihnen wöchentlich Stunden spart? Unser kostenloses Handbuch zeigt Ihnen, wie.Holen Sie sich den kostenlosen Leitfaden →

Die Beweise selbst können umfangreich sein, da sie Maschinencode beschreiben. Sie umfassen etwa 6,5 Millionen Zeilen: 5,3 Millionen Zeilen betreffen den Binärcode, zuzüglich separater Dateien für die beiden Sicherheitsmodelle. Wer den Aussagen in der Überschrift vertrauen möchte, muss dennoch die vertrauenswürdigen Teile lesen: etwa 18.000 Zeilen Spezifikation im Repository, zuzüglich etwa 8.000 Zeilen des Arm-Maschinencodemodells und der auf die ausführbare Datei abgebildeten Symbolnamen. Die kryptografischen Routinen auf niedriger Ebene, zwei Ausgabefunktionen und einige Bibliotheksaufrufe werden vertraglich vorausgesetzt, nicht bewiesen.

Eine Überprüfung auf alte Fehler

Um zu testen, ob die Aussagen ausreichend streng waren, führte das Team zwei zuvor in libsignal gefundene und inzwischen behobene Fehler erneut ein. In beiden Fällen bewiesen sie, dass der Satz über symbolische Sicherheit für die fehlerhafte Binärdatei nicht gilt. Dies ist ein nützlicher Prüfmechanismus: Eine Spezifikation, die selbst bei bekanntem Fehlercode noch “erfolgreich” ist, wäre zu schwach.

Einer dieser Fehler speicherte den Zustand einer neuen Sitzung, einschließlich einer Kopie eines Geheimnisses, nachdem eine Vorab-Schlüsselnachricht nur in einer älteren Sitzung entschlüsselt werden konnte. Der andere akzeptierte einen Handshake, dessen Basisschlüssel manipuliert worden war, und erstellte so eine zweite Sitzung mit demselben gemeinsamen Geheimnis.

Was das Ergebnis nicht aussagt

Die Autoren gehen sorgfältig vor, und die Grenzen sind wichtig. Die Beweise decken nicht alle Aspekte von Signal, alle möglichen Angriffe oder die kryptografischen Primitiven selbst ab. Seitenkanalangriffe werden nicht berücksichtigt. Der rechnergestützte Beweis, der die Erfolgswahrscheinlichkeit eines realen Angreifers begrenzen soll, bietet keine Garantie gegen einen Quantenangreifer, und seine Grenze verliert bei mehreren langen Sitzungen mit vielen Runden ihre Gültigkeit.

Varianten desselben Protokolls werden in WhatsApp, Meta Messenger und Google Messages verwendet, wie in der Studie festgestellt wird. Diese Apps waren jedoch nicht Gegenstand des Beweises. Ein Beweis über libsignal lässt sich nicht automatisch auf jedes Produkt übertragen, das eine ähnliche Sprache verwendet.

Ehren Kret, Chief Technology Officer von Signal, wird in dem Forschungsbeitrag mit den Worten zitiert, dass die strenge Überprüfung der Protokollimplementierung “uns noch größeres Vertrauen in die Datenschutzgarantien unseres Codes gibt”.

Die Beweise und Spezifikationen werden in einem offenen Repository veröffentlicht.

Warum es wichtig ist

Die meisten Menschen, die eine private Nachricht versenden, bekommen die Bibliothek, die diese verschlüsselt, nie zu Gesicht. Eine Methode, die den kompilierten Code dieser Bibliothek innerhalb von Wochen statt Jahren überprüfen kann, stellt eine praktische Verbesserung der Softwareprüfung dar. Es handelt sich dabei nicht um ein Zertifikat, das die Fehlerfreiheit von Signal oder einer anderen Chat-App garantiert. Es ist vielmehr ein maschinell geprüftes Argument zu bestimmten Eigenschaften einer Kernbibliothek, das so schnell generiert wird, dass möglicherweise bald weiterer kritischer Code geprüft wird.

Die meisten alltäglichen Chatprodukte verfügen noch immer nicht über einen solchen Nachweis, und einige beliebte Tools verschlüsseln Nachrichten überhaupt nicht Ende-zu-Ende. In einem früheren Bericht wurde über ein Chat-Tool für Verbraucher berichtet, das Texte ohne diesen Schutz versendet.