安全路透社
当前位置:安全路透社 > 安全客 > 正文

【技术分享】使用符号执行技术解决Android Crackme


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 <serial>
$ 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 参考


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-execution

未经允许不得转载:安全路透社 » 【技术分享】使用符号执行技术解决Android Crackme

赞 (0)
分享到:更多 ()

评论 0

评论前必须登录!

登陆 注册