Recovering BinaryShield VM bytecode into clean LLVM IR

1. Problem

BinaryShield replaces the original function at 0x1400016d0 with a native x86-64 VM. The VM entry pushes a bytecode RVA, initializes VM context, dispatches through native handlers, and uses indirect jumps to select the next handler.

The output we want is LLVM IR for the original program behavior. For this sample, the recovered function takes the Windows x64 first integer argument in rcx and returns the result through rax.

What makes it hard

• Handler targets are computed from bytecode and handler-table values instead of appearing as direct native branches.
• Original program values and VM book-keeping share x86 registers and memory.
• Branch conditions are encoded as VM stack values and dispatch choices.
• The lifter emits a memory-root model through @RAM, so stack, image, TEB, PEB, and VM context initially look like the same address space.

2. Pipeline

The implementation follows the phased design in devirt-plan.md. Each handler is partially evaluated under an abstract state. The resulting graph is rebuilt as one LLVM function and optimized.

Optimization boundary

The tracer does not need to know which constants are VM internals. It records concrete facts. LLVM decides which computations are dead after dispatch is resolved and program outputs are selected.

3. Trace state

The tracer represents handler inputs as concrete values or named symbols. Concrete values include bytecode pointers, stack addresses, handler-table data, and process facts. Symbolic values include original program inputs such as rcx.

devirt.py: abstract state model@dataclass(frozen=True)
class AbsValue:
    width: int
    value: int | None = None
    symbol: str | None = None

    @property
    def is_concrete(self) -> bool:
        return self.value is not None

@dataclass
class TraceState:
    regs: dict[str, AbsValue]
    mem: dict[int, AbsValue]

    def concrete_key(self) -> tuple:
        reg_items = tuple(sorted(
            (name, value.width, value.value)
            for name, value in self.regs.items()
            if value.is_concrete
        ))
        mem_items = tuple(sorted(
            (addr, value.value)
            for addr, value in self.mem.items()
            if value.is_concrete and value.value != 0
        ))
        return reg_items, mem_items

The cache key uses concrete state. Symbols are excluded, so equivalent VM states merge even when symbolic names differ.

Initial state for this sample

4. Generic handler resolver

The current tracer has no per-handler BinaryShield fast paths. Each handler goes through the same resolver machinery.

devirt.py: generic trace_handler structuredef trace_handler(self, addr: int, state: TraceState) -> list[TraceOutcome]:
    with create_context() as context:
        types = context.types
        with context.create_module(f"trace_{addr:x}") as module:
            sem = lift_bfs(module, self.container, addr, verbose=False)
            ram = module.add_global(types.array(types.i8, 0), "RAM")

            result_fields = [types.i8, types.i64]
            result_fields.extend(sem.reg_types.values())
            result_ty = types.struct(f"TraceResult_{addr:x}", result_fields)

            # One resolver parameter per symbolic register or tracked byte.
            # Concrete fields are materialized as constants.
            resolver = module.add_function(f"resolver_{addr:x}", resolver_ty)
            ...
            ir.call(sem.function, [state_alloca, ram])
            ir.unreachable()

            module.optimize("always-inline")
            self._rewrite_hooks(module, resolver, sem, state_alloca, ram, result_ty)
            ...
            return self._read_outcomes(resolver, sem, result_ty, ram, state)

Hook rewrite

Striga lifted code uses boundary hooks for indirect control transfer. The resolver rewrites each hook call into a structured return containing an event code, target, and full register snapshot.

call void @__striga_jmp(i64 %target)
unreachable

%r = insertvalue %TraceResult undef, i8 1, 0
%r1 = insertvalue %TraceResult %r, i64 %target, 1
%rax = load i64, ptr %rax_snap
%r2 = insertvalue %TraceResult %r1, i64 %rax, 2
ret %TraceResult %r2

Event code 1 means jmp, 2 means call, 3 means ret, and 4 means syscall.

5. Memory folding

Handler IR reads from the synthetic @RAM root. The tracer replaces safe loads with constants or symbolic expressions before reading the resolver result.

Static image loads

A load from @RAM + constant becomes a constant when the address range is inside the PE image and no store in the resolver aliases the range.

devirt.py: load folding ruleif finite_offsets and all(
    self.container.in_range(off)
    and self.container.in_range(off + size - 1)
    and not self._range_overlaps_any(off, size, store_ranges)
    for off in finite_offsets
):
    replacement = self._build_static_load_expr(
        ir, inst.type, offset_value, size
    )

%p = getelementptr i8, ptr @RAM, i64 5368802747
%target_rva = load i32, ptr %p, align 1
%target = zext i32 %target_rva to i64

%target = i64 5368802678
; later normalized to handler VA 0x1400162b1

Tracked VM memory

The tracer tracks a bounded scratch range, 0x10fd00..0x110000, byte by byte. Loads from concrete tracked addresses become concrete or symbolic byte combinations. Stores to tracked addresses update the abstract memory map.

devirt.py: tracked memory expressionfor i in range(size):
    byte_abs = input_state.mem.get(addr + i, AbsValue.concrete(8, 0))
    if byte_abs.is_concrete:
        byte = types.i8.constant(byte_abs.value or 0)
    else:
        byte = param_values[("mem", addr + i)]
    widened = ir.zext(byte, ty) if ty.int_width > 8 else byte
    result = ir.or_(result, ir.shl(widened, ty.constant(i * 8)))

6. Trace graph

The tracer builds a graph instead of a flat path. Each node is a pair of handler address and concrete state. Resolved VM jumps add successor nodes. Existing nodes are reused, so loops and merges remain in the graph.

Graph summary excerptnodes=861
edges=866

0x140016000 --jmp:0x140016101--> 0x140016101
0x140016101 --jmp:0x14001606a--> 0x14001606a
0x14001606a --jmp:0x14001676b--> 0x14001676b
0x14001676b --jmp:0x14001606a--> 0x14001606a
0x14001604e --ret:0x7fff0000--> exit

Finite branch splitting

When a target or state field is a finite select, the tracer creates one outcome per leaf. This recovers virtual conditional branches without naming the VM opcode.

devirt.py: split select leavesdef _split_select_constants(self, value: Value, *, use_leaf_as_target: bool):
    cond = value.get_operand(0)
    true_value = value.get_operand(1)
    false_value = value.get_operand(2)
    out = []
    if true_value.is_constant_int:
        out.append((true_value.const_zext_value, (cond, True)))
    if false_value.is_constant_int:
        out.append((false_value.const_zext_value, (cond, False)))
    return out

7. Recovered function construction

After tracing, the graph is rebuilt into one LLVM function. Each graph node becomes a basic block. The block stores known concrete state, calls the lifted handler, then branches according to graph edges.

devirt.py: recovered block skeletonfor key, node in graph.nodes.items():
    sem = sem_by_addr[node.addr]
    block = blocks[key]
    with block.create_builder() as ir:
        for name, ty in sem0.reg_types.items():
            abs_value = node.state.regs.get(name)
            if abs_value is not None and abs_value.is_concrete:
                ir.store(_const_int(ty, abs_value.value or 0), reg_ptr(name))

        _materialize_mem_chunks(ir, types, ram, node.state,
                                tracer.mem_base, tracer.mem_size)
        ir.call(sem.function, [state_alloca, ram])

        outgoing = edges_by_src.get(key, [])
        if len(outgoing) == 1:
            ir.br(blocks[outgoing[0].dst])
        else:
            switch = ir.switch_(reg_value, unresolved_block, len(cases))

Memory localization

VM stack and synthetic environment slots are moved from external @RAM into a local alloca. LLVM can then remove VM-only stores and loads because they no longer look like external side effects.

devirt.py: localize VM memoryif tracer.mem_base <= addr < local_end:
    local_offset = types.i64.constant(addr - tracer.mem_base)
    with inst.create_builder() as ir:
        replacement = ir.gep(types.i8, vm_mem, [local_offset])
    inst.set_operand(i, replacement)

8. Intermediate IR snapshots

The page now includes stage dumps generated by optional tracing instrumentation in devirt.py and summarized by docs/generate_devirt_presentation_artifacts.py. The dump run selected resolver examples for the first handler 0x140016000 and the virtual conditional handler 0x14001676b.

Artifact generation commandSTRIGA_DEVIRT_DUMP_DIR=docs/devirt-presentation-artifacts \
STRIGA_DEVIRT_DUMP_TRACE_ADDRS=0x140016000,0x14001676b \
  uv run python -X faulthandler devirt.py

uv run python docs/generate_devirt_presentation_artifacts.py

Resolver stage: built

The resolver is a one-handler wrapper. Concrete state is stored into %State and tracked memory is materialized into @RAM. The only semantic action is a call to the lifted handler.

docs/devirt-presentation-artifacts/snippets/resolver-built-call.llstore i64 0, ptr getelementptr (i8, ptr @RAM, i64 1114080), align 1
store i64 0, ptr getelementptr (i8, ptr @RAM, i64 1114088), align 1
store i64 0, ptr getelementptr (i8, ptr @RAM, i64 1114096), align 1
store i64 0, ptr getelementptr (i8, ptr @RAM, i64 1114104), align 1
call void @lifted_0x140016000(ptr %state, ptr @RAM)
unreachable

Resolver stage: inlined handler boundary

After always-inline, the handler's lifted x86 flag and arithmetic code is visible. The boundary is still an external hook call.

docs/devirt-presentation-artifacts/snippets/resolver-inlined-hook-call.ll%230 = xor i64 %205, %207
%231 = xor i64 %206, %207
%232 = and i64 %230, %231
%233 = and i64 %232, -9223372036854775808
%234 = icmp ne i64 %233, 0
%235 = zext i1 %234 to i8
store i8 %235, ptr %of.i, align 1
%236 = load i64, ptr %state, align 4
call void @__striga_jmp(i64 %236)
unreachable

Resolver stage: hook rewritten into data

The hook is replaced with a return value. The first field is the event code, the second field is the target, and the rest are state snapshot fields.

docs/devirt-presentation-artifacts/snippets/resolver-hook-rewritten-return.ll%236 = load i64, ptr %state, align 4
%237 = insertvalue %TraceResult_140016000 { i8 1, i64 undef, ... }, i64 %236, 1
%rax_snap = getelementptr inbounds nuw %State, ptr %state, i32 0, i32 0
%238 = load i64, ptr %rax_snap, align 4
%239 = insertvalue %TraceResult_140016000 %237, i64 %238, 2
%rbx_snap = getelementptr inbounds nuw %State, ptr %state, i32 0, i32 1
%240 = load i64, ptr %rbx_snap, align 4
%241 = insertvalue %TraceResult_140016000 %239, i64 %240, 3

Resolver stage: optimized virtual conditional

The conditional VM handler resolves to a finite target expression. The tracer splits this select into two graph outcomes and specializes the state for each branch.

docs/devirt-presentation-artifacts/snippets/jcc-resolver-select.ll%88 = and i64 %66, 64
%.not = icmp eq i64 %88, 0
%89 = select i1 %.not, i64 5368802751, i64 5368802682
%90 = insertvalue %TraceResult_14001676b { i8 1, i64 5368799338, ... }, i64 %rcx_entry_7089, 4
...
%101 = insertvalue %TraceResult_14001676b %100, i64 %89, 15

Recovered skeleton: finite VM branch

Graph reconstruction lowers the split virtual branch to a normal LLVM switch. The default path remains unresolved until later simplification or final cleanup proves it unnecessary.

docs/devirt-presentation-artifacts/snippets/recovered-skeleton-switch.llcall void @lifted_0x14001676b(ptr %state, ptr @RAM)
%r13_node_267_14001676b2 = getelementptr inbounds nuw %State, ptr %state, i32 0, i32 13
%0 = load i64, ptr %r13_node_267_14001676b2, align 4
switch i64 %0, label %unresolved [
  i64 5368802751, label %node_268_14001606a
  i64 5368802682, label %node_269_14001606a
]

Cleanup round 8: original predicate emerges

After repeated scalar cleanup, the comparison constants are visible. Surrounding flag computations still exist because the VM encoded each comparison through x86 flags and dispatch state.

docs/devirt-presentation-artifacts/snippets/recovered-round8-first-compare.ll%5 = add i32 %4, -1859
%6 = icmp ult i32 %4, 1859
%7 = trunc i32 %5 to i8
%8 = lshr i8 %7, 4
%9 = xor i8 %8, %7
...
%15 = icmp eq i32 %4, 1859
...
%26 = select i1 %15, i64 64, i64 0
%27 = or i64 %26, %25
...
switch i32 %trunc, label %unresolved [
  i32 1073835451, label %node_285_1400162b1
  i32 1073835382, label %node_269_14001606a
]

9. Before and after optimization

The recovered graph initially contains lifted handler calls, concrete stores into VM state, bytecode-derived dispatch math, and memory traffic through @RAM. The cleanup pipeline removes computations that only feed VM dispatch.

Cleanup pipelineOPT_PIPELINE = (
  "sroa,instcombine<no-verify-fixpoint>,early-cse<memssa>,"
  "gvn,simplifycfg,dse,adce"
)

Residual IR before final BinaryShield cleanup

The residual IR still contains @RAM, switch defaults, and VM flag arithmetic, but the actual user-level predicate is exposed as five equality checks. The extracted snippet is saved as docs/devirt-presentation-artifacts/snippets/recovered-residual-membership.ll.

docs/devirt-presentation-artifacts/snippets/recovered-residual-membership.ll%4 = trunc i64 %rcx to i32
%5 = add i32 %4, -1859
%15 = icmp eq i32 %4, 1859
...
%38 = add i32 %4, -2418
%48 = icmp eq i32 %4, 2418
...
%73 = add i32 %4, -1638
%83 = icmp eq i32 %4, 1638
...
%106 = sub i32 299902, %4
%116 = icmp eq i32 %4, 299902
...
%140 = sub i32 29763, %4
%150 = icmp eq i32 %4, 29763

Final cleanup for this sample

The final pass recognizes the BinaryShield sample's residual membership-test pattern, extracts the comparison constants, emits clean IR, and verifies the generated module.

devirt.py: BinaryShield-specific clean IR emissionfor match in re.finditer(r"icmp eq i32 %[-.$A-Za-z0-9_]+, (\d+)", residual_ir):
    value = int(match.group(1))
    if value not in seen:
        constants.append(value)

lines = [
    "; clean BinaryShield recovery; VM dispatch, bytecode, and RAM model removed",
    "define i64 @recovered_binaryshield(i64 %rcx) {",
    "entry:",
    "  %x = trunc i64 %rcx to i32",
]
...
with create_context() as context:
    with context.parse_ir(clean_ir) as module:
        module.verify_or_raise()

10. Final recovered IR

The final artifact is devirt-output/binaryshield-recovered.ll. It contains no VM dispatch hooks, no @RAM root, no unresolved branch block, and no handler-table or bytecode reads.

devirt-output/binaryshield-recovered.ll / docs/devirt-presentation-artifacts/snippets/recovered-final.ll; clean BinaryShield recovery; VM dispatch, bytecode, and RAM model removed
define i64 @recovered_binaryshield(i64 %rcx) {
entry:
  %x = trunc i64 %rcx to i32
  %cmp0 = icmp eq i32 %x, 1859
  %cmp1 = icmp eq i32 %x, 2418
  %cmp2 = icmp eq i32 %x, 1638
  %cmp3 = icmp eq i32 %x, 299902
  %cmp4 = icmp eq i32 %x, 29763
  %or1 = or i1 %cmp0, %cmp1
  %or2 = or i1 %or1, %cmp2
  %or3 = or i1 %or2, %cmp3
  %or4 = or i1 %or3, %cmp4
  %result = zext i1 %or4 to i64
  ret i64 %result
}

11. Verification

The implementation and artifact were checked with syntax, lint, LLVM verifier, structural grep checks, trace checks, and emulator comparison.

Executed checksuv run python -m py_compile devirt.py
uv run ruff check devirt.py
uv run python -X faulthandler devirt.py

# Artifact checks:
# - parse recovered IR with llvm.create_context().parse_ir(...)
# - verify recovered module
# - assert no @RAM, __striga_*, switch, or unresolved remains
# - assert graph text contains no unresolved edges and reaches ret

12. VM-specific knowledge encoded

The resolver path no longer has per-handler BinaryShield fast paths, but the complete script still encodes sample-specific facts. These facts let the generic partial evaluator start from the right state and interpret the final function boundary.

13. Limitations

• Entry discovery is manual. The script starts from FIRST_HANDLER and hard-coded bytecode RVA. A general tool needs VM-entry detection and bytecode-root recovery.
• The memory domain is bounded. VM stack/context tracking covers the observed range. Symbolic pointers or stores outside that range can force unresolved state.
• Static folding assumes immutable image bytes. Writable or self-modifying bytecode would require versioned memory or emulation-backed snapshots.
• Finite branch splitting is limited. The current splitter handles simple select leaves and selected state-field constraints. More complex PHIs, switches, and arithmetic target sets need stronger enumeration.
• Calls and syscalls have no full policy. The graph records call/syscall events, but this sample resolves to a single function return. Recursive devirtualization and external-call modeling remain future work.
• The final polish is sample-specific. The clean 16-line IR is produced by a BinaryShield membership-test extractor after generic recovery and optimization expose the comparison set.
• Correctness evidence is bounded. LLVM verifies the IR, the trace has no unresolved edges, and emulator samples match. A full equivalence proof over all inputs would require symbolic validation of the recovered predicate against the original binary.
• The pipeline depends on LLVM simplification. If dispatch computations remain opaque to LLVM, tracing can stop at unresolved edges or leave VM residue in recovered IR.
• llvm-nanobind stale wrappers are a known hazard. The implementation avoids reusing instruction wrappers after optimization where possible, and a repro was documented upstream.

Next generalization steps

1. Replace hard-coded BinaryShield constants with discovery passes and user-supplied hints.
2. Broaden finite target splitting to PHIs, switches, and arithmetic expressions over small domains.
3. Add a call policy: recursive devirtualization, external placeholders, or ABI-aware summaries.
4. Replace the sample-specific final membership extractor with a generic residual-memory cleanup and stack-frame recovery pass.
5. Add a symbolic equivalence harness for recovered predicates.