KI-Modelle und Plattformen
Google DeepMind setzt KI-Agenten ein, um den zentralen Maschinencode von Signal zu verifizieren
Unite.AI zu deinen bevorzugten Quellen auf Google hinzufügen
Am 10. November 2026 stellte Google DeepMind AlphaProof Code vor. Dabei kamen Teams von KI-Agenten zum Einsatz, die maschinengeprüfte Lean-Beweise für festgelegte Sicherheitseigenschaften des kompilierten libsignal-Codes von Signal erstellten. Das fünfköpfige Forschungsteam schloss die Beweisarbeit innerhalb von vier Wochen ab und veröffentlichte seine Spezifikationen und Verifikationsartefakte zur externen Prüfung.
Die Arbeit ging über ein abstraktes Modell des Protokolldesigns von Signal hinaus und bezog dessen kompilierte Implementierung ein. Die Forschenden banden die unveränderten Crates libsignal v0.105.4 und SPQR v1.6.0 in ein kleines Kommandozeilenprogramm ein und verwendeten anschließend den standardmäßigen rustc-Compiler, um eine statisch gelinkte ausführbare Datei für AArch64 Linux zu erstellen. Das Fachpapier bezeichnet das Ergebnis als die ersten Sicherheitsbeweise auf Protokollebene für den unveränderten Code einer weit verbreiteten Implementierung eines kryptografischen Protokolls.
So teilte AlphaProof Code die Arbeit auf
Fünf Forschende arbeiteten vier Wochen lang an den Beweisen und ließen die Agenten kontinuierlich auf ihren Arbeitsrechnern laufen, während sie parallel symbolische und rechnerische Beweise erarbeiteten. Dem Fachpapier zufolge generierten die Agenten rund 6,5 Millionen Zeilen maschinengeprüften Lean-Beweiscodes, der auf etwa 26.000 Zeilen vertrauenswürdiger Spezifikationen und AArch64-Semantik beruhte.
Die Menschen wählten die Eigenschaften aus, klärten Mehrdeutigkeiten und sicherheitsbezogene Abwägungen, prüften die Spezifikationen und behielten die endgültige Entscheidungsbefugnis. Von Gemini 4 Carbon und Claude Opus 5.5 gesteuerte Agenten entwarfen und prüften diese Spezifikationen; dabei erfolgte auch eine Prüfung durch ein Modell aus einer anderen Modellfamilie. Anschließend generierten Agententeams mit Gemini 4 Carbon den gesamten Beweiscodes; keiner der Autorinnen und Autoren schrieb Beweiscodes. Bei typischen Durchläufen kamen 40 bis 80 Agenten auf einem Rechner 24 bis 72 Stunden lang zum Einsatz. Ein Orchestrator und Teamleitungen koordinierten die Beweisagenten, während Personen in den Rollen Architektur und Integration die gemeinsame Beweisgrundlage pflegten.
Eine Prüfinstanz akzeptierte einen Beweis erst, nachdem der Lean-Kernel ihn geprüft und ein Vergleichsmechanismus bestätigt hatte, dass er mit der zurückgehaltenen, von Menschen genehmigten Spezifikation übereinstimmte – einschließlich aller transitiven Definitionen und unter ausschließlicher Verwendung der Standardaxiome von Lean. Wenn Beweise Probleme in einer Spezifikation aufdeckten, konnten Agenten kleinere Änderungen vorschlagen. Änderungen an vertrauenswürdigen Annahmen erforderten jedoch die Zustimmung eines Menschen oder eine vom Nutzer festgelegte Richtlinie und wurden mit Begründungen protokolliert. Diese Kontrolle begegnet einem dokumentierten Risiko agentengenerierter Beweise: Eine Spezifikation kann indirekt über eine ihrer Definitionen abgeschwächt werden.
Abdeckung der Sicherheitsbeweise und Tests mit historischen Fehlern
Verifiziert wurde der Code für Eins-zu-eins-Sitzungen, der den PQXDH-Handshake und Nachrichtenübermittlung mit Triple Ratchet umfasst. Die Forschenden berichten von zwei unabhängigen Beweisführungen: zehn symbolischen Theoremen unter idealisierten kryptografischen Annahmen sowie einem rechnerischen Beweis, der den Vorteil eines Angreifers mithilfe kryptografischer Annahmen und statistischer Terme begrenzt. Zu den untersuchten Eigenschaften zählen Forward Secrecy, die frühere Nachrichten schützt, wenn der aktuelle Zustand gestohlen wird, Authentifizierung, Post-Compromise-Sicherheit, die sich mit der Wiederherstellung nach einem Sicherheitsvorfall befasst, sowie Geheimhaltung des Handshakes. Die symbolische Beweisführung deckt zusätzlich die Geheimhaltung des Handshakes nach einem späteren Durchbruch des Diffie–Hellman-Verfahrens ab.
Um zu prüfen, ob die Spezifikationen echte Fehler aufdecken konnten, machte das Team die Korrekturen für zwei zuvor behobene libsignal-Fehler rückgängig, die als „schwacher Zustand“ und „kleine Untergruppe“ bekannt sind, und kompilierte die veränderten Binärdateien erneut. In beiden Fällen erstellte es Lean-Beweise dafür, dass der symbolische Sicherheitssatz nicht galt. Das öffentlich zugängliche Verifikations-Repository trennt die Materialien zu den rechnerischen und symbolischen Beweisen, zu den gemeinsam genutzten Binärdateien und zur AArch64-Semantik. Außerdem dokumentiert es, wie sich die Beweise neu erstellen und unabhängig überprüfen lassen.
Signal-Technologiechef Ehren Kret sagte, die Arbeit „gibt uns noch größeres Vertrauen in die Datenschutzgarantien unseres Codes“.
Grenzen und nächste Schritte
Die Garantien reichen bei Weitem nicht aus, um die vollständigen Anwendungen von Signal zu zertifizieren. Sie beziehen sich auf den libsignal-cli-Build der Forschenden, der als neuer Prozess ausgeführt wird. Die Schlüsselgenerierung wurde nicht verifiziert, Gruppenkommunikation blieb künftigen Arbeiten vorbehalten, und Seitenkanäle sowie der Zustand mehrerer Geräte liegen außerhalb des untersuchten Szenarios. Niedrigstufige kryptografische Primitive sowie ausgewählte Ausgabe- und Bibliotheksroutinen werden durch vertrauenswürdige Verträge abgebildet. Das Ergebnis hängt daher auch von diesen Verträgen, den genehmigten Spezifikationen, dem Lean-Kernel, der AArch64-Semantik und Annahmen über die Primitive ab.
Dem Fachpapier zufolge beweist keine der beiden Beweisführungen die Post-Quanten-Wiederherstellung, die SPQR ergänzen soll: Der rechnerische Satz behandelt klassische Angreifer, während die symbolischen Ratchet-Theoreme dem Angreifer erlauben, SPQR-Schlüssel auszuwählen. Das rechnerische Modell schränkt außerdem mehrere Handlungen des Angreifers ein und wird bei hinreichend großen Nachrichten- und Sitzungsumfängen nichtssagend. Diese Grenzen legen fest, was externe Prüfende als vertrauenswürdig voraussetzen müssen, bevor sie die maschinengeprüften Beweise als Sicherheitsgarantie für eine bestimmte Bereitstellung ansehen.
Als nächste Schritte nennen die Forschenden, die Theoreme zu stärken, die vertrauenswürdige Basis zu verkleinern, indem weitere eingebundene Routinen verifiziert und kryptografische Verträge mit verifizierten Implementierungen verknüpft werden, sowie die Abdeckung auf Gruppenkommunikation, Sealed Sender und serverseitige Protokolle auszuweiten. Ihr Ziel, neue libsignal-Versionen vor der Veröffentlichung zu verifizieren, ist ein Forschungsziel und keine angekündigte Einführung.
Die unmittelbare Bedeutung des Ergebnisses liegt in der Arbeitsteilung, die es veranschaulicht: Die Agenten übernahmen die Konstruktion der Beweise, während die Absicherung weiterhin auf von Menschen geprüften Spezifikationen und expliziten Annahmen beruht. Die Veröffentlichung der Beweise und Prüfverfahren ermöglicht externen Prüfern, diese Grundlage zu testen, während die Forschenden daran arbeiten, den Arbeitsablauf in die laufende Entwicklung von libsignal zu integrieren.
