预估稿费：180RMB

投稿方式：发送邮件至linwei#360.cn，或登陆网页版在线投稿

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简单的安装：

$ pip install angr

建议用Virtualenv创建一个专用的虚拟环境，因为它的一些依赖项包含覆盖原始版本的分支版本Z3和PyVEX(如果不使用这些库，则可以跳过此步骤 – 另一方面， 使用Virtualenv总是一个好主意)。

Angr在gitbooks上提供了非常容易理解的文档，包括安装指导，教程和用法示例。还有完整的API参考提供。

在安卓设备中运行可执行文件能得到如下的输出。

$ 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

$ adb shell /data/local/tmp/validate 12345

Incorrect serial (wrong format).

到目前为止，一切都很好，但是我们不知道任何关于可靠的授权序列号是啥样的。通过IDA先大致浏览以下代码。

在反汇编中主要功能定位到地址0x1874处(注意到这是一个开启PIE的二进制文件，并且IDA选择了0x0作为映像基址)。函数名称是没有的，但是我们能看到一些调试字符串的引用：出现在base32解密输入字符串中(调用到sub_1340)。在main函数开始处，对于loc_1898有个长度校验用来验证输入字符串的长度是否是16。因此我们需要一个16个字符的base32加密的字符串。解码输入被传入函数sub_1760中，验证授权序列号的可靠性。

16个字符的base32字符串被解码成10个字节，因此我们知道验证函数希望有个10字节的二进制字符串。接下来，我们看下位于0x1760的验证函数：

.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可执行文件，因此我们必须将这个添加到上述地址中。解决方案如下。

#!/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 angr

import claripy

import 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)

注意到程序的最后一部分，能获得我们最终想要的输入字符串。然而我们从符号内存中读不到任何字符串或指针。真实发生的是求解器计算的具体的值能在程序状态中找到。

运行脚本能得到以下输出：

(angr) $ python solve.py

WARNING | 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 参考

Axel Souchet, Jonathan Salwan, Jérémy Fetiveau – Keygenning with KLEE –http://doar-e.github.io/blog/2015/08/18/keygenning-with-klee/