Signal-Verschlüsselung: DeepMind-KI prüft Code in vier Wochen

Was ist formale Verifikation?

Dabei wird mit Mathematik statt mit Tests gezeigt, dass Software sich wie vorgesehen verhält. Sie gilt als stärkste verfügbare Sicherheitsgarantie, war aber bisher langsam und aufwendig. Meist endet die Verifikation kryptografischer Protokolle in der Entwurfsphase. DeepMind sagt, man habe die tatsächliche Implementierung geprüft, und dort verstecken sich oft die Fehler der Praxis. Es sei die erste formale Verifikation der Implementierung eines weit verbreiteten Protokolls, mit oder ohne KI.

Wie funktioniert AlphaProof Code?

Das System kombiniert mehrere KI-Modelle mit menschlichen Experten. DeepMind-Forscher und KI-Modelle übersetzten Signals Sicherheitsziele in formale Spezifikationen, Menschen prüften jede einzelne. Agenten auf Basis von Gemini Carbon schrieben dann die Beweise: über sechs Millionen Zeilen in Lean, einer Sprache, in der ein Computer Beweise automatisch prüfen kann. Danach kontrollierten die Agenten ihre eigene Arbeit und markierten rund 1 % des Codes für eine zweite menschliche Prüfung.

Die Beweise decken etwa ab, dass Nachrichten vor und nach einer vorübergehenden Kompromittierung eines Geräts geschützt bleiben.

Hat die KI Fehler gefunden?

In den untersuchten Teilen von Signal tauchten keine neuen Schwachstellen auf. Um zu testen, ob das System guten von schlechtem Code unterscheidet, bauten die Forscher zwei echte, bereits behobene Fehler in eine isolierte Version des Codes wieder ein. In beiden Fällen lieferte das System laut DeepMind einen maschinell geprüften Beweis, dass die fehlerhafte Version unsicher war.

Grenzen gibt es: Die komplette Signal-App wurde nicht verifiziert, und DeepMind profitierte von früherer Verifikationsarbeit der Signal Foundation. Signal-Technikchef Ehren Kret sagte, diese habe kleinere Codeteile betroffen, DeepMinds Ansatz erlaube eine deutliche Ausweitung.

Forscher Swarat Chaudhuri will vermeiden, dass die KI Ziele und Beweise selbst schreibt und sich quasi selbst benotet. Deshalb prüften Menschen die Spezifikationen und markierten Abschnitte.

Offen bleibt, ob sich das skalieren lässt und was es kostet. DeepMind führte die Analyse kostenlos als Forschungsprojekt durch und nennt weder Kosten noch Pläne für ein kommerzielles Produkt. Die Verifikationsartefakte werden quelloffen veröffentlicht. Langfristig könnte der Ansatz auch Firmware von Medizingeräten und Software für Stromnetze erreichen.