Reverify : quand l'outil déterministe arbitre les affirmations du modèle

Le problème précis : un modèle qui invente des offsets

Le README pose le constat sans détour : un modèle de langage est bon pour lire du code source et peu fiable pour reconstruire une structure ou un algorithme à partir d'un binaire. Il produit des offsets, des tailles et des comportements plausibles, énoncés sur le ton de la certitude. En analyse de binaires, cette tendance est plus marquée qu'ailleurs, parce que rien dans le contexte ne permet de contredire l'affirmation. La question « est-ce que le modèle vient d'inventer cela ? » est présentée comme le principal frein à l'usage d'un assistant pour de la rétro-ingénierie réelle. Reverify vise donc un public précis : analystes malware, joueurs de CTF, chercheurs en interopérabilité, et plus généralement toute personne qui fait travailler un agent sur un artefact binaire dont elle a le droit d'analyse. Le projet rappelle cette condition dans son README et renvoie à SECURITY.md. Ce n'est pas un outil d'exploration libre de binaires tiers.

La boucle de vérification : le modèle propose, l'outil tranche

Le mécanisme central tient en une inversion de rôle. Une affirmation, appelée claim, est une hypothèse sur le binaire. Elle est transmise à des outils déterministes qui renvoient VERIFIED, REFUTED ou INCONCLUSIVE, accompagnés des octets réellement observés. Le modèle ne peut donc pas poser un fait de lui-même. Les types de claims listés dans le README couvrent des lectures typées comme bytes_at, u16_at, u32_at et u64_at, des recherches de motifs et de chaînes, des séquences d'instructions avec mnémoniques et éventuellement opérandes, l'émulation avec emulate_result, la comparaison de comportement via behavior_equiv, la preuve avec prove_equiv, la dissection Protobuf, et des vérifications d'imports, d'exports et de sections. Les offsets sont des offsets de fichier sauf mention contraire : un claim peut préciser "space": "rva" ou "va", et le vérificateur traduit via la table des sections en renvoyant les trois adresses. Ce détail compte, car c'est exactement le genre de conversion qu'un modèle rate en silence. Le noyau déterministe couvre l'analyse PE, ELF et Mach-O, le désassemblage x86, x64, ARM et ARM64, le balayage de motifs AOB, l'émulation CPU, la dissection Protobuf et TLV, et la génération de hooks Frida.

Le noyau pur Python et ses moteurs optionnels

L'installation de base est en Python pur, sans Ghidra, et le README insiste sur le fait qu'elle s'installe proprement. C'est un choix de conception qui a un coût : le noyau maison est nécessairement moins complet que des bibliothèques éprouvées. Reverify traite ce point par une mise à niveau en place. `pip install "reverify[full]"` remplace le cœur par capstone pour le désassemblage, unicorn pour l'émulation CPU réelle, lief pour les formats PE, ELF et Mach-O, et Z3 pour les preuves. `pip install "reverify[angr]"` ajoute angr pour les frontières de fonctions, le graphe d'appels et les références croisées. Si un moteur n'est pas installé, le système retombe sur le noyau pur Python. La commande `reverify backends` indique ce qui est actif. Le point à retenir : le comportement du vérificateur dépend de votre environnement d'installation. Deux machines peuvent rendre des verdicts différents sur le même claim, non par bug mais parce que l'une dispose d'unicorn et l'autre non. Pour un usage en intégration continue, cela impose de figer les extras installés, sinon la porte de vérification n'a pas la même sensibilité d'un runner à l'autre.

Mise en route : commandes et clés de configuration

Le README donne deux chemins. Depuis PyPI : `pip install reverify`, puis `reverify auto sample.bin --json`. Depuis un checkout, sans rien installer : `python reverify/cli.py auto sample.bin --json`, `python reverify/cli.py parse-pe sample.exe --json`, ou encore `python reverify/cli.py disasm 90505831C0C3 --arch x86_64`. La vérification d'un claim passe par `reverify verify sample.bin --claim` suivi d'un objet JSON, par exemple un claim de type instructions avec un offset, une liste de mnémoniques et une note. Un claim d'émulation s'écrit avec `reverify verify - --claim` et un objet contenant le code, l'architecture et les registres attendus. Le tiret seul indique que l'entrée vient de l'entrée standard. Les claims peuvent être regroupés dans un fichier et passés via `--claims-file claims.json`. Le détail qui rend l'outil utilisable dans un pipeline : le CLI sort avec un code non nul si quoi que ce soit est réfuté. Un agent ou un job d'intégration peut donc s'arrêter sur une reconstruction non fondée. Le serveur MCP, lui, expose les mêmes outils aux agents qui le prennent en charge, Claude Code et Cursor étant cités.

Le terrain d'épreuve : 71 fichiers système Windows

Le README choisit la rétro-ingénierie de binaires comme terrain de démonstration, au motif que c'est là que l'hallucination est la plus grave. Sur 71 fichiers système Windows réels, la réponse « de manuel » du modèle était fausse dans 97 % des cas selon les chiffres avancés, et reverify aurait attrapé chacune de ces erreurs sans jamais accepter une affirmation fausse, soit 0 sur 71. La même porte tournerait en intégration continue sous Linux et macOS à chaque push, et une exécution indépendante sur aarch64 aurait donné le même résultat. Les sources citées sont EXAMPLE.md, BENCHMARK.md et le script `python benchmarks/prologue_prior.py`. Ces chiffres proviennent du projet lui-même et je ne les ai pas reproduits. Le script est fourni, ce qui permet de les contester ou de les confirmer sur vos propres fichiers, et c'est la bonne façon de traiter une telle affirmation. Un point de méthode mérite d'être noté : ce corpus est mono-plateforme à l'origine, ce qui explique probablement pourquoi la version v0.9.1 corrige un routage ARM64 et pourquoi la v0.10.0 met en avant des benchmarks sur trois plateformes. La couverture multi-architecture s'est construite après coup, pas dès le départ.

La couche sémantique et la question des moteurs absents

Les claims de type function_at, calls, references et reachable_from_entry forment ce que le README appelle la couche sémantique. Ce sont eux qui dépendent le plus des moteurs optionnels. Le titre de la v0.9.1 est explicite : « ARM64 routing fix (#5) + soundness without the engines ». Autrement dit, la solidité du raisonnement en l'absence des moteurs a été traitée comme un sujet à part entière, ce qui suggère que ce n'était pas acquis. Ma lecture est que le noyau pur Python reste le mode le plus fragile sur les claims sémantiques, précisément parce qu'il ne dispose ni des frontières de fonctions d'angr ni de la désassemblage de capstone. Un verdict INCONCLUSIVE sur un claim function_at n'a donc pas la même valeur selon les extras installés. C'est une limite réelle, pas un détail d'installation, et elle doit figurer dans la façon dont vous interprétez les résultats.

reverify equiv : la vérification hors binaire

Le projet ne se limite pas aux binaires. La commande `reverify equiv <reference> <candidate> --lang python`, également disponible pour C, exécute une implémentation candidate et une implémentation de référence sur des entrées partagées et vérifie qu'elles produisent le même résultat. Une réfutation revient avec l'entrée et les deux sorties. L'usage visé est la réécriture ou le refactoring produit par une IA : testé plutôt que cru. C'est une approche différente de la revue de code, parce que la charge de la preuve change de camp. Le modèle ne dit pas « ce code est équivalent », il fournit un candidat que le harnais compare. La limite est celle de tout test différentiel : la qualité du verdict dépend des entrées partagées. Le README ne décrit pas la stratégie de génération de ces entrées, donc je ne peux pas dire si elle est aléatoire, exhaustive ou fournie par l'utilisateur. C'est une zone à examiner avant de s'appuyer dessus pour valider une refonte.

rollover : garder le contexte sans le résumer

Le second usage de Reverify ne concerne pas la vérité mais la mémoire de session. `reverify rollover` transfère la session dans un fichier et en démarre une nouvelle, au lieu de produire un résumé automatique avec perte. Le README cite Claude Code, Codex, Gemini CLI et OpenCode. La version v0.11.0, publiée le 4 septembre 2026, annonce un « lossless context rollover » sur ces quatre outils. L'argument est que les longues tâches dérivent ou obligent à faire un /clear. Le mécanisme est un passage de relais par fichier, ce qui évite la compression destructive. Le point à vérifier soi-même : le format du fichier de passation et la façon dont chaque agent le relit ne sont pas détaillés dans le matériel fourni. La promesse de ne rien perdre repose sur la fidélité de ce fichier, et je ne peux pas la confirmer à partir de ce que j'ai.

Limites, coût de maintenance et alternatives

La limite la plus concrète est celle des moteurs optionnels : sans capstone, unicorn, lief ou Z3, vous n'utilisez qu'une partie du vérificateur, et les verdicts s'en ressentent. La deuxième est le périmètre d'analyse : le projet s'adresse à de la rétro-ingénierie autorisée, et le README renvoie à SECURITY.md pour les conditions. La troisième tient à la nature de la vérification : un claim REFUTED ou INCONCLUSIVE ne dit rien sur ce qu'il faudrait croire à la place, il constate seulement que l'hypothèse ne tient pas. Le rythme de publication est rapide, avec plusieurs versions en quelques jours début septembre 2026, ce qui implique de suivre les notes de version si vous épinglez une version en production. La licence est MIT, ce qui autorise la réutilisation et la modification, y compris dans un contexte commercial, à condition de conserver l'avis de licence et de copyright. Ce paragraphe n'est pas un conseil juridique. Comme alternative, on peut citer l'usage direct de capstone, unicorn ou lief depuis un script maison : vous gardez le contrôle total du pipeline et de la stratégie de vérification, mais vous écrivez vous-même la logique de verdict, la traduction d'adresses entre offset de fichier, RVA et VA, et l'agrégation en code de sortie. Reverify fournit cette couche déjà assemblée, au prix d'une dépendance à ses choix de conception et à son rythme de publication.

Conclusion éditoriale

Reverify convient aux équipes qui font déjà travailler un agent sur des binaires et qui veulent un point d'arrêt déterministe avant qu'une hypothèse ne devienne un fait : le CLI sort en code non nul dès qu'une affirmation est réfutée, ce qui permet de bloquer une reconstruction non fondée. Il ne convient pas à qui cherche un désassembleur interactif ou une couverture multi-architecture complète, ni à qui analyse du code sans droit d'analyse. Avant de l'adopter, lancer `reverify backends` pour connaître les moteurs réellement actifs, puis `python benchmarks/prologue_prior.py` pour reproduire la mesure sur vos propres fichiers.

Sources officielles

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