AlphaProof Code: Google-KI beweist Sicherheit von Signals libsignal

Beweis statt Test

Tests und Audits können zeigen, dass kein Fehler gefunden wurde, aber nicht, dass es keinen gibt. Die formale Verifikation beweist dagegen wie bei einem Theorem, dass Code bestimmte Eigenschaften nicht verletzen kann. Die Methode gilt als extrem teuer: Die 2009 abgeschlossene Verifikation des Betriebssystemkerns seL4 erforderte den Aufwand von zwanzig Personenjahren.

Hier legten menschliche Experten auf Basis wissenschaftlicher Arbeiten zu Signal fest, was bewiesen werden soll. Die Agenten, die mit Gemini 4 Carbon arbeiteten, schrieben rund 6,5 Millionen Zeilen Beweis in der Sprache Lean, deren Prüfer jeden Schritt automatisch kontrolliert. Nach Angaben der Forscher schrieb keiner von ihnen selbst eine Zeile.

Im Mittelpunkt steht der „Ratchet“, der Mechanismus, der die Schlüssel fortlaufend erneuert. Die Beweise zeigen: Wer die auf einem Telefon gespeicherten Schlüssel stiehlt, kann frühere Nachrichten nicht lesen, da jeder Schlüssel aus dem vorherigen abgeleitet und danach gelöscht wird. Zudem wird die Unterhaltung wieder sicher, sobald beide Seiten neue Nachrichten ausgetauscht haben, und niemand kann sich als einer der Teilnehmer ausgeben. Zur Kontrolle bauten die Forscher zwei alte, inzwischen behobene Fehler wieder ein; das System wies nach, dass diese Versionen die Garantien nicht mehr erfüllten.

Klare Grenzen

Signals Technikchef Ehren Kret nannte das Ergebnis einen „großen Fortschritt“. Google weist dennoch auf Einschränkungen hin: Der Beweis gilt nur für Unterhaltungen zwischen zwei Personen, setzt voraus, dass die kryptografischen Grundbausteine fehlerfrei arbeiten, ohne sie zu prüfen, und bezieht sich auf eine Testversion unter Linux, nicht auf die Mobil-Apps.

Die Autoren ziehen eine grundsätzliche Lehre: Wenn Beweise billig werden, lautet die schwierige Frage, was man beweisen soll.