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贡献了使用Manticore运行Magic所需的功能。

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

页面内容挑战结构策略使用Binary Ninja API提取地址

通过操作码识别的符号解决方案
通过地址钩子的具体解决方案
通过地址钩子的符号解决方案将所有内容整合在一起开始更智能地使用Manticore 接受Manticore挑战最近帖子 Trail of Bits的Buttercup在AIxCC挑战中获得第二名 Buttercup现已开源！ AIxCC决赛：记录攻击者的提示注入工程：利用GitHub Copilot 发现NVIDIA Triton中的内存损坏（作为新员工） © 2025 Trail of Bits。使用Hugo和Mainroad主题生成。

探索Manticore：下一代二进制分析的魔法之旅

本文详细介绍了如何使用Manticore和Binary Ninja解决DEFCON CTF中的Magic挑战，涵盖三种不同的符号执行策略，包括操作码识别、地址钩子和混合方法，展示了现代二进制分析工具的强大功能。