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的context存储值。context字典实际上是多进程管理器的字典。当开始使用多个工作器时，需要使用context在它们之间共享数据。
函数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数组有一个奇怪的更新模式。它们需要重新分配到context字典，以通知多进程管理器它们已更改。
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所需的功能。