Formale Verifikation nimmt kein Vertrauen weg, sie verkleinert es
Serguey Asael Shinder2 Min. LesezeitGeorge und Kev haben auf ethresear.ch den ersten Teil einer Analyse der Trusted Computing Base von Ethereum veröffentlicht, mit Dank an Alex Hicks. Die Rahmung ist das Wertvolle. Ihre Motivation ist unverblümt - "es ist 2026, und KI zerlegt neuerdings das Internet", und formale Verifikation sehe für Verteidiger nach dem langfristigen Vorteil aus -, doch die bequeme Fassung dieser Behauptung verweigern sie sofort.
Die vorgeschlagene Linse ist die TCB: jede Komponente, Spezifikation, jedes Werkzeug und jede Annahme, der vertraut statt bewiesen wird - genau das, was Menschen weiterhin prüfen müssen. Formale Verifikation, so schreiben sie klar, kann die TCB nicht beseitigen, sie kann sie deutlich verkleinern. Die lohnende Frage ist also nicht, ob ein Client verifiziert ist, sondern wie seine TCB danach aussieht.
Der Rahmen ist bewusst eng: nicht das Ethereum-Protokoll, das sie als umfangreich und komplex bezeichnen, sondern ein abstrakter Ethereum-Client. Zwei Themen tragen den Beitrag - wie Software in Module zerlegt wird, die sich formal verifizieren lassen, und wie man Verifikation von Ende zu Ende erreicht statt einer Sammlung geprüfter Teile. Ihr Beweisassistent ist Lean4, laut Text ein Zeichen der Zeit und keine Voraussetzung: das Argument hält mit jedem Beweissystem.
Was das bedeutet
"Formal verifiziert" ist auf dem Weg, ein Etikett zu werden, das keine Information mehr trägt, und die TCB-Rahmung ist das Gegenmittel. Ein Beweis besteht immer relativ zu einer Spezifikation, einem Compiler, einer Laufzeitumgebung und einem Satz Annahmen - ist die Spezifikation falsch, garantiert der Beweis, dass der Code den Fehler getreu umsetzt. Die Frage, was vertraut bleibt, verwandelt ein Werbeadjektiv in eine Liste, und eine Liste kann man prüfen, bestreiten und absichtlich kürzen.
Beim Thema Ende-zu-Ende liegt die eigentliche Schwierigkeit, und es ist ein bekanntes Versagen auch in gewöhnlicher Technik. Module einzeln zu verifizieren und dann zu komponieren lässt die Schnittstellen unbewiesen - und dort sitzen die interessanten Fehler; eine Reihe grüner Modulbeweise verträgt sich bestens mit einem kaputten System. Das ist derselbe strukturelle Punkt wie bei einer Schutzmaßnahme, deren sichtbare Hälfte installiert ist und deren entscheidende nie läuft: die Teile bestehen, das Ganze nicht.
Wer Sicherheitsaussagen über Clients liest, bekommt aus diesem Beitrag eine kurze Frage: was steckt in der TCB, und wer hat es geprüft? Ein Client-Team, das mit einer konkreten Liste antwortet - diese Spezifikation, dieser Compiler, diese Annahmen über die Ausführungsumgebung -, betreibt Verifikation. Wer "wir nutzen Lean4" antwortet, nennt ein Werkzeug. Teil 2 wird das vermutlich vom Client auf das Protokoll ausweiten, und dort werden die Annahmen wirklich schwierig.