DeepMind-KI beweist mathematisch zentrale Sicherheitsgarantien des Signal-Protokolls

Worum es geht

Google DeepMind, die KI-Forschungsabteilung von Google, hat mit einem neuen KI-Werkzeug namens AlphaProof Code mehrere zentrale Sicherheitsgarantien des Signal-Protokolls mathematisch bewiesen. Das berichtete zuerst das US-Magazin WIRED. Das Signal-Protokoll ist das Verschlüsselungsverfahren hinter der Messenger-App Signal, steckt aber auch in WhatsApp und Google Messages – es schützt also die Nachrichten von sehr vielen Menschen weltweit.

Das Projekt war ein Forschungsvorhaben, eine Art Machbarkeitsnachweis, und dauerte nur vier Wochen. Die Forscher fanden in den untersuchten Teilen keine neuen Schwachstellen. Wichtig ist die Einschränkung: Bewiesen wurden ausgewählte Eigenschaften des Protokolls, nicht die Sicherheit der kompletten Signal-App oder von WhatsApp und Google Messages insgesamt.

Was formale Verifikation ist

Formale Verifikation bedeutet, mit Mathematik zu zeigen, dass Software bestimmte festgelegte Anforderungen erfüllt. Statt Programme nur mit vielen Beispielen zu testen – was immer Lücken lassen kann –, wird ein lückenloser Beweis geführt, ähnlich wie in der Mathematik ein Satz bewiesen wird. In der Softwaresicherheit gilt das deshalb seit Langem als eine Art heiliger Gral, wie WIRED schreibt.

Der Ablauf hat drei Schritte: Zuerst beschreiben Fachleute, welche Eigenschaften die Software haben soll – etwa dass niemand außer den Gesprächspartnern eine Nachricht lesen kann. Dann werden diese Beschreibungen in mathematische Formeln übersetzt, die sogenannte Spezifikation. Schließlich wird der Beweis entwickelt, dass die Software diese Formeln erfüllt. Vor dem KI-Zeitalter war das extrem zeitaufwendig. Laut WIRED kann agentische KI – also KI, die selbstständig mehrere Arbeitsschritte hintereinander erledigt und sich dabei selbst korrigiert – vor allem den letzten Schritt, das Beweisen, stark beschleunigen.

Entscheidend ist dabei: Die Festlegung der Anforderungen ist eine eigene Aufgabe. Ein Beweis ist nur so gut wie die Spezifikation, gegen die er geführt wird.

Was AlphaProof Code herausgefunden hat

Die Forscher führten zwei Untersuchungen durch, die unterschiedlich ausgingen:

Der zweite Test ist eine Art Gegenprobe: Er zeigt, dass das Werkzeug nicht einfach alles „durchwinkt“, sondern bei fehlerhaften Versionen tatsächlich scheitert – so wie es sein soll. DeepMind veröffentlicht die entwickelte Spezifikation und den Beweis, damit andere Forscher darauf aufbauen können.

Mensch und KI im Wechselspiel

DeepMind betont, dass die KI die Sicherheitsforscher nicht ersetzt hat. Forscher Swarat Chaudhuri beschreibt gegenüber WIRED einen „Mensch-KI-Kollaborationsprozess“: KI-Agenten tragen in fast jeder Phase etwas bei und korrigieren ihre eigene Arbeit, an entscheidenden Stellen holen sie aber menschlichen Input und eine Überprüfung ein. Menschen legten die Anforderungen fest und kontrollierten wichtige Etappen.

„Wir wollen keine Art Vibe-Welt, in der die KI die Ziele erzeugt und die KI die Beweise erzeugt und im Grunde selbstgeschriebene Tests besteht. Es gibt einen Mittelweg.“ – Swarat Chaudhuri, Google DeepMind

Der Punkt ist wichtig: Würde eine KI sowohl festlegen, was bewiesen werden soll, als auch den Beweis führen, könnte sie sich die Prüfung im Zweifel zu leicht machen.

Vorarbeit von Signal und große Ambitionen

Die kurze Projektdauer von vier Wochen hatte eine Grundlage: Laut den DeepMind-Forschern verschaffte ihnen frühere Verifikationsarbeit der Signal Foundation einen Vorsprung. Signals Technikchef Ehren Kret erklärte, die bisherige formale Verifikation habe kleinere Teile des Codes betroffen, DeepMinds Ansatz ermögliche eine deutliche Ausweitung.

„Da KI-getriebene Sicherheitsbedrohungen zunehmen, gibt uns die rigorose Verifikation der Signal-Protokoll-Implementierung noch mehr Vertrauen in die Datenschutzgarantien unseres Codes.“ – Ehren Kret, CTO von Signal

Pushmeet Kohli, Chefwissenschaftler bei Google Cloud und Forschungs-Vizepräsident bei DeepMind, sieht großes Potenzial: Banken und andere Unternehmen, die auf Zusicherungen angewiesen sind und sich vor Fehlern fürchten, könnten künftig sagen, sie könnten bestimmte Eigenschaften ihrer Software beweisen. Chaudhuri formuliert das Fernziel noch größer: Man wolle die Verifikation auf „die gesamte Software der Welt“ skalieren – davon sei man aber noch weit entfernt.

Offene Fragen: Kosten und Skalierung

Unbeantwortet bleibt die praktische Frage: Lässt sich das Verfahren auf sehr viel größere Codemengen ausweiten, und das zu vertretbaren Kosten? DeepMind hat die Signal-Analyse kostenlos als Forschungsprojekt durchgeführt. Google wollte WIRED nicht sagen, was die Arbeit gekostet hat, und äußerte sich auch nicht dazu, ob ein kommerzielles Produkt oder ein Dienst für formale Verifikation geplant ist. Wie aufwendig die menschliche Begleitung war, bleibt ebenfalls offen.

Auch andere Firmen setzen auf die Kombination aus formaler Verifikation und Sprachmodellen: Laut Mezha.net hat etwa das Start-up Pramaana Labs 27 Millionen US-Dollar eingesammelt, um überprüfbare KI für Bereiche wie Recht, Medikamentenentwicklung und Steuerberatung zu bauen.

Einordnung

Das Ergebnis ist in zweierlei Hinsicht bedeutsam: Es liefert eine weitere unabhängige Bestätigung für Kryptografie, auf die sich Milliarden Nachrichten täglich verlassen, und es zeigt, dass KI-Agenten aufwendige mathematische Beweise über echte, sicherheitskritische Software in kurzer Zeit mitentwickeln können. Gerade weil KI auch Angreifern hilft, Schwachstellen zu finden, wird solche nachweisbare Sicherheit wichtiger.

Gleichzeitig sollte man den Befund nicht überdehnen. Verifiziert wurden ausgewählte Garantien des Protokolls, nicht die Apps als Ganzes – Fehler in anderen Teilen der Software, im Betriebssystem oder in der Bedienung sind damit nicht ausgeschlossen. Die Spezifikationen stammen weiterhin von Menschen, die Projektkosten sind unbekannt, und Signal hatte bereits Vorarbeit geleistet. Es handelt sich also um eine begrenzte Forschungsdemonstration, nicht um den Beleg für einen skalierbaren Dienst. Positiv ist, dass Spezifikation und Beweis veröffentlicht werden – so können Dritte die Arbeit überprüfen.