0x00 前言
二进制分析框架提供给我们强大的自动化分析的方法。本文中，我们将看下Angr，一个python实现的用于静态和动态分析的分析框架。它基于Valgrind的VEX中间层语言。使用一个精简的加载器“CLE Loads Everything”，这个加载器不是完全精确的，但是能够加载ELF/ARM的可执行文件，因此对于处理Android的原生库有帮助。
我们的目标程序是一个授权验证程序。虽然在应用商店中不会总是发现类似的东西，但是用来描述基本的符号分析是足够的。您可以在混淆的Android二进制文件中以许多创造性的方式使用这些技术。
0x01 符号执行
在21世纪后期，基于符号执行的测试就在用于确认安全漏洞的领域非常流行。符号“执行”实际上是指代表通过程序的可能路径作为一阶逻辑中的公式的过程，其中变量由符号值表示。通过SMT解释器来验证并给这些公式提供解决方案，我们能得到到达每个执行点的需要的数据。
简单来说，工作过程如下：
1. 将程序的一个路径翻译为一个逻辑表达式，其中的一些状态用符号表示
2. 解决公式
3. 得到结果
这是一个简化的描述，实际上更加复杂。执行引擎首先枚举程序中所有可能的路径。对于每个分支，引擎将由分支条件施加的约束保存在分支所依赖的符号变量上。最终得到一个非常大的路径公式，并解决相关的公式，你将得到覆盖所有路径的输入变量。
然而，解决公式是困难的一部分。为了理解这个如何工作，让我们回顾下布尔可满足性(SAT)问题。SAT是一个确定命题逻辑公式的是否满足的问题，例如(x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3)（意思是，根据输入可能产生一个true的结果）。然而命题逻辑不足以编码在我们的程序中发生的所有可能的约束：毕竟，分支决定依赖符号变量之间的复杂的关系。
因此我们需要将SAT扩展到SMT。SMT能用非二进制变量的集合断言代替SAT公式。每个断言的输出是一个二进制值。一个线性代数中的断言可以是“2x+3y>1”。因此，当“2x+3y>1”满足时一个特殊的分支可能被采用。
每个路径公式都是SMT问题。负责解决问题的SAT解释器简单地将理论断言的连接传递给各个理论的专用求解器，例如线性算术，非线性算术和位向量。最终，问题被简化为SAT求解程序，可以处理的一个普通的布尔SAT实例。
0x02 实例分析
符号执行对于需要找到到达特定代码块的正确输入是很有用的。在下面的例子中，将使用Angr来自动化解决一个简单Android Crackme。这个crackme采用的原生ELF二进制文件在这里下载到。
安装Angr
Angr使用python 2编写，在PyPi提供。可以通过pip简单的安装：
|
1
|
$ pip install angr |
建议用Virtualenv创建一个专用的虚拟环境，因为它的一些依赖项包含覆盖原始版本的分支版本Z3和PyVEX（如果不使用这些库，则可以跳过此步骤 - 另一方面， 使用Virtualenv总是一个好主意）。
Angr在gitbooks上提供了非常容易理解的文档，包括安装指导，教程和用法示例。还有完整的API参考提供。
在安卓设备中运行可执行文件能得到如下的输出。
|
1
2
3
4
5
6
7
|
$ adb push validate /data/local/tmp[100%] /data/local/tmp/validate$ adb shell chmod 755 /data/local/tmp/validate$ adb shell /data/local/tmp/validateUsage: ./validate <serial>$ adb shell /data/local/tmp/validate 12345Incorrect serial (wrong format). |
到目前为止，一切都很好，但是我们不知道任何关于可靠的授权序列号是啥样的。通过IDA先大致浏览以下代码。
在反汇编中主要功能定位到地址0x1874处（注意到这是一个开启PIE的二进制文件，并且IDA选择了0x0作为映像基址）。函数名称是没有的，但是我们能看到一些调试字符串的引用：出现在base32解密输入字符串中（调用到sub_1340）。在main函数开始处，对于loc_1898有个长度校验用来验证输入字符串的长度是否是16。因此我们需要一个16个字符的base32加密的字符串。解码输入被传入函数sub_1760中，验证授权序列号的可靠性。
16个字符的base32字符串被解码成10个字节，因此我们知道验证函数希望有个10字节的二进制字符串。接下来，我们看下位于0x1760的验证函数：
|
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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
.text:00001760 ; =============== S U B R O U T I N E =======================================.text:00001760.text:00001760 ; Attributes: bp-based frame.text:00001760.text:00001760 sub_1760 ; CODE XREF: sub_1874+B0.text:00001760.text:00001760 var_20 = -0x20.text:00001760 var_1C = -0x1C.text:00001760 var_1B = -0x1B.text:00001760 var_1A = -0x1A.text:00001760 var_19 = -0x19.text:00001760 var_18 = -0x18.text:00001760 var_14 = -0x14.text:00001760 var_10 = -0x10.text:00001760 var_C = -0xC.text:00001760.text:00001760 STMFD SP!, {R4,R11,LR}.text:00001764 ADD R11, SP, #8.text:00001768 SUB SP, SP, #0x1C.text:0000176C STR R0, [R11,#var_20].text:00001770 LDR R3, [R11,#var_20].text:00001774 STR R3, [R11,#var_10].text:00001778 MOV R3, #0.text:0000177C STR R3, [R11,#var_14].text:00001780 B loc_17D0.text:00001784 ; ---------------------------------------------------------------------------.text:00001784.text:00001784 loc_1784 ; CODE XREF: sub_1760+78.text:00001784 LDR R3, [R11,#var_10].text:00001788 LDRB R2, [R3].text:0000178C LDR R3, [R11,#var_10].text:00001790 ADD R3, R3, #1.text:00001794 LDRB R3, [R3].text:00001798 EOR R3, R2, R3 ; Aha! You're XOR-ing a byte with the byte next to it. In a loop! You bastard..text:0000179C AND R2, R3, #0xFF.text:000017A0 MOV R3, #0xFFFFFFF0.text:000017A4 LDR R1, [R11,#var_14].text:000017A8 SUB R0, R11, #-var_C.text:000017AC ADD R1, R0, R1.text:000017B0 ADD R3, R1, R3.text:000017B4 STRB R2, [R3].text:000017B8 LDR R3, [R11,#var_10].text:000017BC ADD R3, R3, #2.text:000017C0 STR R3, [R11,#var_10].text:000017C4 LDR R3, [R11,#var_14].text:000017C8 ADD R3, R3, #1.text:000017CC STR R3, [R11,#var_14].text:000017D0.text:000017D0 loc_17D0 ; CODE XREF: sub_1760+20.text:000017D0 LDR R3, [R11,#var_14].text:000017D4 CMP R3, #4.text:000017D8 BLE loc_1784.text:000017DC LDRB R4, [R11,#var_1C] ; Now you're comparing the xor-ed bytes with values retrieved from - somewhere....text:000017E0 BL sub_16F0.text:000017E4 MOV R3, R0.text:000017E8 CMP R4, R3.text:000017EC BNE loc_1854.text:000017F0 LDRB R4, [R11,#var_1B].text:000017F4 BL sub_170C.text:000017F8 MOV R3, R0.text:000017FC CMP R4, R3.text:00001800 BNE loc_1854.text:00001804 LDRB R4, [R11,#var_1A].text:00001808 BL sub_16F0.text:0000180C MOV R3, R0.text:00001810 CMP R4, R3.text:00001814 BNE loc_1854.text:00001818 LDRB R4, [R11,#var_19].text:0000181C BL sub_1728.text:00001820 MOV R3, R0.text:00001824 CMP R4, R3.text:00001828 BNE loc_1854.text:0000182C LDRB R4, [R11,#var_18].text:00001830 BL sub_1744.text:00001834 MOV R3, R0.text:00001838 CMP R4, R3.text:0000183C BNE loc_1854.text:00001840 LDR R3, =(aProductActivat - 0x184C) ; This is where we want to be!.text:00001844 ADD R3, PC, R3 ; "Product activation passed. Congratulati"....text:00001848 MOV R0, R3 ; char *.text:0000184C BL puts.text:00001850 B loc_1864.text:00001854 ; ---------------------------------------------------------------------------.text:00001854.text:00001854 loc_1854 ; CODE XREF: sub_1760+8C.text:00001854 ; sub_1760+A0j ....text:00001854 LDR R3, =(aIncorrectSer_0 - 0x1860) ; This is where we DON'T wanna be!.text:00001858 ADD R3, PC, R3 ; "Incorrect serial.".text:0000185C MOV R0, R3 ; char *.text:00001860 BL puts.text:00001864.text:00001864 loc_1864 ; CODE XREF: sub_1760+F0.text:00001864 SUB SP, R11, #8.text:00001868 LDMFD SP!, {R4,R11,PC}.text:00001868 ; End of function sub_1760 |
我们能在loc_1784看到异或操作，应该是解码操作。从loc_17DC开始，我们能看到一系列的解码值的比较。尽管它看起来高度复杂，我们还需要更多的逆向分析并生成授权传给它。但是通过动态符号执行，我们不需要做更多的深入分析。符号执行引擎能够映射一条在校验授权的开始处（0x1760）和输出消息“Product activation passed”的地方（0x1840）之间的路径，决定每种输入的约束。求解引擎能发现满足那些约束的输入值即可靠的授权序列号。
我们只需要提供几种输入给符号执行引擎：
1. 开始执行的地址。我们使用串行验证函数的第一条指令来初始化状态。这能使任务变得简单，因为我们避免了符号执行base32实现。
2. 我们想要执行到达的代码块地址。在这个例子中，我们想找到一个输出“Product activation passed”消息的有效路径。这个块的其实地址是0x1840。
3. 我们不想到达的地址。这种情况下，我们对于任何到达输出“incorrect serial”消息的路径不感兴趣（0x1854）。
Angr加载器在基址0x400000处加载PIE可执行文件，因此我们必须将这个添加到上述地址中。解决方案如下。
|
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
|
#!/usr/bin/python # This is how we defeat the Android license check using Angr!# The binary is available for download on GitHub:# https://github.com/b-mueller/obfuscation-metrics/tree/master/crackmes/android/01_license_check_1# Written by Bernhard -- bernhard [dot] mueller [at] owasp [dot] org import angrimport claripyimport base64 load_options = {} # Android NDK library path:load_options['custom_ld_path'] = ['/Users/berndt/Tools/android-ndk-r10e/platforms/android-21/arch-arm/usr/lib'] 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. state = b.factory.blank_state(addr=0x401760) initial_path = b.factory.path(state)path_group = b.factory.path_group(state) # 0x401840 = Product activation passed# 0x401854 = Incorrect serial path_group.explore(find=0x401840, avoid=0x401854)found = path_group.found[0] # Get the solution string from *(R11 - 0x24). addr = found.state.memory.load(found.state.regs.r11 - 0x24, endness='Iend_LE')concrete_addr = found.state.se.any_int(addr)solution = found.state.se.any_str(found.state.memory.load(concrete_addr,10)) print base64.b32encode(solution) |
注意到程序的最后一部分，能获得我们最终想要的输入字符串。然而我们从符号内存中读不到任何字符串或指针。真实发生的是求解器计算的具体的值能在程序状态中找到。
运行脚本能得到以下输出：
|
1
2
3
|
(angr) $ python solve.pyWARNING | 2017-01-09 17:17:03,664 | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.JQAE6ACMABNAAIIA |
最终的授权序列号应该能使程序输出成功的消息。
同时，符号执行是一种强大的技术，能用于漏洞挖掘，解混淆和逆向工程。
0x03 参考
Angr - http://angr.io
Axel Souchet, Jonathan Salwan, Jérémy Fetiveau - Keygenning with KLEE - http://doar-e.github.io/blog/2015/08/18/keygenning-with-klee/
Logic for Computer Science - http://www.cs.ru.nl/~herman/onderwijs/soflp2013/reeves-clarke-lcs.pdf
Concolic Testing: https://en.wikipedia.org/wiki/Concolic_testing
本文由 安全客 翻译，转载请注明“转自安全客”，并附上链接。
原文链接：http://www.vantagepoint.sg/blog/81-solving-an-android-crackme-with-a-little-symbolic-execution0day
文章评论