Google DeepMind verifiziert das Signal-Protokoll formal mit KI

Forscher von Google DeepMind haben mit einem agentischen KI-Framework namens AlphaProof Code mehrere zentrale kryptografische Garantien des Signal-Protokolls mathematisch bewiesen, wie Wired berichtet. Die Arbeit, ein in vier Wochen abgeschlossener Machbarkeitsnachweis, ist ein Beispiel für formale Verifikation: ein Verfahren, das mit Mathematik prüft, ob Software wie vorgesehen funktioniert, statt nur Stichproben zu testen.

Das Signal-Protokoll ist das Verschlüsselungsverfahren hinter der Signal-App und schützt, wie Wired anmerkt, auch die Kommunikation in Google Messages und WhatsApp. Die Analyse gilt daher als weitere unabhängige Bestätigung einer Kryptografie, die sehr viele Nachrichten schützt. Wired nennt sie einen Meilenstein für die Kryptografie und für die KI selbst, betont aber den begrenzten Umfang.

Was hat DeepMind genau bewiesen?

Das Team bewies „eine Reihe“ der zentralen Garantien des Protokolls, nicht alle. Wired stellt klar, dass die gesamte mobile Signal-App nicht formal verifiziert wurde, und die Forscher beschreiben ihr Ergebnis als einen Meilenstein in einem größeren Prozess. „Wir freuen uns sehr über dieses Ergebnis, aber es ist ein weiter Weg, bis wir das auf die gesamte Software der Welt skalieren können, und das wollen wir“, sagte Swarat Chaudhuri, Forscher bei DeepMind, zu Wired.

Laut demselben Artikel fand die Analyse in den untersuchten Teilen des Protokolls keine neue Schwachstelle. Die Forscher ließen AlphaProof Code außerdem auf ältere Signal-Versionen mit bekannten, längst behobenen Schwachstellen laufen: Das Werkzeug erkannte sie korrekt und zeigte, dass sich diese Versionen nicht formal verifizieren ließen. Der Test ist wichtig, weil er zeigt, dass die Methode scheitern kann, wenn ein Fehler vorliegt, und nicht nur gelingt, wenn keiner vorliegt.

• Werkzeug: AlphaProof Code, ein neues agentisches KI-Framework von Google DeepMind.
• Dauer: vier Wochen, als Machbarkeitsprojekt.
• Ergebnis: zentrale kryptografische Garantien bewiesen; keine neue Schwachstelle in den analysierten Teilen.
• Ältere Versionen: bekannte, längst behobene Fehler erkannt, Protokoll als nicht verifizierbar eingestuft.
• Veröffentlichung: Spezifikation und Beweis werden freigegeben, um weitere Verifikationsarbeit zu unterstützen.
• Kosten: nicht genannt; die Analyse erfolgte kostenlos als Forschungsprojekt.

Wie teilten sich KI und Menschen die Arbeit?

Vor der KI-Ära mussten Menschen die gewünschten Eigenschaften beschreiben, in Formeln übersetzen und anschließend den Beweis entwickeln. Wired erklärt, dass agentische KI den Aufwand für den letzten Schritt stark senken kann, was die Signal-Auswertung in vier Wochen möglich machte. Die DeepMind-Forscher fügen hinzu, dass sie einen Vorsprung hatten, weil die Signal Foundation bereits formale Verifikation an kleineren Teilen des Codes durchgeführt hatte.

Ehren Kret, Technikchef von Signal, sagte in einer von Wired zitierten Stellungnahme: „Während sich frühere formale Verifikation auf kleinere Teile des Codes konzentrierte, ermöglicht der Ansatz von Google DeepMind eine deutliche Ausweitung.“ Die strenge Verifikation der Implementierung gebe Signal noch mehr Vertrauen in die Datenschutzgarantien seines Codes, da KI-getriebene Sicherheitsbedrohungen zunähmen.

DeepMind sieht seinen wichtigsten Fortschritt in einem „Mensch-KI-Zusammenarbeitsprozess“: Agenten tragen in fast jeder Phase bei und korrigieren sich selbst, während Menschen an Schlüsselstellen prüfen. „Wir wollen keine Welt, in der die KI die Ziele und die Beweise erzeugt“, sagte Chaudhuri. Ein formaler Beweis garantiert nur die Eigenschaften, die aufgeschrieben wurden; deshalb bleibt die menschliche Prüfung der Spezifikation zentral.

Ein paralleles Vorhaben rund um Signal

Die Arbeit von DeepMind ist nicht der einzige Versuch, Signals Kryptografie zu beweisen. Die Beneficial AI Foundation hat gemeinsam mit Rolfe Schmidt von Signal und dem Lean FRO „Signal Shot“ gestartet, ein öffentliches Projekt zur Verifikation des Protokolls und seiner Rust-Implementierung mit dem Beweisassistenten Lean. Geplant ist, Signals Rust-Code mit dem Werkzeug Aeneas nach Lean zu übersetzen; zu den aufgeführten Komponenten zählen der postquantensichere Schlüsselaustausch PQXDH, der Double Ratchet und der SPQR/Triple Ratchet. Wired verknüpft diese Initiative nicht mit der von DeepMind: Es sind zwei getrennte Vorhaben.

Was bleibt unsicher?

Die offene Frage, so Wired, ist, ob KI-automatisierte formale Verifikation zu tragbaren Kosten skalieren kann. Google lehnte es ab, die Kosten der Signal-Analyse zu nennen, und wollte nicht sagen, ob ein kommerzielles Produkt oder ein Dienst für formale Verifikation geplant ist. Pushmeet Kohli, Chief Scientist bei Google Cloud und Forschungs-Vizepräsident von DeepMind, stellt sich vor, dass Banken und andere Unternehmen, die Fehler fürchten, künftig sagen könnten, sie könnten bestimmte Eigenschaften ihrer Software beweisen. Das ist eine Vision, kein angekündigtes Angebot.

Was das für Unternehmen ändert

Für ein Unternehmen, das einen Messenger auswählt oder auf dem Signal-Protokoll aufbaut, ist das Ergebnis ein beruhigendes Signal zum Protokolldesign, aber kein Zertifikat für jede App, die es nutzt: Die vollständige Signal-App wurde nicht verifiziert, und Betrieb, Server und Einstellungen eines Produkts liegen außerhalb des Beweises. Die veröffentlichte Spezifikation und der Beweis geben Sicherheitsteams Material zum Studieren und Wiederverwenden. Da Kosten und ein mögliches kommerzielles Angebot unbekannt sind, sollten Firmen noch nicht darauf setzen, den eigenen Code so formal zu verifizieren; sie können aber schon bei Lieferanten kritischer Software nachfragen, welche Eigenschaften spezifiziert und bewiesen sind.