1

我正在尝试使用 angr 通过为给定结果导出正确的输入来验证函数的行为。该函数修改了一个缓冲区，在这种情况下，它只是将输入复制到其中，因此我在堆上设置了符号变量，并对其应用了等式约束。然后我为函数的输入创建一个符号变量。我打算发生的事情是 angr 本质上运行该函数，直到找到输入，这样当它被复制到缓冲区时，它满足放置在其上的约束。但是，当它运行时，我只得到一个死分支，其中输出具有正确的值，但输入没有。我在下面附上了求解器和测试程序源。这是我的实施失败吗？还是这种解决问题的方法无效

求解器

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'


    program = angr.Project(path)
    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')
        ))

    str_in = claripy.BVS('input', 8 * len(word))
    fn_call_state = program.factory.call_state(fn_addr, angr.calling_conventions.PointerWrapper(str_in), cc=cc)
    ptr_out = fn_call_state.heap.allocate(len(word))

    chars = []
    for i, v in enumerate(word):
        ch = claripy.BVS('char_{}'.format(i), 8)
        chars.append(ch)
        fn_call_state.solver.add(ch == int(v))
    word_sym = claripy.Concat(*chars)
    fn_call_state.memory.store(buf_addr, ptr_out)
    fn_call_state.memory.store(ptr_out, word_sym)

    simgr = program.factory.simgr(fn_call_state, save_unsat=True)
    simgr.run()
    print(simgr)
    for s in simgr.deadended:
        print(s.solver.eval(str_in, cast_to=bytes))
        print(s.solver.eval(word_sym, cast_to=bytes))

测试程序

#include <string.h>
#include <stdlib.h>
#include <stdio.h>

char* buffer;

void test_fn(char* input) {
        strcpy(buffer, input);
        return;
}

int main(int argc, char** argv) {
        buffer = (char*) malloc(100);
        test_fn("hello");
}

当我运行求解器时，我得到如下输出，尽管第一个值（输入值）看似随机变化。有没有办法应用这个约束，以便程序的副作用优先？我不明白这两个值有何不同。这是我准备记忆的方式错误吗？

b'\x01\x01\x01\x04\x01\x02'
b'hello\x00'
4

0 回答 0