Signals Verschlüsselung besteht einen KI-Beweis mit 6,5 Millionen Zeilen

Signals Verschlüsselungscode kann nun etwas vorweisen, worauf sich kaum eine weit verbreitete Software berufen kann: einen mathematischen Beweis dafür, dass er hält, was er verspricht. Ein Team von KI-Agenten hat libsignal untersucht, die Bibliothek hinter dem Signal-Protokoll, und bewiesen, dass Einzelchats geheim bleiben, die Identität des Gegenübers bestätigen und Angreifer erneut aussperren, nachdem ein Schlüssel gestohlen wurde. Neue Schwachstellen fanden sie nicht.

Das ist weit über Signals eigene Nutzer hinaus von Bedeutung. Das Protokoll ist der weltweite Standard für Ende-zu-Ende-verschlüsselte Nachrichten, und Varianten davon schützen Chats in WhatsApp, Messenger und Google Messages. Echten, bereits veröffentlichten Code so gründlich zu überprüfen, war bislang so zeitaufwendig, dass es kaum jemand versuchte: Einer der größten Erfolge auf diesem Gebiet, ein verifizierter Betriebssystemkern, erforderte den Einsatz von 20 Personenjahren. Diese Arbeit dauerte vier Wochen.

Das von Google DeepMind entwickelte Werkzeug heißt AlphaProof Code. Zunächst überführten menschliche Fachleute und KI-Modelle Signals Sicherheitsziele in formale Aussagen in Lean, einer Programmiersprache für mathematische Beweise; jede einzelne wurde von einem Menschen überprüft. Anschließend erstellten Teams aus 40 bis 80 Agenten, angetrieben von Gemini Carbon, die Beweise. Sie liefen jeweils 24 bis 72 Stunden auf einem einzigen Rechner. Das Ergebnis umfasst rund 6,5 Millionen Zeilen Lean-Code.

Niemand muss diesen Millionen Zeilen vertrauen. Der Lean-Kern überprüft jeden Schritt und verwirft jeden ungültigen Beweis. Daher spielt es keine Rolle, welches Modell ihn geschrieben hat oder wie oft es sich auf dem Weg dorthin geirrt hat. Vertrauen müssen Menschen nur in einen wesentlich kleineren Teil: rund 26.000 Zeilen Spezifikationen sowie ein Modell dafür, wie ein ARM-Prozessor Code ausführt.

Die Beweise decken jene Teile von Signal ab, die eine Unterhaltung schützen: den PQXDH-Handshake, der einen Chat einrichtet, und den Triple Ratchet, der für jede Nachricht den Schlüssel wechselt – einschließlich der Post-Quanten-Schicht, die künftigen Quantencomputern widerstehen soll. Konkret bedeutet das: Wer die aktuellen Schlüssel eines Telefons stiehlt, kann damit keine älteren Nachrichten entschlüsseln. Sobald die beiden Seiten neue Schlüssel ausgetauscht haben, verliert der Dieb außerdem wieder den Zugriff.

Um zu zeigen, dass das System guten von fehlerhaftem Code unterscheiden kann, bauten die Forschenden zwei alte, bereits behobene Fehler in libsignal wieder ein. Bei einem davon behielt die Bibliothek eine Kopie eines geheimen Schlüssels, den sie hätte verwerfen müssen. In beiden Fällen erzeugte AlphaProof Code einen maschinell überprüften Beweis dafür, dass die fehlerhafte Version unsicher war.

Die Grenzen des Verfahrens sind deutlich. Der Beweis gilt nur für Einzelchats; Gruppenunterhaltungen führt DeepMind als mögliche künftige Arbeit auf. Er bezieht sich auf libsignal Version 0.105.4, kompiliert mit dem Standard-Rust-Compiler für ARM Linux innerhalb eines kleinen Testprogramms – nicht auf die vollständigen Signal-Apps für iPhone, Android oder Desktop. Die kryptografischen Bausteine auf niedriger Ebene werden als sicher vorausgesetzt, aber nicht bewiesen. Ein Fehler in den von Menschen geprüften Spezifikationen würde die Garantie schwächen. Außerdem verwenden WhatsApp und die anderen Apps eigene Versionen des Protokolls, sodass sich das Ergebnis nicht automatisch auf sie übertragen lässt. Google wollte Wired auch nicht mitteilen, was die Analyse gekostet hat oder ob das Unternehmen plant, sie als Dienstleistung anzubieten.

Signal begrüßte das Ergebnis. „Angesichts der zunehmenden Bedrohungen für die Sicherheit durch KI gibt uns die rigorose Überprüfung der Implementierung des Signal-Protokolls noch mehr Vertrauen in die Datenschutzgarantien unseres Codes“, sagte Ehren Kret, Technikchef von Signal, in einer Stellungnahme. Swarat Chaudhuri, Forschungswissenschaftler bei DeepMind, äußerte sich gegenüber Wired zurückhaltender: Bis sich die Methode „auf die gesamte Software der Welt“ skalieren lasse, sei es noch „ein weiter Weg“.

Für alle, die Signal nutzen, gibt es nichts zu installieren und keine Einstellung zu ändern. Der Beweis bezieht sich auf Code, der bereits in der App steckt.

DeepMind veröffentlichte die Arbeit am 10. November zusammen mit einer technischen Studie und stellte die Spezifikationen und Beweise als Open Source auf GitHub bereit. Das Unternehmen bezeichnet das Signal-Projekt als Meilenstein auf dem Weg zu einer im April formulierten großen Herausforderung der formalen Verifikation. Als nächste Systeme, die es überprüfen möchte, nennt es Firmware für medizinische Geräte und Software für Stromnetze.

Chaudhuri zog auch eine Grenze dafür, wie viel der Arbeit Maschinen übernehmen sollten. „Wir wollen keine solche Vibe-Welt, in der die KI die Ziele vorgibt und die Beweise erstellt“, sagte er gegenüber Wired. Was als sicher gilt, entscheiden weiterhin Menschen – die KI beweist es lediglich.

Schlagwörter: Cybersicherheit, Google DeepMind, AlphaProof Code, Ende-zu-Ende-Verschlüsselung, formale Verifikation, libsignal