Trail of Bits hat Claude und Codex sechs Monate lang nicht primär zum Finden von Bugs eingesetzt, sondern zum Bau der Werkzeuge, die ein Security-Audit einer neuen Plattform erst praktikabel machten.
Das Ziel war Miden, eine Zero-Knowledge-VM mit eigener Assembly-Sprache und zu Beginn kaum bestehendem Entwickler- und Analyse-Tooling. Für die Vorbereitung des Audits ließ Trail of Bits Agenten einen Language Server, einen Decompiler, eine Static-Analysis-Engine und ein formales Modell des VM-Executors in Lean entwickeln.
Nach Angaben des Unternehmens erzeugten die Agenten in diesen sechs Monaten mehr als 100 Commits bei leichter menschlicher Aufsicht.
Die Werkzeuge wurden anschließend im realen Audit verwendet. Die Static Analysis fand laut Trail of Bits eine schwerwiegende Validierungslücke sowie mehr als 400 kleinere Stellen mit fehlenden Prüfungen. Das Lean-Modell produzierte 95 maschinell geprüfte Korrektheitsbeweise und machte zwei Fehler sichtbar, die die vorhandenen Unit-Tests nicht gefunden hatten.
Für Miden fehlte ein großer Teil der üblichen Audit-Infrastruktur
Miden verwendet eine eigene stackbasierte Assembly-Sprache. Eingaben und Ausgaben von Instruktionen sind dadurch weniger explizit als in vielen verbreiteten Hochsprachen.
Für die junge Plattform existierte außerdem noch kein reifes Ökosystem aus IDE-Unterstützung, Lintern, Decompilern und etablierten Analysewerkzeugen.
Trail of Bits wusste nach eigenen Angaben ungefähr sechs Monate vor dem eigentlichen Review, dass die Implementierung noch nicht fertig war. Das Team nutzte diese Zeit, um Agenten auf den Aufbau der fehlenden Werkzeuge anzusetzen.
Der Language Server machte die Sprache für Entwickler und Auditoren besser navigierbar. Aus der Arbeit am Decompiler entstanden interne Repräsentationen, die Trail of Bits später für statische Analysen wiederverwendete. Das Lean-Modell übersetzte Teile der VM-Logik in eine Umgebung, in der Eigenschaften formal geprüft werden konnten.
Diese Werkzeuge ersetzen den Audit nicht. Sie verschieben, welche Untersuchungen während des Audits überhaupt wirtschaftlich machbar sind.
Der Agent baut zuerst den Hebel für die eigentliche Analyse
Bei einem klassischen Security-Engagement gibt es einen starken Kostendruck auf Vorarbeiten.
Ein eigener Decompiler oder ein formales Modell kann technisch sinnvoll sein, obwohl sich der Aufwand für einen einzelnen Auftrag kaum rechtfertigen lässt. Bei einer proprietären oder jungen Sprache ist dieser Effekt besonders stark: Das Audit-Team muss zunächst Infrastruktur bauen, bevor es systematisch prüfen kann.
Trail of Bits beschreibt den Nutzen der Agenten genau an dieser Stelle. Claude und Codex erzeugten genügend Tooling, dass aus einmaliger Vorarbeit wiederverwendbare Analyse-Infrastruktur wurde.
Ein statischer Analyzer kann dieselbe Regel über die gesamte Codebasis prüfen, Findings nach Änderungen erneut testen und später in die Entwicklung übernommen werden. Trail of Bits schreibt, dass das Miden-Team den Analyzer nach Abschluss des Audits weiterverwendete.
Das ist ein anderes Arbeitsmodell als ein Coding-Agent, der Quelltext liest und direkt eine Liste möglicher Schwachstellen ausgibt.
Formalisierung fand zwei Fehler außerhalb der Unit-Tests
Der Lean-Teil des Projekts zeigt eine zweite Form von Agentenarbeit.
Trail of Bits baute einen minimalen Miden-VM-Executor in Lean. Agenten halfen anschließend dabei, MASM-Prozeduren in das formale Modell zu übertragen und Korrektheitsbeweise zu erstellen.
Der Lean-Kernel prüft die erzeugten Beweise. Menschen mussten deshalb vor allem kontrollieren, ob die formulierten Theoreme tatsächlich die gewünschte Eigenschaft der jeweiligen Prozedur beschreiben.
Nach Angaben von Trail of Bits entstanden 95 maschinell geprüfte Beweise für die binären arithmetischen Komponenten der Core-Library. Dabei wurden zwei Fehler entdeckt, die die vorhandenen Unit-Tests nicht abgedeckt hatten.
Das ist kein Beweis für die Sicherheit der gesamten VM. Formale Verifikation gilt nur für das modellierte Verhalten und die Eigenschaften, die tatsächlich als Theorem formuliert wurden. Ein falsches oder unvollständiges Modell kann weiterhin relevante Fehler auslassen.
Der Vorteil liegt in der Aufgabenteilung: Der Agent kann große Mengen an Formalisierung erzeugen, während ein Proof Assistant die formale Gültigkeit kontrolliert und Menschen die Bedeutung der Spezifikation prüfen.
Agent-generiertes Audit-Tooling wird selbst sicherheitsrelevant
Trail of Bits beschreibt den Prozess nicht als autonomen Security-Audit. Menschen bestimmten die Zielarchitektur, wählten die Werkzeuge, prüften Ergebnisse und verantworteten die Sicherheitsbewertung.
Die Agenten arbeiteten damit innerhalb eines geplanten Review-Prozesses. Sie erhielten keinen offenen Auftrag, reale Systeme selbstständig anzugreifen.
Für Engineering-Teams ist gerade das interessant. Der Einsatz lässt sich auf Bereiche übertragen, in denen bestehende Analysewerkzeuge fehlen: interne DSLs, neue VMs, Protokolle oder spezialisierte Build-Systeme.
Dabei entsteht eine neue Fehlerquelle. Ein agent-generierter Analyzer kann systematisch falsche Ergebnisse produzieren. Ein Decompiler kann Semantik verlieren. Ein formales Modell kann die falsche Eigenschaft beweisen.
Deshalb muss das Tooling selbst wie Security-Code behandelt werden: reproduzierbare Builds, Tests gegen bekannte Referenzfälle und unabhängige Prüfung der Regeln und Spezifikationen.
Trail of Bits veröffentlicht konkrete Ergebnisse, aber keine False-Positive-Rate der Static Analysis. Genau diese Zahl wäre für den dauerhaften Einsatz im Entwicklungsprozess wichtig: Nicht nur wie viele Findings ein Agenten-Tool erzeugt, sondern wie viel davon ein menschliches Security-Team tatsächlich noch verifizieren muss.