[TOC]
本片分析文章通过一道看雪CTF题讲述作者的整个分析流程,学习WebAssemble、Z3库、IDC脚本、多元线性方程等内容
安装应用后,出现一个输入框和一个按钮
jadx反编译apk后先查看manifest清单文件的注册组件,只有一个入口活动类,进入查看
<application android:theme="@style/AppTheme" android:label="@string/app_name" android:icon="@mipmap/ic_launcher" android:allowBackup="true" android:supportsRtl="true" android:usesCleartextTraffic="true" android:roundIcon="@mipmap/ic_launcher_round" android:appComponentFactory="android.support.v4.app.CoreComponentFactory"> <activity android:name="com.example.assemgogogo.MainActivity"> <intent-filter> <action android:name="android.intent.action.MAIN"/> <category android:name="android.intent.category.LAUNCHER"/> </intent-filter> </activity>
第一眼:看到Congratulations
,我们的目标是打印出这里的字符串,也就是点击按钮后调用本地方法check_key返回值为1即可
再仔细看看:这里有个WebView组件,这个组件表示有访问网络的操作,但是手机界面并没有看页面,我们去布局文件中看看,我们只需要看一个属性android:visibility
表示控件是否可见,只有WebView可见,按钮、输入框什么的都是隐藏的,并且这个webview占据的整个界面,所以我们看到的输入框和按钮都是网页展示的,所以我们需要关注的点就是sayHello这个本地方法,它传入的url是哪里的,这是我们下一步的要干的事
public String u = gogogoJNI.sayHello(); static { System.loadLibrary("gogogo"); } protected void onCreate(Bundle bundle) { super.onCreate(bundle); setContentView((int) R.layout.activity_main); this.eText1 = (EditText) findViewById(R.id.editText); this.txView1 = (TextView) findViewById(R.id.textView); ((WebView) findViewById(R.id.text1View)).loadUrl(this.u); ((WebView) findViewById(R.id.text1View)).getSettings().setJavaScriptEnabled(true); this.button1 = (Button) findViewById(R.id.button); this.button1.setOnClickListener(new OnClickListener() { public void onClick(View view) { if (gogogoJNI.check_key(MainActivity.this.eText1.getText().toString()) == 1) { MainActivity.this.txView1.setText("Congratulations!"); } else { MainActivity.this.txView1.setText("Not Correct!"); } } });
<EditText android:id="@+id/editText" android:visibility="invisible" android:layout_width="wrap_content" android:layout_height="wrap_content" android:text="Name" android:ems="10" android:inputType="textPersonName" android:layout_marginStart="14dp" app:layout_constraintBottom_toBottomOf="@+id/button" app:layout_constraintStart_toEndOf="@+id/textView"/> <Button android:id="@+id/button" android:visibility="invisible" android:layout_width="wrap_content" android:layout_height="wrap_content" android:layout_marginTop="52dp" android:text="check" android:layout_marginEnd="38dp" app:layout_constraintEnd_toEndOf="0" app:layout_constraintTop_toTopOf="0"/> <TextView android:id="@+id/textView" android:visibility="invisible" android:layout_width="wrap_content" android:layout_height="wrap_content" android:layout_marginTop="68dp" android:text="key" android:layout_marginStart="22dp" app:layout_constraintStart_toStartOf="0" app:layout_constraintTop_toTopOf="0"/> <WebView android:id="@+id/text1View" android:visibility="visible" android:layout_width="390dp" android:layout_height="733dp" android:layout_marginStart="4dp" app:layout_constraintStart_toStartOf="0" app:layout_constraintTop_toTopOf="0"/>
打开lib文件夹,出现四个abi架构对应的so文件,基本现在手机的芯片都是支持的,这里ARM64在ida6.8不能使用F5大法,所以我们就分析armeabi-v7这个就行了
我们可以看看第一步我们排除的check_key方法,这里逻辑是输出的32位数都为1即可返回1,实际尝试是错误的,混淆视听
在导出表中找到sayhello方法,要使用F5大法先右键将这个区域代码创建为函数。接着讲这个字节数组异或计算即可的到URL地址。下面写了一个简短的idc脚本获取到URL地址为 http://127.0.0.1:8000
分析到这里,虽然我们探索URL已经完成,但是却没有看见服务端处理的函数,这个才是我们访问URL的时候,处理我们访问请求的函数
#include <idc.idc> static main() { auto addr = 0x2d28; auto i; for(i=0; i !=21; ++i) { Message("%c", Byte(addr+i)^0x66); } }
从java层分析的逻辑中并没有服务端的线索,而so层也只有初始化的JNIonload、init节还没有探索,这是我们接下来的目标
第一步排除init节,so加载后首先执行的节代码,这里可以看出没有这个节,所以排除,那么就直接分析JNIonload方法,java中调用loadlibray的时候调用的方法
JNI_Onload分析:往进call两层,最终调用下面这个函数
int (__cdecl *inti_proc(void))(int)
{
return inti_proc();
}
这个函数 一开始就对data段中一块大小为34291的数据进行异或0x67解密,接着创建线程用socket链接将刚才解密的内容构造称HTTP的响应数据包,一旦有socket链接连接过来就发送这样的数据包回去。
逻辑分析清除,下面我们针对细节进行解决
针对需要解密的字节流,通过idc脚本进行处理,解密后的数据是html页面,使用到了WebAssembly技术,web汇编的灵魂就是将其他语言如C汇编成前端可以解释的语言,即用C语言写页面的一些逻辑。
#include <idc.idc> static main() { auto addr = 0x4004; auto i = 34291; while(i) { --i; Message("%c", Byte(addr++)^0x67); } }
分析这里的逻辑得知,我们需要让输入内容为32位并且check_key()函数返回结果为1,即可完成这道题
<!DOCTYPE html> <html><head> <meta http-equiv="content-type" content="text/html; charset=UTF-8"> <meta charset="utf-8"> <style> body { background-color: rgb(255, 255, 255); } </style> </head> <script> var instance; WebAssembly.compile(new Uint8Array(` 00 61 73 6D 01 00 00 00 01 1B 05 60 00 00 60 04 7F 7F 7F 7F 01 7F 60 02 7F 7F 01 7F 60 01 7F 01 ....... 66 6C 61 67 0A 12 73 65 74 5F 69 6E 70 75 74 5F 66 6C 61 67 5F 6C 65 6E 0B 09 63 68 65 63 6B 5F 6B 65 79 0C 03 78 78 78 `.trim().split(/[\s\r\n]+/g).map(str => parseInt(str, 16)) )).then(module => { new WebAssembly.instantiate(module).then(results => { instance = results; }).catch(console.error);}) function check_flag(){ var value = document.getElementById("key_value").value; if(value.length != 32) { document.getElementById("tips").innerHTML = "Not Correct!"; return; } instance.exports.set_input_flag_len(value.length); for(var ii=0;ii<value.length;ii++){ instance.exports.set_input_flag(value[ii].charCodeAt(),ii); } var ret = instance.exports.check_key(); if (ret == 1){ document.getElementById("tips").innerHTML = "Congratulations!" } else{ document.getElementById("tips").innerHTML = "Not Correct!" } } </script> <body> <div>Key: <input id="key_value" type="text" name="key" style="width:60%" ;="" value=""> <input type="submit" value="check" onclick="check_flag()"></div> <div> <label id="tips"></label></div> </body></html>
下面我们进入web汇编来探索内部实现逻辑
我们在这部分探索的目标就是先用16进制内容构成对应的wasm二进制文件,然后将wasm二进制文件转成c,接着生成ELF文件,用IDA进行分析。
先生成data.bin二进制文件
import array, struct hexstring = "\x00\x61\x73\x6D\x01\x00\x00\x00\x01\x1B\x05\x60\x00\x00\x60\x04\x7F\x7F\x7F\x7F\x01\x7F\x60\x02\x7F\x7F\x01\x7F\x60\x01\x7F\x01\x7F\x60\x00\x01\x7F ............. \x6C\x61\x67\x0A\x12\x73\x65\x74\x5F\x69\x6E\x70\x75\x74\x5F\x66\x6C\x61\x67\x5F\x6C\x65\x6E\x0B\x09\x63\x68\x65\x63\x6B\x5F\x6B\x65\x79\x0C\x03\x78\x78\x78" f = open('c:\\Users\\xxx\\Desktop\\data.bin','wb') f.write(hexstring) f.close()
接着用wasm2c.exe生成c文件
wasm2c.exe data.bin -o test.c
直接gcc wasm.c会报错,因为很多wasm的函数没有具体的实现。所以只编译就好了
用IDA打开.o文件
首先JS中调用将输入的字符长度保存到内存中,接着将输入的字符也保存到内存0x400处
接着就是主要的check_key函数,最终目标是xxx函数返回结果为1,即可完成逆向工作
这里前8个o函数对我们输入的32内容依次进行了处理,我们具体分析一下
经过简单分析,这里其实是对输入内容进行了异或计算,然后将结果替换内存中原来的数据。下面图中的条件是肯定满足的,因为我们输入的内容在33到127之间,最小的33*4也等于132肯定不为-1,这个语句恒执行else的内容,至于其余几个都是相同的内容,即在这里对输入内容进行第一次加密
接着我们分析xxx函数,我们的目标也是满足xxx函数返回值为1
从内存中奖一重加密后的输入内容读取到变量中,可以看到顺序做过修改
)
接下来就是下图中看到的32元方程组,如果有兴趣和数学基础的同学可以用矩阵解法写个类似的小脚本,这里我用到的是z3库解决
pip安装z3-solver
接着用python脚本写一个求解语句,先初始化32个变量,接着将ida的内容拷贝过来,将符号修改一下即可
# *-* coding:utf-8 -*- from z3 import * # 生面32元变量 v5 = Int('m53') v6 = Int('m52') v7 = Int('m51') v8 = Int('m50') v9 = Int('m49') v10 = Int('m48') v11 = Int('m47') v12 = Int('m46') v13 = Int('m45') v14 = Int('m44') v15 = Int('m43') v16 = Int('m42') v17 = Int('m41') v18 = Int('m40') v19 = Int('m39') v20 = Int('m38') v21 = Int('m37') v22 = Int('m36') v23 = Int('m35') v24 = Int('m34') v25 = Int('m33') v26 = Int('m32') v27 = Int('m31') v28 = Int('m30') v29 = Int('m29') v30 = Int('m28') v31 = Int('m27') v32 = Int('m26') v33 = Int('m24') v34 = Int('m25') v35 = Int('m55') v36 = Int('m54') # 实例化一个求解器对象 s = Solver() s.add(And(45 * v5 + 248 * v6 + 20 * v7 + 67 * v8 + 90 * v9 + 135 * v10 + 106 * v11 + 112 * v12 + 40 * v13 + 231 * v14 + 153 * v15 + 233 * v16 + 19 * v17 + 188 * v18 + 232 * v19 + 127 * v20 + 15 * v21 + 67 * v22 + 50 * v23 + 161 * v24 + 103 * v25 + 144 * v26 + 81 * v27 + 126 * v28 + 240 * v29 + 124 * v30 + 194 * v31 + 92 * v32 + 108 * v33 + 111 * v34 + 174 * v35 + 48 * v36 == 359512 ..... , 244 * v5 + 196 * v6 + 30 * v7 + 100 * v8 + 168 * v9 + 7 * v10 + 249 * v11 + 84 * v12 + 252 * v13 + 171 * v14 + 210 * v15 + 206 * v16 + 108 * v17 + 153 * v18 + 67 * v19 + 189 * v20 + 141 * v21 + 239 * v22 + 177 * v23 + 10 * v24 + 15 * v25 + 164 * v26 + 142 * v27 + 97 * v28 + 27 * v29 + 173 * v30 + 146 * v31 + 133 * v33 + 105 * v34 + 75 * (v32 + v35) + 197 * v36 == 393331 )) s.add(185 * v5 + 196 * v6 + 135 * v7 + 218 * (v24 + v9) + 241 * v8 + 210 * v10 + 127 * v11 + 221 * v12 + 47 * v13 + 179 * v14 + 61 * v15 + 59 * v16 + 197 * v17 + 204 * v18 + 198 * v19 + 75 * v20 + 146 * v21 + 156 * v22 + 235 * v23 + 63 * v25 + 220 * v26 + 3 * v27 + 167 * v28 + 230 * v29 + 69 * v30 + 186 * v31 + 57 * v32 + 147 * v33 + 221 * v34 + 79 * v35 + 53 * v36 == 430295) # sat表示计算出结果 if s.check() == sat: t = [] print "compute result: " m = s.model() t.append(str(m[v33])) t.append(str(m[v34])) t.append(str(m[v32])) t.append(str(m[v31])) t.append(str(m[v30])) t.append(str(m[v29])) t.append(str(m[v28])) t.append(str(m[v27])) t.append(str(m[v26])) t.append(str(m[v25])) t.append(str(m[v24])) t.append(str(m[v23])) t.append(str(m[v22])) t.append(str(m[v21])) t.append(str(m[v20])) t.append(str(m[v19])) t.append(str(m[v18])) t.append(str(m[v17])) t.append(str(m[v16])) t.append(str(m[v15])) t.append(str(m[v14])) t.append(str(m[v13])) t.append(str(m[v12])) t.append(str(m[v11])) t.append(str(m[v10])) t.append(str(m[v9])) t.append(str(m[v8])) t.append(str(m[v7])) t.append(str(m[v6])) t.append(str(m[v5])) t.append(str(m[v36])) t.append(str(m[v35])) t = map(int, t) t = map(chr, t) print "".join(t) else: print "failed"
这里直接用的大佬的脚本,将上面解密的数据进行异或计算,即可返回最终我们需要输入的内容
int main(int argc, char** argv) { unsigned char c[33] = "S0m3time_l1tt1e_c0de_1s_us3ful33"; unsigned char in[33] = { 0 }; unsigned int t1 =0,t2= 0,t3=0,t4=0; printf((const char *)c); printf("\n"); in[0] = c[0] ^ 0x18; in[1] = c[1] ^ 0x9; in[2] = c[2] ^ 0x3; in[3] = c[3] ^ 0x6b; in[4] = c[4] ^ 0x1; in[5] = c[5] ^ 0x5A; in[6] = c[6] ^ 0x32; in[7] = c[7] ^ 0x57; in[8] = c[8] ^ 0x30; in[9] = c[9] ^ 0x5d; in[10] = c[10] ^ 0x40; in[11] = c[11] ^ 0x46; in[12] = c[12] ^ 0x2b; in[13] = c[13] ^ 0x46; in[14] = c[14] ^ 0x56; in[15] = c[15] ^ 0x3d; in[16] = c[16] ^ 0x02; in[17] = c[17] ^ 0x43; in[18] = c[18] ^ 0x17; in[19] = c[19]; in[20] = c[20] ^ 0x32; in[21] = c[21] ^ 0x53; in[22] = c[22] ^ 0x1F; in[23] = c[23] ^ 0x26; in[24] = c[24] ^ 0x2a; in[25] = c[25] ^ 0x01; in[26] = c[26]; in[27] = c[27] ^ 0x10; in[28] = c[28] ^ 0x10; in[29] = c[29] ^ 0x1E; in[30] = c[30] ^ 0x40; in[31] = c[31]; printf((const char *)in); return 0; }
【1】 多元线性方程式可以通过python的z3-solver库快速计算
最开始做这道题我是卡在了最后一步,我用sage并未求出结果。
主要原因是:我甚至未能清除的理解这个算法的本质,当时并未意识到这是个多元方程求解的计算,只想着怎么求出这个结果,结果在网上找到一个相似题的解决方法,用sage计算,但在这里却并未算出
结论:解决问题时,不要求对所有细节了如执掌,但是题的主干脉络、根本思路是我们需要探索的
【1】[原创]第五题:丛林的秘密https://bbs.pediy.com/thread-252191.htm
【2】Z3 API in Python https://nen9ma0.github.io/2018/03/14/z3py/
【3】IDC脚本 - IDC脚本语言官方教程 https://bbs.pediy.com/thread-219016.htm
【4】线性方程组矩阵解法 https://www.shuxuele.com/algebra/systems-linear-equations-matrices.html