> For the complete documentation index, see [llms.txt](https://devirt.gitbook.io/devirt/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://devirt.gitbook.io/devirt/glossary.md).

# Glossary

Glossary of binary devirtualization and reverse engineering terms: VM-based obfuscation, bytecode, VM handler, dispatcher, lifting, LLVM IR, equivalence checks and the coverage ledger outcomes.

## Protection and devirtualization

### Binary devirtualization

Recovering the logic of a program whose code was translated into bytecode for a private virtual machine, and rewriting it as native-shaped functions that are readable again. This is Devirt's core service.

### Virtualization-based obfuscation

A protection technique that replaces selected native instructions with bytecode run by an interpreter embedded in the program. VMProtect, Themida and Code Virtualizer use it.

### Bytecode

The instruction stream of a protector's virtual machine. Its format is private to the protector.

### VM handler

A routine inside the embedded interpreter that carries out one virtual instruction, such as a push, an arithmetic operation or a branch.

### Dispatcher

The interpreter loop that fetches the next bytecode instruction and transfers control to the matching handler.

### Virtual machine state

The virtual registers, stack and flags the interpreter keeps while it runs bytecode. Devirt reconstructs this state and the virtual machine's control flow.

### Native-shaped function

A recovered function expressed as ordinary code, in IDA, pseudocode or LLVM IR, instead of as interpreter activity.

### Lifting

Translating machine code or recovered operations into an intermediate representation for analysis.

### LLVM IR

The intermediate representation of the LLVM compiler infrastructure. Devirt delivers LLVM IR as an output format and uses it in its differential check.

### Compiler devirtualization

A C++ optimization in GCC and LLVM that replaces virtual function calls with direct calls. It is a different subject from binary devirtualization.

## Checks and results

### Solver check

A search, inside a declared model, for any input on which recovered and original code behave differently. An UNSAT answer supports equivalence within the model, a SAT answer exposes a disagreement, and a timeout means the question stays open.

### Differential check

A comparison of recovered operations, lifted to LLVM IR, against what the original program was observed to do and against native execution on selected inputs.

### Coverage ledger

The inventory delivered with each Devirt recovery: it lists the code in scope, assigns every part one of four outcomes and records the exact build and assumptions.

### Proven

The ledger outcome for code whose comparison succeeded under the stated assumptions.

### Runtime-dependent

The ledger outcome for code that can only be settled with a real input or environment.

### Unresolved

The ledger outcome for code the available evidence was not able to decide.

### Permanently bounded

The ledger outcome for code where a stated limit rules out any stronger conclusion.

### Agreed scope

The code and inputs a job is defined to cover. Verification applies inside that scope, not to every behavior the program might have.

## Ways to start

### Browser check

A no-cost, local inspection of a file's format and protection signs that never uploads the file.

### Community Triage

A no-cost inventory of a file and its protection indicators, available to verified accounts.

### Feasibility assessment

A no-cost review of a complex file that ends in a written scope, a coverage estimate and a quote; paid work waits for the customer's approval.