Google DeepMind hat mit dem neuen Verfahren AlphaProof Code zentrale Sicherheitseigenschaften der Verschlüsselung vom Messenger »Signal« mathematisch nachgewiesen. Die Beweise reichen bis zum Maschinencode, also zu den Befehlen, die der Prozessor ausführt.
Anzeige
Was DeepMind für Signal bewiesen hat
Die Forscher haben die unveränderte Signal-Bibliothek »libsignal« in ein kleines Testprogramm eingebunden und für ARM-Prozessoren unter Linux kompiliert. Die Beweise decken ab, wie zwei Teilnehmer eine verschlüsselte Unterhaltung beginnen und Nachrichten ver- und entschlüsseln.
Unter den geprüften Bedingungen bleiben ältere Nachrichten vertraulich, wenn ein Angreifer später die aktuellen Schlüssel erbeutet. Nach einem vorübergehenden Zugriff können neue Nachrichten wieder vertraulich sein, sobald beide Seiten frische Schlüssel ableiten.
Diese Aussagen gelten für den geprüften Maschinencode unter den Annahmen der Studie. Dazu zählt, dass die verwendeten kryptografischen Grundfunktionen ihre jeweiligen Sicherheitsanforderungen erfüllen. Gruppenchats und die Signal-Apps als Ganzes lagen außerhalb des untersuchten Ausschnitts.
KI-Agenten schreiben die Beweise, Lean prüft sie
Mithilfe von KI-Agenten übersetzten die Forscher die Sicherheitsanforderungen in mathematische Aussagen und gaben sie frei. Anschließend suchten Agenten mit Gemini Carbon nach Beweisen. Der Beweisassistent Lean kontrollierte automatisch, ob die Beweise die Anforderungen tatsächlich abdecken.
Fünf Forscher arbeiteten vier Wochen an den Beweisen. Die Agenten erzeugten dafür rund 6,5 Millionen Zeilen Beweiscode.
In einem Kontrollversuch setzte das Team zwei bereits behobene Fehler wieder in eine Testversion ein. Für beide Fälle lieferte AlphaProof Code einen von Lean geprüften Nachweis, dass die fehlerhafte Version eine Sicherheitsanforderung verletzte.
DeepMind hat die Spezifikationen und Beweise als Open Source auf GitHub veröffentlicht.
