Signal: Was die KI tatsächlich über seinen Code bewiesen hat

Google DeepMind gibt an, AlphaProof Code eingesetzt zu haben, um bestimmte Eigenschaften des kompilierten Codes von libsignal zu beweisen. Das Ergebnis verdeutlicht das Potenzial der KI, aber auch die genauen Grenzen eines formalen Beweises.

Um zu beurteilen, ob eine Software Nachrichten korrekt verschlüsselt, reicht es nicht aus, Tests durchzuführen und ihr Verhalten in einigen Situationen zu beobachten. Es muss auch möglich sein, durch eine überprüfbare Argumentation festzustellen, dass bestimmte Eigenschaften bei allen vom Modell abgedeckten Ausführungen gelten. Google DeepMind gibt an, sein System AlphaProof Code für diese Arbeit an kompiliertem Code des Signal-Protokolls eingesetzt zu haben – mit KI-Agenten und dem Beweisassistenten Lean.

Das Experiment befasst sich mit konkreten kryptografischen Garantien, nicht mit der absoluten Sicherheit der Signal-App. Es zeigt vor allem, wie KI an einer anspruchsvollen formalen Überprüfung mitwirken kann, wobei wichtige Entscheidungen den Forschenden überlassen bleiben und die abschließende mathematische Kontrolle einer spezialisierten Software obliegt.

Vom kryptografischen Modell zum ausgeführten Code

Ein Verschlüsselungsprotokoll beschreibt die Regeln, mit denen beispielsweise ein Austausch geschützt und die Identität der Gesprächspartner bestätigt werden kann. Doch ein korrektes Konzept allein reicht nicht aus: Das Programm, das es umsetzt, kann einen Fehler enthalten. Die formale Verifikation soll mathematisch nachweisen, dass der Code zuvor definierte Eigenschaften erfüllt – unter ebenso ausdrücklich festgelegten Annahmen.

DeepMind zufolge arbeitete das Team mit kompiliertem Code von libsignal, der Bibliothek, die das Signal-Protokoll implementiert. Dieser Schritt ist wichtig: Das Team beschränkte sich nicht auf eine theoretische Beschreibung des Protokolls, sondern versuchte, Sicherheitsgarantien mit dem nach der Kompilierung erzeugten Code zu verknüpfen.

Das AlphaProof Code genannte System verteilt die Arbeit auf mehrere Modelle und Agenten. Laut der von Google DeepMind veröffentlichten Beschreibung übersetzten Forschende zunächst die Sicherheitsziele in mathematische Spezifikationen; anschließend erstellten mit Gemini ausgestattete Agenten formale Beweise. Im Beitrag von DeepMind ist von mehr als sechs Millionen Zeilen in der Sprache Lean die Rede. Das bedeutet nicht, dass die KI sechs Millionen Zeilen Software geschrieben hat: Gemeint sind Artefakte, die dazu dienen, die Beweise zu formalisieren und zu überprüfen.

Was Lean überprüft – und was die Forschenden entscheiden

Lean ist ein Beweisassistent. Es kontrolliert, ob ein Beweis den logischen Regeln des Systems entspricht und das formulierte Ergebnis tatsächlich belegt. Es entscheidet jedoch nicht selbst, ob die gewählten Eigenschaften allen Erwartungen der Nutzenden entsprechen oder ob die zugrunde liegenden Annahmen die reale Welt korrekt beschreiben.

Diese Unterscheidung ist zentral. Laut DeepMind waren Fachleute an der Festlegung dessen beteiligt, was bewiesen werden sollte, und prüften die Spezifikationen. Anschließend untersuchten die Agenten mögliche Beweiswege, während Lean deren formale Gültigkeit überprüfte. Das System kann somit einen Teil der Arbeit bei der Suche nach einem Beweis verringern, doch den Umfang des Beweises legen weiterhin Menschen fest.

Ein formaler Beweis ist also kein umfassendes Audit. Ist eine Eigenschaft nicht in den Spezifikationen enthalten, wird sie vom Beweis nicht abgedeckt. Wird eine kryptografische Funktion als sicher vorausgesetzt, ohne dass ihre Implementierung überprüft wird, bleibt diese Annahme außerhalb des Ergebnisses. Die korrekte Schlussfolgerung ist daher bedingt: Der Code erfüllt die formalisierten Eigenschaften innerhalb des festgelegten Rahmens und unter den zugrunde gelegten Annahmen.

Vier Wochen, zwei wieder eingeführte Bugs

DeepMind gibt an, dass das Experiment vier Wochen dauerte. Um zu testen, ob die Methode konformen von fehlerhaftem Code unterscheiden konnte, führte das Team außerdem zwei bekannte, zuvor behobene Bugs in einer isolierten Codeversion erneut ein. Dem Unternehmen zufolge erzeugte das System daraufhin maschinell geprüfte Beweise, die zeigten, dass diese Varianten die untersuchten Garantien nicht mehr erfüllten.

Dieser Test ist nützlich, weil er die Methode mit konkreten Fehlern konfrontiert, statt nur zu messen, ob sie für eine korrekte Version einen Beweis erstellen kann. Er liefert jedoch keine allgemein übertragbare Erkennungsrate: Zwei erneut eingeführte Fehler stehen weder für alle Kategorien von Schwachstellen noch für alle Softwareprodukte oder alle Arten, auf die ein System versagen könnte.

Die Grenzen des Beweises bleiben klar umrissen

Die untersuchten Garantien betreffen den kryptografischen Kern und einzelne Kommunikationsvorgänge. Der beschriebene Umfang lässt die Anwendung als Ganzes, Gruppengespräche und die Nutzung auf mehreren Geräten außen vor. Ebenso handelt es sich nicht um eine Überprüfung von WhatsApp oder Google Messages, auch wenn diese Dienste Bestandteile des Signal-Protokolls verwenden. Eine gemeinsame Bibliothek oder ein gemeinsames Protokoll macht die Anwendungen, die sie integrieren, ihre Versionen und ihre Konfigurationen nicht identisch.

Die Verifikation bedeutet auch nicht, dass keine unbekannten Schwachstellen mehr bestehen. Sie verringert die Unsicherheit hinsichtlich definierter Eigenschaften und des in die Analyse einbezogenen Codes. Andere Komponenten, Schnittstellen, Betriebssysteme, die Schlüsselverwaltung oder Funktionen außerhalb des Untersuchungsumfangs können eigene Fragen aufwerfen.

Für die Nutzenden liegt der unmittelbare Nutzen daher weniger in einer neuen Einstellung als in einer Kontrollmethode, die bestimmte Garantien schwerer anzufechten oder versehentlich zu verletzen machen könnte. Für Teams, die kritische Software entwickeln, stellt sich die Frage, ob Agenten den menschlichen Aufwand für Beweise verringern können, die bislang umfangreiche Spezialarbeit erforderten. DeepMind nennt mögliche Anwendungen auf andere Software, doch ob sich dieser Ansatz auf größere Systeme ausweiten lässt, muss sich erst noch zeigen.

Die von DeepMind veröffentlichten Spezifikationen und Beweise ermöglichen es anderen Fachleuten, die Arbeit zu prüfen und zu reproduzieren. Diese Möglichkeit der Kontrolle macht es zusammen mit einem klar definierten Umfang möglich, den Beitrag der KI zu beurteilen: nicht als allgemeine Zertifizierung von «Sicherheit», sondern als Hilfe beim Nachweis bestimmter Eigenschaften des Codes – wobei Menschen entscheiden, worauf es ankommt, und ein formaler Verifikator den Beweis kontrolliert.