Eine private Nachricht soll auch dann vertraulich bleiben, wenn der Weg durchs Internet öffentlich ist. Google DeepMind hat nun untersucht, ob ein zentraler Teil der dafür verwendeten Signal-Technik seine festgelegten Sicherheitsversprechen tatsächlich einhält. Das Team nutzte KI-Agenten, um mathematische Beweise für Eigenschaften des ausgeführten Programmcodes zu erstellen.
Das Ergebnis betrifft die Referenzimplementierung libsignal und einen bestimmten Maschinenbefehlssatz. Es ist keine Prüfung aller Funktionen einer Messenger-App. Die Ankündigung vom 10. November und die zugehörige Forschungsarbeit beschreiben, wie Menschen und KI die Aufgabe aufteilten.
Von der Sicherheitsregel zum Beweis
Signal ist der Name eines Messengers und eines kryptografischen Protokolls. Dieses Protokoll legt fest, wie Geräte Schlüssel austauschen und Nachrichten schützen. Ein Entwurf kann sicher aussehen und trotzdem beim Übersetzen in ausführbaren Code Fehler enthalten. Genau diese Lücke zwischen Regel und tatsächlichem Programm interessiert die Forschenden.
Ein gewöhnlicher Test probiert konkrete Fälle aus. Eine formale Verifikation beginnt dagegen mit einer präzisen Beschreibung der gewünschten Eigenschaft und ihrer Voraussetzungen. Danach wird mathematisch gezeigt, dass der untersuchte Code diese Eigenschaft unter den festgelegten Bedingungen erfüllt. Der Beweis steht und fällt damit, ob die formulierte Regel wirklich das beschreibt, was geschützt werden soll.
Bei AlphaProof Code formulierten Forschende gemeinsam mit KI-Agenten solche Regeln, sogenannte Spezifikationen, und prüften sie selbst. Weitere Agenten erzeugten anschließend die Beweise. Das Programm Lean kontrollierte deren logische Schritte. Es muss also nicht darauf vertraut werden, dass die KI von sich aus immer richtig argumentiert.
Welche Teile untersucht wurden
Die Forschungsarbeit nennt den Schlüsselaustausch PQXDH und den Triple Ratchet. Vereinfacht sorgt der erste für den Aufbau gemeinsamer Geheimnisse; der zweite erneuert Schlüssel im Verlauf einer Unterhaltung. Das Team untersuchte unter anderem Vertraulichkeit und Authentizität von Nachrichten sowie Schutz vor und nach einer zeitweisen Kompromittierung von Schlüsseln.
Ein Beispiel für die Bedeutung solcher Eigenschaften: Wenn ein Schlüssel später in falsche Hände gerät, sollen dadurch nicht automatisch frühere Nachrichten lesbar werden. Ein anderes Ziel ist, dass Kommunikation nach einer vorübergehenden Kompromittierung unter den beschriebenen Voraussetzungen wieder geschützt sein kann. Welche Aussagen gelten, hängt jeweils von den Annahmen des Modells ab.
Für die Untersuchung wurde unveränderter libsignal-Code in ein kleines Kommandozeilenprogramm eingebunden und für AArch64 unter Linux übersetzt. Die Arbeit beschreibt rund 6,5 Millionen Zeilen maschinengeprüften Lean-Beweiscode. Weitere rund 26.000 Zeilen Spezifikation und Maschinenmodell gehören zu den Grundlagen, denen die Aussage vertraut. Als Plausibilitätsprobe führte das Team zwei bereits behobene Fehler in isolierten Fassungen wieder ein und zeigte, dass diese gegen die entsprechenden Eigenschaften verstoßen.
Was der Nachweis offenlässt
Lean prüft, ob ein Beweis zur formalen Aussage passt. Es entscheidet nicht selbst, ob die Menschen alle wichtigen Sicherheitsziele richtig erfasst haben. Die Forschenden nennen außerdem Annahmen über kryptografische Grundbausteine und Schnittstellen außerhalb des überprüften Bereichs. Ein Fehler in diesen Grundlagen oder eine zu schwache Spezifikation kann die Aussage einschränken.
Auch ein mathematischer Nachweis dieses Codeausschnitts schützt ein entsperrtes oder kompromittiertes Gerät nicht automatisch. Das Ergebnis ist daher am besten als überprüfbarer Baustein zu verstehen: Es verbindet ausgewählte Sicherheitsziele mit einer konkreten Implementierung, während andere Teile eines Nachrichtendienstes eigene Prüfungen benötigen. Google hat die Verifikationsartefakte zur weiteren Verwendung veröffentlicht.
Quellen
- Google DeepMind: Introducing AlphaProof Code, 10. November 2026.
- Chaudhuri und weitere: AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level, 10. November 2026.
- Google DeepMind: Verifikationsartefakte.
Für diesen Artikel wurden KI-gestützte Recherche- und Editierwerkzeuge verwendet. Der Inhalt wurde redaktionell geprüft.
