reverify: Ein Prüfwerkzeug, das Behauptungen von KI-Modellen gegen Binärdaten testet

Das Problem: Wenn das Modell Offsets erfindet

Sprachmodelle sind gut darin, Quellcode zu lesen, und unzuverlässig beim Reverse Engineering. Das README formuliert es so: Man bittet ein Modell, eine Struktur oder einen Algorithmus aus einer Binärdatei zu rekonstruieren, und es erfindet selbstbewusst Offsets, Größen und Verhalten. In der Binäranalyse sei dieses Halluzinationsproblem weitaus schlimmer als bei Quellcode, und die Frage 'hat das Modell sich das gerade ausgedacht?' sei der größte Blocker für den Einsatz von KI in der echten RE-Arbeit. Genau hier setzt reverify an. Der Ansatz ist nicht, das Modell besser zu machen, sondern ihm die Autorität über Fakten zu entziehen. Das Modell schlägt vor, deterministische Werkzeuge entscheiden. Eine Hypothese über eine Struktur oder einen Algorithmus wird erst dann berichtet, wenn sie gegen die tatsächlichen Bytes geprüft wurde, also disassembliert, per Musterabgleich gefunden oder im Emulator ausgeführt. Die Zielgruppe sind laut README Personen, die autorisierte Reverse-Engineering-Arbeit leisten: Malware-Analyse, CTF, Interoperabilitätsforschung und Software, die man besitzt oder analysieren darf. Das ist keine allgemeine Programmierhilfe, sondern ein Prüfwerkzeug für eine spezifische, fehleranfällige Domäne.

Der Prüfmechanismus: Claim, Judge, Verdikt

Der Kern ist ein dreistufiger Ablauf. Zuerst formuliert das Modell einen Claim, also eine Hypothese über die Binärdatei. Dann prüft ein deterministisches Werkzeug diesen Claim gegen das Artefakt. Zurück kommt VERIFIED, REFUTED oder INCONCLUSIVE, zusammen mit den Bytes, die tatsächlich beobachtet wurden. Das Modell darf niemals selbst eine Tatsache behaupten. Die Claims sind typisiert, und die Typen bestimmen, welche Prüfung greift. Es gibt byte-orientierte Arten wie bytes_at, pattern_present und string_present, typisierte Leseoperationen wie u16_at, u32_at und u64_at, die laut README keine Endianness-Arithmetik erfordern, sowie strukturelle Arten wie import_present, export_present und section_present. Für Verhalten gibt es emulate_result und behavior_equiv, für Beweise prove_equiv. Dazu kommen semantische Arten: function_at, calls, references und reachable_from_entry. Die semantische Schicht benötigt laut README angr für Funktionsgrenzen, Aufrufgraphen und Querverweise. Ohne angr fällt das Werkzeug auf den pure-Python-Kern zurück. Das ist eine wichtige Einschränkung: Die semantischen Claims hängen von einem optionalen Backend ab, und wer sie nutzt, sollte prüfen, ob dieses Backend installiert ist. Offsets sind Datei-Offsets, sofern ein Claim nicht explizit space auf rva oder va setzt. Dann übersetzt der Verifier über die Section-Tabelle und gibt alle drei Adressen zurück.

Installation und erste Befehle

Die Installation erfolgt aus PyPI. Der Befehl pip install reverify installiert den pure-Python-Kern. Wer capstone für Disassembly, unicorn für echte CPU-Emulation, lief für PE/ELF/Mach-O und Z3 für Beweise möchte, installiert pip install "reverify[full]". Für angr, das Funktionsgrenzen, Aufrufgraphen und Querverweise liefert, gibt es pip install "reverify[angr]". Der pure-Python-Kern installiert sich laut README sauber ohne Ghidra. Wer aus einem Checkout heraus arbeiten will, kann python reverify/cli.py auto sample.bin --json aufrufen, ohne etwas zu installieren. Weitere Beispiele aus dem README: python reverify/cli.py parse-pe sample.exe --json und python reverify/cli.py disasm 90505831C0C3 --arch x86_64. Der Verify-Aufruf nimmt einen Claim als JSON entgegen. Ein Beispiel aus dem README prüft einen Funktionsprolog an Offset 4096 mit den Mnemonics push, mov und sub. Ein zweites Beispiel prüft ein Emulationsergebnis: Der Code b805000000b90300000001c8c3 soll im x86-Modus den Wert 8 in eax erzeugen. Claims lassen sich über --claims-file claims.json bündeln. Der CLI-Prozess beendet sich mit einem von null verschiedenen Exit-Code, sobald irgendetwas widerlegt wurde. Damit lässt sich eine Pipeline oder ein CI-Job an einer fundierten Rekonstruktion aufhängen.

Der Rollover: Kontextwechsel ohne Verlust

Das zweite Standbein ist reverify rollover. Statt einer verlustbehafteten automatischen Zusammenfassung übergibt der Befehl die Sitzung an eine Datei und startet eine frische. Das soll verhindern, dass lange Aufgaben abdriften oder ein /clear nötig wird. Laut Release Notes zu v0.11.0 funktioniert das über Claude Code, Codex, Gemini CLI und OpenCode. Das ist ein anderer Ansatz als das übliche Vorgehen, bei dem ein Modell den bisherigen Verlauf zusammenfasst und dabei Details verliert. Ob der Rollover in der Praxis tatsächlich verlustfrei arbeitet, lässt sich aus dem vorliegenden Material nicht belegen. Das README behauptet es, und die Versionsnummer trägt die Formulierung 'lossless context rollover'. Wer das Werkzeug einsetzt, sollte diesen Punkt selbst überprüfen, weil die Qualität des Kontextwechsels direkt davon abhängt, was das Modell in der neuen Sitzung noch weiß. Unabhängig davon ist die Idee klar umrissen: Der Zustand liegt in einer Datei, nicht im Gesprächsverlauf, und die neue Sitzung liest ihn von dort.

Die Benchmark-Zahlen und was sie belegen

Das README nennt konkrete Zahlen. Auf 71 echten Windows-Systemdateien sei die textbook-Antwort der KI in 97 Prozent der Fälle falsch gewesen. reverify habe jeden dieser Fälle erkannt und nie einen falschen Claim akzeptiert, also 0 von 71. Dieselbe Prüfung laufe laut README bei jedem Push in CI auf Linux und macOS, und ein unabhängiger aarch64-Lauf habe dasselbe Ergebnis gefunden. Verwiesen wird auf EXAMPLE.md, BENCHMARK.md und das Skript python benchmarks/prologue_prior.py. Diese Zahlen sind der stärkste Teil des Projekts, weil sie einen konkreten Fehlerfall benennen und eine Gegenmaßnahme messbar machen. Sie sind aber auch eng gefasst: 71 Windows-Systemdateien, ein Prolog-Szenario, drei Plattformen. Wer daraus ableitet, dass reverify in jeder Domäne gleich gut funktioniert, überinterpretiert die Daten. Die Release Notes zu v0.10.0 sprechen von 'CI-gated benchmarks on three platforms, confusion matrix, reproducible corpus, receipts'. Das deutet auf eine bewusste Messdisziplin hin, ersetzt aber keine eigene Prüfung an den Artefakten, mit denen man tatsächlich arbeitet.

Wo das Werkzeug an Grenzen stößt

Die deutlichste Einschränkung ist die Abhängigkeit von optionalen Engines. Der pure-Python-Kern deckt PE/ELF/Mach-O-Parsing, x86/x64/ARM/ARM64-Disassembly, AOB-Mustersuche, CPU-Emulation, Protobuf/TLV-Zerlegung und Frida-Hook-Generierung ab. Für anspruchsvollere Prüfungen braucht es jedoch capstone, unicorn, lief, Z3 oder angr. Ohne diese Backends fällt das Werkzeug zurück, und die Frage ist, wie belastbar die Ergebnisse des Kerns in Grenzfällen sind. Das README sagt dazu nur, dass der Kern einspringt, nicht, wie groß der Genauigkeitsunterschied ist. Ein zweiter Punkt: Das Claim-Modell verlangt, dass man weiß, was man prüfen will. Wer explorativ arbeitet und noch keine Hypothese hat, muss erst eine formulieren, bevor reverify etwas tun kann. Das Werkzeug prüft, es entdeckt nicht. Drittens: Der Nonzero-Exit bei jeder Widerlegung ist für CI sinnvoll, kann aber in interaktiven Abläufen störend sein, wenn man bewusst mit unsicheren Vermutungen arbeitet. Und schließlich ist die Domäne begrenzt. Wer Quellcode-Refactorings absichern will, kann reverify equiv mit --lang python oder C nutzen. Für andere Sprachen oder für Systeme ohne ausführbare Referenzimplementierung fehlt dieser Weg.

Alternative: angr allein oder ein Modell ohne Prüfschicht

Der naheliegendste Vergleich ist angr, das reverify selbst als optionales Backend einbindet. angr ist ein symbolischer Ausführungsrahmen für Binäranalyse und liefert Funktionsgrenzen, Aufrufgraphen und Querverweise. Der Unterschied liegt im Ansatz: angr ist ein Analysewerkzeug, das Ergebnisse produziert, die man interpretieren muss. reverify setzt eine Prüfschicht darüber und macht aus einer Analyse ein Verdikt mit Beleg. Wer angr bereits nutzt, kann reverify als Gate davorschalten, um zu verhindern, dass ein Modell angr-Ausgaben falsch zusammenfasst. Der zweite Vergleich ist der Einsatz eines Sprachmodells ohne jede Prüfschicht. Das ist schneller und billiger, aber das README liefert mit den 97 Prozent falscher textbook-Antworten ein Argument dafür, dass Geschwindigkeit hier trügt. Wer allerdings ausschließlich mit Formaten arbeitet, die reverify nicht parst, oder wer keine reproduzierbare Prüfung benötigt, für den ist der zusätzliche Schritt reine Reibung. reverify ist kein Ersatz für angr, sondern eine Kontrollinstanz davor.

Wartung, Lizenz und was vor dem Einsatz zu prüfen ist

Das Projekt steht unter der MIT-Lizenz. Das ist eine permissive Lizenz, die kommerzielle Nutzung, Veränderung und Weitergabe erlaubt, solange der Lizenztext und der Urheberrechtsvermerk beibehalten werden. Rechtliche Beratung ist das nicht, und wer reverify in ein Produkt einbettet, sollte die genauen Bedingungen selbst prüfen. Die letzte Veröffentlichung ist v0.11.0 vom 4. September 2026, davor v0.10.0 und v0.9.1 am selben Tag. Diese Taktung deutet auf aktive Entwicklung hin. Die Versionsnummern liegen im Bereich 0.x, was bedeutet, dass sich Schnittstellen und Claim-Formate noch ändern können. Wer reverify in eine Pipeline einbaut, sollte die Claim-Dateien versionieren und bei Upgrades die Release Notes lesen, insbesondere zu Änderungen an Claim-Arten oder am Exit-Code-Verhalten. Die optionale Abhängigkeit von angr, capstone, unicorn, lief und Z3 bedeutet zudem, dass die Wartungslast nicht nur bei reverify liegt, sondern auch bei diesen Bibliotheken. Vor dem Einsatz lohnt es sich, reverify backends auszuführen und zu dokumentieren, welche Engines in der eigenen Umgebung aktiv sind, weil davon abhängt, welche Claim-Arten überhaupt prüfbar sind.

Redaktionelles Fazit

Wer KI-gestützte Reverse-Engineering-Aufgaben oder Code-Refactorings absichert und dabei auf nachvollziehbare Belege angewiesen ist, findet in reverify ein Werkzeug, das den Prüfschritt erzwingt. Wer schnelle, explorative Analysen ohne formale Verifikation sucht oder mit Binärformaten arbeitet, die die Toolbox nicht abdeckt, wird mit dem Claim-Modell und dem Nonzero-Exit bei Refutation mehr Reibung als Nutzen erleben. Vor dem produktiven Einsatz sollte die Ausgabe von reverify backends geprüft werden, um zu sehen, ob capstone, unicorn, lief und Z3 aktiv sind oder der pure-Python-Kern verwendet wird, denn davon hängt ab, welche Claim-Arten tatsächlich belastbare Ergebnisse liefern.

Offizielle Quellen

1. 2akouwu/reverify on GitHub
2. Issues
3. License: MIT
4. README
5. Releases