Magic with Manticore - The Trail of Bits Blog

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

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

1
2
3


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

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

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

挑战结构

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

策略

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

基于操作码识别的符号执行解决方案，钩住每条指令以发现字符检查函数的位置
基于地址钩子的具体执行解决方案，钩住每个字符检查函数的地址并从操作码中读取值
基于地址钩子的符号执行解决方案，钩住每个字符检查函数的地址并求解值

这并非使用Manticore的所有可能方法。有句谚语说"条条大路通罗马"；Manticore就是通往罗马的机器。

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

使用Binary Ninja API提取地址

为了提取字符检查函数的地址以及end_hook()地址，我们将使用Binary Ninja。Binary Ninja是为快节奏CTF环境设计的逆向工程平台，用户友好且具有强大的分析功能。

 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

1. 基于操作码识别的符号执行解决方案

每个字符检查函数具有相同的指令。这意味着我们可以检查操作码并将其作为到达目标函数的指示。

在每个指令上设置钩子
检查操作码是否匹配检查函数的前几条指令
在正向分支上设置钩子以求解寄存器值RDI并存储值
在负向分支上设置钩子以放弃该状态
在分支前（当前指令）设置钩子检查是否已知求解值

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


def symbolic(m, end_pc):
    @m.hook(None)
    def hook_all(state):
        cpu = state.cpu
        pc = cpu.PC
        instruction = cpu.read_int(pc)

        if (instruction & 0xFFFFFF == 0xff8348) and (instruction >> 32 & 0xFFFF == 0x0e74):
            target = pc + 0x14
            if target not in m.context['values']:
                set_hooks(m, pc)

    end_hook(m, end_pc)

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

但在这种情况下，我们可以利用具体化优势。当值写入寄存器时，它不再具有符号性，使分支明确并跳过求解。

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


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
            state.cpu.write_register('RDI', val)
            
            _target = _pc + 0x14
            values = m.context['values']
            values[_target] = val
            m.context['values'] = values

3. 基于地址钩子的符号执行解决方案

如果每个字符检查函数在比较结果之前执行任意位运算，我们就不想为静态提取重新实现所有指令。这时混合方法就很有用。

1
2
3
4


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


def main():
    path = sys.argv[1]
    m = Manticore(path)
    m.context['values'] = {}
    m.context['target_order'] = []

    pcs, end_pc = get_pcs(path)
    symbolic_pcs(m, pcs, end_pc)
    m.run()

开始更智能地使用Manticore

Manticore在编译代码的较小部分上提供符号执行。它可以非常快速地发现到达特定路径所需的输入。将符号执行的机械效率与人类直觉相结合，增强您的能力。

接受Manticore挑战

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

用Manticore施展魔法：三种二进制分析策略解析

本文详细介绍了如何使用Manticore符号执行工具解决DEFCON CTF中的Magic挑战。通过三种不同策略（基于操作码识别的符号执行、基于地址钩子的具体执行和混合符号执行），展示了如何自动化分析200个二进制文件并提取关键字符串。