Google DeepMinds AlphaProof Code verifiziert Signals kryptografisches Protokoll formal

Google DeepMind sagt, es habe einen Meilenstein in der Softwaresicherheit erreicht, der lange als große Herausforderung galt: Seine Forscher führten KI-Agenten dazu, zentrale Sicherheitseigenschaften des tatsächlichen Codes zu beweisen, auf dem das Signal-Protokoll basiert – die Technologie, die Milliarden privater Gespräche in Apps wie Signal und Google Messages schützt, indem sie Nachrichten Ende-zu-Ende verschlüsselt, sodass nur Absender und beabsichtigter Empfänger sie lesen können. Die Ankündigung wurde von Pushmeet Kohli und Swarat Chaudhuri im Google DeepMind Blog veröffentlicht.

Das Ergebnis wurde mit AlphaProof Code erzielt, einem neuartigen agentischen Framework für formale Verifizierung in beispielloser Tiefe, das menschliche Expertise mit KI-Agenten kombiniert. Formale Verifizierung – der mathematische Nachweis, dass Code fehlerfrei korrekt läuft – ist der höchste Standard der Sicherheitszusicherung, aber sie ist schwierig und oft arbeitsintensiv. Konventionelles Testen stichprobenartig das Verhalten eines Programms; ein formaler Beweis schließt Fehler über jede mögliche Ausführung aus – ein Sicherheitsniveau, dessen Erzeugung so kostspielig ist, dass es selten breit eingesetzte Software erreicht hat.

Laut dem Unternehmen markiert die Arbeit das erste Mal, dass KI verwendet wurde, um ein breit eingesetztes kryptografisches Protokoll in dieser Tiefe formal zu verifizieren. Es ist auch das erste Mal, dass die Implementierung eines breit eingesetzten Protokolls dieser Art überhaupt mit einer Methode – mit oder ohne KI – formal verifiziert wurde.

Wie Google DeepMind Signal verifizierte

AlphaProof Code ist ein Multi-LLM-agentisches Framework, das die Arbeit der formalen Verifizierung so aufteilt, wie es ein Forschungsteam tun würde: Menschliche Experten entscheiden gemeinsam mit der KI, was bewiesen werden soll, und eine Gruppe von KI-Agenten führt die Beweise durch.

Zunächst arbeiteten die Google-DeepMind-Forscher mit einer Mischung von Modellen zusammen, um Signals Sicherheitsziele in formale mathematische Spezifikationen zu übersetzen, wobei menschliche Experten jede einzelne prüften. Anschließend erstellten von Gemini Carbon angetriebene Agenten die Beweise und erzeugten dabei mehr als sechs Millionen Zeilen Lean, eine Computersprache, die die Korrektheit von Code mathematisch beweist.

Die Agenten prüften anschließend den Beweis und kennzeichneten die Bereiche, die eine zweite Prüfung durch einen Menschen erforderten – nur ein Prozent der Codebasis, was das Unternehmen als enorme Zeitersparnis beschreibt. Da Lean den Rest automatisch überprüft, konnten sich die Experten auf die Prüfung konzentrieren, wo menschliches Urteilsvermögen am wichtigsten ist.

Sicherheitsnachweis bis zum laufenden Code

Kryptografische Protokolle bilden das Fundament nahezu der gesamten digitalen Kommunikation, vom Online-Banking bis zum Surfen im Web, und ein einziger Fehler kann gleichzeitig Millionen von Menschen gefährden. Deshalb analysieren Experten sie seit Jahrzehnten formal, wobei die meisten Protokollverifizierungen auf der Entwurfsebene stehen blieb.

Die Agenten von Google DeepMind gingen weiter: Sie bewiesen, dass der kompilierte Code zentrale Sicherheitseigenschaften erfüllt – etwa den Schutz von Nachrichten vor und nach einer vorübergehenden Kompromittierung eines Geräts, Garantien, die Kryptografen als Forward Secrecy und Post-Compromise-Sicherheit kennen – bis hin zum exakten Code, der auf den Geräten läuft. Reale Schwachstellen verstecken sich oft in der Lücke zwischen Entwurf und Implementierung, und die Überbrückung dieser Lücke macht diese Beweise erheblich komplexer.

Selbst bei diesem Komplexitätsgrad dauerte der Verifizierungsprozess nur vier Wochen – eine Aufgabe, die laut dem Unternehmen historisch Expertenteams Jahre kostete – und belegte, dass Signals kryptografischer Kerncode die vom Forschungsteam spezifizierten Schutzmechanismen liefert.

Um zu bestätigen, dass AlphaProof Code korrekten Code von fehlerhaftem Code unterscheiden kann, führte das Team zwei echte, zuvor behobene Fehler in eine isolierte Version von Signals Code wieder ein. In beiden Fällen erzeugte das System einen maschinell geprüften Beweis, dass die fehlerhafte Version unsicher war – eine Prüfung, die zählt, denn ein Verifizierer, der fehlerhaften Code nicht kennzeichnen kann, würde falsche Sicherheit vermitteln.

In AlphaProof Code helfen KI-Agenten den Nutzern, eine Spezifikation zu schreiben, und beweisen dann autonom, dass die Implementierung sie erfüllt. Jeder Beweis wird von Lean überprüft, um die Arbeit der Agenten zu verifizieren.

Die Reaktion von Signal

„Während sich frühere formale Verifizierungen auf kleinere Teile des Codes konzentrierten, ermöglicht Google DeepMinds Ansatz eine erhebliche Ausweitung", sagte Ehren Kret, Chief Technology Officer von Signal. „Der Einsatz von KI-Agenten, um laufenden Code in gültige Lean-Theoreme zu übersetzen, ist ein großer Durchbruch. Da KI-gestützte Sicherheitsbedrohungen zunehmen, gibt uns die rigorose Verifizierung der Signal-Protokollimplementierung noch mehr Vertrauen in die Datenschutzzusicherungen unseres Codes."

Die Zukunft der Sicherheit

Google DeepMind argumentiert, dass die Bewältigung dieser lange bestehenden Herausforderung zeigt, wie KI erstklassige Sicherheitszusicherung für Unternehmen, Regierungen und kritische Infrastruktur bringen kann und so zur Abwehr agentengesteuerter Cyber-Bedrohungen beiträgt. Die Verifizierung von Signals Kryptografiekern, so das Unternehmen, lege den Grundstein, um andere lebenswichtige Systeme zu sichern – von der Firmware medizinischer Geräte bis zur Software von Stromnetzen.

Die Skalierung dieser Techniken erfordert weitere Forschung. In Kombination mit automatisierten Verteidigungsagenten wie CodeMender kann formale Verifizierung dazu beitragen, der Geschwindigkeit und dem Umfang moderner Cyber-Bedrohungen zu begegnen und Software zu schaffen, deren Schutzfunktionen mathematisch bewiesen sind.

Google DeepMind veröffentlicht seine Artefakte der formalen Verifizierung als Open Source für die Community, gehostet unter google-deepmind.github.io/code-verification. Das vollständige technische Paper steht als PDF zur Verfügung. Für die Sicherheitsforschungs-Community bietet diese Veröffentlichung eine Möglichkeit, die maschinell geprüften Beweise und die Methodik direkt zu inspizieren – und wie weit sich die Verifizierung in dieser Tiefe über Signal hinaus verbreitet, in die medizinischen, industriellen und Infrastruktursysteme, die das Unternehmen nennt, ist die nächste Entwicklung, die man beobachten sollte.

Danksagungen

Die Forschung wurde von Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton und Pushmeet Kohli entwickelt.

Das Team dankte Eric Wieser für seine Hilfe beim Open-Sourcing des Codes, Owen Jones für die Unterstützung im Programmmanagement sowie Martín Abadi, Christopher Henson, Katerina Hristova, Henryk Michalewski, Jonathan Protzenko und George Tsoukalas für hilfreiche Diskussionen. Die Forscher dankten außerdem Signals Rolfe Schmidt, Michael Rosenberg und Ehren Kret für ihr Feedback zur Methodik sowie Tulsee Doshi, Four Flynn, Kate Olszewska, Alicia Huang, Andy Liu, Benoit Schillings, Raluca Ada Popa, Melvin Johnson, Koray Kavukcuoglu, Demis Hassabis und Sundar Pichai für ihre Unterstützung des Projekts.