Blogs / Symbolic exploration

Finding an Input with Triton

Suppose a function copies its first argument into RAX. What value should we pass to make it return 7? Triton's Python API can find one. HydIR brings that symbolic analysis to selected x86-64 functions and shows the path conditions and return expressions it finds.

Start with one instruction

Open the Triton console at the bottom of the HydIR workbench. Enter these lines one at a time:

from triton import *
ctx = TritonContext(ARCH.X86_64)
ctx.setConcreteRegisterValue(ctx.registers.rip, 0x40000)
ctx.symbolizeRegister(ctx.registers.rdi, 'arg0')
ctx.processing(Instruction(b'\x48\x89\xf8'))
rax = ctx.getSymbolicRegister(ctx.registers.rax)
ctx.getModel(rax.getAst() == 7)

The bytes 48 89 f8 are mov rax, rdi. We mark RDI as an unknown input, process the instruction, then ask Triton for an input that makes the resulting RAX equal 7. The console prints {0: arg0:64 = 0x7}: the model found arg0 = 7. It is a small example, but it shows the useful part of symbolic execution: we ask about an output and get a possible input back.

This console has its own context. The instruction bytes above are supplied by the example; they are not read from whichever ELF is open in the workbench. The console accepts a limited set of Triton operations, one statement at a time, and replays up to 64 accepted statements. It does not offer general Python imports, file access, shell commands, or network access.

Now try a function from an ELF

For a named function in a local ELF, HydIR can do the setup for you. Point it at a Python interpreter with Triton installed, check the bridge, then request a report:

export HYDIR_TRITON_PYTHON=/path/to/python-with-triton
cargo run --locked --bin hydirctl -- doctor
cargo run --locked --bin hydirctl -- triton /path/to/program.elf function_name

doctor checks whether that interpreter can import Triton. The last command reads a non-stripped, named x86-64 function and emits JSON. In the desktop app, selecting a local function and pressing Run Triton requests the same kind of report. The report includes the binary identity and function entry, instruction expressions, explored return paths, and a final RAX expression.

Inside the bridge, RDI and RSI become symbolic inputs arg0 and arg1. HydIR processes instructions along each direct path with a fresh Triton context. For multiple return paths, the report records path conditions and a textual ite expression for RAX.

Read the report

The report covers a selected function of up to 4,096 bytes, with up to 64 direct paths and 1,024 instructions per path. It records the decoded bytes, per-instruction symbolic expressions, path conditions, and final RAX expression.

The bridge tests include a two-path fixture and model queries. For HydIR's separate LLVM lift and finite execution checks, follow the max2 worked example. The quick start has the local build commands.