我该如何使用Angr进行一致执行并收集输入约束？

我有一个程序，将字符串（具有某种结构）作为输入。我的目的是收集有关信息的信息，这些信息将使用输入执行时解析输入中的每个字符。解决这个问题的正确方法是什么？

我的主题是一个用于表达式的简单递归下降解析器，它接受1+(2*3)等格式的输入。

我尝试了什么到目前为止：

编写了一个程序，该程序构造一个带有字符串参数的初始状态，一次执行一次，最后收集约束。

br />
执行此命令时，我得到的约束为零。使用state.add_constraints向输入中的每个字符添加约束，并查找最后产生的约束。

import sys
import angr

class Program:
    def __init__(self, exe):
        self.exe = exe
        self.project = angr.Project(exe, load_options={'auto_load_libs': False})

    def set_input(self, arg):
        self.arg1 = arg

        self.initial_state = self.project.factory.entry_state(
                args=[self.exe, self.arg1],
                # does not seem to startup the unicorn engine
                add_options=angr.options.unicorn,
                )

    def run(self):
        state = self.initial_state
        while True:
            succ = state.step()
            if len(succ.successors) > 1:
                raise Exception('more successors %d' % len(succ.successors))
            if not succ.successors: return state
            state, = succ.successors

def main(exe, arg):
    prog = Program(exe)
    prog.set_input(arg)
    res = prog.run()
    print("constraints: %d" % len(res.solver.constraints))
    for i in res.solver.constraints:
        print(i)
    print('done')

if __name__ == '__main__':
    assert len(sys.argv) >= 3
    main(sys.argv[1], sys.argv[2])

这会导致大量约束最后，我无所适从如何将这些约束解释为我想要的-与输入字符进行比较。约束相当复杂，但是每个项目中都有很多重复的部分。将这些如下所示的约束转换为实际字符比较的任何建议将不胜感激。

import sys
import angr
import claripy

class Program:
    ARG_PREFIX = 'sym_arg'
    def __init__(self, exe):
        self.exe = exe
        self.project = angr.Project(exe, load_options={'auto_load_libs': False})

    def set_input(self, arg):
        # generate arg1 from individual characters.
        self.arg1 = self.make_symbolic_char_args(arg)

        self.initial_state = self.project.factory.entry_state(
                args=[self.exe, self.arg1],
                add_options=angr.options.unicorn,
                # does not seem to affect the number of constraints created
                # remove_options=angr.options.simplification
                )
        self.constrain_input_chars(self.initial_state, self.arg1a, arg)
        self.string_terminate(self.initial_state, self.arg1a, arg)

    def string_terminate(self, state, symarg, inarg):
        state.add_constraints(symarg[len(inarg)] == 0)

    def constrain_input_chars(self, state, symarg, sarg):
        constraints = []
        for i,a in enumerate(sarg):
            state.add_constraints(symarg[i] == a)

    def run(self):
        state = self.initial_state
        while True:
            succ = state.step()
            if len(succ.successors) > 1:
                raise Exception('more successors %d' % len(succ.successors))
            if not succ.successors: return state
            state, = succ.successors

    def make_symbolic_char_args(self, instr, symbolic=True):
        if not symbolic: return instr
        input_len = len(instr)
        largs = range(0, input_len+1)
        arg1k = ['%s_%d' % (Program.ARG_PREFIX, i) for i in largs]
        self.arg1h = {k:claripy.BVS(k, 8) for k in arg1k}
        self.arg1a = [self.arg1h[k] for k in arg1k]
        return reduce(lambda x,y: x.concat(y), self.arg1a)


def main(exe, arg):
    prog = Program(exe)
    prog.set_input(arg)
    res = prog.run()
    print("constraints: %d" % len(res.solver.constraints))
    for i in res.solver.constraints:
        print(i)
    print('done')

if __name__ == '__main__':
    assert len(sys.argv) >= 3
    main(sys.argv[1], sys.argv[2])

问题：太慢了

即使输入了几个字符，该方法也需要很长时间才能执行。我尝试在具有几个字符输入的表达式的简单递归下降解析器上执行上述操作：（1+4/1+4/(1+4)）。解析花费了30多分钟！而运行解析器的时间不到一秒钟。如果没有其他出路的话，那时候我会没事的，但是这很固执，我无法撼动必须有更好的办法的感觉。

我的想法是，我从输入约束开始，使每个符号字符等于相应的输入。然后，我提供自己的执行路径，以便仅选择满足输入约束的路径以进行进一步执行。我的想法是，由于我没有在初始状态下启动原始字符约束，所以我可以检查最终状态以确定每个字符上积累的其他约束。

...
<Bool (((if (sym_arg_0_0_8 == 0) then 0x0 else (if (sym_arg_1_1_8 == 0) then 0x1 else (if (sym_arg_2_2_8 == 0) then 0x2 else (if (sym_arg_3_3_8 == 0) then 0x3 else 0x4)))) + 0x7fffffffffeffd4) - 0x7fffffffffeffd4) == strlen_5_64>
<Bool 0x1 <= strlen_5_64>
<Bool ((0#56 .. 0#7 .. __invert__((if ((sym_arg_0_0_8 == 40) && (sym_arg_0_0_8[7:7] == 0)) then 1 else 0))) & 0xff) != 0x0>
<Bool (((if (sym_arg_0_0_8 == 0) then 0x0 else (if (sym_arg_1_1_8 == 0) then 0x1 else (if (sym_arg_2_2_8 == 0) then 0x2 else (if (sym_arg_3_3_8 == 0) then 0x3 else 0x4)))) + 0x7fffffffffeffd4) - 0x7fffffffffeffd4) == strlen_6_64>
<Bool 0x1 <= strlen_6_64>
<Bool ((0#56 .. 0#7 .. (if ((sym_arg_0_0_8 == 49) && (sym_arg_0_0_8[7:7] == 0)) then 1 else 0)) & 0xff) != 0x0>
<Bool (((if (sym_arg_0_0_8 == 0) then 0x0 else (if (sym_arg_1_1_8 == 0) then 0x1 else (if (sym_arg_2_2_8 == 0) then 0x2 else (if (sym_arg_3_3_8 == 0) then 0x3 else 0x4)))) + 0x7fffffffffeffd4) - 0x7fffffffffeffd4) == strlen_7_64>
<Bool 0x2 <= strlen_7_64>
<Bool ((0#56 .. 0#7 .. (if ((sym_arg_1_1_8 == 49) && (sym_arg_1_1_8[7:7] == 0)) then 1 else 0)) & 0xff) == 0x0>
<Bool (((if (sym_arg_0_0_8 == 0) then 0x0 else (if (sym_arg_1_1_8 == 0) then 0x1 else (if (sym_arg_2_2_8 == 0) then 0x2 else (if (sym_arg_3_3_8 == 0) then 0x3 else 0x4)))) + 0x7fffffffffeffd4) - 0x7fffffffffeffd4) == strlen_8_64>
<Bool 0x2 <= strlen_8_64>
...

这再次不起作用，因为解析甚至几个字符都需要很长时间。

我考虑过的其他选项


编写一个内存挂钩监视何时从中读取输入字符串的内存。
但这对我不起作用，因为在比较之前可能会复制字符。

我现在已经多次阅读过angr文档，但无法弄清楚该怎么办。我不能动摇它的感觉，因为angr是支持符号执行的符号执行引擎，它应该更简单，而我正在做的几乎是普通的vanila协议执行。接下来我该怎么办？

任何帮助将不胜感激！。