Devirt (devirt.re) is a binary devirtualization and reverse engineering service for security researchers and malware analysts. Protectors such as VMProtect and Themida hide a program's logic inside a private virtual machine. Devirt follows the protected program as it runs, reconstructs the virtual machine's state and control flow, converts that behavior into native-shaped functions and checks them against the original. Customers choose the output they need: an IDA database, annotated pseudocode, a reverse engineering report, LLVM IR or structured JSON.

That is the short version. This first issue explains what it means in practice.

The problem Devirt works on

Some software protectors do more than pack or encrypt a file. They take selected functions, translate them into bytecode for a virtual machine that exists only inside that program, and ship an interpreter to run it. Open the result in IDA or any other disassembler and you are reading the interpreter: a dispatcher, a set of handlers and a lot of indirection. The logic you actually care about is no longer there in readable form.

Recovering it by hand is slow, careful work. Someone has to rebuild the dispatcher, work out what every handler does, and then convince themselves that each recovered function really behaves like the original. Only after all that does the real question, what does this code do, become answerable.

What Devirt does instead

Devirt watches the protected program execute and rebuilds the virtual machine's state and control flow from what it observes. It then rewrites that behavior as ordinary, native-shaped functions and puts each one through three checks:

• A solver check. A solver hunts, inside a declared model, for an input that makes the two versions behave differently. If it proves none exists (UNSAT), that supports equivalence within the model; if it finds one (SAT), there is a real disagreement; if time runs out, the comparison stays open.
• A differential check. Devirt lifts what it recovered into LLVM IR, then runs it side by side with the original program's observed behavior and with native execution on a set of chosen inputs.
• An IDA persistence check. When the delivery is an IDA database, Devirt writes it to disk, opens it again and confirms that every function name and typed call survived.

Saying exactly what is proven

Every Devirt result comes with a coverage ledger. It lists the code in scope and gives each function one of four outcomes:

• Proven: the comparison passed under the stated assumptions.
• Runtime-dependent: it cannot be settled until a real input or environment is supplied.
• Unresolved: what Devirt could observe did not settle the question either way.
• Permanently bounded: a limit, written down in the ledger, prevents any stronger claim.

Each ledger names the exact build it describes and the assumptions it relies on, so a coverage figure never travels without its limits.

Which protections

VMProtect, Themida and Code Virtualizer have automated paths, with eligibility confirmed for each exact build. Enigma Protector, Obsidium, Loki-based virtual machines, JavaScript virtual machines, .NET virtualizers and custom virtual machines start with a free assessment of every file. Ordinary, unprotected binaries can be analyzed too. The current list is on devirt.re/supported-protectors.

Who sends files to Devirt

Reverse engineering consultancies, malware analysts, vulnerability researchers, software owners, interoperability teams, supply-chain security teams, and trust and safety teams. Devirt only analyzes software that its customers own or are authorized to examine, and it returns inspectable logic, not the original source code.

Trying it

There are three ways to start without paying anything: a browser check that inspects a file on your own device without uploading it, Community Triage for a verified account, and a feasibility assessment, in which a complex file gets a written scope, an estimate of expected coverage and a price. Paid work only starts once that quote is approved. Prices are on devirt.re/pricing.

One last note, because the word causes confusion: Devirt (devirt.re) is not related to compiler devirtualization, the C++ optimization in GCC and LLVM that replaces virtual function calls with direct calls.

Later issues will look at individual topics in more depth. In the meantime, the research archive is at devirt.re/research and the knowledge base is at devirt.gitbook.io/devirt.