Google DeepMind nutzt KI zur formalen Verifizierung von Signals kryptografischem Code

KI-Agenten verifizieren Signals Implementierung

AlphaProof Code ist ein agentisches Multi-LLM-Framework für die formale Verifizierung. Es beweist mathematisch, dass Code fehlerfrei und korrekt läuft. Die Forscher von Google DeepMind nutzten es, um die tatsächliche Implementierung des kryptografischen Signal-Protokolls zu untersuchen, statt sich auf den Entwurf des Protokolls zu beschränken.

Im Mittelpunkt standen Sicherheitseigenschaften wie der Schutz von Nachrichten vor und nach einer vorübergehenden Kompromittierung eines Geräts. Laut Google DeepMind übersetzten die Forscher die Sicherheitsziele von Signal zunächst mithilfe einer Kombination verschiedener Modelle in formale mathematische Spezifikationen. Menschliche Experten prüften jede Spezifikation, bevor die Beweisarbeit begann.

Von Gemini Carbon angetriebene KI-Agenten erzeugten anschließend mehr als sechs Millionen Zeilen Lean-Code. Lean ist eine Computersprache, mit der sich die Korrektheit von Code mathematisch beweisen lässt. Die Agenten prüften außerdem die Beweise und ermittelten Bereiche, die eine zusätzliche menschliche Kontrolle erforderten. Nach Angaben von Google DeepMind betrafen diese Bereiche ein Prozent der Codebasis, während Lean den Rest automatisch überprüfte.

Ein vierwöchiger Prozess für eine langjährige Sicherheitsherausforderung

Kryptografische Protokolle unterstützen digitale Kommunikation, etwa beim Online-Banking und beim Surfen im Web. Eine einzige Schwachstelle kann Millionen Menschen gefährden. Experten analysieren solche Systeme daher seit Jahrzehnten formal, doch die Verifizierung von Protokollen konzentrierte sich meist auf die Entwurfsebene.

Google DeepMind zufolge überbrückt der Ansatz die Lücke zwischen einem kryptografischen Entwurf und dem kompilierten Code, der auf Geräten läuft. Dadurch wird die Verifizierung deutlich komplexer, da zwischen dem vorgesehenen Entwurf und seiner Implementierung Schwachstellen entstehen können.

Trotz dieser Komplexität dauerte der Verifizierungsprozess nach Angaben des Unternehmens vier Wochen. Vergleichbare Aufgaben durch Expertenteams nehmen traditionell Jahre in Anspruch. Um zu testen, ob AlphaProof Code korrekten von fehlerhaftem Code unterscheiden kann, führten die Forscher zwei reale, zuvor behobene Fehler erneut in eine isolierte Version des Signal-Codes ein. In beiden Fällen erzeugte das System einen maschinell geprüften Beweis dafür, dass die fehlerhafte Version unsicher war.

„KI-Agenten einzusetzen, um laufenden Code in gültige Lean-Theoreme zu übersetzen, ist ein großer Durchbruch“, sagte Ehren Kret, Chief Technology Officer von Signal, laut der Ankündigung von Google DeepMind. Eine rigorose Verifizierung der Implementierung des Signal-Protokolls gebe Signal größeres Vertrauen in die Datenschutzgarantien seines Codes, erklärte Kret.

Was die Arbeit für die Softwaresicherheit bedeuten könnte

Google DeepMind zufolge könnte die Forschung dazu beitragen, die formale Verifizierung auf Unternehmen, Regierungen und kritische Infrastrukturen auszuweiten, während die durch KI getriebenen Sicherheitsbedrohungen zunehmen. Als mögliche Einsatzbereiche nennt das Unternehmen Systeme wie die Firmware medizinischer Geräte und Software für Stromnetze.

Das Unternehmen erklärt außerdem, AlphaProof Code könne Nutzern dabei helfen, zunächst eine Spezifikation zu erstellen und anschließend autonom zu beweisen, dass eine Implementierung diese erfüllt. Jeder Beweis wird dabei von Lean geprüft. Google DeepMind hat seine Artefakte zur formalen Verifizierung zur Nutzung durch die Community als Open Source veröffentlicht, betont jedoch, dass die Skalierung der Techniken weitere Forschung erfordert.

Die Arbeit wird als Grundlage für die Verbindung formaler Verifizierung mit automatisierten Verteidigungsagenten wie CodeMender präsentiert. Für Nutzer liegt die unmittelbare Bedeutung in der zusätzlichen mathematischen Absicherung, die für den zentralen kryptografischen Code von Signal beansprucht wird. Für den breiteren Softwaremarkt weist die Forschung auf eine Möglichkeit hin, tiefe, maschinell geprüfte Verifizierung auf Produktivsysteme anzuwenden. Bisher war dafür traditionell ein erheblicher manueller Aufwand erforderlich.