DeepMind: KI beweist Sicherheit von Signals Verschlüsselungscode

Google DeepMind hat mit dem neuen System AlphaProof Code zentrale Sicherheitseigenschaften der Signal-Verschlüsselung formal verifiziert, also mathematisch bewiesen. Das Besondere: Der Beweis gilt nicht für das Design des Protokolls, sondern für den kompilierten Code der Bibliothek libsignal. DeepMind hat die Arbeit am 10. November 2026 veröffentlicht. Der Umfang ist gross, die Grenzen sind es auch.

6,5 Millionen Zeilen Beweis in vier Wochen

Laut DeepMind übersetzten Forschende die Sicherheitsziele von Signal zusammen mit KI-Modellen in formale Aussagen, jede davon von Fachleuten geprüft. Danach schrieben Agenten auf Basis von Gemini Carbon die Beweise in Lean, einer Sprache, in der ein Programm jeden Beweisschritt automatisch prüft. Das Paper im Repository nennt rund 6,5 Millionen Zeilen. Der Blogbeitrag spricht von «über sechs Millionen».

Bewiesen wurden unter anderem Vorwärtsgeheimnis (alte Nachrichten bleiben geschützt, wenn später ein Schlüssel auffliegt), Authentifizierung und Schutz nach einer vorübergehenden Kompromittierung. Dauer: vier Wochen. Das dauere bei Expertenteams «historisch» Jahre, schreibt DeepMind. Die Agenten markierten rund ein Prozent des Codes für einen zweiten menschlichen Blick.

Zwei alte Fehler als Gegenprobe

Um zu zeigen, dass das System echten von fehlerhaftem Code unterscheidet, baute DeepMind zwei früher behobene Signal-Bugs wieder ein. In beiden Fällen erzeugte das System einen maschinell geprüften Beweis, dass die Version unsicher ist. In den untersuchten Teilen fand es laut Wired keine neuen Schwachstellen. Einen Vorsprung hatte das Team zudem durch frühere Verifikationsarbeiten der Signal Foundation.