Vitalik: Was ist der Schlüssel zur nächsten Phase von Ethereum?

Autor: Vitalik Buterin

Übersetzt von: Jiahua, ChainCatcher

Besonderer Dank gilt Yoichi Hirai, Justin Drake, Nadim Kobeissi und Alex Hicks für ihr Feedback und ihre Rezension.

In den letzten Monaten hat sich ein neues Programmierparadigma in den Entwicklerkreisen von Ethereum und vielen anderen Bereichen der Informatik rasant durchgesetzt: das direkte Schreiben von Code in sehr hardwarenahen Sprachen (wie EVM-Bytecode, Assemblersprache) oder Lean und die Verwendung von automatisch überprüfbaren mathematischen Beweisen, die in Lean geschrieben sind, um die Korrektheit zu bestätigen.

Bei korrekter Anwendung birgt dies nicht nur das Potenzial, extrem effizienten Code zu erzeugen, sondern ist auch wesentlich sicherer als bisherige Programmiermethoden. Yoichi Hirai bezeichnet dies als die „ultimative Form der Softwareentwicklung“.

Dieser Artikel versucht, die zugrunde liegenden Prinzipien aufzuzeigen, zu untersuchen, was die formale Verifikation von Software leisten kann, und ihre Schwächen und Grenzen in Ethereum und anderen Bereichen zu identifizieren.

Was ist formale Verifikation?

Formale Verifikation bezeichnet das Schreiben von Beweisen für mathematische Theoreme, die automatisch überprüft werden können. Ein relativ einfaches, aber dennoch interessantes Beispiel ist der Grundsatz der Fibonacci-Folge: Jede dritte Zahl ist gerade, die übrigen sind ungerade.

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 …

Ein einfacher Weg, dies zu beweisen, ist die vollständige Induktion, bei der man jeweils drei Schritte vorwärts geht.

Zunächst der Basisfall. Sei F1 = F2 = 1, F3 = 2. Durch Beobachtung sehen wir, dass die Aussage („Fi ist gerade, wenn i ein Vielfaches von 3 ist, ansonsten ist es ungerade“) vor x = 3 gilt.

Als Nächstes betrachten wir den Induktionsfall. Angenommen, die Aussage gilt vor 3k+3, d. h., wir wissen bereits, dass die Parität von F3k+1, F3k+2 und F3k+3 ungerade, ungerade bzw. gerade ist. Wir können die Parität der nächsten Dreiergruppe von Zahlen berechnen:

F3k+4 = F3k+2 + F3k+3 = ungerade + gerade = ungerade

F3k+5 = F3k+3 + F3k+4 = gerade + ungerade = ungerade

F3k+6 = F3k+4 + F3k+5 = ungerade + ungerade = gerade

Aus der Erkenntnis, dass die Aussage vor 3k+3 gilt, schließen wir, dass sie auch vor 3k+6 gilt. Dieses Vorgehen lässt sich beliebig oft anwenden, um sich zu vergewissern, dass diese Regel für alle ganzen Zahlen gilt.

Dieses Argument mag Menschen überzeugen. Was aber, wenn man etwas hundertmal Komplexeres beweisen und absolut sichergehen will, keinen Fehler gemacht zu haben? Nun, man kann einen Beweis liefern, der auch einen Computer überzeugt.

So wird es präsentiert:

-- Fibonacci mit fib 0 = 0, fib 1 = 1, fib 2 = 1 (Indizes um 1 versetzt)

def fib : Nat → Nat

| 0 => 0

| 1 => 1

| n + 2 => fib (n + 1) + fib n

-- Behauptung: fib (3k+1) ist ungerade, fib (3k+2) ist ungerade, fib (3k+3) ist gerade.

-- Äquivalent dazu: Jede dritte Fibonacci-Zahl, beginnend mit Fibonacci 3, ist gerade.

-- Wir beweisen alle drei gleichzeitig durch Induktion über k, da jeder Fall

-- des nächsten Blocks wird aus dem vorherigen Block gebaut.

Satz fib_triple (k : Nat) :

fib (3 * k + 1) % 2 = 1 ∧

fib (3 * k + 2) % 2 = 1 ∧

fib (3 * k + 3) % 2 = 0 := by

Induktion k mit

| Null => entscheiden

| succ k ih =>

-- Schreibe die neuen Indizes in die Form (etwas) + 2 um, damit die Fibonacci-Folge entfaltet wird.

Verfeinern ⟨?_, ?_, ?_⟩

· show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1

Omega

· show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1

Omega

· show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)

+ (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0

Omega

Es handelt sich um dieselbe Argumentationslogik, nur in Lean ausgedrückt. Lean ist eine Programmiersprache, die häufig zum Schreiben und Überprüfen mathematischer Beweise verwendet wird.

Dies unterscheidet sich aus gutem Grund von dem oben genannten "menschlichen" Beweis: Was für einen Computer intuitiv ist (im traditionellen Sinne von "Computer", d. h. ein "deterministisches" Programm, das aus Wenn-Dann-Anweisungen besteht, und nicht aus großen Sprachmodellen), ist grundlegend anders als das, was für Menschen intuitiv ist.

Im obigen Beweis haben Sie nicht die Tatsache hervorgehoben, dass fib(3k+4) = fib(3k+3) + fib(3k+2), sondern vielmehr, dass fib(3k+3) + fib(3k+2) ungerade ist, während eine Strategie in Lean namens Omega dies automatisch mit ihrem Wissen über die Definition von fib(3k+4) kombiniert.

Bei komplexeren Beweisen muss man manchmal explizit angeben, welches mathematische Gesetz den aktuellen Schritt erlaubt, und manchmal muss man obskure Namen wie Prod.mk.inj verwenden.

Andererseits kann man riesige Polynomausdrücke in einem einzigen Schritt erweitern und ihre Gültigkeit mit einem einzigen Ausdruck wie „omega“ oder „ring“ beweisen.

Diese unintuitive und umständliche Natur erklärt weitgehend, warum das Gebiet trotz seit fast 60 Jahren existierender maschinenüberprüfbarer Beweise ein Nischengebiet bleibt. Andererseits werden durch die rasante Entwicklung der künstlichen Intelligenz viele ehemals unmögliche Dinge nun schnell möglich.

Wenn mathematische Beweise anfangen, Code zu schützen

Bis hierhin mag man denken: Nun, Computer können Beweise mathematischer Theoreme überprüfen, also können wir endlich feststellen, welche verrückten neuen Schlussfolgerungen über Primzahlen wahr sind und welche nur Fehler in hundertseitigen PDF-Abhandlungen sind.

Vielleicht können wir sogar herausfinden, ob Shinichi Mochizukis Ansichten zur ABC-Vermutung richtig sind!

Aber mal abgesehen von der Neugier, na und?

Es gibt viele mögliche Antworten. Eine Antwort, die mir jedoch sehr wichtig ist, ist die Überprüfung der Korrektheit von Computerprogrammen, insbesondere solcher, die kryptografische oder sicherheitsrelevante Aufgaben ausführen.

Schließlich sind Computerprogramme mathematische Objekte, daher ist der Beweis, dass ein Computerprogramm auf eine bestimmte Weise abläuft, selbst ein mathematischer Lehrsatz.

Nehmen wir beispielsweise an, Sie möchten beweisen, ob eine verschlüsselte Kommunikationssoftware wie Signal tatsächlich sicher ist. Sie können mathematisch definieren, was „sicher“ in diesem Kontext bedeutet.

Im Prinzip beweisen Sie, dass – unter der Annahme, dass bestimmte kryptografische Voraussetzungen erfüllt sind – nur diejenigen, die den privaten Schlüssel besitzen, Informationen über den Inhalt der Nachricht erhalten können. In der Realität spielen jedoch viele verschiedene Sicherheitsaspekte eine entscheidende Rolle.

Es gibt tatsächlich ein Team, das genau dieses Problem zu lösen versucht! Eines ihrer Sicherheitstheoreme sieht folgendermaßen aus:

Satz passive_secrecy_le_ddh

(g : G)

(adv : PassiveAdversary G SK) :

passiveSecrecyAdvantage (F := F) g adv ≤

ProbComp.boolDistAdvantage

(DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))

(DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

Hier eine Zusammenfassung der Bedeutung von Leanstral:

Der Satz von passivesecrecycle_ddh ist eine kompakte Reduktion, die zeigt, dass die passive Nachrichtenvertraulichkeit von X3DH mindestens so schwer zu beweisen ist wie die DDH-Annahme im Random-Oracle-Modell. Wenn ein Angreifer die passive Nachrichtenvertraulichkeit von X3DH brechen kann, kann er auch DDH brechen.

Da wir davon ausgehen, dass DDH schwer zu knacken ist, ist X3DH auch gegen passive Angriffe sicher. Dieser Satz beweist, dass ein Angreifer, der die Schlüsselaustauschnachrichten von Signal passiv beobachten kann, den von Signal erzeugten Sitzungsschlüssel mit einer Wahrscheinlichkeit von mehr als vernachlässigbar wenig von einem zufälligen Schlüssel unterscheiden kann.

Kombiniert man dies mit einem korrekten Beweis für die Implementierung der AES-Verschlüsselung, erhält man den Beweis, dass die Verschlüsselung des Signal-Protokolls gegen passive Angreifer sicher ist.

Ähnliche Projekte haben auch bewiesen, dass Implementierungen von TLS und anderen Teilen der browserinternen Kryptographie sicher sind.

Wenn Sie eine vollständige formale End-to-End-Verifikation durchführen, beweisen Sie nicht nur, dass eine theoretische Beschreibung des Protokolls sicher ist, sondern auch, dass der von den Benutzern ausgeführte Code in der Praxis sicher ist.

Aus der Sicht des Benutzers erhöht dies das Vertrauen erheblich: Um dem Code vollständig vertrauen zu können, muss man nicht die gesamte Codebasis überprüfen; es genügt, die Aussagen darüber zu überprüfen, die sich als wahr erwiesen haben.

Es gibt jedoch einige wichtige Einschränkungen zu beachten, insbesondere hinsichtlich der Bedeutung des entscheidenden Wortes „sicher“.

Man vergisst leicht, die wirklich wichtigen Aussagen zu beweisen. Man stellt leicht fest, dass die zu beweisenden Aussagen manchmal nicht einfacher zu beschreiben sind als der Code selbst.

Es ist leicht, unbeabsichtigt Annahmen in den Beweis einzuführen, die sich letztendlich als falsch erweisen. Ebenso leicht kann man entscheiden, dass nur ein Teil des Systems formal bewiesen werden muss, nur um dann auf schwerwiegende Sicherheitslücken in anderen Teilen (sogar in der Hardware) zu stoßen.

Selbst die Lean-Implementierung kann Fehler enthalten. Doch bevor wir all diese lästigen Details besprechen, wollen wir uns zunächst mit dem idealen Szenario befassen, das sich aus einer korrekten und perfekten formalen Verifizierung ergeben könnte.

Formale Verifizierung – entwickelt für maximale Sicherheit

Fehler im Computercode sind beängstigend.

Wenn man Kryptowährung in unveränderliche Blockchain-Smart-Contracts einbindet und Nordkorea automatisch alle Gelder abziehen kann, sobald ein Fehler im Code auftritt, und man keine Möglichkeit hat, dagegen vorzugehen, werden Fehler im Code noch beängstigender.

Wenn das alles in Zero-Knowledge-Beweisen verpackt ist, werden Fehler noch beängstigender, denn wenn es jemandem gelingt, in das Zero-Knowledge-Beweissystem einzudringen, kann er das gesamte Geld abgreifen, und wir haben keine Ahnung, was schiefgelaufen ist (noch schlimmer, wir wissen nicht einmal, wann es schiefgelaufen ist).

Wenn wir in zwei Jahren über leistungsstarke KI-Modelle wie Claude Mythos verfügen, die diese Fehler automatisch erkennen können, werden Fehler im Code noch viel beängstigender.

Die Reaktion einiger Menschen auf diese Realität besteht darin, sich für die Aufgabe der Grundidee von Smart Contracts auszusprechen und sogar zu glauben, dass das Internet kein Bereich sein kann, in dem Verteidiger einen asymmetrischen Vorteil gegenüber Angreifern haben können.

Einige Zitate:

Um ein System abzusichern, müssen Sie mehr Token ausgeben, als der Angreifer zur Ausnutzung der Schwachstellen verwendet.

Und:

Unsere Branche basiert auf deterministischem Code. Wir schreiben ihn, testen ihn, stellen ihn bereit und sind zuversichtlich, dass er funktioniert – aber meiner Erfahrung nach wird dieser Vertrag nicht eingehalten.

Bei den führenden Betreibern von Unternehmen, die ausschließlich auf KI setzen, ist die Codebasis zu etwas geworden, dem man "vertrauen" muss, und man kann die Erfolgswahrscheinlichkeit nicht mehr genau bestimmen.

Noch schlimmer ist, dass manche Leute glauben, die einzige Lösung sei, Open Source aufzugeben.

Für die Cybersicherheit wäre dies eine düstere Zukunftsprognose. Insbesondere für diejenigen unter uns, denen die Dezentralisierung und Freiheit des Internets am Herzen liegen, ist dies ein äußerst pessimistischer Ausblick.

Der gesamte Cypherpunk-Geist basiert im Grunde auf der Idee, dass im Internet die Verteidiger im Vorteil sind und der Aufbau einer digitalen "Burg" (sei es durch Verschlüsselung, Signaturen oder Beweise) viel einfacher ist als deren Zerstörung.

Verlieren wir das, dann kann Internetsicherheit nur noch durch Skaleneffekte, durch die weltweite Jagd auf potenzielle Angreifer und, allgemeiner gefasst, nur noch durch die Wahl zwischen Herrschaft und Zerstörung erreicht werden.

Ich sehe das anders; ich habe eine optimistischere Vision für die Zukunft der Cybersicherheit.

Ich glaube, die Herausforderungen durch leistungsstarke KI-gestützte Schwachstellenerkennung sind zwar gravierend, aber nur eine Übergangsphase. Sobald sich die Lage beruhigt hat und ein neues Gleichgewicht erreicht ist, werden wir ein Umfeld vorfinden, das für Verteidiger günstiger ist als bisher.

Mozilla teilt meine Ansicht. Um sie zu zitieren:

Möglicherweise müssen Sie die Prioritäten aller anderen Dinge neu ordnen und dieser Aufgabe anhaltende und konzentrierte Energie widmen, aber es gibt Licht am Ende des Tunnels.

Wir sind sehr stolz darauf, wie unser Team diese Herausforderung meistert, und andere werden es auch sein. Unsere Arbeit ist noch nicht getan, aber wir haben die schwierigste Phase überstanden und können eine Zukunft erahnen, die nicht nur mithalten kann, sondern deutlich besser ist.

Die Verteidiger haben endlich die Chance, einen entscheidenden Sieg zu erringen. … Die Schwächen sind begrenzt, und wir betreten eine Welt, in der wir sie endlich alle finden können.

Wenn Sie nun in Mozillas Beitrag mit Strg+F nach den Wörtern „formal“ und „Verifizierung“ suchen, erhalten Sie keine Treffer. Die positive Zukunft der Cybersicherheit hängt nicht allein von formaler Verifizierung oder einer anderen einzelnen Technologie ab.

Wovon hängt es ab? Im Wesentlichen von dieser Grafik:

Entwicklung der CVE-Schwachstellen im Laufe der Zeit

Seit Jahrzehnten haben viele Technologien zum Rückgang der Anzahl von Sicherheitslücken beigetragen:

Typsysteme

speichersichere Sprachen

Verbesserungen der Softwarearchitektur (einschließlich Sandboxing, Berechtigungskontrolle und einer allgemeineren Unterscheidung zwischen „vertrauenswürdiger Rechenbasis“ und „anderem Code“)

Bessere Testmethoden

Eine ständig wachsende Wissensdatenbank über sichere und unsichere Codierungsmuster

Eine zunehmende Anzahl vorgefertigter und geprüfter Softwarebibliotheken

Die KI-gestützte formale Verifikation sollte nicht als ein völlig neues Paradigma, sondern vielmehr als ein starker Beschleuniger für bereits im Gange befindliche Trends und Paradigmen betrachtet werden.

Formale Verifikation ist kein Allheilmittel. Sie eignet sich jedoch besonders gut für Situationen, in denen das Ziel deutlich einfacher ist als die Implementierung. Dies gilt insbesondere für einige äußerst komplexe und knifflige Technologien, die wir in der nächsten großen Ethereum-Iteration einsetzen müssen: quantenresistente Signaturen, STARKs, Konsensalgorithmen und ZK-EVMs.

STARK ist eine sehr komplexe Software. Die grundlegenden Sicherheitsfunktionen, die sie implementiert, sind jedoch leicht zu verstehen und zu formalisieren: Wenn ein Hash H auf das Programm P, die Eingabe x und die Ausgabe y zeigt, dann gilt entweder (i) der in STARK verwendete Hash-Algorithmus wurde geknackt oder (ii) P(x) = y.

So gibt es das Arklib-Projekt, das versucht, eine vollständig formal verifizierte STARK-Implementierung zu erstellen (siehe VCV-io, das die grundlegende Oracle-Computing-Infrastruktur für die formale Verifikation verschiedener anderer kryptografischer Protokolle bereitstellt, von denen viele Abhängigkeiten von STARK sind).

Noch ambitionierter ist evm-asm: ein Projekt zum Aufbau einer vollständig formal verifizierten EVM-Implementierung.

Die Sicherheitseigenschaften sind hier nicht so einfach: Im Wesentlichen geht es darum, die Äquivalenz zu einer anderen EVM-Implementierung in Lean nachzuweisen, wobei diese Implementierung so geschrieben sein kann, dass Intuitivität und Lesbarkeit maximiert werden, ohne die spezifische Laufzeiteffizienz zu berücksichtigen.

Es ist möglich, dass wir zehn EVM-Implementierungen erhalten, die alle nachweislich gleichwertig sind, und dass alle denselben fatalen Fehler aufweisen, der es einem Angreifer ermöglicht, sämtliche ETH von Adressen abzuzweigen, zu denen er keinen Zugriff hat.

Dies ist jedoch deutlich unwahrscheinlicher als die Möglichkeit, dass solche Fehler in einigen aktuellen EVM-Implementierungen vorhanden sind. Eine weitere Sicherheitseigenschaft, deren Bedeutung wir erst nach schmerzhaften Erfahrungen erkannten, nämlich die Resistenz gegen DoS-Angriffe, lässt sich ebenfalls leicht formalisieren.

Zwei weitere wichtige Bereiche sind:

Byzantinischer fehlertoleranter Konsens. Die Formalisierung aller erwarteten Sicherheitseigenschaften ist hier gleichermaßen schwierig, aber angesichts der Häufigkeit von Fehlern ist ein Versuch lohnenswert. Daher gibt es laufende Lean-Implementierungen und Beweise für Konsensprotokolle in Lean.

Programmiersprachen für Smart Contracts: siehe formale Verifikation in Vyper und Verity.

In all diesen Fällen besteht einer der größten Vorteile der formalen Verifikation darin, dass diese Beweise wirklich durchgängig sind. Typischerweise sind die lästigsten Fehler Interaktionsfehler, die an der Schnittstelle zweier unabhängig voneinander betrachteter Teilsysteme auftreten.

Für Menschen ist es zu komplex, das gesamte System von Anfang bis Ende zu durchdenken. Automatisierte Regelprüfungssysteme hingegen können das.

Formale Verifikation – geboren für Effizienz

Betrachten wir evm-asm noch einmal genauer. Es handelt sich dabei um eine EVM-Implementierung. Diese EVM-Implementierung ist jedoch direkt in RISC-V-Assembler geschrieben.

Echt.

Hier ist der ADD-Opcode:

import EvmAsm.Rv64.Program

namespace EvmAsm.Evm64

open EvmAsm.Rv64

/-- 256-Bit EVM ADD: Binär, entfernt 2 Elemente, fügt 1 Element hinzu.

Gliedmaße 0: LD, LD, ADD, SLTU (Tragen), SD (5 Anweisungen).

Gliedmaßen 1-3: LD, LD, ADD, SLTU (carry1), ADD (carryIn), SLTU (carry2), OR (carryOut), SD (jeweils 8).

Dann ADDI sp, sp, 32.

Register: x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1. -/

def evm_add : Program :=

-- Gliedmaße 0 (5 Anweisungen)

LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;

ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;

-- Gliedmaße 1 (8 Anweisungen)

LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;

ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;

-- Gliedmaße 2 (8 Anweisungen)

LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;

ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;

-- Gliedmaße 3 (8 Anweisungen)

LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;

ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;

-- sp Einstellung

ADDI .x12 .x12 32

end EvmAsm.Evm64

Die Wahl von RISC-V liegt darin begründet, dass die entwickelten ZK-EVM-Beweiser typischerweise RISC-V beweisen und Ethereum-Clients in RISC-V kompilieren. Wenn Sie also eine direkt in RISC-V geschriebene EVM-Implementierung haben, ist dies die schnellste verfügbare Lösung.

RISC-V lässt sich auch auf normalen Computern sehr effizient simulieren (und es gibt RISC-V-Laptops auf dem Markt).

Um wirklich eine durchgängige Verifizierung zu erreichen, muss man natürlich die Implementierung von RISC-V selbst (oder die Arithmetik des Beweisers) formal verifizieren, aber keine Sorge, es gibt bereits Arbeiten in diesem Bereich.

Das direkte Schreiben von Code in Assembler war vor fünfzig Jahren üblich. Seitdem haben wir diese Praxis zugunsten der Programmierung in höheren Programmiersprachen aufgegeben.

Höhere Programmiersprachen gehen zwar mit Einbußen bei der Effizienz einher, ermöglichen aber im Gegenzug ein wesentlich schnelleres Codieren und, was noch wichtiger ist, ein wesentlich schnelleres Verständnis des Codes anderer, was für die Sicherheit unerlässlich ist.

Durch die Kombination von formaler Verifikation und künstlicher Intelligenz haben wir die Möglichkeit, „in die Zukunft zurückzukehren“.

Konkret können wir eine KI Assembler-Code schreiben lassen und anschließend einen formalen Beweis verfassen, um zu überprüfen, ob der Assembler-Code die gewünschten Eigenschaften besitzt.

Die gewünschten Eigenschaften können zumindest einfach die perfekte Äquivalenz zu einer Implementierung darstellen, die auf Lesbarkeit optimiert und in einer für Menschen benutzerfreundlichen höheren Programmiersprache verfasst wurde.

Wir benötigen kein einzelnes Codeobjekt mehr, um Lesbarkeit und Effizienz in Einklang zu bringen; stattdessen haben wir zwei unabhängige Objekte: eines (die Assembler-Implementierung), das ausschließlich auf Effizienz optimiert ist und gleichzeitig die Anforderungen seiner spezifischen Ausführungsumgebung berücksichtigt; das andere (die Sicherheitsanweisung oder die Implementierung in einer höheren Programmiersprache), das ausschließlich auf Lesbarkeit optimiert ist, und dann beweisen wir die Äquivalenz zwischen den beiden durch einen mathematischen Beweis.

Die Benutzer können diesen Nachweis einmalig (automatisch) überprüfen und müssen danach nur noch die schnelle Version ausführen.

Dieser Ansatz ist unglaublich wirkungsvoll, und es gibt einen Grund dafür, dass Yoichi Hirai ihn als die „ultimative Form der Softwareentwicklung“ bezeichnet.

Formale Verifizierung ist kein Allheilmittel

In den Bereichen Kryptographie und Informatik gibt es eine Tradition, die fast so alt ist wie die Geschichte der formalen Methoden selbst: die Tradition der Kritik an formalen Methoden (oder allgemeiner, an der Abhängigkeit von „Beweisen“).

Diese Schriften sind voller praktischer Anwendungsfälle. Beginnen wir mit handschriftlichen Beweisen aus der frühen Ära der einfachen Kryptographie und beziehen wir uns dabei auf die Kritik von Menezes und Koblitz aus dem Jahr 2004:

1979 schlug Rabin eine kryptographische Funktion vor, die in gewissem Sinne "beweisbar" sicher war, was bedeutete, dass sie eine reduktionistische Sicherheitseigenschaft besaß.

Die reduktionistische Sicherheitsaussage besagt, dass jeder, der die Nachricht m aus dem Chiffretext y ermitteln kann, auch n faktorisieren kann. … Kurz nachdem Rabin sein Verschlüsselungsverfahren vorgeschlagen hatte, wies Rivest darauf hin, dass ironischerweise genau diese Eigenschaft, die dem Verfahren zusätzliche Sicherheit verleiht, im Falle eines Angreifers, der als „gewählter Chiffretext“ bekannt ist, zu einem vollständigen Zusammenbruch führen würde.

Das heißt, wenn der Angreifer Alice irgendwie dazu bringen kann, den von ihm gewählten Geheimtext zu entschlüsseln, dann kann der Angreifer die gleichen Schritte befolgen, die Sam im vorherigen Absatz verwendet hat, um n zu faktorisieren.

Menezes und Koblitz lieferten daraufhin weitere Beispiele. Das gemeinsame Muster besteht darin, dass Entwürfe, die Verschlüsselungsprotokolle „beweisbarer“ machen sollen, diese oft weniger „natürlich“ gestalten und somit die Wahrscheinlichkeit von Fehlern erhöhen, die die Entwickler nie in Betracht gezogen haben.

Kehren wir nun zu maschinenüberprüfbaren Beweisen und Code zurück. Hier ist eine Veröffentlichung aus dem Jahr 2011, die Schwachstellen in einem formal verifizierten C-Compiler aufdeckte: [Veröffentlichungstext]

Das zweite CompCert-Problem, das wir gefunden haben, manifestiert sich in zwei Fehlern, die zur Generierung des folgenden Codes führen: stwu r1, -44432(r1), wobei ein großer PowerPC-Stack-Frame zugewiesen wird.

Das Problem besteht darin, dass das 16-Bit-Verschiebungsfeld übergelaufen ist. Die PPC-Semantik von CompCert legte keine Begrenzung für die Breite dieses unmittelbaren Werts fest; sie ging davon aus, dass der Assembler Werte außerhalb des zulässigen Bereichs erkennen würde.

Es gibt auch eine Veröffentlichung aus dem Jahr 2022:

In CompCert-KVX wurde mit Commit e2618b31 ein Fehler behoben: Die „nand“-Anweisung wurde als „and“ ausgegeben; „nand“ wurde nur im seltenen Muster ~ (a & b) verwendet. Dieser Fehler wurde durch das Kompilieren zufällig generierter Programme entdeckt.

Und heute, im Jahr 2026, beschreibt Nadim Kobeissi auf folgende Weise Schwachstellen in formal verifizierter Software in Cryspen:

Im November 2025 berichtete Filippo Valsorda unabhängig davon, dass libcrux-ml-dsa v0.0.3 bei gleichen deterministischen Eingaben auf verschiedenen Plattformen unterschiedliche öffentliche Schlüssel und Signaturen erzeugte.

Der Fehler lag in der internen Wrapper-Funktion vxarqu64, die die in der Keccak-f-Permutation von SHA-3 verwendete XAR-Operation implementierte. Der Fallback-Mechanismus übergab falsche Parameter an die Schiebeoperation, wodurch der SHA-3-Digest auf ARM64-Plattformen ohne Hardware-SHA-3-Unterstützung verfälscht wurde.

Dies fällt unter einen Fehler vom Typ I: Die interne Funktion wurde zwar markiert, aber das gesamte NEON-Backend hat keinen Nachweis über Laufzeitsicherheit oder Korrektheit erbracht.

Und:

Die libcrux-psq-Bibliothek implementiert ein Post-Quantum-Pre-Shared-Key-Protokoll. In der Methode `decrypt_out` ruft der AES-GCM-128-Entschlüsselungspfad `.unwrap()` auf dem Entschlüsselungsergebnis auf, anstatt Fehler weiterzugeben. Ein fehlerhafter Chiffretext kann zum Absturz des Prozesses führen.

Alle vier dieser Probleme lassen sich in eine der folgenden beiden Kategorien einteilen:

Fälle, in denen nur ein Teil des Codes verifiziert wurde (weil die Verifizierung des restlichen Codes zu schwierig war), was zur Entdeckung führte, dass der nicht verifizierte Code mehr Schwachstellen aufwies, als die Autoren angenommen hatten (und zwar auf tödlichere Weise).

Fälle, in denen die Autoren vergessen haben, wichtige Eigenschaften anzugeben, die bewiesen werden mussten.

Nadims Artikel enthält eine Klassifizierung der Fehlermodi bei der formalen Verifikation; er nennt auch andere Arten von Fehlermodi (zum Beispiel ist ein weiterer wichtiger Fall, dass „die formale Spezifikation selbst falsch ist oder der Beweis falsche Aussagen enthält, die vom konstruierten System stillschweigend akzeptiert werden“).

Abschließend können wir uns mit dem Versagen formaler Verifikation an der Schnittstelle zwischen Software und Hardware befassen. Ein häufiges Problem hierbei ist die Überprüfung der Resistenz gegen Seitenkanalangriffe.

Selbst wenn Sie über absolut sichere kryptografische Verfahren zum Schutz Ihrer Nachrichten verfügen, sind Sie immer noch unsicher, wenn jemand in wenigen Metern Entfernung Schwankungen in den elektrischen Signalen auffangen und Ihren privaten Schlüssel nach Hunderttausenden von Verschlüsselungen extrahieren kann.

Dies ist ein Artikel über die „Differenzielle Leistungsanalyse“, ein gut verstandenes Beispiel für solche Techniken: Artikel.

Die differentielle Leistungsanalyse ist eine gängige Art von Seitenkanalangriffen. Quelle: Wikipedia

Es gab immer wieder Versuche, die Sicherheit gegen solche Angreifer nachzuweisen. Jeder solche Beweis erfordert jedoch ein mathematisches Modell des Angreifers, das es ermöglicht, die Sicherheit dagegen zu beweisen.

Manchmal wird ein „d-Probing-Modell“ verwendet: Dabei wird angenommen, dass die Anzahl der Stellen, die ein Angreifer im Schaltkreis abfragen kann, begrenzt ist. Allerdings werden einige Formen von Datenlecks von diesem Modell nicht erfasst.

Wie in diesem Artikel erläutert, ist ein häufiges Problem die transiente Leckage: Wenn man ein Signal beobachten kann, das nicht nur vom Wert an einer bestimmten Stelle abhängt, sondern auch davon, wie sich dieser Wert ändert, reicht dies oft aus, um die benötigten Informationen aus zwei Werten (dem alten und dem neuen Wert) anstatt nur aus einem Wert zu gewinnen.

Dieser Artikel bietet Klassifizierungen anderer Leckageformen.

Jahrzehntelang haben diese Kritikpunkte an der formalen Verifikation dazu beigetragen, diese zu verbessern. Im Vergleich zu früher sind wir heute besser darin, solchen Problemen vorzubeugen. Doch auch heute ist sie nicht perfekt.

Im Großen und Ganzen lässt sich ein roter Faden erkennen: Formale Verifikation ist ein mächtiges Werkzeug.

Doch egal, wie Marketingbegriffe die formale Verifizierung auch klingen lassen mögen, als liefere sie „beweisbare Korrektheit“, die sogenannte „beweisbare Korrektheit“ beweist grundsätzlich nicht, dass Software (oder Hardware) „korrekt“ ist.

Im allgemeinen menschlichen Verständnis bedeutet „korrekt“ so etwas wie: „Das Verhalten der Dinge entspricht dem Verständnis des Benutzers hinsichtlich der Absicht des Entwicklers.“

Und „sicher“ bedeutet so viel wie: „Das Verhalten der Dinge entspricht nicht den Erwartungen des Nutzers und schadet nicht den Interessen des Nutzers.“

In beiden Fällen läuft Korrektheit und Sicherheit letztlich auf einen Vergleich zwischen mathematischen Objekten und menschlichen Absichten oder Erwartungen hinaus.

Menschliche Absichten und Erwartungen sind an sich schon mathematisch komplexe Gebilde; schließlich ist das menschliche Gehirn Teil des Universums und unterliegt physikalischen Gesetzen, die simuliert werden können, wenn man über genügend Rechenleistung verfügt.

Es handelt sich jedoch um unglaublich komplexe mathematische Objekte, die weder Computer noch wir selbst verstehen oder gar lesen können.

Praktisch gesehen sind sie Blackboxes; wir haben nur deshalb ein Verständnis unserer Absichten und Erwartungen, weil jeder von uns jahrelange Erfahrung darin hat, seine eigenen Gedanken zu beobachten und auf die Gedanken anderer zu schließen.

Und weil wir menschliche Absichten nicht in einen Computer einprogrammieren können, kann die formale Verifikation keinen Vergleich mit menschlichen Absichten ermöglichen.

Daher beweisen „beweisbare Korrektheit“ und „beweisbare Sicherheit“ nicht wirklich die „Korrektheit“ und „Sicherheit“, die wir Menschen verstehen. Das kann nichts leisten, solange wir das menschliche Gehirn nicht vollständig simulieren können.

Wozu ist es also gut?

Ich neige dazu, Test-Suites, Typsysteme und formale Verifikation als unterschiedliche Implementierungen desselben zugrunde liegenden Ansatzes zur Sicherheit von Programmiersprachen zu betrachten (was möglicherweise auch der einzig vernünftige Ansatz ist).

Es geht dabei immer darum, unsere Absichten redundant auf unterschiedliche Weise zu spezifizieren und dann automatisch zu überprüfen, ob diese verschiedenen Spezifikationen miteinander kompatibel sind.

Nehmen Sie diesen Python-Code als Beispiel:

def fib(n: int) -> int:

falls n < 0:

raise Exception("Negative Werte werden nicht unterstützt")

elif 0 <= n < 2:

return n

anders:

return fib(n-1) + fib(n-2)

if __name__ == '__main__':

assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

assert fib(15) == 610

Hier können Sie Ihre Absichten auf drei verschiedene Arten ausdrücken:

Konkret durch die Implementierung der Fibonacci-Formel im Code

Implizit durch das Typsystem (das festlegt, dass Eingaben, Ausgaben und Zwischenschritte in der Rekursion allesamt ganze Zahlen sind).

Mithilfe der „Beispielpaket“-Methode: Testfälle

Beim Ausführen der Datei wird die Formel anhand der Beispiele überprüft. Der Typchecker kann feststellen, ob die Datentypen kompatibel sind: Die Addition zweier Ganzzahlen ist eine zulässige Operation und ergibt wieder eine Ganzzahl.

Typsysteme sind oft eine gute Möglichkeit, die Arbeit in der Physik zu überprüfen: Wenn man die Beschleunigung berechnet, aber am Ende ein Ergebnis in Metern pro Sekunde anstatt in Metern pro Sekunde² erhält, weiß man, dass man einen Fehler gemacht hat.

Und Testfälle sind ein Beispiel für die Definition eines „Beispielpakets“, was für Menschen oft eine natürlichere Art ist, mit Konzepten umzugehen, als direkte explizite Definitionen.

Je mehr verschiedene Möglichkeiten Sie haben, Ihre Absichten zu spezifizieren, idealerweise auf eine Weise, die Sie dazu zwingt, über das Problem anders nachzudenken, desto wahrscheinlicher ist es, dass Sie tatsächlich das ausdrücken, was Sie wirklich wollen, sobald sich gezeigt hat, dass all diese Ausdrucksformen miteinander kompatibel sind.

Bei sicherer Programmierung geht es darum, seine Absichten auf verschiedene Weisen auszudrücken und dann automatisch zu überprüfen, ob all diese Ausdrücke miteinander kompatibel sind.

Die formale Verifikation ermöglicht es, diesen Ansatz weiter auszubauen. Mithilfe der formalen Verifikation können Sie Ihre Absichten auf nahezu unendlich viele verschiedene, redundante Arten spezifizieren, und das Programm kann nur dann validiert werden, wenn alle diese Varianten kompatibel sind.

Sie können eine hochoptimierte und eine sehr ineffiziente, aber lesbare Implementierung festlegen und überprüfen, ob sie übereinstimmen. Sie können zehn Freunde bitten, eine Liste mathematischer Eigenschaften zu erstellen, die Ihr Programm ihrer Meinung nach erfüllen sollte, und anschließend prüfen, ob es alle diese Anforderungen erfüllt.

Falls es nicht funktioniert, prüfen Sie, ob das Programm fehlerhaft ist oder die mathematischen Eigenschaften falsch spezifiziert wurden. Mithilfe von KI lassen sich all diese Operationen äußerst effizient durchführen.

Wie fange ich also an?

Realistisch betrachtet, werden Sie die Beweise nicht selbst schreiben. Der Grund, warum formale Methoden nie wirklich populär geworden sind, liegt darin, dass die meisten Menschen nicht verstehen, wie man diese komplexen Dinge formuliert. Können Sie mir die Bedeutung des folgenden Codes erklären?

/-- Hilfsfunktion: Punktweises ≤ auf der foldl-Ebene mit einem Akkumulator. -/

private theorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (ab : Nat) (hAcc : a ≤ b)

(hLE : Forall₂ (· ≤ ·) ds1 ds2) :

List.foldl (λ acc d => acc * w + d) a ds1 ≤

List.foldl (λ acc d => acc * w + d) b ds2 := by

match ds1, ds2, hLE with

| [], [], .nil => exakte hAcc

| d1::ds1', d2::ds2', .cons hd htl =>

simp [List.foldl]

refine foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl

genaue Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

(Falls Sie sich wundern: Dies ist eines von vielen Teillemmas im Beweis einer spezifischen Sicherheitsaussage für eine Variante von SPHINCS-Signaturen.)

Die Aussage lautet konkret: Sofern keine Hash-Kollision auftritt, benötigt die Signatur einer aus einem Hash-Digest (dig1) generierten Nachricht mindestens an einer Stelle der Hash-Hierarchie einen höheren Wert als die Signatur jeder anderen Nachricht und enthält somit Informationen, die aus der anderen Signatur nicht berechnet werden können.

Sie müssen keinen Code und keine Beweise manuell schreiben; lassen Sie einfach die KI Programme für Sie schreiben (entweder direkt in Lean oder, um die Geschwindigkeit zu erhöhen, in Assemblersprache) und beweisen Sie dabei alle gewünschten Eigenschaften.

Der Vorteil dieser Aufgabe besteht darin, dass sie selbstvalidierend ist, sodass keine Überwachung erforderlich ist; man lässt die KI einfach mehrere Stunden lang kontinuierlich laufen.

Im schlimmsten Fall tritt es auf der Stelle, ohne Fortschritte zu erzielen (oder, wie es mein Leantral einmal tat, es ersetzt die Aussage, die es beweisen sollte, um seine Arbeitsbelastung zu verringern).

Am Ende müssen Sie lediglich prüfen, ob die bewiesenen Aussagen Ihren Anforderungen entsprechen.

Im Falle der SPHINCS-Signaturvariante lautet die abschließende Aussage:

Satz wots_fullDigits_incomparable

{dig1 dig2 : List Nat} {w l1 l2 : Nat}

(hw : 0 < w)

(hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)

(hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)

(hL2suff : l1 * (w - 1) < w ^ l2)

(hNeq : dig1 ≠ dig2) :

¬ Forall₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧

¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

Das ist tatsächlich kaum noch lesbar:

Wenn die aus einem Hash-Digest (dig1) generierten Zahlen nicht mit denen eines anderen Hash-Digests (dig2) übereinstimmen

Dann ist keine der folgenden beiden Bedingungen erfüllt:

Für alle Zahlen gilt: Die Zahlen aus dig1 sind kleiner oder gleich den Zahlen aus dig2.

Für alle Zahlen gilt: Die Zahlen aus dig2 <= die Zahlen aus dig1

In den durch Addition von Prüfsummen erzeugten „erweiterten Zahlen“ (wotsFullDigits) gibt es zwangsläufig Stellen in der Erweiterung von dig1, an denen die Zahlen höher sind, während an anderen Stellen die Zahlen in der Erweiterung von dig2 höher sind.

Was die Verwendung großer Sprachmodelle zum Schreiben von Beweisen angeht, halte ich sowohl Claude als auch Deepseek 4 Pro für geeignet. Leanstral ist ein kleineres Open-Source-Gewichtsmodell, das speziell für das Schreiben von Lean optimiert wurde und eine vielversprechende Alternative darstellt.

Es verfügt über 119 Milliarden Parameter, wobei 6 Byte pro Token aktiviert werden, und kann lokal ausgeführt werden, ist jedoch langsamer (etwa 15 Token/Sekunde auf meinem Laptop). Laut Benchmarks übertrifft Leanstral deutlich größere allgemeine Modelle.

Nach meiner bisherigen Erfahrung ist es etwas weniger effektiv als Deepseek 4 Pro, aber immer noch sehr effektiv.

Formale Verifikation kann nicht alle unsere Probleme lösen.

Wenn wir jedoch wollen, dass das Modell der Internetsicherheit nicht länger auf dem Vertrauen in einige wenige mächtige Organisationen beruht, müssen wir uns dem Vertrauen in den Code zuwenden, und zwar auch dem Vertrauen in den Code selbst angesichts mächtiger KI-Gegner.

Die KI-gestützte formale Verifizierung hat uns einen wichtigen Schritt in Richtung dieses Ziels gebracht.

Ähnlich wie Blockchain und ZK-SNARKs sind auch künstliche Intelligenz und formale Verifikation hochgradig komplementäre Technologien.

Blockchain bietet Ihnen offene Überprüfbarkeit und Zensurresistenz auf Kosten der Privatsphäre und Skalierbarkeit, während ZK-SNARKs Ihnen Privatsphäre und Skalierbarkeit zurückgeben (tatsächlich sogar mehr als zuvor).

Künstliche Intelligenz ermöglicht es Ihnen, riesige Mengen an Code zu schreiben, allerdings auf Kosten der Genauigkeit. Die formale Verifikation hingegen liefert Ihnen die Genauigkeit zurück (tatsächlich sogar mehr als zuvor).

Standardmäßig erzeugt die KI eine große Menge extrem hastig generierten Codes, wodurch die Anzahl der Fehler zunimmt.

Tatsächlich ist es in manchen Fällen der richtige Kompromiss, eine Zunahme von Fehlern in Kauf zu nehmen: Wenn die Fehler geringfügig sind, ist selbst Software mit Fehlern besser als gar keine Software.

Hier hat die Cybersicherheit jedoch eine optimistische Zukunft: Software wird sich (weiterhin) in „unsichere Randteile“ um einen „sicheren Kern“ aufspalten.

Unsichere Randkomponenten werden in Sandboxes ausgeführt und erhalten nur die minimal erforderlichen Berechtigungen, um ihre Aufgaben zu erfüllen.

Der sichere Kern verwaltet alles. Fällt der sichere Kern aus, ist alles betroffen, einschließlich Ihrer persönlichen Daten, Ihres Geldes usw. Sollte jedoch eine unsichere Komponente ausfallen, schützt Sie der sichere Kern weiterhin.

Im Hinblick auf den sicheren Kern können wir die Verbreitung fehlerhaften Codes nicht zulassen. Wir werden radikale Maßnahmen ergreifen, um den sicheren Kern klein zu halten und ihn sogar noch weiter zu verkleinern.

Stattdessen werden wir die gesamte durch KI erzielte zusätzliche Leistung in die Verbesserung der Sicherheit des Kernsystems investieren, damit es den extrem hohen Vertrauensanforderungen, die wir in einer hochdigitalisierten Gesellschaft an es stellen, gerecht werden kann.

Der Kernel eines Betriebssystems (oder zumindest ein Teil davon) wird zu einem solchen sicheren Kern.

Ethereum wird ein weiteres sein.

Hoffentlich wird zumindest für alle nicht rechenintensiven Aufgaben die verwendete Hardware nur noch ein Drittel ausmachen.

Systeme im Zusammenhang mit dem Internet der Dinge werden das vierte System sein.

Zumindest bei diesen sicheren Kernsystemen wird die alte Weisheit „Fehler sind unvermeidlich; man kann nur versuchen, sie zu finden, bevor der Angreifer sie findet“ widerlegt und durch eine hoffnungsvollere Welt ersetzt, in der man echte Sicherheit erreichen kann.

Aber wenn Sie bereit sind, Ihre Vermögenswerte und Daten einer schlecht programmierten Software anzuvertrauen, die sie versehentlich in einem schwarzen Loch verschlucken könnte, nun, dann steht Ihnen diese Freiheit natürlich auch zu.