Google DeepMind sagt, es habe eine langjährige Hürde in der Cybersicherheit überwunden: den Einsatz KI-gestützter formaler Verifikation, um den tatsächlich kompilierten Code hinter Signals Verschlüsselung zu prüfen, statt nur das Design des Protokolls.

Die Arbeit ist bedeutsam, weil kryptografische Systeme auf dem Papier solide sein können, während bei der Entwicklung und Kompilierung der Software Fehler entstehen. DeepMind erklärte, sein AlphaProof-Code-Framework habe menschliche Experten – die die Sicherheitsspezifikationen definierten und überprüften – mit durch Gemini Carbon betriebenen Agenten kombiniert, die mehr als sechs Millionen Zeilen Lean-Beweiscode erzeugten. Das System markierte anschließend etwa 1 % der Codebasis für zusätzliche menschliche Prüfung.¹

Das Unternehmen sagt, der vierwöchige Aufwand habe zentrale Eigenschaften nachgewiesen, darunter den Schutz von Nachrichten vor und nach einer vorübergehenden Kompromittierung eines Geräts. Um zu testen, ob das Framework sichere von fehlerhafter Software unterscheiden könne, stellten die Forscher zwei zuvor behobene Fehler in einer isolierten Version von Signal wieder her; in beiden Fällen erzeugte es maschinell geprüfte Beweise dafür, dass der veränderte Code unsicher war.¹

Das Ergebnis wurde öffentlich als Premiere dargestellt. In einer erneut veröffentlichten Ankündigung hob DeepMind-Chef Demis Hassabis die Behauptung seines Teams hervor, zentrale Sicherheitseigenschaften des Signal zugrunde liegenden Maschinencodes bewiesen zu haben, und bezeichnete dies als die erste formale Verifikation von tatsächlichem Produktivcode für ein weit verbreitet eingesetztes Protokoll.Demis Hassabis (demishassabis)²

Signals Technologiechef Ehren Kret bezeichnete die Entwicklung weniger als Ersatz für menschliches Urteilsvermögen denn als wesentliche Erweiterung dessen, was Verifikation abdecken kann. „Der Einsatz von KI-Agenten, um aktiven Code in gültige Lean-Theoreme zu übersetzen, ist ein bedeutender Durchbruch“, sagte er und argumentierte, dass der Prozess Signal angesichts wachsender KI-getriebener Bedrohungen mehr Vertrauen in seine Datenschutzversprechen gebe.¹

Axios berichtete, dass DeepMind-Forschungswissenschaftler Swarat Chaudhuri das umfassendere Ziel als das Erreichen „dieser Welt unhackbarer Software“ beschrieb, wobei das aktuelle System weiterhin ein Forschungsprojekt und kein kommerzielles Cybersicherheitswerkzeug sei.³ DeepMind plant, seine Verifikationsartefakte als Open Source bereitzustellen und Verbindungen zu Werkzeugen wie CodeMender und Project Zero zu untersuchen – ein früher Schritt, um mathematische Absicherung in die alltägliche Softwareentwicklung zu bringen.¹