Blogs / Binary semantics

Lifting a VM Handler into a Transfer Function

A handler's native address locates its code; its transfer function describes the virtual instruction. We read a stack-add handler from a linked ELF with HydIR, execute its bytes with Triton, and express the resulting state transformation in LLVM IR.

The checked-in assembly fixture contains the vm_vadd handler and an ELF entry stub. Its state layout and handler boundary are explicit, so each derived state effect can be checked against the machine bytes.

The machine whose state we are recovering

The handler receives a pointer to a 176-byte VMState in host register RDI. The layout header checks every offset at compile time:

typedef struct {
    uint64_t vreg[4];    /* 0..31 */
    uint64_t stack[16];  /* 32..159 */
    uint64_t sp;         /* 160: next free slot */
    uint64_t vpc;        /* 168: current virtual opcode */
} VMState;

Let \(R\) be the four virtual registers, \(M\) the 16 physical stack words, \(sp\) the next free stack index, and \(vpc\) the virtual program counter. The state is \(S=(R,M,sp,vpc)\). The fixture calls this operation VADD and advances \(vpc\) by one under its one-byte opcode convention. The entry condition is \(2\leq sp\leq16\), with RDI pointing to the complete state.

Under this convention, the two operands are \(M[sp-2]\) and \(M[sp-1]\). The physical slot \(M[sp-1]\) survives the pop. It is outside the logical stack once \(sp\) decreases, but its bytes remain in memory. A transfer function that zeroed it would describe different native behavior.

Read the native instructions as state accesses

The reproducible build produces a linked x86-64 ELF. In the run recorded for this article, HydIR's inspect report found vm_vadd at 0x201120 with a 40-byte symbol extent. Its analyze report decoded eight reachable instructions and marked unknown_global_effects: true for the RDI-based memory accesses.

The following addresses, bytes, and disassembly come from that ELF. Offsets are relative to the state pointer in RDI:

The unusual 0x10 displacement is just layout arithmetic: the stack starts at byte 32, while its lower operand is two 8-byte slots below sp. Thus \(32+8(sp-2)=16+8sp\). Likewise, \(32+8(sp-1)=24+8sp\). The host registers RCX and RAX are temporary carriers; neither is one of the four virtual registers in \(R\).

Derive the transfer function

Reading the writes in order gives a compact semantic description. All additions are 64-bit modular operations:

This is \(S'=H_{\mathrm{VADD}}(S)\) for states satisfying the entry condition. In particular, \(M'[sp-1]=M[sp-1]\). Host flags changed by add, dec, and inc are absent from \(S\): the caller's contract does not treat them as VM state. The host ret changes the native instruction pointer and stack pointer, while the virtual PC changes only at the explicit store to [rdi+0xa8].

For a concrete trace, set \(sp=2\), \(vpc=12\), \(M[0]=7\), and \(M[1]=9\). The handler leaves \(M'[0]=16\) and \(M'[1]=9\), then sets \(sp'=1\) and \(vpc'=13\). Triton produced precisely those four values from the ELF bytes. All four virtual registers and every stack word except \(M[0]\) remained byte-for-byte unchanged in that run.

Use Triton to interrogate the bytes

HydIR's triton command extracted the 40-byte symbol and decoded eight instructions on one return path. The worked-example script reads the same symbol from the ELF, sets RDI to a mapped 176-byte VMState, initializes a valid sp, and processes the bytes in a Triton x86-64 context. The state setup makes the handler's memory effects observable.

The decisive query is small. After setting the concrete pointer and stack depth, the script symbolizes the two words at the effective addresses, processes the handler bytes, then asks for a counterexample to the proposed sum:

low = MemoryAccess(STATE_BASE + 32 + (sp - 2) * 8, CPUSIZE.QWORD)
high = MemoryAccess(STATE_BASE + 32 + (sp - 1) * 8, CPUSIZE.QWORD)
ctx.symbolizeMemory(low, "stack_low")
ctx.symbolizeMemory(high, "stack_high")
a = ctx.getMemoryAst(low)
b = ctx.getMemoryAst(high)
offset = 0
while offset < len(code):
    inst = Instruction(code[offset:offset + 16])
    inst.setAddress(address + offset)
    ctx.processing(inst)
    offset += inst.getSize()
result = ctx.getMemoryAst(low)
unchanged_high = ctx.getMemoryAst(high)
sum_counterexample = ctx.isSat(result != a + b)
high_counterexample = ctx.isSat(unchanged_high != b)

For the symbolic check, it replaces the two operand words with independent 64-bit symbolic values \(a\) and \(b\). After processing the native bytes, it asks Triton's solver whether the output word can differ from \(a+b\) modulo \(2^{64}\), and whether the old top word can differ from \(b\). Both counterexample queries were unsatisfiable at each fixed valid stack depth, \(sp=2,\ldots,16\). This establishes those two properties for the supplied memory layout and straight-line handler under each of those fixed-depth contexts. The script also compares the entire state against the stated transfer function for 68 concrete states: four boundary/overflow cases and 64 seeded cases.

Write the operation in LLVM IR

The checked-in LLVM file implements the transfer function derived above. Its key instructions are:

%sp = load i64, ptr %sp.ptr, align 8
%lo = sub i64 %sp, 2
%hi = sub i64 %sp, 1
%lo.ptr = getelementptr %VMState, ptr %state, i32 0, i32 1, i64 %lo
%hi.ptr = getelementptr %VMState, ptr %state, i32 0, i32 1, i64 %hi
%a = load i64, ptr %lo.ptr, align 8
%b = load i64, ptr %hi.ptr, align 8
%sum = add i64 %a, %b
store i64 %sum, ptr %lo.ptr, align 8

The full IR also stores \(sp-1\) and \(vpc+1\). getelementptr computes an address within the stated structure; the load and store instructions access it. We omit nsw and nuw on add i64: the native addition wraps, while those LLVM flags would make an overflowing result poison. The state precondition supplies the array bounds; it does not come from the native handler. See LLVM's integer addition semantics and GEP explanation.

The script runs opt -passes=verify on the IR and generates an LLVM harness with the 68 native Triton outputs as expected values. lli executes the transfer function on the same 68 initial states and compares all 22 words after each call. All 68 full-state comparisons passed. The symbolic Triton queries separately check the sum and retained old-top word at each valid stack depth.

Separate native execution from virtual meaning

A native execution contains more state than the virtual machine exposes: host registers, flags, the host stack, and the instruction pointer. Let \(\iota(S)\) place a virtual state in memory, point RDI at it, and provide a return address on the host stack. Let \(N_h\) execute the handler's native instructions, and let \(\pi_{\mathrm{VM}}\) read the virtual-state structure afterward. The handler's meaning is the projection:

This equation explains why RAX and RCX appear prominently in the disassembly but do not appear in the final virtual-state equation. They carry intermediate native values. The memory writes through RDI determine the next virtual state.

The frame condition

A transfer function describes preserved state as precisely as modified state. For this handler, the virtual-state read set is \(\{sp,vpc,M[sp-2],M[sp-1]\}\). Its write set is \(\{sp,vpc,M[sp-2]\}\). The corresponding frame condition is:

The old top word \(M[sp-1]\) is therefore still present in physical memory after the virtual pop. The logical stack has one fewer element because \(sp'=sp-1\). Keeping these two views separate matters: a model that clears the old word changes the physical state, even though both models show the same active stack immediately after VADD.

The handler address identifies this native implementation. The projected state relation identifies the virtual instruction: a 64-bit stack addition with explicit changes to \(sp\) and \(vpc\), and a frame condition for every other virtual-state component.