MASTG-TECH-0037: 符号执行
符号执行是你工具箱中一个非常有用的技术，尤其是在处理需要找到正确输入才能到达特定代码块的问题时。在本节中，我们将通过使用 Angr 二进制分析框架作为我们的符号执行引擎，来解决一个简单的 Android 破解程序。
为了演示这项技术，我们将使用一个名为 Android License Validator 的破解程序。 该破解程序由单个 ELF 可执行文件组成，可以通过按照以下说明在任何 Android 设备上执行
$ adb push validate /data/local/tmp
[100%] /data/local/tmp/validate
$ adb shell chmod 755 /data/local/tmp/validate
$ adb shell /data/local/tmp/validate
Usage: ./validate <serial>
$ adb shell /data/local/tmp/validate 12345
Incorrect serial (wrong format).
到目前为止一切顺利，但我们对有效的许可证密钥是什么样子一无所知。 首先，在反汇编程序（如 iaito 中打开 ELF 可执行文件。 main 函数位于反汇编中的偏移量 0x00001874 处。 重要的是要注意，此二进制文件已启用 PIE，并且 iaito 选择在 0x0 处加载二进制文件作为镜像基址。
函数名称已从二进制文件中删除，但幸运的是，有足够的调试字符串为我们提供代码上下文。 展望未来，我们将从偏移量 0x00001874 的入口函数开始分析二进制文件，并记下所有容易获得的讯息。 在此分析期间，我们还将尝试识别适合符号执行的代码区域。
strlen 在偏移量 0x000018a8 处被调用，并且返回的值在偏移量 0x000018b0 处与 0x10 进行比较。 紧随其后，输入字符串在偏移量 0x00001340 处被传递给 Base32 解码函数。 这为我们提供了有价值的讯息，即输入许可证密钥是一个 Base32 编码的 16 个字符的字符串（总共为 10 个原始字节）。 然后，解码后的输入被传递到偏移量 0x00001760 处的函数，该函数验证许可证密钥。 该函数的反汇编如下所示。
我们现在可以使用有关预期输入的此讯息来进一步研究 0x00001760 处的验证函数。
╭ (fcn) fcn.00001760 268
│ fcn.00001760 (int32_t arg1);
│ ; var int32_t var_20h @ fp-0x20
│ ; var int32_t var_14h @ fp-0x14
│ ; var int32_t var_10h @ fp-0x10
│ ; arg int32_t arg1 @ r0
│ ; CALL XREF from fcn.00001760 (+0x1c4)
│ 0x00001760 push {r4, fp, lr}
│ 0x00001764 add fp, sp, 8
│ 0x00001768 sub sp, sp, 0x1c
│ 0x0000176c str r0, [var_20h] ; 0x20 ; "$!" ; arg1
│ 0x00001770 ldr r3, [var_20h] ; 0x20 ; "$!" ; entry.preinit0
│ 0x00001774 str r3, [var_10h] ; str.
│ ; 0x10
│ 0x00001778 mov r3, 0
│ 0x0000177c str r3, [var_14h] ; 0x14
│ ╭─< 0x00001780 b 0x17d0
│ │ ; CODE XREF from fcn.00001760 (0x17d8)
│ ╭──> 0x00001784 ldr r3, [var_10h] ; str.
│ │ ; 0x10 ; entry.preinit0
│ ╎│ 0x00001788 ldrb r2, [r3]
│ ╎│ 0x0000178c ldr r3, [var_10h] ; str.
│ ╎│ ; 0x10 ; entry.preinit0
│ ╎│ 0x00001790 add r3, r3, 1
│ ╎│ 0x00001794 ldrb r3, [r3]
│ ╎│ 0x00001798 eor r3, r2, r3
│ ╎│ 0x0000179c and r2, r3, 0xff
│ ╎│ 0x000017a0 mvn r3, 0xf
│ ╎│ 0x000017a4 ldr r1, [var_14h] ; 0x14 ; entry.preinit0
│ ╎│ 0x000017a8 sub r0, fp, 0xc
│ ╎│ 0x000017ac add r1, r0, r1
│ ╎│ 0x000017b0 add r3, r1, r3
│ ╎│ 0x000017b4 strb r2, [r3]
│ ╎│ 0x000017b8 ldr r3, [var_10h] ; str.
│ ╎│ ; 0x10 ; entry.preinit0
│ ╎│ 0x000017bc add r3, r3, 2 ; "ELF\x01\x01\x01" ; aav.0x00000001
│ ╎│ 0x000017c0 str r3, [var_10h] ; str.
│ ╎│ ; 0x10
│ ╎│ 0x000017c4 ldr r3, [var_14h] ; 0x14 ; entry.preinit0
│ ╎│ 0x000017c8 add r3, r3, 1
│ ╎│ 0x000017cc str r3, [var_14h] ; 0x14
│ ╎│ ; CODE XREF from fcn.00001760 (0x1780)
│ ╎╰─> 0x000017d0 ldr r3, [var_14h] ; 0x14 ; entry.preinit0
│ ╎ 0x000017d4 cmp r3, 4 ; aav.0x00000004 ; aav.0x00000001 ; aav.0x00000001
│ ╰──< 0x000017d8 ble 0x1784 ; likely
│ 0x000017dc ldrb r4, [fp, -0x1c] ; "4"
│ 0x000017e0 bl fcn.000016f0
│ 0x000017e4 mov r3, r0
│ 0x000017e8 cmp r4, r3
│ ╭─< 0x000017ec bne 0x1854 ; likely
│ │ 0x000017f0 ldrb r4, [fp, -0x1b]
│ │ 0x000017f4 bl fcn.0000170c
│ │ 0x000017f8 mov r3, r0
│ │ 0x000017fc cmp r4, r3
│ ╭──< 0x00001800 bne 0x1854 ; likely
│ ││ 0x00001804 ldrb r4, [fp, -0x1a]
│ ││ 0x00001808 bl fcn.000016f0
│ ││ 0x0000180c mov r3, r0
│ ││ 0x00001810 cmp r4, r3
│ ╭───< 0x00001814 bne 0x1854 ; likely
│ │││ 0x00001818 ldrb r4, [fp, -0x19]
│ │││ 0x0000181c bl fcn.00001728
│ │││ 0x00001820 mov r3, r0
│ │││ 0x00001824 cmp r4, r3
│ ╭────< 0x00001828 bne 0x1854 ; likely
│ ││││ 0x0000182c ldrb r4, [fp, -0x18]
│ ││││ 0x00001830 bl fcn.00001744
│ ││││ 0x00001834 mov r3, r0
│ ││││ 0x00001838 cmp r4, r3
│ ╭─────< 0x0000183c bne 0x1854 ; likely
│ │││││ 0x00001840 ldr r3, [0x0000186c] ; [0x186c:4]=0x270 section..hash ; section..hash
│ │││││ 0x00001844 add r3, pc, r3 ; 0x1abc ; "Product activation passed. Congratulations!"
│ │││││ 0x00001848 mov r0, r3 ; 0x1abc ; "Product activation passed. Congratulations!" ;
│ │││││ 0x0000184c bl sym.imp.puts ; int puts(const char *s)
│ │││││ ; int puts("Product activation passed. Congratulations!")
│ ╭──────< 0x00001850 b 0x1864
│ ││││││ ; CODE XREFS from fcn.00001760 (0x17ec, 0x1800, 0x1814, 0x1828, 0x183c)
│ │╰╰╰╰╰─> 0x00001854 ldr r3, aav.0x00000288 ; [0x1870:4]=0x288 aav.0x00000288
│ │ 0x00001858 add r3, pc, r3 ; 0x1ae8 ; "Incorrect serial." ;
│ │ 0x0000185c mov r0, r3 ; 0x1ae8 ; "Incorrect serial." ;
│ │ 0x00001860 bl sym.imp.puts ; int puts(const char *s)
│ │ ; int puts("Incorrect serial.")
│ │ ; CODE XREF from fcn.00001760 (0x1850)
│ ╰──────> 0x00001864 sub sp, fp, 8
╰ 0x00001868 pop {r4, fp, pc} ; entry.preinit0 ; entry.preinit0 ;
讨论函数中的所有指令超出了本章的范围，相反，我们将仅讨论分析所需的重要点。 在验证函数中，在 0x00001784 处存在一个循环，该循环在偏移量 0x00001798 处执行 XOR 操作。 该循环在下面的图形视图中更清楚地可见。
XOR 是一种非常常用的技术，用于加密以混淆为目标而不是安全性的讯息。 **XOR 不应用于任何严肃的加密**，因为它可以使用频率分析来破解。 因此，在这种验证逻辑中仅存在 XOR 加密始终需要特别注意和分析。
继续前进，在偏移量 0x000017dc 处，从上面获得的 XOR 解码值与子函数调用 0x000017e8 的返回值进行比较。
显然，此函数并不复杂，可以手动分析，但仍然是一项繁琐的任务。 特别是在处理大型代码库时，时间可能是一个主要制约因素，并且希望自动化此类分析。 动态符号执行在完全相同的情况下很有帮助。 在上面的破解程序中，符号执行引擎可以通过映射许可证检查的第一条指令（位于 0x00001760）和打印“产品激活已通过”消息的代码（位于 0x00001840）之间的路径来确定输入字符串的每个字节的约束。
从上述步骤获得的约束被传递给求解器引擎，该引擎找到满足它们的输入-有效的许可证密钥。
你需要执行多个步骤来初始化 Angr 的符号执行引擎
-
将二进制文件加载到
Project中，这是 Angr 中任何类型分析的起点。 -
传递应从其开始分析的地址。 在这种情况下，我们将使用序列号验证功能的第一条指令初始化状态。 这使得问题更容易解决，因为你避免了象征性地执行 Base32 实现。
-
传递分析应到达的代码块的地址。 在这种情况下，偏移量为
0x00001840，负责打印“产品激活已通过”消息的代码位于此处。 -
此外，指定分析不应到达的地址。 在这种情况下，在
0x00001854处打印“不正确的序列号”消息的代码块不有趣。
请注意，Angr 加载器将使用
0x400000的基址加载 PIE 可执行文件，需要在将其传递给 Angr 之前将其添加到 iaito 的偏移量中。
最终的解决方案脚本如下所示
import angr # Version: 9.2.2
import base64
load_options = {}
b = angr.Project("./validate", load_options = load_options)
# The key validation function starts at 0x401760, so that's where we create the initial state.
# This speeds things up a lot because we're bypassing the Base32-encoder.
options = {
angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS,
}
state = b.factory.blank_state(addr=0x401760, add_options=options)
simgr = b.factory.simulation_manager(state)
simgr.explore(find=0x401840, avoid=0x401854)
# 0x401840 = Product activation passed
# 0x401854 = Incorrect serial
found = simgr.found[0]
# Get the solution string from *(R11 - 0x20).
addr = found.memory.load(found.regs.r11 - 0x20, 1, endness="Iend_LE")
concrete_addr = found.solver.eval(addr)
solution = found.solver.eval(found.memory.load(concrete_addr,10), cast_to=bytes)
print(base64.b32encode(solution))
如前文“动态二进制插桩”部分所述，符号执行引擎构建给定程序输入的运算的二叉树，并为可能采取的每条路径生成数学方程式。 在内部，Angr 探索了我们指定的两个点之间的所有路径，并将相应的数学方程式传递给求解器以返回有意义的具体结果。 我们可以通过 simulation_manager.found 列表访问这些解决方案，其中包含 Angr 探索的满足我们指定搜索标准的所有可能路径。
仔细查看脚本的后半部分，其中正在检索最终解决方案字符串。 字符串的地址是从地址 r11 - 0x20 获得的。 这起初可能看起来很神奇，但仔细分析 0x00001760 的函数会发现线索，因为它确定给定的输入字符串是否是有效的许可证密钥。 在上面的反汇编中，你可以看到函数的输入字符串（在寄存器 R0 中）是如何存储到本地堆栈变量 0x0000176c str r0, [var_20h] 中的。 因此，我们决定使用此值来检索脚本中的最终解决方案。 使用 found.solver.eval 你可以问求解器这样的问题，“给定此操作序列的输出（found 中的当前状态），输入（在 addr 处）必须是什么？”。
在 ARMv7 中，R11 被称为 fp（函数指针），因此
R11 - 0x20等价于fp-0x20：var int32_t var_20h @ fp-0x20
接下来，脚本中的 endness 参数指定数据以“little-endian”方式存储，这几乎是所有 Android 设备的情况。
此外，脚本似乎只是从脚本的内存中读取解决方案字符串。 但是，它是从符号内存中读取的。 字符串和字符串指针都不存在。 求解器确保它提供的解决方案与将程序执行到该点时相同。
运行此脚本应返回以下输出
$ python3 solve.py
WARNING | ... | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.
b'JACE6ACIARNAAIIA'
现在你可以在你的 Android 设备上运行验证二进制文件来验证解决方案（请参阅 Android License Validator）。
使用脚本你可能会获得不同的解决方案，因为可能有多个有效的许可证密钥。
总之，学习符号执行起初可能看起来有点令人生畏，因为它需要深入的理解和大量的实践。 但是，考虑到与手动分析复杂的反汇编指令相比，它可以节省宝贵的时间，因此这种努力是合理的。 通常你会使用混合技术，就像在上面的示例中一样，我们对反汇编的代码执行手动分析，以便为符号执行引擎提供正确的条件。 请参阅 iOS 章节，了解更多 Angr 用法的示例。