DeepMinds KI weist nach, dass Signals Verschlüsselungscode seine Zusagen einhält

Google DeepMind erklärt, ihre KI-Agenten hätten mathematisch bewiesen, dass der Verschlüsselungscode von Signal für Einzelchats seine wichtigsten Sicherheitsversprechen hält. Für die am 10. November vorgestellte Arbeit nutzte das Team das neue System AlphaProof Code und prüfte das kompilierte Programm selbst, also den Code, der tatsächlich läuft. Laut DeepMind ist es das erste Mal, dass die Implementierung eines weit verbreiteten kryptografischen Protokolls überhaupt formal verifiziert wurde, mit oder ohne KI. In den geprüften Teilen fanden sich keine neuen Schwachstellen.

Was genau bewiesen wurde

Formale Verifikation heißt: Man schreibt eine Sicherheitseigenschaft als mathematische Aussage auf und beweist, dass das Programm sie immer erfüllt, statt es nur an Beispielen zu testen. Meist endet die Prüfung von Protokollen wie Signal beim Entwurf. DeepMind ging bis zum Maschinencode: Das Team nahm libsignal in Version 0.105.4 und die Bibliothek spqr, kompilierte sie mit dem normalen Rust-Compiler für 64-Bit-ARM-Linux und bewies die Eigenschaften an der fertigen ausführbaren Datei, heißt es in der technischen Beschreibung.

Zunächst übersetzten Forscher zusammen mit mehreren KI-Modellen die Sicherheitsziele von Signal in formale Spezifikationen, und jede davon prüfte ein Mensch. Dann schrieben Agenten auf Basis von Gemini Carbon die Beweise in Lean, einer Sprache, deren Prüfprogramm jeden Schritt automatisch bestätigt. Herausgekommen sind rund 6,5 Millionen Zeilen. Etwa 1 % davon markierten die Agenten zur Durchsicht durch Menschen, das gesamte Projekt dauerte vier Wochen. Zu den zehn bewiesenen Theoremen gehören Forward Secrecy, die alte Nachrichten schützt, wenn ein Schlüssel später bekannt wird, und Post-Compromise Security, die den Schutz wiederherstellt, nachdem ein Gerät vorübergehend gehackt war.

Um zu prüfen, ob das System korrekten von fehlerhaftem Code unterscheiden kann, baute das Team zwei echte, längst behobene Signal-Fehler wieder in eine isolierte Kopie des Codes ein. In beiden Fällen lieferte AlphaProof Code einen maschinell geprüften Beweis, dass die fehlerhafte Version unsicher ist.

Was der Beweis nicht abdeckt

Die Beschreibung listet die Grenzen genau auf. Die Mobil-Apps wurden nicht direkt geprüft, die Autoren erwarten lediglich, dass die Ergebnisse übertragbar sind, wenn die Apps den Protokollcode unverändert ausführen. Gruppenchats bleiben künftiger Arbeit überlassen. Seitenkanäle, etwa Lecks über Laufzeit oder Stromverbrauch, gehören nicht dazu, ebenso wenig die Schlüsselerzeugung und die Nutzung auf mehreren Geräten. Außerdem setzen die Beweise voraus, dass die zugrunde liegenden kryptografischen Bausteine sicher sind. Signals Technikchef Ehren Kret sagte, die Arbeit gebe „noch mehr Vertrauen“ in die Datenschutzgarantien des Codes.

Im Blog von DeepMind werden Signal und Google Messages als Apps mit diesem Protokoll genannt. WhatsApp hat das Signal-Protokoll vor Jahren übernommen, geprüft wurde aber Signals eigener libsignal-Code und nicht die Software von WhatsApp, über WhatsApp sagt das Ergebnis also nichts Neues. Teilweise baute die Arbeit auf einer früheren formalen Prüfung von Signal ohne KI auf. Zudem ist die Methode aufwendig: Google sagte Wired, der Ansatz sei rechenintensiv, und der Forscher Swarat Chaudhuri meinte, es sei noch „ein weiter Weg“, bis sich das auf alle Software der Welt ausweiten lasse, berichtet 9to5Mac. DeepMind hat die Beweise auf GitHub veröffentlicht, damit externe Fachleute sie nachprüfen können.