Google DeepMind prüft Signal-Sicherheit mit AlphaProof Code

So lief das Verfahren ab

Zunächst übersetzten die Forscher mit verschiedenen Modellen die Sicherheitsziele von Signal in eine von Menschen geprüfte mathematische Spezifikation. Anschließend erzeugten Gemini-Carbon-Agenten Lean-Code, der die Korrektheit der libsignal-Implementierung beweist. Es entstanden 6,5 Millionen Zeilen Lean; ein Audit-Durchlauf markierte Stellen, die Menschen prüfen mussten.

Das Ergebnis ist theoretisch: Es setzt perfekte Kryptografie voraus und garantiert nicht die rechnerische Geheimhaltung von Bytes. Dennoch ist es eine belastbare Aussage zur Korrektheit – und ein Schritt in Richtung einer Aufgabe, die die Beneficial AI Foundation im April gestellt hat: das Signal-Protokoll und die App mit Lean formal zu verifizieren.

Warum das wichtig ist

Formale Verifikation war bislang extrem aufwendig: Beim seL4-Mikrokernel waren es 20 Personenjahre, beim verifizierten C-Compiler CompCert sechs Jahre. Die Signal-Arbeit dauerte laut dem Paper vier Wochen mit fünf Personen und „ziemlich vielen Tokens“.

Swarat Chaudhuri von Google DeepMind sagt, das Verifizieren selbst lasse sich nun skalieren; die schwierige Frage sei, was überhaupt zu verifizieren ist – ein Prozess mit Menschen im Loop. Angesichts wachsender offensiver KI-Fähigkeiten und vieler unsicherer Systeme wolle man die Methode künftig schon beim Softwaredesign und für Code allgemein einsetzen. „Die nächste Grenze ist nicht der Beweis, sondern die Spezifikation“, so Chaudhuri.