Protected binary analysis:
a practical workflow
A protected binary analysis workflow is a repeatable method for studying an executable whose code was packed, obfuscated or virtualized to resist analysis. This guide divides the work into six stages: identify the protection, classify the functions that matter, recover them, validate the recovery, review the output in your own tools, and document the evidence boundary.
Each stage produces what the next one needs: a protection profile, a function list, recovered code, a validation record and reviewed output. The last stage writes down what the evidence still does not prove. The guide is written for authorized work, such as malware research, security audits and interoperability, and it covers methods, not tool recipes.
What is a protected binary analysis workflow?
A protected binary analysis workflow is a repeatable sequence that turns a protected executable into validated evidence: recovered code that behaves like the original, in a format your tools can open, with its limits written down. General reverse engineering workflows treat protection as an obstacle met along the way. A protected binary analysis workflow starts from it, and adds the stages that protection makes necessary.
Two published models describe the general reverse engineering process. Lenny Zeltser's four stages of malware analysis, first published in 2014, take the malware analysis process from fully automated analysis through static properties and interactive behavior analysis to manual code reversing. A 2020 USENIX Security study by Daniel Votipka and colleagues observed 16 reverse engineers and modeled their work in three phases: overview, sub-component scanning and focused experimentation.
Zeltser's stages and the Votipka model both meet protection early. In the Votipka study, two participants unpacked malware samples before starting their overview, because strings and imported functions only became intelligible after unpacking. Virtualized code goes further: unpacking does not make it readable, as stage 3 explains.
A protected binary analysis workflow assumes the analysis is authorized. Devirt's acceptable use policy requires that you own or have authorization to analyze every binary you submit, and it states that a supported VM family does not establish permission to analyze a particular binary.
Stage 1: Identify the protection
Identifying the protection is the first stage of a protected binary analysis workflow: name the protector family and the techniques it applied before reading any code.
MITRE ATT&CK technique T1027.002 describes two protection techniques. Software packing compresses or encrypts an executable, and most decompression techniques restore the code in memory. Virtual machine software protection translates the original code into a special format that only a special virtual machine can run.
A commercial protector can combine packing and virtualization. VMProtect's user manual describes protecting different parts of one program with different methods: part of the code virtualized, part obfuscated, and critical fragments protected with a combined method. One file can therefore hold native, obfuscated and virtualized functions side by side. The VMProtect research hub and the Themida research hub cover those two families in detail.
The evidence for identifying the protection is static. Zeltser lists packer signatures, header details, strings and embedded resources among a file's static properties, and his SANS guide to learning malware analysis adds entropy as a check for packed or obfuscated code.
Record anti-analysis checks in the protection profile as well. MITRE ATT&CK describes debugger evasion and virtualization and sandbox evasion, in which a program checks for a debugger, a virtual machine or a sandbox and changes its behavior based on the result. A sample with those checks can behave differently in a lab, which limits what observation alone can show.
The output of stage 1 is a protection profile: the protector family, the techniques in use, and the parts of the file each technique covers.
Stage 2: Classify the functions that matter
Classifying the functions is the second stage: decide which functions carry the logic your question depends on, and which protection each of those functions sits behind.
Reverse engineers already classify functions this way. In the Votipka study, participants used their overview to prioritize sub-components, such as functions, and reviewed in detail only the ones most likely to yield useful results. Protection raises the cost of every detailed review, so the prioritization matters more here.
A working classification records, for every function on the list:
- the question the function answers for your investigation;
- its protection group: unprotected, packed only, obfuscated, or virtualized;
- whether your conclusion needs the function proven or only readable.
Only the virtualized functions need devirtualization. A packed-only function becomes readable once the code is unpacked; a virtualized function does not.
Fix the unit of analysis during classification too. Functions, basic blocks, instruction handlers and reachable paths are different units, and two results are only comparable when they count the same one. The function list from stage 2 becomes the denominator that stage 6 reports against.
Stage 3: Unpack, deobfuscate or devirtualize
Recovery, the third stage, gives each function only the treatment its protection requires: unpacking for packed code, deobfuscation for obfuscated code, and devirtualization for virtualized code.
The guide Devirtualization vs deobfuscation vs unpacking sets out what each of the three recovers and what it leaves unsolved.
Unpacking restores code that a packer compressed or encrypted. It does not restore virtualized functions. VMProtect's manual states that virtualized fragments are executed by the interpreter of its virtual machine without being transformed into machine language code of the physical processor, so the unpacked program still contains the interpreter and its bytecode, not the original instructions.
Deobfuscation removes transformations that make code harder to read without changing what it computes. VMProtect's manual describes its mutation method as adding garbage commands, dead code and random conditional jumps, and as rewriting original commands. Deobfuscation reverses that kind of change so the original operations can be read again.
Devirtualization recovers the original logic of a virtualized function. The manual approach, as VMProtect's documentation puts it, comes down to building a disassembler for the architecture the virtual machine imitates and then analyzing the disassembled code. The same manual notes that one application can use several virtual machines, and each one needs that work. Automated approaches can work from execution traces instead. In a 2018 paper, Jonathan Salwan, Sébastien Bardin and Marie-Laure Potet combined taint analysis, symbolic path exploration and recompilation to recover devirtualized code from virtualized functions.
VMProtect's manual calls creating a disassembler for a properly implemented virtual machine quite a difficult task, which is why stage 2 matters: devirtualize the functions your question needs, not every function the protector touched. Devirt's devirtualization methods research compares the main approaches.
Stage 4: Validate the semantics
Validating the semantics is the fourth stage: check that each recovered function computes what the protected original computes, and state the conditions under which that check holds.
Devirtualization does not give back the original bytes. The 2018 paper by Salwan, Bardin and Potet notes that recovering 100% of the original binary code is impossible in general, so the goal is code that is semantically equivalent to the original.
Readable output is not the same as correct output. A recovered function can look plausible and still disagree with the original on inputs nobody tried.
These two validation methods establish different things:
- Comparison on inputs. Run the original and the recovery on the same inputs and compare the results. Agreement covers the inputs that were tested and nothing more.
- Solver-based equivalence checking. Ask a solver for any input on which the two versions disagree under a stated model. UNSAT, meaning no such input exists within the model, supports equivalence within those assumptions. SAT returns a counterexample. A timeout leaves the question unresolved.
The 2018 DIMVA paper draws this line formally. Local correctness means the recovered and original programs behave the same for a given input; completeness means that holds for every input. Local correctness can often be guaranteed, depending on the properties of each step in the method, but completeness is lost in general because it requires exploring every path through the virtualized program. It can be recovered for functions with few paths, which is the case for many hash functions. The paper's controlled experiment used 20 hash algorithms.
Devirt applies both kinds of validation check. Eligible operations receive formal checks, and the lifted LLVM representation and independently compiled native execution are compared with the original observations. Solver counterexamples and timeouts remain visible in the result, and they are not counted as proof. The how it works page shows each check in turn.
Stage 5: Review tool-ready output
The fifth stage is a review of tool-ready output: open the recovered code in your own tools and check it against the validation record before you rely on it.
Tool-ready output means the analysis continues where your team already works. Votipka and colleagues found that reverse engineers chose to use a tool when its input and output could be closely associated with the code and when the tool improved code readability. Recovered output that opens in your existing disassembler meets both conditions.
Devirt delivers recovered work in five formats: an IDA database, annotated pseudocode, a full reverse engineering report, LLVM IR and structured API JSON. IDA output is checked after it is saved and reopened.
Before relying on recovered output, confirm three things:
- Named functions and typed calls match the functions in the validation record.
- Every function your conclusion depends on is marked proven, not only readable.
- The build, the unit of analysis and the assumptions match the ones set in stages 1 and 2.
Stage 6: Document the evidence boundary
Documenting the evidence boundary is the final stage: write down what the analysis proved, what it did not, and why, against the denominator fixed in stage 2.
Devirt reports every unit in one of four coverage categories:
- Proven: verified within the declared model.
- Runtime-dependent: a real input or environment still matters.
- Unresolved: the available evidence did not settle an in-scope unit.
- Permanently bounded: an explicit analysis limit remains.
The four coverage counts must sum to the total, so a unit cannot disappear from the result because it was difficult. A result should also name its analysis unit, the exact build and the execution assumptions, because a percentage without them cannot show whether two analyses are comparable.
Counterexamples and timeouts belong in the evidence record. A counterexample indicates a mismatch under the tested conditions, and a timeout indicates a question that did not settle within its budget. Neither is a proof. The note on how to read a devirtualization coverage figure explains how to read each category.
Nothing disappears from the denominator.
This teaching ledger contains 100 selected operations: 86 proven, 7 runtime-dependent, 2 unresolved, and 5 permanently bounded. Every unit is counted exactly once.
Synthetic, not a service benchmark. Solver SAT and timeout counts are separate outcomes, not extra coverage buckets.
How static, dynamic and devirtualization stages combine
Static analysis, dynamic analysis and devirtualization answer different questions, so a protected binary analysis workflow uses each one where its evidence is strongest.
A 2019 survey of binary code similarity by Irfan Ul Haq and Juan Caballero sets out the trade-off between static and dynamic analysis. Static analysis examines code without running it and can cover all of the code it can see. Dynamic analysis examines one execution at a time, and it knows runtime values that static analysis has to work out, such as memory addresses and the targets of indirect jumps. Votipka's participants used more static analysis in their first two phases and switched to dynamic methods during focused experimentation.
| Technique | What it reads | What it can establish | What protection hides from it |
|---|---|---|---|
| Static analysis | The file without running it: headers, strings, imports, disassembly | Structure and every path in the visible code | Packed code until it is unpacked; the logic of virtualized functions |
| Dynamic analysis | One execution at a time, in an isolated lab | Behavior for the inputs and environment observed | Paths that did not run; behavior that changes when a debugger, virtual machine or sandbox is detected |
| Unpacking | The code a packer compressed or encrypted | The original code of packed-only functions | Virtualized functions, which stay virtualized |
| Devirtualization | The virtual machine's bytecode and handlers | The original logic of virtualized functions, as far as validation supports it | Conditions that depend on a real input or environment |
| Validation | The recovery next to the original | Equivalence within a stated model, or agreement on tested inputs | Anything outside that model or those inputs |
Read against Zeltser's pyramid, protection touches every level: static properties meet the packer first, automated and interactive behavior analysis meet anti-analysis checks, and manual code reversing meets the virtualized functions. The binary analysis research hub covers static and dynamic analysis in more depth.
When to use Devirt
Devirt fits stages 3 and 4 of the workflow when the functions you need sit behind a supported virtual machine protector. Supported families include VMProtect 2.x and 3.x, Themida and Code Virtualizer, Enigma Protector, Obsidium, and known Loki derivatives such as Obfuscator X and Griffin. Every Loki-derived binary needs its own free assessment; these protections are not offered as automated profiles. The VMProtect devirtualization, Themida devirtualization and Enigma Protector devirtualization pages list what each service supports, as do the Obsidium devirtualization and Loki VM devirtualization pages.
Each Devirt result arrives in the output you choose, with its ledger, proof summary and remaining limits: the evidence boundary described above. Complex or unfamiliar builds receive a free feasibility assessment after you create an account and upload your file. We email the estimated coverage and written quote; the synthetic sample assessment shows what that report contains.
For work beyond devirtualization, the protected binary analysis service covers packed, obfuscated and virtualized executables, software reverse engineering services cover protected and ordinary binaries, and the malware analysis service produces an evidence-backed behavioral report for an unknown file.