Google DeepMind erklärt, mit AlphaProof Code zentrale Sicherheitseigenschaften in libsignal mathematisch überprüft zu haben – der Referenzimplementierung des Signal-Messaging-Protokolls. Die Arbeit dauerte vier Wochen. Laut DeepMind hätte eine vergleichbare Überprüfung durch Expertenteams früher Jahre in Anspruch genommen.
Das System verband menschliche Forschende mit KI-Agenten. Gemeinsam überführten sie Signals Sicherheitsziele in mathematische Spezifikationen, die anschließend von Menschen geprüft wurden. Danach erzeugten von Gemini Carbon angetriebene Agenten rund 6.5 Millionen Zeilen Lean-Beweiscodes. Lean ist eine Programmiersprache, deren Prüfer feststellen kann, ob ein mathematischer Beweis ihren Regeln entspricht. Die Agenten markierten etwa ein Prozent der Codebasis zur menschlichen Prüfung.
Was deckt der Beweis ab?
Die Forschenden überprüften den kompilierten Maschinencode für den Post-Quanten-Handshake PQXDH und den Triple Ratchet von libsignal. Sie bewiesen bestimmte Eigenschaften, darunter Forward Secrecy, Authentifizierung und Schutz nach einer Kompromittierung des Geräts. Laut Forschungsarbeit wurde der Code mit einem Standardcompiler aus unverändertem Rust kompiliert und anschließend als AArch64-Maschinencode geprüft.
Damit geht die Arbeit über den Nachweis hinaus, dass ein abstrakter Entwurf sicher ist: Sie verknüpft festgelegte Sicherheitsgarantien mit kompiliertem Code. DeepMind bezeichnet sie als erste formale Verifikation einer weit verbreiteten Implementierung eines kryptografischen Protokolls in dieser Tiefe. Das Team fügte außerdem zwei zuvor behobene Fehler in einer isolierten Codeversion wieder ein. Das System erstellte Beweise dafür, dass die fehlerhaften Versionen die festgelegten Sicherheitseigenschaften nicht erfüllten.
Der Beweis hat Grenzen
Es handelt sich nicht um eine mathematische Garantie, dass jeder Teil von Signal oder jede App, die das Protokoll verwendet, frei von Sicherheitsproblemen ist. Der Beweis umfasst ausgewählte Eigenschaften von libsignal, nicht die gesamte App. Außerdem stützt er sich auf geprüfte Spezifikationen, den Prüfer von Lean und Verträge für kryptografische Routinen auf niedriger Ebene. The Register merkt an, dass das Ergebnis nicht die rechnergestützte Geheimhaltung tatsächlicher Nachrichteninhalte beweist. DeepMinds Arbeit beschreibt Beweise sowohl in symbolischen als auch in rechnergestützten Modellen; diese beruhen auf Annahmen über die zugrunde liegenden kryptografischen Primitiven.
DeepMind will die Verifikationsmaterialien anderen zur Verfügung stellen. Das Unternehmen hofft, die Methode etwa auf die Firmware medizinischer Geräte und Software für Stromnetze anwenden zu können, erklärt aber, dass für eine Ausweitung noch weitere Forschung nötig sei. Die Arbeit ist ein Schritt hin zur Überprüfung weiterer Software aus der Praxis, aber kein Beleg dafür, dass diese anderen Systeme bereits verifiziert wurden.
Warum es wichtig ist
Für Signal-Nutzerinnen und -Nutzer liefert die Arbeit einen maschinell geprüften Beweis für bestimmte Sicherheitseigenschaften der zentralen Protokollimplementierung. Sie belegt nicht, dass die gesamte App fehlerfrei ist, und beruht auf Annahmen über kryptografische Komponenten.
