Wie Wired berichtet, lief das Ganze als eine Art Proof-of-Concept-Projekt in nur vier Wochen.
Google DeepMind zufolge teilt AlphaProof Code die formale Verifikation so auf wie ein Forschungsteam: Menschliche Experten entscheiden gemeinsam mit der KI, was bewiesen werden soll, und eine Gruppe von KI-Agenten führt die Beweise aus.
Nicht nur Design, sondern laufender Code
Der Unterschied zu früheren Verifikationen liegt weniger im Beweisziel als im Weg dorthin. Laut Google DeepMind übersetzten die Forscher die Sicherheitsziele von Signal mit mehreren Modellen in formale mathematische Spezifikationen – und menschliche Experten prüften jede einzelne davon. Deshalb führte das Team zwei bereits behobene echte Fehler wieder in eine isolierte Version des Signal-Codes ein, wie Google DeepMind berichtet. So ließ sich testen, ob AlphaProof Code korrekten von fehlerhaftem Code unterscheiden kann – eine Frage, die sich am Papier nicht beantworten lässt.
In den untersuchten Teilen des Signal-Protokolls fand die Analyse von Google DeepMind keine neuen Schwachstellen, wie Wired berichtet. Ein Prüfer, der nur Ja sagt, wäre wertlos; dieser hier sagt auch Nein, wenn es Nein heißen muss.
DeepMind hat nicht den gesamten Signal-Code verifiziert, wie ZDNET berichtet. Der Test sei laut DeepMind dennoch ein Schritt zu einer besseren Sicherheitsinfrastruktur. Das klingt nach einer Einschränkung, die man nicht wegdiskutieren sollte.
Wired zufolge erlebt KI-gestützte formale Verifikation gerade einen Aufschwung. Gleichzeitig bleibt laut Wired unklar, wie praktikabel sie für den breiten Einsatz und wie wirksam sie bei der Absicherung großer Codemengen ist. Die offene Frage in der Tech-Branche ist Wired zufolge, ob KI-automatisierte formale Verifikation wirklich skalieren kann und ob das zu tragbaren Kosten möglich ist.
Die Forscher veröffentlichen die von ihnen entwickelte Spezifikation und den Beweis für die Signal-Protokollanalyse als Open Source, um andere Arbeiten zur formalen Verifikation zu unterstützen.