Projekt · Werkzeug für Reverse Engineering
pe-analyzer
Beantwortet eine einzige Frage: Liefern diese zwei Funktionen bei gleichem Input den gleichen Output? Wenn nicht, kommt die konkrete Eingabe heraus, bei der sie auseinanderlaufen.
Wozu
Beim Reverse Engineering muss man nicht den Originalquelltext rekonstruieren, sondern irgendeinen lesbaren Quelltext, der dasselbe tut. Was dabei fehlt, ist ein belastbares Kriterium, ob ein Kandidat wirklich dasselbe tut. Genau das ist dieses Werkzeug – ohne LLM, ohne Raten.
Wie
Beide Funktionen werden mit denselben symbolischen Eingaben ausgeführt, dann fragt ein SMT-Solver je Pfadpaar, ob es Eingaben gibt, bei denen die Ergebnisse abweichen. Ein Beispiel aus den Tests: x*2+y mit -O3 (eine einzige Instruktion) gegen dieselbe Rechnung mit -O0 (zwölf Instruktionen) – bewiesen äquivalent.
Jedes gefundene Gegenbeispiel wird zusätzlich nativ auf der CPU nachgeprüft. Ein Solver-Timeout wird nie als Beweis durchgereicht, und jedes Ergebnis nennt seine Annahmen im Klartext.
Tech-Stack
| Ebene | Technologie |
|---|---|
| Sprache | Python |
| Symbolische Ausführung | angr, VEX |
| Solver | Z3 |
| Formate | PE/COFF und ELF, AMD64 |
| Tests | pytest, native Gegenprüfung, MinGW für PE-Fälle |
Skills
Weitere Projekte
Ähnliches vor?
Erzählen Sie mir per E-Mail, was Sie vorhaben. Das Erstgespräch ist kostenlos.