Reference
Tools, and what each one actually produced
A catalogue organised around one column: did this tool produce a working rewritten binary of the original specimen? For most of them the answer is no, and that is not a criticism.
Tool catalogues usually list capabilities. This one lists outputs, because the difference between an expression, a proof, a graph, a lifted module and a rewritten executable is the difference this course exists to teach. A tool that emits a simpler expression has done something valuable and has not deobfuscated a binary, and saying so is not a complaint about the tool.
Obfuscators
Four compilers and one post-link rewriter. Note that "working rewritten binary?" here asks about deobfuscation of the original specimen — an obfuscator producing a valid obfuscated program is the input to this course, not an output of it.
| Tool | Purpose / abstraction | Project use | Strongest retained result | Strongest limitation | Working rewritten binary? |
|---|---|---|---|---|---|
| OLLVM-16 (wwh1004 port) | LLVM IR substitution, bogus control flow and flattening | Independent treatments and O0–O3 comparisons on frozen showcase | All 24 intended O0 SUB IR sites; useful BCF/FLA positive controls for downstream rewriting | SUB canonicalization; global fallback after inactive annotation pilot; modern port is not the historical original implementation | Produces obfuscated PEs, not deobfuscation; downstream BCF/FLA rewrites passed. |
| Hikari LLVM15 | LLVM IR SUB/BCF/FLA/splitting | Existing locally patched production compiler; retained matrix and transfer cases | Working O0 FLA input and stock rewrite with 28/28 successor pairs | Annotation-only SUB pilot inactive; global enable flags used. BCF gates fold in native code; exact BCF IR text cannot be reparsed in tested frontend | Obfuscated originals passed; downstream O0 FLA rewrite passed. Not universal Hikari support. |
| Polaris LLVM16 | LLVM IR passes plus separate X86 MIR/backend transformations | Individual smoke validation, selected IR matrix and MBA/BCF/FLA studies | Strong executable MBA expansion; generic BCF proof/rewrite transfer; backend-obfu worked in separate smoke lane | Same requested seed insufficient for MBA/MIR reproducibility; stock FLA rewrite is WRONG; IR and MIR metrics cannot be conflated | Obfuscated originals passed; downstream BCF rewrite passed, stock FLA rewrite failed. |
| Tigress 4.0.11 | C source-to-source obfuscation | Environment-matched generated C for EncodeArithmetic, AddOpaque, Flatten; same C reused across optimization levels | Arithmetic remains substantial at /Ox; generated source exposes state/dispatch provenance | Initialized-state proof assumptions; stock indirect CFG discovery failure; whole generated file not seed-reconstructed reliably | Obfuscated originals passed; no working deobfuscated Tigress PE in this study. |
| BinProtect | Post-link x64 PE instruction/control-flow transformations | Eight controlled protected outputs and static follow-on analysis; virtualization disabled | Visible post-link arithmetic expansion and useful counterexample to naive opacity claims | 0/8 protected outputs valid at runtime; global processing can include runtime code; no exposed seed | No valid protected output in this study, hence no working end-to-end deobfuscation lane. No protected PE bundled. |
Semantic analysis and deobfuscation
Read the "strongest limitation" column beside the "strongest result" column. Every row on this site has both, and a page that shows you one without the other is not finished.
| Tool / workflow | Purpose / abstraction | Project use | Strongest retained result | Strongest limitation | Working rewritten binary? |
|---|---|---|---|---|---|
| Miasm | Native disassembly, semantic IR and symbolic execution | Extract local/whole-function expressions and support stock successor recovery | Usable ground-truth-linked expression and CFG evidence across families | Polaris complex MBA flag-AST growth; stock tool's Tigress jump-table discovery incomplete—do not generalize this to all Miasm integrations | Framework can support rewriting; here outputs depend on the integrating tool, notably ollvm-unflattener. |
| msynth AST/oracle | Simplify symbolic expressions via rewrites/oracle matches | Repeated-site and composed-expression comparisons with independent SMT checks | Selected local reductions; controls distinguish pre-existing canonical expressions from new recovery | Weak on remaining native MBA; oracle activity is not a causal proof of recovery; no full complex-return recovery | No; expressions and proof records only. |
| SiMBA | Algebraic linear-MBA simplification | Separate msynth pipeline mode, not stochastic search | Tigress partial reduction, including 305→79 nodes in a complex mixed return | Reduced expression may remain far from source; restricted representation/class assumptions | No; expression output, not PE reconstruction. |
| msynth Synthesizer | Search for smaller candidate expressions from behavior | Small three-XOR pilot, then a separate preregistered 12-site expansion and complete-expression probes | Ten of twelve expanded isolated-site candidates accepted with SMT proof | Two UNKNOWN; complete-expression searches failed within budget, including clean controls. Sampling alone is insufficient | No; candidates require independent equivalence checks. |
| ollvm-unflattener | Native CFG discovery plus Miasm symbolic successor recovery and patching | Untouched stock tool on O0/O2 cases, separately labelled diagnostics/assistance | OLLVM/Hikari O0 working canonical rewrites | Polaris wrong rewrite; Tigress discovery failure; optimized layouts and metadata assumptions | Yes for retained OLLVM/Hikari O0; not for all cases. |
| RPISEC llvm-deobfuscator methodology | Binary Ninja SSA state def/use traversal and local patching | Source inspection only; alternative conceptual comparison | Explains a different state-identification and patching strategy | No plugin execution or corpus success demonstrated; SSA alone does not resolve indirect discovery or multiway semantic-switch errors | Upstream is a patching methodology; no working output from it was produced here. |
| Triton | Actual-instruction dynamic symbolic analysis and SMT branch reasoning | Generic bounded harness, genuine-branch controls, symbolic writable globals and initialized Tigress state | 22/22 OLLVM and 16/16 Polaris gates proved; 3/3 Tigress under captured state | Exploration/model limits; state assumptions and UNKNOWN must be explicit. This is Salwan's DBA library, not GPU Triton | Not by the analysis alone. A separate project-local proof consumer produced passing OLLVM/Polaris branch-patched PEs. |
| Mergen | x64 PE function lifting to LLVM IR with internal simplification | Seventeen selected cases, raw/internal stages plus ordinary LLVM O2 and runtime contracts | 68 verifier-valid/recompilable modules; passing Polaris MBA lift with residual complexity | OLLVM SUB raw lift already wrong; helper/memory contracts restrict execution; valid IR is insufficient | No rewritten original PE. Recompiled validation harnesses are a different deliverable. |
Manual inspection
No core exercise in this course requires a paid decompiler or a commercial binary-analysis platform. Every lab has a route that works from the supplied source, IR, text disassembly, result files and SVGs — on Linux, offline. A disassembler makes some of them faster and none of them possible.
| Tool | Purpose / abstraction | Project use | Strongest result | Limitation | Working rewritten binary? |
|---|---|---|---|---|---|
| IDA | Native disassembly, graph navigation; optional decompiler depending on installation | User-provided target graphs and instruction comparisons | Readable semantic landmarks and a Tigress switch/jump-table view | A recovered view is not a complete/correctness proof; licensing/features vary; supplied images are not pseudocode | No automatic recovery result claimed. |
| Diaphora | Function matching and binary-diff views within IDA | User-supplied primary/secondary graph and assembly comparisons | Side-by-side structure makes residual code and rewritten routing visible | Colours/similarity are not equivalence; database hashes/tool versions not supplied; two screenshot identities need review | No working rewrite claim; diff analysis only. |
| x64dbg | Windows native debugging | Intended manual setup/use for the retained PE examples; export/RVA instructions supplied | Enables optional breakpoint/step/return-value observation on Windows | No new debugger session was run or validated in this handoff; not a native Linux tool; stale PDB and ASLR caveats | No automated deobfuscation result claimed. |
What each workflow emits
The same question, as a single table: given an input, what comes out, and what is the boundary on it?
What does each deobfuscator actually produce?
Expression recovery, a branch proof, LLVM IR and a rewritten PE are different outputs.
| Workflow | Input / idea | Delivered result | Boundary to remember |
|---|---|---|---|
| msynth AST/oracle | Extracted expression; rewrite / match | Simpler expression | No rewritten PE in this study. |
| SiMBA | Algebraic MBA simplification | Simpler expression | Partial reduction is not full recovery. |
| Synthesizer | Search for a small expression | Candidate expression | Accept only after equivalence proof. |
| ollvm-unflattener | Discover states; recover successors | Rewritten PE or failure | A produced PE can have wrong semantics. |
| Triton DSE/SMT | Symbolic branch conditions | Proof / witness | Analysis itself does not patch the PE. |
| Proof-driven rewriter | Consume proofs and exact bytes | Patched PE | Predicates and dead bytes can remain. |
| Mergen | Lift x64 instructions | LLVM IR | Valid IR can silently miscompute. |
| Ordinary LLVM O2 | Optimize retained or lifted IR | Optimized IR | Cannot repair an unsound lift. |
Ask two questions: what representation was recovered, and how was its correctness checked?
PE = Windows Portable Executable. The Mergen test harness is not a rewritten original PE.Open the original lecture figure (SVG)
Two names that collide
Triton in this course is Jonathan Salwan's dynamic binary-analysis and SMT framework. It is not the GPU kernel compiler of the same name, and searching for the wrong one will waste an afternoon.
Virtualization in this course means translating protected behaviour into custom bytecode run by an embedded interpreter. It does not mean the Windows virtual machine the lab runs in. No virtualization or devirtualization experiment was performed in this corpus, so week 12 treats it as an endpoint the course can point at and cannot measure.
Lab access and the execution boundary
All twenty-one specimens are Windows x64 PE files. Reading them — source, IR, disassembly, graphs, result files — works on any platform, and that is the route every core exercise uses. Executing or debugging them needs the course's Windows x64 lab image. No Wine or Linux-rebuild equivalence is claimed: a Linux rebuild would be a different specimen with a different ABI and different lowering, and it must not be silently substituted for these results.
See BINARY_GUIDE.md for the per-specimen execution status, and the evidence page for why no executable is downloadable from this site.