Trail of Bits Miden-Audit fand Falcon-Schwachstelle, nachdem Agenten die fehlenden Tools entwickelt hatten

Trail of Bits bereitete sich sechs Monate lang auf das Miden-Audit vor und fand dann mit Werkzeugen, die seine KI-Agenten von Grund auf entwickelt hatten, eine Schwachstelle hoher Schwere. Das Miden-Audit von Trail of Bits bestand aus mehr, als ein Modell auf Quellcode anzusetzen. Die Agenten erstellten einen LSP-Server, einen Decompiler, eine Engine für statische Analysen und ein Lean-Modell, bevor die formale Prüfung begann.

Diese Vorbereitung deckte einen unzureichend eingeschränkten Wert auf, der es Berichten zufolge einem böswilligen Prover ermöglichen könnte, Falcon-Signaturen zu fälschen und betroffene Konten leerzuräumen. Die Analysetools identifizierten zudem mehr als 400 Stellen, an denen sich die Typvalidierung verbessern ließe. Parallel dazu lieferte der Aufwand zur formalen Verifikation 95 maschinell geprüfte Korrektheitsbeweise und deckte zwei Fehler auf, die bestehende Unit-Tests übersehen hatten.

Der entscheidende Wettbewerb lautet nicht KI-Agenten gegen menschliche Auditoren. Es geht um direkte KI-Codeprüfung gegenüber der agentengestützten Konstruktion jener Infrastruktur, die schwierige Codeprüfung überhaupt erst ermöglicht. Trail of Bits setzte weiterhin auf menschliche Aufsicht, manuelle Prüfung von Theoremen und konventionelles Sicherheitsurteil. Die Agenten veränderten, welche unterstützenden Projekte wirtschaftlich realisierbar waren.

Das Miden-Audit von Trail of Bits begann sechs Monate früher

Die entscheidende Arbeit begann, bevor die Auditoren ein fertiges Prüfziel zur Inspektion erhielten.

Das Miden-Team wandte sich Ende 2025 an Trail of Bits, wie aus dem ausführlichen Bericht zum Miden-Audit der Firma hervorgeht. Miden wollte Teile seiner Zero-Knowledge Virtual Machine vor dem Start prüfen lassen. Ein Bereich umfasste eine Kernbibliothek mit kryptografischen Primitiven, die in Miden Assembly oder MASM geschrieben waren.

Eine Zero-Knowledge Virtual Machine, häufig zkVM abgekürzt, beweist die korrekte Ausführung eines Programms, ohne dass jeder Verifizierer diese Berechnung wiederholen muss. Miden verwendet eine Stack-Machine-Architektur. Instruktionen entnehmen Werte einem Stack und legen ihre Ergebnisse wieder darauf ab.

Diese Architektur ist wichtig, weil Ein- und Ausgaben in MASM-Code häufig implizit sind. Ein Prüfer muss nachverfolgen, wie jede Instruktion den Stack verändert, und diesen Zustand dann über Verzweigungen, Schleifen und Prozeduraufrufe hinweg fortführen. Vertraute Hinweise auf Quellcodeebene können dabei verschwinden.

MASM fehlte zudem ein Großteil der Tooling-Unterstützung, die Auditoren üblicherweise erwarten. Es gab wenig Editor-Unterstützung, keinen ausgereiften, auf Prüfungen zugeschnittenen Language Server und nur begrenzte automatisierte Analysen für die Kernbibliothek. Trail of Bits wusste, dass die Implementierung noch nicht vollständig war, aber auch, dass die Prüfung erst in sechs Monaten stattfinden würde.

Die Firma nutzte dieses Zeitfenster, um ihre eigene Prüfungsumgebung aufzubauen. Claude erzeugte laut Trail of Bits innerhalb weniger Tage einen ersten Language-Server-Prototyp. Der daraus entstandene MASM language server bietet Navigation, Referenzsuche, Hover-Dokumentation, Syntaxdiagnosen, Instruktionsbeschreibungen und Informationen zu Stack-Effekten.

Diese Funktionen klingen nach gewöhnlichen Entwicklererleichterungen. In einer unbekannten Assemblersprache werden sie Teil der Sicherheitsmethode. Navigation hilft Auditoren, einen Wert über Prozedurgrenzen hinweg nachzuverfolgen. Inline-Stack-Effekte verringern wiederholte manuelle Rekonstruktion. Diagnosen legen Annahmen offen, bevor daraus Findings werden.

Trail of Bits erweiterte das Projekt anschließend um Dekompilierung, statische Analyse, Kommandozeilen-Tooling und formale Modellierung. Claude übernahm Planungs- und Implementierungsaufgaben, während Codex an der Codeprüfung beteiligt war. Die Agenten wechselten auch die Rollen, wodurch die generierte Arbeit einen separaten Prüfungsdurchlauf erhielt.

Dabei handelte es sich nicht um einen einmaligen Generierungsprozess. Nach der Implementierung eines Features ließ das Team Agenten randomisierte Prozeduren dekompilieren und die Ergebnisse mit dem ursprünglichen MASM vergleichen. Regressionen wurden zu Tests, und das Modell arbeitete anschließend gegen diese Tests.

Diese Rückkopplungsschleife ist zentral für die Geschichte. Die Agenten wurden nicht als Autoritäten behandelt, deren Output automatisches Vertrauen verdiente. Sie arbeiteten innerhalb eines wachsenden Verifikationssystems aus Tests, Prüfphasen, Analysetools und später einem Proof Checker.

Das Audit begann daher mit einer anderen Frage als üblich. Trail of Bits fragte nicht nur, ob ein Agent Schwachstellen finden könne. Es fragte, welche fehlenden Instrumente Auditoren – einschließlich Agenten – daran hinderten, den Code überhaupt zu verstehen.

Diese Verschiebung des Umfangs schuf die Voraussetzungen für die späteren Findings. Sie erhöhte zugleich den Druck auf Sicherheitsteams, die KI-Prüfung vor allem als schnelleres Scannen von Quellcode vermarkten. Der Ansatz von Trail of Bits erforderte mehr Vorbereitung, verwandelte diese Vorbereitung jedoch in wiederverwendbare technische Infrastruktur.

Der Decompiler wurde wertvoller als sein Output

Der Decompiler war vor allem wichtig, weil seine interne Repräsentation anderen Analysen eine verlässliche Grundlage bot.

Die Dekompilierung von MASM bestand nicht einfach darin, Assembler-Instruktionen durch lesbare Ausdrücke zu ersetzen. Den meisten Prozeduren der Kernbibliothek fehlten deklarierte Signaturen, sodass die Tools ihre Ein- und Ausgaben häufig aus dem Kontext ableiten mussten. Den Prozeduren fehlte außerdem eine einheitliche Calling Convention.

Schleifen schufen ein weiteres Problem. Eine MASM-While-Schleife muss zwischen Iterationen nicht dieselbe Stack-Form bewahren. Ihre Bedingung kann an eine andere Stack-Position wandern und damit einfache Versuche durchkreuzen, den Eingaben von Instruktionen stabile Namen zuzuweisen.

Auch bedingte Verzweigungen können unterschiedliche Stack-Effekte erzeugen. Wenn ein Zweig ein Element hinzufügt, während ein anderer eines entfernt, kann der Decompiler ihre Zustände nicht blind zusammenführen. Fehler bei der Ableitung von Stack-Effekten können sich dann durch jede Prozedur fortpflanzen, die den betroffenen Code aufruft.

Trail of Bits reagierte mit einer begrenzten Zusage. Sein MASM decompiler zielt auf eine klar definierte Teilmenge, statt für jede Prozedur perfekte Rekonstruktion zu behaupten. Diese Entscheidung stellte Korrektheit über oberflächliche Abdeckung.

Der Decompiler wurde zum größten Tooling-Aufwand des Projekts. Trail of Bits berichtet von mehr als 100 KI-generierten Commits über mehrere Monate hinweg. Dennoch war der fertige Pseudocode nicht sein folgenreichstes Ergebnis.

Das Projekt schuf eine Zwischenrepräsentation oder IR, die Ein- und Ausgaben von Prozeduren als analysierbare Ausdrücke darstellte. Eine IR ist eine strukturierte Version von Code, die für Transformation oder Analyse konzipiert ist. Sobald MASM-Instruktionen in dieser Form vorlagen, konnte das Team etablierte Techniken für Datenfluss- und statische Analyse anwenden.

Das Analysewerkzeug konnte fragen, ob vom Prover bereitgestellte Werte vor ihrer Verwendung validiert wurden. Es konnte nachverfolgen, ob Code erwartete Typen wie 32-Bit-Ganzzahlen oder boolesche Werte durchsetzte. Außerdem konnte es feststellen, ob lokale Variablen auf jedem möglichen Ausführungspfad initialisiert wurden.

Trail of Bits nutzte für Teile dieser Arbeit abstrakte Interpretation. Abstrakte Interpretation bewertet Kategorien möglicher Werte, statt ein Programm mit einer konkreten Eingabe auszuführen. Ein Wert könnte etwa als gültige 32-Bit-Ganzzahl, als boolescher Wert oder als unbekannter Wert dargestellt werden.

Die Analyse wird wiederholt, bis sie einen stabilen Zustand erreicht, in dem keine neuen Informationen mehr auftreten. Bei einer sounden Auslegung überapproximiert sie, was reale Ausführungen leisten können. Das kann False Positives erzeugen, sollte jedoch kein reales Verhalten, das vom Modell abgedeckt wird, stillschweigend ausschließen.

Das zeigt, warum sich das Miden-Audit von Trail of Bits von einer allgemeinen KI-Coding-Demonstration unterscheidet. Dem agentengenerierten Decompiler wurde nicht vertraut, den Code für sicher zu erklären. Er half dabei, ein Substrat zu konstruieren, auf dem explizite, überprüfbare Analysen laufen konnten.

Der Workflow brachte auch Vorteile für Menschen. Dekompilierte Prozeduren erleichterten die Prüfung von Steuerungs- und Datenfluss auf hoher Ebene im Editor. Stack-Anmerkungen reduzierten den mentalen Buchhaltungsaufwand. Kommandozeilenschnittstellen machten dieselben Fähigkeiten für automatisierte Prüfprozesse verfügbar.

Darin liegt eine weitergehende Lehre für Teams, die Coding-Agenten bewerten. Das wertvollste generierte Artefakt muss nicht das sein, das Nutzer sehen. Ein teilweise abgegrenzter Decompiler kann seine Kosten dennoch rechtfertigen, wenn Parser, Kontrollflussmodell und IR mehrere höherwertige Prüfungen ermöglichen.

Diese Schlussfolgerung verändert auch, wie Teams Projektkontext bewahren sollten. Agent-Prompts, Regressionsfälle, Architekturentscheidungen und Reviewer-Kommentare werden zu dauerhaften Engineering-Eingaben. Eine durchsuchbare Wissensdatenbank kann helfen, diese Materialien über lange Sicherheitsprojekte hinweg verfügbar zu halten.

Direkte KI-Prüfung beginnt üblicherweise mit dem Zielcode und sucht nach Defekten. Trail of Bits setzte Agenten stattdessen ein, um die Prüfungsoberfläche zu verändern. Das nächste Ergebnis zeigte, warum diese Unterscheidung wichtig war.

Eine fehlende Prüfung erreichte die Falcon-Authentifizierung

Ein einziger nicht validierter Restwert machte Berichten zufolge aus einem arithmetischen Hilfsprogramm einen Weg zu gefälschter Authentifizierung.

Während des Audits identifizierten die statischen Analysen mehr als 400 einzigartige Stellen, an denen sich die Typvalidierung verbessern ließe. Trail of Bits zufolge waren alle über die öffentliche API der Kernbibliothek erreichbar. Viele entstanden, weil öffentlich zugängliche Prozeduren ohne die Annahmen aufgerufen werden konnten, die ihre ursprünglichen Autoren erwartet hatten.

Eine öffentliche Prozedur kann sich nicht sicher darauf verlassen, dass jeder Aufrufer einen Wert des vorgesehenen Typs liefert. In einem Proof System ist es besonders wichtig, zwischen einem vom Prover bereitgestellten Wert und einem durch den Proof eingeschränkten Wert zu unterscheiden. Allein das Einbringen von Daten in eine Berechnung belegt nicht, dass sie die behauptete Ganzzahl oder den behaupteten booleschen Wert darstellen.

Das Finding hoher Schwere konzentrierte sich auf mod_12289, eine Prozedur, die einen 64-Bit-Wert modulo 12.289 reduziert. Der Prover lieferte über einen Advice-Mechanismus einen Quotienten und einen Restwert. Advice-Werte sind außerhalb der VM berechnete Ausführungshinweise, die oft eingesetzt werden, um aufwendige Berechnungen innerhalb der VM zu vermeiden.

Der Quotient erhielt eine Prüfung, die bestätigte, dass er in die erwartete 64-Bit-Repräsentation passte. Der Restwert erhielt vor dem Eintritt in u32overflowing_sub, eine 32-Bit-Subtraktionsinstruktion, keine entsprechende Validierung.

Trail of Bits zufolge konnte ein Angreifer Quotient und Restwert variieren und dennoch die Subtraktionsbeschränkungen erfüllen. Dadurch konnte mod_12289 etwas anderes als den mathematisch korrekten Restwert zurückgeben.

Die Reichweite des Fehlers ging über ein falsches arithmetisches Ergebnis hinaus. Die Prozedur unterstützte die Falcon-Signaturverifikation. Falcon ist ein postquantensicheres digitales Signaturverfahren, und Miden verwendete eine Variante für die Kontoauthentifizierung.

Nach Angaben von Trail of Bits könnte ein böswilliger Prover den unzureichend eingeschränkten Wert ausnutzen, um eine Falcon-Signatur zu fälschen und ein von einem Falcon-Schlüsselpaar kontrolliertes Konto leerzuräumen. Dies ist die technische Behauptung der Firma, kein unabhängig reproduzierter Exploit, der im öffentlichen Artikel vorgestellt wird.

Die Schwere ergibt sich aus Midens Ausführungsmodell. Das Miden VM design unterstützt nichtdeterministische Eingaben, die während der Proof-Erzeugung bereitgestellt werden. Diese Eingaben können die Effizienz verbessern, müssen vom Programm jedoch sorgfältig eingeschränkt werden.

Ein Verifizierer leitet nicht die Absicht des Entwicklers ab. Er prüft, ob der eingereichte Proof die kodierten Beschränkungen erfüllt. Akzeptieren diese Beschränkungen einen ungültigen Restwert, kann der Proof gültig bleiben, selbst wenn die behauptete arithmetische Beziehung falsch ist.

Das ist die zentrale Umkehrung. Zero-Knowledge-Proofs können die getreue Ausführung eines spezifizierten Systems belegen, aber sie können keine unvollständige Spezifikation reparieren. Ein kryptografischer Proof eines unzureichend eingeschränkten Programms kann Vertrauen in die falsche Eigenschaft schaffen.

Unabhängiger Kontext aus einem späteren Miden-Contract-Audit untermauert den allgemeinen Punkt. OpenZeppelin beschrieb Miden-Transaktionen als gültig, wenn ein entsprechender Beweis vorliegt, wodurch jede MASM-Prüfung Teil der Bedingungen wird, die ein Prover erfüllen muss.

Dieser separate Auftrag betraf einen anderen Repository-Umfang und sollte nicht mit der Überprüfung von Trail of Bits gleichgesetzt werden. Beide Berichte zeigen jedoch, warum Authentifizierungslogik, vom Prover kontrollierte Eingaben und On-Chain-Annahmen ausdrücklich behandelt werden müssen.

Auch die mehr als 400 Stellen zur Typvalidierung sollten mit Bedacht interpretiert werden. Sie wurden nicht als 400 ausnutzbare Schwachstellen beschrieben. Vielmehr handelte es sich um Stellen, an denen die Validierung verbessert werden könnte; darunter befand sich ein gemeldetes Problem mit hoher Schwere.

Diese Unterscheidung ist wichtig, weil statische Analysen häufig Bedingungen finden, die zunächst bewertet werden müssen. Ein solides Analysewerkzeug kann absichtlich mehr Fälle melden, als sich letztlich als Sicherheitsmängel erweisen. Sein Wert liegt darin, Annahmen, die geprüft werden sollten, systematisch aufzuspüren.

Für Sicherheitsteams setzt das Ergebnis eine verbreitete Abkürzung unter Druck: einen Agenten verdächtige Funktionen zusammenfassen zu lassen, ohne zuvor die Wertregeln der Zielsprache zu modellieren. Ein Modell kann erklären, was der Code offenbar tut. Der Analyzer kann fragen, ob jede zulässige Ausführung tatsächlich den erforderlichen Typ respektiert.

Der Falcon-Fund entstand durch die Kombination beider Fähigkeiten. Agenten beschleunigten die Entwicklung, während die statische Semantik eine Intuition über vom Prover kontrollierte Daten in eine wiederholbare Prüfung verwandelte.

Lean-Beweise fanden, was Unit-Tests übersahen

Formale Verifikation ersetzte Tests nicht, zwang das Team jedoch dazu, Verhalten präzise genug zu formulieren, um zwei ungetestete Fehler offenzulegen.

Trail of Bits verfolgte formale Modellierung auch nach dem Aufbau des Editors und der Werkzeuge zur statischen Analyse weiter. Die Frage war bewusst eine andere: Wenn eine Bibliotheksprozedur keinen offensichtlichen Fehler enthielt, konnte das Team beweisen, dass ihre Implementierung dem beabsichtigten arithmetischen Verhalten entsprach?

Das Unternehmen entwickelte einen minimalen Miden-VM-Executor in Lean. Lean ist ein interaktiver Theorembeweiser, dessen kleiner vertrauenswürdiger Kernel prüft, ob ein eingereichter Beweis aus seinen Definitionen und Annahmen folgt. Claude half außerdem beim Aufbau eines Übersetzers von MASM-Prozeduren in Lean-Repräsentationen.

Mehrere Agenten arbeiteten anschließend parallel an Prozedurbeweisen. Das daraus entstandene MASM-Lean-Modell enthält ausführbare VM-Semantik, übersetzte Prozeduren, gemeinsame Beweisunterstützung und individuelle Korrektheitstheoreme.

Das Repository führt 95 geprüfte Prozedurbeweise auf: 31 für 64-Bit-Operationen, 36 für 128-Bit-Operationen, 17 für 256-Bit-Operationen und 11 für Wortoperationen. Zusammen decken sie die von Trail of Bits beschriebenen Teile der Binärarithmetik ab.

Dabei handelte es sich nicht um Beweise dafür, dass jeder Teil von Miden sicher war. Sie behandelten definierte Korrektheitseigenschaften bestimmter Prozeduren. Diese Grenze ist entscheidend, weil ein Theorembeweiser das ihm vorgelegte Theorem verifiziert, nicht die unausgesprochene Absicht im Kopf eines Entwicklers.

Trail of Bits erklärt, dass sich menschliche Prüfer deshalb auf die Überprüfung der Theoremaussagen konzentrierten. Wenn ein Agent ein Theorem bewies, das eine kritische Vorbedingung ausließ oder das falsche Ergebnis ausdrückte, würde die Annahme durch den Kernel allein die Software nicht korrekt machen.

Auf hoher Ebene folgten viele Theoreme einem erkennbaren Muster. Bei einem Stack mit bestimmten Eingaben sollte die Ausführung einer Prozedur terminieren und das mathematisch erwartete Ergebnis oben auf dem Stack hinterlassen. Nicht zusammenhängende, dem Aufrufer gehörende Stack-Werte sollten an den erwarteten Positionen verbleiben.

Dieser Spezifikationsdruck deckte zwei Fehler auf, die bestehende Unit-Tests übersehen hatten. Der erste betraf eine 64-Bit-Rechtsrotationsprozedur namens rotr. Sie verhielt sich bei großen Eingaben oberhalb der Goldilocks-Primzahl falsch, wenn der Rotationsbetrag ein Vielfaches von 32 war.

Die Goldilocks-Primzahl definiert den von der VM verwendeten Körper, weshalb Werte nahe oder jenseits dieser Grenze sorgfältig repräsentiert werden müssen. Während der Beweisarbeit ließ sich das gewünschte Theorem nicht herleiten, ohne eine Annahme hinzuzufügen, die den problematischen Shift-Fall ausschloss.

Ein fehlgeschlagener Beweis ist nicht automatisch ein Beleg für einen Codefehler. Auch das Theorem, das Modell oder unterstützende Lemmata können falsch sein. Hier führte die manuelle Prüfung des Hindernisses das Team zu dem Sonderfall in der Implementierung.

Der zweite Fehler trat in der 256-Bit-Prozedur wrapping_mul auf. Trail of Bits zufolge entfernte sie vor der Rückkehr dem Aufrufer gehörende Werte vom Stack. Gewöhnliche Tests des Multiplikationsergebnisses konnten bestehen, ohne die Erhaltung des umgebenden Stack-Zustands zu prüfen.

Dieser Fehler zeigt, warum präzise Nachbedingungen wichtig sind. Eine Prozedur kann die korrekte numerische Antwort berechnen und dennoch ihren Aufrufvertrag verletzen. In einer Stack-Maschine kann die Beschädigung benachbarter Zustände die spätere Ausführung beeinflussen, selbst wenn das oberste Element korrekt aussieht.

Unit-Tests spielen weiterhin eine zentrale Rolle. Sie laufen schnell, schützen vor bekannten Regressionen und decken Integrationsverhalten ab, für das möglicherweise noch kein formales Modell besteht. Der Lean-Ansatz lieferte eine andere Form der Absicherung für ausdrücklich formulierte Eigenschaften.

Der wesentliche Vorteil war kompositorisch. Agenten konnten Beweisversuche in großem Maßstab erzeugen, während Leans Kernel ungültige Herleitungen zurückwies. Menschen mussten nicht dem sprachlichen Selbstvertrauen eines Modells vertrauen. Sie mussten die Definitionen prüfen und bestätigen, dass akzeptierte Theoreme die beabsichtigten Garantien abbildeten.

Dies ist eine stärkere Kontrollgrenze, als ein anderes Sprachmodell zu fragen, ob generierter Code korrekt aussieht. Es beseitigt menschliches Urteilsvermögen nicht, verlagert es jedoch stärker auf Spezifikationen und Annahmen.

Für Engineering-Verantwortliche legt der Fall eine praktische Arbeitsteilung nahe. Agenten können wiederkehrendes Beweisgerüst, Übersetzer und Kandidatenlemmata erzeugen. Menschliche Spezialisten entscheiden, was bewiesen werden muss, und untersuchen, warum wichtige Aussagen scheitern.

Das Ergebnis macht autonome Audits nicht vertrauenswürdig

Das Projekt unterstützt agentengestütztes Audit-Engineering, nicht unbeaufsichtigte Sicherheitszertifizierung.

Trail of Bits beschreibt die wirtschaftliche Veränderung direkt. Einige Jahre zuvor hätte das Unternehmen kaum rechtfertigen können, für einen einzelnen Auftrag Monate in explorative Werkzeuge zu investieren. Solche Nebenprojekte hatten ungewisse Ergebnisse und ließen sich schwer verkaufen, bevor ihr Wert sichtbar wurde.

Das Unternehmen argumentiert, dass Agenten die Kosten der Exploration weit genug gesenkt hätten, um diese Rechnung zu verändern. Fehlgeschlagene Experimente kosten zunehmend Tokens und Betreuungszeit statt der vollständigen Zuweisung spezialisierter Engineering-Arbeit.

Diese Behauptung verdient eine sorgfältige Einordnung. Bis zum Audit vergingen weiterhin sechs Monate, und allein der Decompiler sammelte mehr als 100 KI-generierte Commits. Der öffentliche Bericht liefert keinen kontrollierten Vergleich von Arbeitsstunden, gesamten Modellkosten oder Fehlerausbeute mit einem konventionellen Auftrag.

Er belegt auch nicht, dass Agenten für jede ungewöhnliche Sprache gleichwertige Werkzeuge entwickeln können. MASM bot Eigenschaften, die Analyse und formale Modellierung begünstigten. Die Miden VM verfügt über einen kompakten Befehlssatz, und viele Operationen vermeiden komplexe Seiteneffekte.

Selbst bei diesem günstigen Ziel konnte der Decompiler nicht jede Prozedur sicher abdecken. Trail of Bits begrenzte die unterstützte Teilmenge, weil inkonsistente Stack-Effekte und fehlende Signaturen eine vollständige, zuverlässige Dekompilierung unpraktikabel machten.

Der Lean-Workflow brachte eine weitere Einschränkung mit sich. Vom Kernel geprüfte Beweise etablieren nur das formulierte Theorem unter der modellierten Semantik. Eine fehlerhaft übersetzte Instruktion, ein unvollständiges VM-Modell oder ein schwaches Theorem können eine Lücke zwischen bewiesenem Verhalten und realem Einsatz erhalten.

Die menschliche Überprüfung blieb während des gesamten Prozesses sichtbar. Auditoren prüften von Agenten erzeugten Code, wandelten Regressionen in Tests um, untersuchten Theoremaussagen und analysierten fehlgeschlagene Beweise. Claude und Codex wechselten zwischen Entwicklung und Überprüfung, statt als unbeobachtete Autorität zu agieren.

Dadurch wird der zentrale Vergleich präziser. Direkte KI-Überprüfung fordert ein Modell dazu auf, Schwachstellen in einer bestehenden Repräsentation zu erkennen. Tool-bauende Agenten helfen Experten, eine Repräsentation zu schaffen, in der fehlende Einschränkungen, ungültige Typen und falsche Nachbedingungen explizit werden.

Keiner der Ansätze sollte allein stehen. Modelle können Hypothesen aufwerfen, die statische Analyzer nicht kodieren. Statische Analyse kann Ausführungspfade abdecken, die ein probabilistischer Prüfer übersehen könnte. Ein formaler Beweis kann anschließend ausgewählte Eigenschaften nach einem maschinenprüfbaren Standard behandeln.

Der Prozess schafft auch Wartungspflichten. Parser müssen Sprachänderungen folgen. Analyzer benötigen Regressionssuiten. Formale Modelle müssen mit der VM-Semantik abgestimmt bleiben. Generierte Werkzeuge, die veralten, können falsche Sicherheit vermitteln.

Trail of Bits berichtet, dass das Miden-Team die Engine für statische Analyse für künftige Aktualisierungen der Kernbibliothek übernommen hat. Das ist ein wichtiges Signal, weil die Werkzeuge damit über eine einzelne Momentaufnahme des Audits hinausgehen. Die fortlaufende Nutzung wird zeigen, ob der Analyzer nützlich bleibt, während sich Sprache und Bibliothek weiterentwickeln.

Organisationen, die einen ähnlichen Workflow erwägen, sollten auch die Herkunftsnachverfolgbarkeit einplanen. Teams müssen wissen, welches Modell eine Änderung erzeugt hat, welcher Mensch sie überprüfte, welche Tests liefen und welche Annahmen in einen Beweis eingeflossen sind. Ein Engineering-Workflow ist nur so überprüfbar wie die dazu erhaltenen Aufzeichnungen.

Die öffentlichen Belege stützen daher eine begrenzte Schlussfolgerung. Agenten machten ein ambitioniertes Vorbereitungsprogramm für diesen Auftrag realisierbar. Die Sicherheitsgewährleistung entstand weiterhin durch das Zusammenspiel von Fachexperten, Tests, expliziten Analysen und Beweisprüfung.

Dieses System ist interessanter als die Behauptung, eine KI habe einen Fehler gefunden. Es bietet ein konkretes Modell für den Einsatz unvollkommener Agenten, ohne ihr Selbstvertrauen als Beweis zu behandeln.

Drei Signale werden zeigen, ob dieses Audit-Modell Bestand hat

Der nächste Test besteht darin, ob von Agenten entwickelte Absicherungswerkzeuge nach den Schlagzeilenfunden korrekt, übernommen und produktiv bleiben.

Das erste Signal ist die fortgesetzte Integration des MASM-Analyzers in Midens Entwicklungsprozess. Trail of Bits erklärt, dass das Miden-Team die Engine für statische Analyse für künftige Änderungen an der Kernbibliothek übernommen hat. Der routinemäßige Einsatz in Continuous Integration würde die These stärken, dass Audit-Werkzeuge zu präventiver Infrastruktur werden können.

Die wichtige Kennzahl ist nicht, wie viele Warnungen sie ausgibt. Entscheidend ist, ob neue öffentliche Prozeduren vor der Veröffentlichung die erforderliche Validierung erhalten und ob Aktualisierungen des Analyzers Änderungen in der MASM-Semantik nachverfolgen. Anhaltende False Positives oder veraltete Modelle würden das Ergebnis schwächen.

Das zweite Signal ist die Erweiterung und Pflege der 95 Lean-Beweise. Zusätzliche verifizierte Prozeduren würden zeigen, dass das ursprüngliche Modell fortlaufende Arbeit unterstützt statt eine feste Demonstration zu bleiben. Änderungen an bestehendem Arithmetik-Code sollten zudem Aktualisierungen oder Fehlschläge der Beweise auslösen.

Beobachten Sie die Grenze zwischen übersetztem Code und manuell geprüften Spezifikationen. Automatisierung, die die Anzahl der Beweise erhöht, ohne die Theoremabdeckung zu stärken, würde nicht dieselbe Absicherung bieten. Eine klare Dokumentation der Annahmen wird ebenso wichtig sein wie die reine Gesamtzahl.

Das dritte Signal ist die Replikation durch andere Audit-Teams und Sprachökosysteme. Miden bot eine ungewöhnlich geeignete Kombination: eine eigene Sprache, fehlende Werkzeuge, explizite Beweissemantik und Monate an Vorbereitungszeit.

Ein wiederkehrendes Muster über unterschiedliche zkVMs oder Low-Level-Sprachen hinweg würde die umfassendere wirtschaftliche Behauptung von Trail of Bits stützen. Wenn es sich bei Systemen mit Nebenläufigkeit, komplexem Speicher oder großen Abhängigkeitsgraphen nicht reproduzieren lässt, würde das seine Grenzen offenlegen.

Das Miden-Audit von Trail of Bits hat bereits mehr als einen spekulativen Workflow hervorgebracht. Es lieferte eine Editor-Integration, einen Decompiler, einen Analyzer, ein VM-Modell, geprüfte Beweise und konkrete Sicherheitsbefunde.

Die entscheidende Frage bleibt, ob Teams diese Artefakte mit den Systemen, die sie schützen sollen, in Einklang halten können. Entwickler, die agentengestützte Sicherheit bewerten, sollten die Repositories prüfen, die modellierten Annahmen untersuchen und fragen, an welchen Stellen maschinell überprüfbare Kontrollen das Vertrauen in Modelle ersetzen. Das ist der Maßstab, den es in die nächste Prüfung mitzunehmen gilt.