AlphaProof Code verifiziert Signal-Code formal

Google DeepMind hat ein Verfahren vorgestellt, das erstmals eine breit eingesetzte kryptografische Implementierung vollständig formal verifiziert. Forscher des Unternehmens nutzten dazu AlphaProof Code, ein agentisches System für formale Verifikation, das menschliche Sicherheitsexpertise mit mehreren KI-Agenten verbindet. Das Team prüfte damit den Schlüsselcode des Signal-Protokolls, das in Diensten wie Signal und Google Messages Milliarden private Konversationen absichert. Der Durchbruch besteht darin, nicht nur das Design des Protokolls, sondern den tatsächlich ausgeführten Code mathematisch auf zentrale Sicherheitseigenschaften hin zu beweisen. In der Praxis zerlegten die Forscher die Arbeit wie in einem Forschungsteam: Menschen und Modelle formulierten gemeinsam die Sicherheitsziele als formale Spezifikationen, die anschließend vollständig von Menschen überprüft wurden. Danach führten KI-Agenten auf Basis von Gemini Carbon die Beweise durch und erzeugten mehr als sechs Millionen Zeilen in der Beweissprache Lean. Die Agenten überprüften die Beweise zusätzlich selbst und markierten nur rund ein Prozent des Codebestands für eine manuelle Nachprüfung; den Rest validierte Lean automatisch. Damit konzentrierten sich die Spezialisten auf die Stellen, an denen menschliches Urteil entscheidend ist. Der eigentliche Gewinn liegt in der Verbindung von Entwurf und Implementierung. Viele Angriffe entstehen nicht im theoretischen Protokollentwurf, sondern in der daraus erzeugten Software. AlphaProof Code bewies, dass die kompilierte Implementierung Eigenschaften wie den Schutz von Nachrichten vor und nach einer vorübergehenden Kompromittierung eines Geräts erfüllt. Das Verfahren dauerte laut DeepMind vier Wochen. Solche Verifikationen haben früher Expertenteams häufig Jahre gekostet. Zur Kontrolle der Beweiskraft bauten die Autoren zwei bekannte, bereits behobene Schwachstellen in eine isolierte Version des Signal-Codes ein. In beiden Fällen lieferte AlphaProof Code einen maschinell überprüfbaren Beweis, dass die jeweilige Version unsicher war. Die Arbeit wurde von einem DeepMind-Team unter Beteiligung von Swarat Chaudhuri und Pushmeet Kohli sowie weiteren Forschern getragen. Rückmeldungen von Signal unterstreichen die praktische Relevanz. Der Fall zeigt, dass formale Verifikation von Hochrisikosoftware durch KI-Agenten deutlich skalierbarer werden kann. Kryptografische Protokolle sind Grundlage digitaler Kommunikation, von Online-Banking bis Webzugriff; eine einzige Implementierungslücke kann Millionen betreffen. Die Verifikation des Signal-Codes gilt deshalb als Markstein für vertrauenswürdige Software, deren Korrektheit mathematisch nachgewiesen statt nur getestet wird.