如何在angr中对堆侧效应施加约束以获取符合目标输出的函数输入

• 约束逻辑倒置：你要求解的是执行strcpy后buffer内容为hello，但当前代码是在strcpy执行前就给buffer指向的内存写死了hello，函数运行时strcpy会直接覆盖这块内存，你没有为strcpy执行后的结果加任何约束，符号输入str_in无任何约束限制，求解器会返回任意合法值，自然每次运行结果随机。
• 无效初始化逻辑：你构造的word_sym以及对应赋值、添加约束的代码完全多余，这些初始值会被strcpy覆盖，不会对最终结果产生任何约束作用。

正确逻辑是：先确保buffer指针有效，执行完test_fn之后，再给buffer指向的内存添加等于hello\0的约束，再求解输入，修改后代码如下：

import angr
import claripy
import angr.sim_type as T

if __name__ == '__main__':
    path = './test'
    target = 'test_fn' 
    target_buf = 'buffer' 

    word = b'hello\0'
    word_len = len(word)

    program = angr.Project(path, auto_load_libs=False)
    fn = program.loader.find_symbol(target)
    buf = program.loader.find_symbol(target_buf)

    fn_addr = fn.rebased_addr
    buf_addr = buf.rebased_addr

    cc = program.factory.cc(func_ty=T.SimTypeFunction(
        args=[T.parse_type('char*')],
        returnty=T.parse_type('void')
        ))
    
    # 自定义返回地址用于定位函数执行完成的位置
    ret_addr = 0xdeadbeef
    str_in = claripy.BVS('input', 8 * word_len)
    fn_call_state = program.factory.call_state(
        fn_addr, 
        angr.calling_conventions.PointerWrapper(str_in), 
        cc=cc,
        ret_addr=ret_addr
    )
    # 给全局buffer指针分配有效堆内存
    ptr_out = fn_call_state.heap.allocate(word_len)
    fn_call_state.memory.store(buf_addr, ptr_out)

    simgr = program.factory.simgr(fn_call_state)
    # 执行到函数返回
    simgr.explore(find=ret_addr)
    
    if simgr.found:
        s = simgr.found[0]
        # 添加约束：strcpy执行完成后buffer内容等于目标字符串
        final_buf_content = s.memory.load(ptr_out, word_len)
        s.solver.add(final_buf_content == word)
        # 求解得到正确输入
        print(s.solver.eval(str_in, cast_to=bytes))

运行上述代码会输出预期结果b'hello\x00'。

内容的提问来源于stack exchange，提问作者ragingSloth