Magic with Manticore - The Trail of Bits Blog

Manticore是一款下一代二进制分析工具，具有简单而强大的API，支持符号执行、污点分析和插桩。使用Manticore可以识别“有趣”的代码位置，并推导出到达这些位置的输入。这可以生成输入以提高测试覆盖率，或快速引导执行到漏洞位置。

我利用Manticore的能力解决了Magic，这是今年DEFCON CTF资格赛中的一个挑战，包含200个独特的二进制文件，每个文件都有一个单独的密钥。当在每个二进制文件中输入正确的密钥时，它会打印出一个总和：

输入代码： ==== 药物有帮助总和是12

逆向工程200个可执行文件以逐个提取字符串需要大量时间。这个挑战需要自动化。随着CTF中这类挑战的增多，现代工具将成为保持竞争力的必要条件。

我们将结合两种工具——Binary Ninja和Manticore——的威力，通过三种不同的解决方案展示如何将它们应用到您的工作中。

挑战结构

Magic二进制文件具有简单的结构。有一个主函数提示输入密钥，从stdin读取，运行检查器函数，然后打印出总和。检查器函数逐个加载输入字符串的字节，并调用一个函数来检查每个字符。字符检查函数与固定字符值进行比较。如果匹配，函数返回一个要累加的值；如果不匹配，程序退出。

主函数、检查器函数和单个字符检查函数

Manticore的API非常直接。我们将使用钩子在到达指令时调用函数，使用CPU类访问寄存器，以及求解器。工作流程包括通过提供路径加载二进制文件，并在该二进制文件中的指令上添加分析钩子。之后，运行Manticore。当地址到达时，您的钩子被执行，您可以推理程序的状态。

定义为钩子的函数接受一个参数：state。state包含创建符号值或缓冲区、求解符号值和放弃路径的功能。它还包含一个成员cpu，用于保存寄存器的状态，并允许读写内存和寄存器。

策略

解决Magic有很多方法。我们将展示三种方法以展示Manticore的灵活性。

一种符号解决方案，钩住每条指令以发现字符检查函数的位置。当Manticore处于字符检查函数时，它设置钩子以求解必要的值。
一种具体解决方案，钩住每个字符检查函数的地址，并简单地从操作码中读取值。
一种符号解决方案，钩住每个字符检查函数的地址并求解值。

这不是您可以使用Manticore采取的方法的详尽列表。有句俗话说“有很多方法剥猫皮”；Manticore是一个剥猫皮机器。

函数地址将使用Binary Ninja提取。所有策略都需要一个终止钩子的地址以打印解决方案。后两种策略需要字符检查函数的地址。

使用Binary Ninja API提取地址

为了提取字符检查函数的地址以及end_hook()地址，我们将使用Binary Ninja。Binary Ninja是一个为快节奏CTF环境设计的逆向工程平台。它用户友好且具有强大的分析功能。我们将使用其API定位我们想要的地址。在Binary Ninja API中加载文件非常直接。

1

bv = binja.BinaryViewType.get_view_of_file(path)

为了到达检查器函数，我们首先需要可执行文件的主函数。我们首先检索程序入口函数的入口块。我们知道主函数的地址在LLIL的第11条指令中加载。从该指令中，我们进行健全性检查，确保它是一个加载到RDI中的常量，然后提取常量（主函数的地址）。使用主函数的地址调用get_function_at()返回主函数。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12


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()。它定位从主函数调用的检查器函数的地址。然后它加载该地址的函数并返回它。

1. 通过操作码识别的符号解决方案

每个字符检查函数具有相同的指令。这意味着我们可以检查操作码，并使用它们作为到达目标函数的指示。我们喜欢这种解决方案，适用于我们可能不一定知道需要设置钩子的位置但可以识别何时到达的情况。

设置每条指令的钩子。
检查操作码是否匹配检查函数的前几条指令。
在正分支设置钩子以求解寄存器值RDI并存储值。
在负分支设置钩子以放弃该状态。
在预分支（当前指令）设置钩子以检查是否知道求解的值。如果我们知道该值，设置RDI以便不需要再次求解。
在终止指令设置钩子。

负分支上的state.abandon()调用至关重要。这停止Manticore推理该分支，这在更复杂的代码中可能需要一段时间。没有放弃，您可能需要3小时解决；有了它，1分钟。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23


def symbolic(m, end_pc):
    # 使用None作为地址钩住每条指令
    @m.hook(None)
    def hook_all(state):
        # 在程序计数器读取整数
        cpu = state.cpu
        pc = cpu.PC
        instruction = cpu.read_int(pc)

        # 检查指令是否匹配
        # cmp   rdi, ??
        # je    +0xe
        if (instruction & 0xFFFFFF == 0xff8348) and (instruction >> 32 & 0xFFFF == 0x0e74):
            # 正分支距离函数开头0x14字节
            target = pc + 0x14

            # 如果目标地址尚未看到
            #   添加到列表并声明求解器钩子
            if target not in m.context['values']:
                set_hooks(m, pc)

    # 设置终止执行的结束钩子
    end_hook(m, end_pc)

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

函数set_hooks()将在策略3中重用：通过地址钩子的符号解决方案。它设置预分支、正分支和负分支钩子。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51


def set_hooks(m, pc):
    # 预分支
    @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

    # 负分支
    neg = pc + 0x6

    @m.hook(neg)
    def bail(state):
        if debug:
            print 'Abandoning state at %s...' % hex(neg)

        state.abandon()

    # 目标分支
    target = pc + 0x14

    @m.hook(target)
    def solve(state):
        _cpu = state.cpu
        _target = _cpu.PC
        _pc = _target - 0x14

        # 如果已知，跳过求解步骤
        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']])

注意，values字典和target_order数组有一个奇怪的更新模式。它们需要重新分配到上下文字典中以通知多进程管理器它们已更改。

end_hook()函数在所有三种策略中用于声明终止点。它在所有检查字符函数之后声明一个钩子。该钩子打印发现的字符，然后终止Manticore。

1
2
3
4
5
6


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()

2. 通过地址钩子的具体解决方案

由于这个挑战对每个字符执行简单的相等检查，很容易提取值。静态解决会更高效。事实上，可以用一行丑陋的bash解决。

1

$ ls -d -1 /path/to/magic_dist/* | while read file; do echo -n "'"; grep -ao $'\x48\x83\xff.\x74\x0e' $file | while read line; do echo $line | head -c 4 | tail -c 1; done; echo "'"; done

然而，在这种情况下，我们可以利用具体化。当值写入寄存器时，它不再是符号的。这导致分支明确并跳过求解。这也意味着负分支上的放弃钩子不再必要，因为由于具体值，它将始终采取正分支。

设置每个字符检查函数的钩子。
从操作码中提取目标值。
将该目标值写入寄存器RDI。
设置终止指令的钩子。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31


def concrete_pcs(m, pcs, end_pc):
    # 对于每个字符检查函数地址
    for pc in pcs:
        @m.hook(pc)
        def write(state):
            # 检索指令字节
            _pc = state.cpu.PC
            instruction = state.cpu.read_int(_pc)

            # 从指令中提取值
            val = instruction >> 24 & 0xFF

            # 具体化RDI
            state.cpu.write_register('RDI', val)

            # 存储值以在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)

3. 通过地址钩子的符号解决方案

从每个函数静态提取值很容易。然而，如果每个字符检查函数在比较结果之前进行了一些任意位运算，我们不想为静态提取重新实现所有这些指令。这时混合方法会有用。我们静态识别目标函数，然后在每个函数中求解值。

设置每个字符检查函数的钩子。
在正分支设置钩子以求解寄存器值RDI并存储值。
在负分支设置钩子以放弃该状态。
在预分支（当前指令）设置钩子以检查是否知道求解的值。
如果我们知道该值，将其写入RDI以便不需要再次求解。
设置终止指令的钩子。

1
2
3
4
5


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

    end_hook(m, end_pc)

将所有内容整合

通过这三个函数，我们有所需的目标地址。将所有内容整合到main()中，我们有一个用于挑战Magic的动态求解器。您可以在此处找到完整代码列表。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13


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()

启用调试打印语句的运行将帮助显示此脚本的执行。第一次击中正分支时，我们看到Reached target [addr]. Current Key:语句和到此为止的密钥。有时会采取负分支并放弃状态。当我们使用先前求解的值具体化分支时，我们看到Writing [chr] at [addr]…。最后，当击中end_hook()时，我们看到GOAL:和我们的最终密钥。

开始更智能地使用Manticore

Manticore在编译代码的较小部分提供符号执行。它可以非常快速地发现到达特定路径所需的输入。将符号执行的机械效率与人类直觉相结合，增强您的能力。凭借直接的API和强大功能，Manticore是任何从事二进制分析工作的人的必备工具。

接受Manticore挑战

您何不尝试一下？我们创建了一个非常类似于Magic的挑战，但设计成您不能简单地grep解决方案。安装Manticore，编译挑战，并步入二进制分析的未来。今天尝试！第一个在5分钟内执行的挑战解决方案将从Manticore团队获得奖金。（提示：使用多个工作器并优化。）

感谢@saelo贡献运行Magic with Manticore所需的功能。

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News

利用Manticore进行符号执行：破解DEFCON CTF挑战的三种策略

本文详细介绍了如何使用Manticore符号执行工具自动化破解DEFCON CTF中的Magic挑战，涵盖三种解决方案：基于操作码识别的符号执行、基于地址钩子的具体执行和混合符号执行方法。