Forschende von Google DeepMind haben gezeigt, dass ein KI-System wichtige Sicherheitseigenschaften des Signal-Messaging-Protokolls mathematisch beweisen kann. Mit einem neuen Framework namens AlphaProof Code überprüfte das Team formal mehrere kryptografische Garantien. Die Arbeit dauerte etwa vier Wochen und war ein Forschungsprojekt, kein kommerzielles Produkt. In den untersuchten Abschnitten wurden keine neuen Fehler gefunden. Bei älteren Versionen des Protokolls erkannte die KI bekannte Schwachstellen, die bereits behoben worden waren.
Formale Verifikation bedeutet, mithilfe mathematischer Methoden zu prüfen, ob sich Software exakt wie vorgesehen verhält – ohne Raum für versteckte Schwachstellen. Bislang mussten Fachleute dafür detaillierte Spezifikationen verfassen, in Formeln übertragen und anschließend den Beweis führen. Das war arbeitsintensiv und konnte Monate dauern. Indem ein agentisches KI-System – also eine KI, die eigene Teilziele setzen und verfolgen kann – einen Großteil der aufwendigen Arbeit übernahm, verkürzte DeepMind den Prozess auf wenige Wochen. Laut den Forschenden war an wichtigen Stellen weiterhin menschliche Aufsicht nötig. Die KI konnte jedoch selbstständig Beweise vorschlagen und korrigieren.
Ehren Kret, Chief Technology Officer von Signal, wies darauf hin, dass frühere Verifikationsarbeiten nur kleine Codefragmente abdeckten. Der Ansatz von DeepMind ermögliche eine „deutliche Ausweitung“ des Prüfungsumfangs, sagte er. Das Team veröffentlicht die erstellte Spezifikation und den Beweis, damit andere Gruppen darauf aufbauen können. Das Ergebnis sei zwar vielversprechend, räumt DeepMind ein, doch die Methode auf ganze Apps oder komplette Software-Lieferketten auszuweiten, bleibe eine Herausforderung. Die Kosten einer solchen KI-gestützten Verifikation wurden nicht bekannt gegeben.
Warum das wichtig ist
Wenn KI die Sicherheit kryptografischer Protokolle zuverlässig beweisen kann, könnten Nutzerinnen und Nutzer von Signal, Google Messages, WhatsApp und ähnlichen Apps stärker darauf vertrauen, dass ihre Nachrichten privat bleiben. Für Unternehmen, die auf verschlüsselte Kommunikation angewiesen sind – etwa Banken, Gesundheitsdienstleister und Journalistinnen und Journalisten –, könnte die Technologie künftig rechtlich nachprüfbare Garantien bieten, dass ihre Software keine kritischen Fehler enthält.
Warum es wichtig ist
Für den Alltag bedeutet die Nachricht, dass die Verschlüsselung von Chats nun durch eine zusätzliche mathematische Prüfung abgesichert ist. Dadurch sinkt die Wahrscheinlichkeit versteckter Fehler. Für Unternehmen, die die Einhaltung von Datenschutzvorschriften nachweisen müssen, könnte KI-gestützte Verifikation künftig eine Möglichkeit bieten, Sicherheit ohne langwierige manuelle Prüfungen zu belegen.
