Google DeepMind veröffentlicht AlphaProof Code: Agenten beweisen Sicherheit von Signals Maschinencode in Lean
Google DeepMind hat am 10. November AlphaProof Code vorgestellt, ein Agentensystem, das rund 6,5 Millionen Zeilen Lean-Beweise für den Maschinencode von libsignal generiert hat, der Referenzbibliothek des Signal-Protokolls. Die Beweise decken den Post-Quanten-Handshake PQXDH sowie das Triple Ratchet ab, wobei die getroffenen Annahmen und Einschränkungen im technischen Bericht detailliert aufgeführt sind.
Die Demonstration wurde bereits beim Start von Gemini 4 Carbon in einem Nebensatz erwähnt; nun ist sie ausführlich dokumentiert. Google DeepMind veröffentlichte am 10. November einen Blogbeitrag und einen technischen Artikel über AlphaProof Code, ein Agentensystem, das Sicherheitseigenschaften des Codes von libsignal, der Referenzbibliothek des Signal-Protokolls, mathematisch bewiesen hat. Dieses Protokoll verschlüsselt in abgewandelter Form auch WhatsApp, Messenger und Google Messages.
Was bewiesen wurde
Das Besondere liegt auf der Ebene des Beweises. Die meisten Verifikationen von Protokollen beschränken sich auf deren Design. Hier kompilierten die Forscher libsignal mit dem regulären Rust-Compiler für AArch64-Prozessoren (Arm 64-Bit) unter Linux und bewiesen anschließend, dass dieser Maschinencode die geforderten Eigenschaften einhält. Diese Beweise umfassen den Post-Quanten-Handshake PQXDH und das Triple Ratchet: Forward Secrecy, Authentifizierung, Sicherheit nach einer vorübergehenden Kompromittierung eines Geräts sowie die Geheimhaltung des Handshakes.
Die Zahlen verdeutlichen die Dimensionen: Rund 6,5 Millionen Zeilen Beweise, geschrieben in Lean, einer Beweissprache, deren Kernel jeden einzelnen Schritt prüft. Diese stützen sich auf etwa 26 000 Zeilen an Spezifikationen und Beschreibungen des Prozessors, die ihrerseits als vertrauenswürdig vorausgesetzt werden müssen. Die Arbeit beanspruchte vier Wochen eines fünfköpfigen Teams. Der Artikel erinnert daran, dass die Verifikation des seL4-Mikro-Kernels zwanzig Personenjahre gekostet hatte und die des Compilers CompCert sechs.
Wie die Agenten arbeiten
AlphaProof Code teilt die Aufgaben wie ein Forschungsteam auf. Menschen entscheiden, was bewiesen werden soll, und prüfen jede Spezifikation, die mit Unterstützung mehrerer Modelle verfasst wird. Von Gemini Carbon angetriebene Agenten schreiben die Beweise anschließend autonom. Ein „Wächter“-Agent akzeptiert einen Beweis nur dann, wenn Lean ihn anhand einer Kopie der genehmigten Spezifikation validiert: Die Zuverlässigkeit des Ergebnisses hängt somit nicht von der Fehlerfreiheit der Agenten ab. Laut Google DeepMind überprüften die Agenten ihre eigene Arbeit im Anschluss selbst und markierten lediglich rund 1 Prozent des Beweiscodes für eine manuelle Begutachtung durch Menschen.
Um sicherzustellen, dass das System sicheren Code von fehlerhaftem Code unterscheiden kann, baute das Team zwei echte Fehler, die inzwischen behoben sind, wieder in eine isolierte Kopie von libsignal ein. In beiden Fällen lieferte das System einen verifizierten Beweis dafür, dass die fehlerhafte Version unsicher war. Der CTO von Signal, Ehren Kret, der im Beitrag zitiert wird, sieht darin einen „bedeutenden Durchbruch“. Die Verifikationsartefakte wurden als Open Source veröffentlicht.
Die Grenzen – schwarz auf weiß festgehalten
Der technische Bericht legt präzise dar, was das System nicht garantiert. Die symbolischen Beweise setzen perfekte Kryptografie voraus und treffen keine Aussage über die rechnerische Vertraulichkeit der einzelnen Bytes. Die rechnerischen Schranken gelten nicht gegenüber einem Quantenangreifer. Die Schlüsselgenerierung wird nicht verifiziert. Die Beschreibung des Prozessors deckt 467 Instruktionen und 31 Systemaufrufe ab, modelliert jedoch weder Threads noch Signale oder dynamisches Verlinken. Schließlich vertraut das Gesamtergebnis dem Lean-Kernel, den kryptografischen Grundbausteinen sowie den Schnittstellenverträgen bestimmter vom Programm aufgerufener Routinen.
Unsere Einschätzung
Formale Verifikation hatte schon immer einen entscheidenden Nachteil: Sie ist für fast jede Software schlicht zu teuer. AlphaProof Code zeigt, dass Agenten den Großteil der Beweise erbringen können, solange Menschen vorgeben, was zu beweisen ist, und Lean alles Übrige rigoros prüft. Das ist eher ein Methodenwechsel als eine isolierte Meisterleistung: Das Vertrauen verlagert sich von den fehlbaren Agenten auf einen mechanischen Verifizierer. Doch das Resultat beschränkt sich auf einen eng umrissenen Rahmen: ein kleines Kommandozeilen-Testprogramm, eine spezifische Architektur und klar definierte kryptografische Annahmen. Der beanspruchte Pionierstatus und der tatsächliche Rechenaufwand müssen noch von unabhängigen Teams begutachtet werden – zumal Google DeepMind nicht angibt, ob das Werkzeug selbst künftig Dritten zur Verfügung gestellt wird. Für Hersteller kritischer Software stellt sich nun eine sehr praktische Frage: Wer schreibt und prüft künftig die Spezifikationen – was fortan die primäre menschliche Aufgabe bleibt?
Quellen
- Google DeepMind — Introducing AlphaProof Code: a breakthrough in verifying complex software at depth (10. November 2026) Primärquelle
- Google DeepMind — AlphaProof Code: Verifying Signal's Security at the Machine-Code Level (technischer Artikel und Lean-Entwicklung) Primärquelle
- The Register — Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques Sekundärquelle
Eine Primärquelle stammt direkt von dem betreffenden Unternehmen, Labor oder der Organisation. Eine Sekundärquelle gibt die Information wieder, ohne ihr Urheber zu sein: Wir kennzeichnen sie als solche. Einen Fehler entdeckt? Lesen Sie unsere Korrekturrichtlinie.
