Manticore在分析二进制文件的符号执行、污染分析（taint analysis）和instrumentation方面具有简单而强大的API。使用Manticore可以识别出特殊的代码位置，并推导出这些代码的输入路径。这样就可以提高测试覆盖率，或者快速发现漏洞。

在今年的Defcon CTF比赛中，我使用Manticore的方法进行了一次挑战，该挑战是由200个单独的二进制文件组成，每个二进制文件都有一个单独的密钥（以下我会把这个文件称为magic文件）。我的目标就是为每个二进制文件输入正确的密码，最后打印出一个总和：

enter code:
==== The meds helped 
sum is 12

译者注：Defcon CTF全球总决赛相当于是信息网络安全领域里的顶级赛事，素有网络安全领域的“世界杯”之称。

可想而知，对200个可执行文件每个进行一次逆向工程来提取一个字符串，是需要花费大量的时间。所以要完成这个挑战就必须要使用自动化，随着CTF挑战的不断升级，用来挑战的工具也必须与时俱进。

接下来，我将向大家介绍我的挑战过程并解析我是如何将Ninja和Manticore这两种二进制工具的函数结合在一起的。

下面我会采用三种不同的解决方案，并展示如何在自己的挑战中应用它们。

magic二进制文件的分析

magic二进制文件结构很简单，它的主要函数就是从stdin读取提示的密码，运行检查器函数，然后打印出总和。检查器函数一次加载一个输入字符串的字节，并调用一个函数来检查每个字符。字符检查函数会与固定字符值进行比较。如果字符值匹配，则该函数会返回一个求和的值，如果没有，则程序退出。

Manticore的API非常简单，当收到指令时，我将使用钩子调用函数，然后访问寄存器的CPU class和solver。

整个工作流程就是通过提供路径加载二进制文件，并在该二进制文件的指令中添加分析钩子，最后运行Manticore。在接收到地址后，钩子开始调用函数，从而推断出程序的运行状态。

我所使用的钩子调用函数采用了独立的state参数，这样该函数就包含了创建符号值或缓冲区，这就解决了符号值和路径丢失的问题。除此之外，它还包含一个成员，一个cpu，cpu负责保存寄存器的状态，并允许对存储器和寄存器进行读取和写入。

Manticore的使用策略

在此，我将分别用三种不同的解决方案来阐述Manticore的灵活性。

首先是符号解决方案，利用符号钩住每个指令，然后发现字符检查函数的具体位置。当Manticore处于字符检查函数时，它将通过对钩子进行设置来处理查询值。

其次是concrete解决方案，钩住每个字符检查函数的地址，并简单地从操作代码中读取值。

最后还是一个符号解决方案，不过与第一个不同，是通过挂钩每个字符检查函数的地址，并处理该值。

函数地址将使用二进制的Ninja来提取，所有的解决方案都需要一个能打印出解决方案的终止钩子的地址，其中第二种和第三种解决方案还需要用到字符检查函数的地址。

Ninja API提取地址的过程

为了提取字符检查函数的地址以及end_hook（）地址，我将使用Ninja。Ninja是专为快速的CTF环境而设计的逆向工程平台，具有用户友好，分析函数强大的特点。我们将使用其API来定位我想要的地址，在Ninja API中加载该文件非常简单。

bv = binja.BinaryViewType.get_view_of_file(path)

为了得到检查函数，我首先需要知道可执行文件的主要函数。接下来，我首先要检索程序输入函数的输入块。我知道主要的地址都会在LLIL. 的第11个指令中加载。从该指令中，我可以做一个全面地检查，它是一个加载到RDI中的常量，检查完后然后提取常量（main的地址）。使用main的地址调用get_function_at（）所给出的主要返回函数。

def get_main(bv):
    entry_fn = bv.entry_function
    entry_block = entry_fn.low_level_il.basic_blocks[0]
    assign_rdi_main = entry_block[11]
    rdi, main_const = assign_rdi_main.operands
 
    if rdi != 'rdi' or main_const.operation != LLIL_CONST:
        raise Exception('Instruction `rdi = main` not found.')
 
    main_addr = main_const.operands[0]
    main_fn = bv.get_function_at(main_addr)
    return main_fn

get_checker（）函数与get_main（）类似，它会定位从main调用的检查器函数的地址，然后加载该地址的函数并将其返回。

通过操作码进行识别的符号解决方案

每个字符检查函数都有相同的指令，这意味着我可以检查操作代码并将其用作目标函数的接收时间。我很喜欢这种解决方案，因为在这种方案下，我虽然不一定知道对挂钩如何进行设置，但可以确定何时接收到它。

在每个指令上设置一个钩子。

   检查操作代码是否和检查函数的前几个指令相匹配。

       在positive branch上设置一个钩子来求解寄存器值RDI并存储该值。

       在negative branch上设置一个钩子来终止该状态。

       在当前指令的pre-branch设置一个钩子，以检查处理过程是否完成，如果已经完成，就设置RDI，后面我就不需要再次处理该过程了。

在终止指令中设置一个钩子。

对negative branch的state.abandon()调用至关重要，因为这可能需要更复杂的代码，所以Manticore就还不能对该branch进行检索。但是我并没有放弃，我要用Manticore把原来需要花费3个小时的逆向过程缩短为1分钟。

def symbolic(m, end_pc):
    # hook every instruction using None as the address
    @m.hook(None)
    def hook_all(state):
        # read an integer at the program counter
        cpu = state.cpu
        pc = cpu.PC
        instruction = cpu.read_int(pc)
 
        # check the instructions match
        # cmp   rdi, ??
        # je    +0xe
        if (instruction & 0xFFFFFF == 0xff8348) and (instruction >> 32 & 0xFFFF == 0x0e74):
            # the positive branch is 0x14 bytes from the beginning of the function
            target = pc + 0x14
 
            # if the target address is not seen yet
            #   add to list and declare solver hook
            if target not in m.context['values']:
                set_hooks(m, pc)
 
    # set the end hook to terminate execution
    end_hook(m, end_pc)

我在这里使用的是Manticore的上下文来存储值，上下文字典实际上是多处理管理器的字典。当我开始使用多个处理器同时工作时，就需要使用上下文在它们之间共享数据。

函数set_hooks（）将在策略3中充分被使用，我主要是通过这个函数的地址挂钩来对符号进行解析，该过程分为pre-branch，positive branch和negative branch。

def set_hooks(m, pc):
    # pre branch
    @m.hook(pc)
    def write(state):
        _pc = state.cpu.PC
        _target = _pc + 0x14
 
        if _target in m.context['values']:
            if debug:
                print 'Writing %s at %s...' % (chr(m.context['values'][_target]), hex(_pc))
 
            state.cpu.write_register('RDI', m.context['values'][_target])
            # print state.cpu
 
    # negative branch
    neg = pc + 0x6
 
    @m.hook(neg)
    def bail(state):
        if debug:
            print 'Abandoning state at %s...' % hex(neg)
 
        state.abandon()
 
    # target branch
    target = pc + 0x14
 
    @m.hook(target)
    def solve(state):
        _cpu = state.cpu
        _target = _cpu.PC
        _pc = _target - 0x14
 
        # skip solver step if known
        if _target in m.context['values']:
            return
 
        val = _cpu.read_register('RDI')
        solution = state.solve_one(val)
 
        values = m.context['values']
        values[_target] = solution
        m.context['values'] = values
 
        target_order = m.context['target_order']
        target_order.append(_target)
        m.context['target_order'] = target_order
 
        if debug:
            print 'Reached target %s. Current key: ' % (hex(_target))
            print "'%s'" % ''.join([chr(m.context['values'][ea]) for ea in m.context['target_order']])

不过要注意的是，字典(Dictionary) values() 函数以列表返回字典中的所有值和target_order数组有一个奇怪的更新模式。它们需要重新分配给上下文字典，以通知处理器管理器它们已经被更改。

在这三个解决方案中，end_hook（）函数的作用都是通知操作员执行结束了，它会在所有的检查字符函数之后声明一个钩子，钩子会打印出检索的属性，然后终止Manticore。

def end_hook(m, end_pc):
    @m.hook(end_pc)
    def hook_end(state):
        print 'GOAL:'
        print "'%s'" % ''.join([chr(m.context['values'][ea]) for ea in m.context['target_order']])
        m.terminate()

通过地址挂钩的Concrete解决方案

由于这个解决方案会对每个文件执行简单的等式检查，因此很容易提取检查值，从而更有效地解决这个静态问题。事实上，这个过程还可以用一行bash 脚本来解决。

$ ls -d -1 /path/to/magic_dist/* | while read file; do echo -n "'"; grep -ao $'x48x83xff.x74x0e' $file | while read line; do echo $line | head -c 4 | tail -c 1; done; echo "'"; done

不过，在这种情况下，我可以结合Concrete方案。当向一个寄存器写入该值时，就会导致branch显而易见，并跳过处理过程。这也意味着我不再需要放弃negative branch，由于Concrete的 values() 函数，总会出现positive branch。

在每个字符检查函数上设置一个钩子。

    从操作代码中提取目标值。

    将该目标值写入寄存器RDI。

在终止指令中设置一个钩子。

def concrete_pcs(m, pcs, end_pc):
    # for each character checking function address
    for pc in pcs:
        @m.hook(pc)
        def write(state):
            # retrieve instruction bytes
            _pc = state.cpu.PC
            instruction = state.cpu.read_int(_pc)
 
            # extract value from instruction
            val = instruction >> 24 & 0xFF
 
            # concretize RDI
            state.cpu.write_register('RDI', val)
 
            # store value for display at end_hook()
            _target = _pc + 0x14
 
            values = m.context['values']
            values[_target] = val
            m.context['values'] = values
 
            target_order = m.context['target_order']
            target_order.append(_target)
            m.context['target_order'] = target_order
 
            if debug:
                print 'Reached target %s. Current key: ' % (hex(_pc))
                print "'%s'" % ''.join([chr(m.context['values'][ea]) for ea in m.context['target_order']])
    end_hook(m, end_pc)

通过地址钩子进行的符号解决方案

虽然从每个函数的静态中提取值很容易，但是，如果每个字符检查函数在比较结果之前都进行了一些任意位数学计算，那么我就不想把这些指令用于静态提取。我会静态识别目标函数，然后求解出每个函数值。

在每个字符检查函数上设置一个钩子。

    在positive branch上设置一个钩子来求解寄存器值RDI并存储该值。

    在negative branch上设置一个钩子来删除该状态。

    在当前指令的pre-branch上设置一个钩子，以检查该值是否处理完毕。

        如果该值已经处理完毕，并写入RDI，那就不需要再重复处理了。

在终止指令中设置一个钩子。

def symbolic_pcs(m, pcs, end_pc):
    for pc in pcs:
        set_hooks(m, pc)
 
    end_hook(m, end_pc)

把所有的解析值都整合起来

通过这三个函数，我现在就得到了有我所需要的目标地址。把所有main() 整合到一起，我就组合成了一个动态的解决方案来挑战magic文件了。你可以在这里找到完整的代码。

def main():
    path = sys.argv[1]
    m = Manticore(path)
    m.context['values'] = {}
    m.context['target_order'] = []
 
    pcs, end_pc = get_pcs(path)
 
    # symbolic(m, end_pc)
    # concrete_pcs(m, pcs, end_pc)
    symbolic_pcs(m, pcs, end_pc)
 
    m.run()

启用调试打印语句的运行将有助于显示此脚本的执行，这样我就第一次看到一个目标[addr]。当我使用先前解决的值来Concrete branch时（也就是第二种解决方案），就会看到[addr]中的[chr]。最后，当end_hook（）被出现时，我的最终目标-找到每个文件的密码也就实现了。

Manticore强大的分析能力

Manticore可以为编译代码提供执行符号， 以便很快地发现接受特定路径所需的输入值。 总之，Manticore可将人类的判断和高效率的符号执行结合在一起，增加二进制文件地分析能力。 对于任何从事二进制分析工作的人来说，具有简洁的API和强大函数的Manticore是一款比不可少的工具。