Project · Reverse engineering tool
pe-analyzer
Answers a single question: do these two functions return the same output for the same input? If not, you get the concrete input where they diverge.
Why
In reverse engineering you do not need the original source code, just some readable source that does the same thing. What is missing is a reliable criterion for whether a candidate really does. That is exactly what this tool provides – no LLM, no guessing.
How
Both functions are executed with the same symbolic inputs, then an SMT solver asks for each pair of paths whether any input makes the results differ. An example from the tests: x*2+y compiled with -O3 (a single instruction) against the same computation with -O0 (twelve instructions) – proven equivalent.
Every counterexample found is additionally checked natively on the CPU. A solver timeout is never passed off as a proof, and every result states its assumptions in plain text.
Tech stack
| Layer | Technology |
|---|---|
| Language | Python |
| Symbolic execution | angr, VEX |
| Solver | Z3 |
| Formats | PE/COFF and ELF, AMD64 |
| Tests | pytest, native cross-check, MinGW for PE cases |
Skills
More projects
Planning something similar?
Tell me by email what you have in mind. The first conversation is free.