Manticore魔法 - Trail of Bits博客

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

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

通过操作码识别的符号解决方案
通过地址钩子的具体解决方案
通过地址钩子的符号解决方案将所有内容整合在一起开始更智能地使用Manticore 接受Manticore挑战最近帖子构建安全消息传递很难：对Bitchat安全辩论的细致看法使用Deptective调查你的依赖项系好安全带，Buttercup，AIxCC的评分回合正在进行中！使你的智能合约超越私钥风险 Go解析器中意想不到的安全陷阱 © 2025 Trail of Bits. 使用Hugo和Mainroad主题生成。

Manticore魔法：利用符号执行自动化破解CTF挑战

本文详细介绍了如何使用Manticore符号执行工具自动化解决DEFCON CTF中的Magic挑战，涵盖三种不同策略：基于操作码识别的符号解法、基于地址钩子的具体解法和混合符号解法，展示了二进制分析的高效技术。