Rund 6,5 Millionen Zeilen Beweistext, geschrieben von KI-Agenten, geprüft von einem kleinen, unbestechlichen Programm: Google DeepMind hat am 10. November 2026 eine Arbeit veröffentlicht, die zentrale Sicherheitsversprechen des Signal-Protokolls formal verifiziert – und zwar nicht für eine Skizze des Protokolls auf dem Papier, sondern für den übersetzten Maschinencode der Bibliothek libsignal. Das Werkzeug dahinter heißt AlphaProof Code. Die Arbeit ist ein Meilenstein, aber sie beweist deutlich weniger, als die Kurzformel „Signal ist mathematisch bewiesen“ nahelegt.

Formale Verifikation: mehr als ein sehr gründlicher Test

Ein Test probiert Fälle aus. Selbst Millionen von Testläufen zeigen nur, dass in genau diesen Läufen nichts schiefging. Formale Verifikation dreht das um: Man beschreibt in der Sprache der Mathematik, was ein Programm leisten soll (die Spezifikation), und beweist dann, dass das Programm diese Aussage für alle möglichen Eingaben und Abläufe erfüllt. Den Beweis prüft kein Mensch Zeile für Zeile, sondern ein Beweisprüfer – hier der Kern des Beweisassistenten Lean. Akzeptiert er den Beweis, gilt die Aussage, gleichgültig, wer oder was ihn geschrieben hat.

Genau diese Eigenschaft macht das Verfahren für KI interessant: Ein Sprachmodell darf sich beim Beweisen beliebig oft irren, solange am Ende ein Beweis steht, den Lean annimmt. Vertrauen muss man dafür nicht dem Modell, sondern dem, was nicht bewiesen, sondern vorausgesetzt wird – und der Frage, ob die Spezifikation wirklich das beschreibt, was man meint. Bisher scheiterte der breite Einsatz am Aufwand: Die Verifikation des Betriebssystemkerns seL4 kostete rund 20 Personenjahre, wie The Register in seinem Bericht zur DeepMind-Arbeit in Erinnerung ruft.

Was genau bewiesen wurde

Untersucht wurde ein kleines Kommandozeilenprogramm, das gegen die unveränderte Rust-Bibliothek libsignal in Version 0.105.4 und die Bibliothek SPQR in Version 1.6.0 gelinkt ist, übersetzt mit dem normalen Rust-Compiler zu einem AArch64-Programm für Linux. Verifiziert sind drei Operationen einer Unterhaltung zwischen zwei Teilnehmern: der Sitzungsaufbau mit dem quantenresistenten Schlüsselaustausch PQXDH sowie das Senden und das Empfangen von Nachrichten. Laut Fachartikel sind das rund 560 KByte Code oder etwa 140.000 Maschinenbefehle.

Dafür liegen zwei voneinander unabhängige Beweise vor. Der erste arbeitet im symbolischen Modell, in dem ein Angreifer das gesamte Netz kontrolliert, die Kryptografie selbst aber als perfekt gilt. Er zeigt unter anderem:

  • Forward Secrecy: Wer später Schlüssel erbeutet, kann frühere Nachrichten nicht entschlüsseln.
  • Post-Compromise Security: Nach einem vorübergehenden Einbruch in ein Gerät erholt sich die Sitzung wieder.
  • Authentizität: Nachrichten stammen vom erwarteten Gegenüber, auch wenn der eigene Langzeitschlüssel bekannt geworden ist.
  • Schutz gegen das Mitschneiden jetzt und Entschlüsseln später („harvest now, decrypt later“) sowie die Unabhängigkeit einzelner Sitzungen.

Der zweite Beweis ist rechnerischer Natur: Er liefert eine konkrete Obergrenze für die Erfolgswahrscheinlichkeit eines Angreifers – unter üblichen kryptografischen Annahmen und nur für klassische, nicht für Quantencomputer. Hinzu kommt eine Robustheitsaussage: Gültige Aufrufe enden regulär oder mit einem kontrollierten Abbruch, das Programm läuft nie in einen Speicherfehler oder eine Endlosschleife.

Dass der Beweis beim Maschinencode ansetzt, hat einen handfesten Vorteil: Dem Compiler muss man nicht vertrauen. Fehler, die erst beim Übersetzen entstehen, wären mit erfasst.

Bildschirmfoto der Signal-App für Android: Ansicht „Sicherheitsnummer verifizieren“ mit QR-Code und Zahlenblöcken

Sicherheitsnummer in der Signal-App für Android: Mit ihr gleichen zwei Gesprächspartner ihre Schlüssel ab. Bild: ShreyasMinocha / Wikimedia Commons, CC0

Welche Rolle die KI spielte

AlphaProof Code ist nach DeepMinds Beschreibung ein Verbund aus Agenten mit festen Rollen. Ein Agent entwirft unter Anleitung von Menschen die Spezifikation, andere kritisieren sie. Ein Orchestrator verteilt die Beweisarbeit an Teams; ein „Gatekeeper“ lässt nur gelten, was der Lean-Kern gegen eine zurückgehaltene Kopie der Spezifikation akzeptiert. Pro Kampagne arbeiteten 40 bis 80 Agenten 24 bis 72 Stunden lang auf einer Maschine.

Die Beweise stammen laut Fachartikel vollständig von Agenten auf Basis von Gemini 4 Carbon. Für die Spezifikationen kamen Gemini 4 Carbon und Claude Opus 5.5 von Anthropic zum Einsatz, wobei jeweils ein Modell der anderen Familie den Entwurf begutachtete. Fünf Menschen arbeiteten vier Wochen an dem Projekt; keiner von ihnen schrieb Beweiscode. Ihre Aufgabe war eine andere: festlegen, was bewiesen werden soll, Mehrdeutigkeiten klären, Spezifikationen und deren Änderungen freigeben. Laut DeepMinds Blog markierten die Agenten etwa ein Prozent der Codebasis zur erneuten Durchsicht durch Menschen.

Vertraut werden muss am Ende rund 26.000 Zeilen: den Definitionen und Aussagen der Spezifikation sowie einem formalen Modell des AArch64-Befehlssatzes und des Linux-Prozessstarts. Dieses Maschinenmodell ist selbst nicht bewiesen, sondern durch Vergleichsläufe gegen das echte Programm abgesichert.

Keine neuen Lücken, zwei alte wiedergefunden

Neue Schwachstellen in libsignal hat die Arbeit nicht zutage gefördert. Um zu zeigen, dass die Spezifikation trotzdem Zähne hat, baute das Team zwei längst behobene Fehler wieder in eine isolierte Kopie ein: einen Fall, in dem beim Entschlüsseln einer ersten Nachricht ein unbestätigter Sitzungszustand gespeichert wurde, und eine fehlende Prüfung eines öffentlichen Schlüssels beim Sitzungsaufbau. Für beide Varianten entstanden maschinengeprüfte Gegenbeweise – der fehlerhafte Code verletzt nachweislich die symbolischen Sicherheitsaussagen.

Was ausdrücklich nicht bewiesen ist

Der Fachartikel listet die Grenzen selbst auf, und sie sind erheblich:

  • Nicht die Apps: Bewiesen ist ein Kommandozeilenprogramm, das frisch startet. Auf Signal für Android und iOS lassen sich die Aussagen nur übertragen, soweit deren Umgebung das Verhalten des Protokollcodes erhält.
  • Nicht die Kryptobausteine: 37 Routinen – also Verfahren wie AES, HMAC oder die Kurvenarithmetik – sind durch Verträge ersetzt. Dass ihre Implementierung korrekt ist, wird vorausgesetzt.
  • Keine Seitenkanäle: Angriffe über Laufzeiten, Stromverbrauch oder Speicherreste liegen außerhalb des Modells.
  • Keine Schlüsselerzeugung: Die Theoreme nehmen die Schlüssel als gegeben an. Der Zufallsgenerator muss funktionieren.
  • Keine Gruppen, keine Metadaten: Gruppenchats, mehrere Geräte pro Konto, „Sealed Sender“ und alles, was auf den Servern geschieht, nennen die Autoren als künftige Arbeit.
  • Kein Quantenangreifer: Die zusätzliche Absicherung durch SPQR gegen künftige Quantencomputer ist nicht Teil der bewiesenen Aussagen.
  • Nur diese Version: Der Beweis gilt für genau dieses Programm. Ein neuer Build braucht laut den Autoren einen neuen Verfeinerungsbeweis, der Sicherheitsbeweis darüber bleibt bestehen.

„Mathematisch bewiesen“ heißt hier also: Für dieses Programm und diese Operationen gelten die genannten Eigenschaften – unter den aufgeführten Annahmen.

Reaktion von Signal und Einordnung

Signal war an der Arbeit beteiligt: Die Autoren danken Rolfe Schmidt, Michael Rosenberg und Ehren Kret für Rückmeldungen zu den Spezifikationen. Technikchef Ehren Kret wird von DeepMind mit den Worten zitiert, es sei ein großer Durchbruch, mit KI-Agenten laufenden Code in gültige Lean-Theoreme zu übersetzen (aus dem Englischen übersetzt). Frühere formale Verifikation habe sich auf kleinere Teile des Codes konzentriert, der neue Ansatz erlaube eine deutliche Ausweitung.

Für dich als Signal-Nutzer ändert sich nichts, und zu tun gibt es auch nichts: Es wurde kein Fehler gefunden und kein Update ausgelöst. Der Wert liegt woanders. Erstens ist es eine weitere, unabhängige Bestätigung für ein Protokoll, das neben Signal auch in Google Messages und nach Angaben von Wired in WhatsApp steckt. Zweitens zeigt die Arbeit, dass sich der Engpass verschiebt: vom Beweisen zum Spezifizieren. Wer festlegt, was „sicher“ bedeutet, bestimmt, was der Beweis wert ist.

Offen bleibt, ob das Verfahren im Alltag bezahlbar ist. Google hat laut Wired die Kosten der Analyse nicht genannt und sich nicht dazu geäußert, ob daraus ein Produkt wird. Spezifikationen und Beweise sind auf GitHub veröffentlicht; wer nachprüfen will, braucht laut Projektbeschreibung mehrere Stunden Rechenzeit und 15 bis 34 GiB Arbeitsspeicher. Unabhängig davon läuft seit April 2026 mit „Signal Shot“ ein offenes Projekt der Beneficial AI Foundation, des Lean-Teams und von Signal mit dem weiter gesteckten Ziel, Protokoll und Implementierung in Lean zu verifizieren.

Quellen

Bildnachweis