The problem of Symbolic Execution Example #5534
Description
Question
I’m trying to run the symbolic execution example, but I encountered an issue when using a binary compiled with stack-based parameter passing (instead of register-based as in the provided example). To accommodate this, I modified the symbolic execution code to manually write arguments onto the stack. My code looks like this:
firstCall_addr = project.loader.main_object.get_symbol("_firstCall")
helloWorld_addr = project.loader.main_object.get_symbol("_helloWorld")
input_arg = claripy.BVS('input_arg', 32)
init_state = project.factory.blank_state(addr=firstCall_addr.rebased_addr)
init_state.options.add("ZERO_FILL_UNCONSTRAINED_REGISTERS")
init_state.options.add("ZERO_FILL_UNCONSTRAINED_MEMORY")
stack_base = 0x7fffffff000
init_state.memory.store(stack_base + 0x8,
input_arg, size=4)
simgr = project.factory.simulation_manager(init_state)
simgr.explore(find=helloWorld_addr.rebased_addr)
if simgr.found:
input_value = simgr.found[0].solver.eval(input_arg)
print(f"Value of input_arg that reaches HelloWorld: {input_value}")
constraints = simgr.found[0].solver.constraints
solver = claripy.Solver()
solver.add(constraints)
min_val = solver.min(input_arg)
max_val = solver.max(input_arg)
print(f"Function arg: min = {min_val}, max = {max_val}")
else:
print("Did not find a state that reaches HelloWorld.")
>> Did not find a state that reaches HelloWorld.
The assembly code of function _firstCall is：
_firstCall:
401475 push ebp
401476 mov ebp, esp
401478 sub esp, 0x8
40147b cmp dword ptr [ebp+0x8], 0x32
40147f jbe 0x40148c
401481 cmp dword ptr [ebp+0x8], 0x63
401485 ja 0x40148c
401487 call _helloWorld
40148c nop
40148d leave
40148e ret
However, when I run the code, the parameter seems to have no actual effect — from the logs, it looks like the symbolic argument was never really written into memory as expected.
DEBUG:angr.engines.vex.heavy.heavy:IMark: 0x401475
DEBUG:angr.storage.memory_mixins.paged_memory.paged_memory_mixin:reg.load(0x1c, 4, Iend_LE) = <BV32 0x0>
DEBUG:angr.storage.memory_mixins.paged_memory.paged_memory_mixin:reg.load(0x18, 4, Iend_LE) = <BV32 0x7fff0000>
DEBUG:angr.engines.vex.heavy.heavy:IMark: 0x401476
DEBUG:angr.engines.vex.heavy.heavy:IMark: 0x401478
DEBUG:angr.engines.vex.heavy.heavy:IMark: 0x40147b
DEBUG:angr.storage.memory_mixins.paged_memory.paged_memory_mixin:mem.load(0x7fff0004, 4, Iend_LE) = <BV32 0x0>
How should I correctly write symbolic parameters to memory for a binary that uses stack-based calling convention?