Z3介绍,什么是Z3?
Z3是由微软公司开发的一个优秀的SMT求解器,它能够检查逻辑表达式的可满足性,可以用来软件/硬件验证和测试,约束求解,混合系统分析,安全性研究,生物学研究(计算机分析)以及几何问题。通俗的来讲我们可以简单理解为它是一个解方程的计算器,Z3py是使用脚本来解决一些实际问题。
Z3在CTF逆向中有什么用?
我们在做CTF逆向题的时候,当我们已经逆向到最后求flag或者具体数值解的时候,例如最简单的:我们知道了未知量x,y,也知道了约束条件x+y=5,那么此时我们就可以使用Z3来求解x和y的值,因为x和y的值肯定有多个解,而我们最后的flag肯定只有一个,那么我们就可以继续添加约束条件来减少解的数量,最后得出正确的flag。
安装Z3
pycharm安装步骤:在File->Settings->Project Interpreter->点击+号->然后搜索框中搜索z3->下载z3和z3-solver 即可
安装后如下图所示:
Linux下安装步骤
git clone https://github.com/Z3Prover/z3.git cd z3 python scripts/mk_make.py cd build make make install
Z3语法简介:
Z3在python中主要有以下数据类型:Int --> 整型Bool --> 布尔型Array --> 数组BitVec('a',8) --> char型(其中的数字不一定是8,例如C语言中的int型可以用BitVec('a',32)表示)
几个常用API
Solver():创建一个通用求解器,创建后我们可以添加我们的约束条件,进行下一步的求解。
add():添加约束条件,通常在solver()命令之后,添加的约束条件通常是一个逻辑等式。
check():通常用来判断在添加完约束条件后,来检测解的情况,有解的时候会回显sat,无解的时候会回显unsat。
model():在存在解的时候,该函数会将每个限制条件所对应的解集取交集,进而得出正解。
更多的使用方法大家可以参考这个说明文档https://arabelatso.github.io/2018/06/14/Z3%20API%20in%20Python/
小练习demo:
我们小时候就知道解方程的大致步骤:1.设未知数--->2.列方程--->3.解方程--->4.得到结果
问题:假设有两个未知数x和y,已知x+y=5且2x+3y=14,让我们求x和y分别是多少?(可能有的小伙伴会问了,你不会是个傻子吧,这还用编程计算?我口算都能算得出来,这里我只是给大家随便举了个简单的例子,大家别往心里去,主要目的是演示Z3用法 -。-)下面我们按照我们刚才的思路使用Z3进行编写:
1.设未知数:
from z3 import * x = Int('x') y = Int('y')
2.列方程:
s = Solver() s.add(x+y==5) s.add(2*x+3*y==14)
3.解方程判断是否有解
if s.check() == sat: result = s.model()
4.输出方程的解,没有解则输出无解
print result else: print '无解'
运行结果如下图所示:求解成功!
可能到了这里大家就会觉得Z3好像也没啥方便的啊,这样的算法我列方程也能很快解出来啊。下面我再为大家演示一道题目,这道题是我学Z3的时候看到的一道公务员考试题目:
这个问题的逻辑比较复杂,比较绕,我们使用Z3来进行以下求解,同样我们也使用上面的解决步骤来:
我们设
a:2014年小李的年龄
b:小李弟弟的年龄
c:小王的年龄
d:小王哥哥的年龄
源码及运行结果如下:
可以看到我们使用Z3求解此类问题还是挺简单的,如果我们手动列方程可能就要计算4个方程了。
Z3在CTF逆向中实战应用
因为前面举的例子都太简单,大家想看一下在CTF实战中应用Z3的例子,下面就以Reversing.kr网站中的一道题目为例,给大家演示以下在实际CTF逆向中使用Z3解题。题目链接:https://pan.baidu.com/s/139KWNuICLpwnFOKyTiQHUg 提取码:iqfq
0x1做题前的信息搜集
打开后题目是这样的,简单来说就是逆向出当Serial为' 76876-77776 '时,Name的值为多少?而且给你了提示,也就是Name是4个字节,最后一个字节为' p '。
根据exeinfoPE显示信息可知程序为MFC程序,无壳。有了这些信息以后我们就可以进行分析了。
0x2找关键函数
因为根据我们打开程序后程序的运行情况可以知道,程序为MFC编写,而且并无按钮,但是有输入框,输入框的内容是实时监测的,如果你输入错误的Name会显示Wrong。那么我们就可以根据这个特性来下获取文本输入框内容的API断点也就是GetWindowTextW。我们在OD中下API断点->bp GetWindowTextW回车后 F9运行程序,程序会断在下图位置。
然后在上图中框选的地方进行栈回溯,到达此处,根据地址可知此处不是关键函数的位置(这里是系统函数的位置)我们需要继续回溯,所以在函数开始的位置(78BA3C63)处使用F2下断点,F9继续运行。
断下来后继续栈回溯会跳到这个函数中,函数开始的位置为(009B1740),分析可知此函数即为关键函数。
我们看一下程序的加载基址为009B0000,所以函数在IDA中的偏移也应该为009B1740-009B0000=1740。
我们使用IDA打开此程序,找到偏移为1740的函数即为sub_401740,然后F5分析此函数。
分析后此函数的伪代码如下:
signed int __stdcall sub_401740(int a1) { int v1; // edi int v3; // esi int v4; // esi __int16 v5; // bx unsigned __int8 v6; // al unsigned __int8 v7; // ST2C_1 unsigned __int8 v8; // al unsigned __int8 v9; // bl wchar_t *v10; // eax __int16 v11; // di wchar_t *v12; // eax __int16 v13; // di wchar_t *v14; // eax __int16 v15; // di wchar_t *v16; // eax __int16 v17; // di wchar_t *v18; // eax __int16 v19; // di unsigned __int8 v20; // al unsigned __int8 v21; // ST2C_1 unsigned __int8 v22; // al unsigned __int8 v23; // bl wchar_t *v24; // eax __int16 v25; // di wchar_t *v26; // eax __int16 v27; // di wchar_t *v28; // eax __int16 v29; // di wchar_t *v30; // eax __int16 v31; // di wchar_t *v32; // eax __int16 v33; // si unsigned __int8 v34; // [esp+10h] [ebp-28h] unsigned __int8 v35; // [esp+10h] [ebp-28h] unsigned __int8 v36; // [esp+11h] [ebp-27h] unsigned __int8 v37; // [esp+11h] [ebp-27h] unsigned __int8 v38; // [esp+13h] [ebp-25h] unsigned __int8 v39; // [esp+13h] [ebp-25h] unsigned __int8 v40; // [esp+14h] [ebp-24h] unsigned __int8 v41; // [esp+14h] [ebp-24h] unsigned __int8 v42; // [esp+19h] [ebp-1Fh] unsigned __int8 v43; // [esp+19h] [ebp-1Fh] unsigned __int8 v44; // [esp+1Ah] [ebp-1Eh] unsigned __int8 v45; // [esp+1Ah] [ebp-1Eh] unsigned __int8 v46; // [esp+1Bh] [ebp-1Dh] unsigned __int8 v47; // [esp+1Bh] [ebp-1Dh] unsigned __int8 v48; // [esp+1Ch] [ebp-1Ch] unsigned __int8 v49; // [esp+1Ch] [ebp-1Ch] int v50; // [esp+20h] [ebp-18h] int v51; // [esp+24h] [ebp-14h] char v52; // [esp+28h] [ebp-10h] int v53; // [esp+34h] [ebp-4h] ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v50); v1 = 0; v53 = 0; ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v51); ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v52); LOBYTE(v53) = 2; CWnd::GetWindowTextW(a1 + 304, &v50); if ( *(_DWORD *)(v50 - 12) == 4 ) { v3 = 0; while ( (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, v3) >= 0x61u && (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, v3) <= 0x7Au ) { if ( ++v3 >= 4 ) { LABEL_7: v4 = 0; while ( 1 ) { if ( v1 != v4 ) { v5 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, v4); if ( (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, v1) == v5 ) goto LABEL_2; } if ( ++v4 >= 4 ) { if ( ++v1 < 4 ) goto LABEL_7; CWnd::GetWindowTextW(a1 + 420, &v51); if ( *(_DWORD *)(v51 - 12) == 11 && (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 5) == 45 ) { v6 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, 0); v7 = (v6 & 1) + 5; v48 = ((v6 >> 4) & 1) + 5; v42 = ((v6 >> 1) & 1) + 5; v44 = ((v6 >> 2) & 1) + 5; v46 = ((v6 >> 3) & 1) + 5; v8 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, 1); v34 = (v8 & 1) + 1; v40 = ((v8 >> 4) & 1) + 1; v36 = ((v8 >> 1) & 1) + 1; v9 = ((v8 >> 2) & 1) + 1; v38 = ((v8 >> 3) & 1) + 1; v10 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v7 + v9, v10, 0xAu, 10); v11 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0); if ( (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 0) == v11 ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); v12 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v46 + v38, v12, 0xAu, 10); v13 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 1); if ( v13 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); v14 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v42 + v40, v14, 0xAu, 10); v15 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 2); if ( v15 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); v16 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v44 + v34, v16, 0xAu, 10); v17 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 3); if ( v17 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); v18 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v48 + v36, v18, 0xAu, 10); v19 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 4); if ( v19 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); v20 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, 2); v21 = (v20 & 1) + 5; v49 = ((v20 >> 4) & 1) + 5; v43 = ((v20 >> 1) & 1) + 5; v45 = ((v20 >> 2) & 1) + 5; v47 = ((v20 >> 3) & 1) + 5; v22 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, 3); v35 = (v22 & 1) + 1; v41 = ((v22 >> 4) & 1) + 1; v37 = ((v22 >> 1) & 1) + 1; v23 = ((v22 >> 2) & 1) + 1; v39 = ((v22 >> 3) & 1) + 1; v24 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v21 + v23, v24, 0xAu, 10); v25 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 6); if ( v25 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); v26 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v47 + v39, v26, 0xAu, 10); v27 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 7); if ( v27 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); v28 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v43 + v41, v28, 0xAu, 10); v29 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 8); if ( v29 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); v30 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v45 + v35, v30, 0xAu, 10); v31 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 9); if ( v31 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); v32 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52); itow_s(v49 + v37, v32, 0xAu, 10); v33 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 10); if ( v33 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) ) { ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1); ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v52); ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v51); ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v50); return 1; } } } } } } } } } } } goto LABEL_2; } } } } } LABEL_2: ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v52); ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v51); ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v50); return 0; }
0x3分析关键函数
我们根据下图所示可知,Name的取值可能为a到z之间的所有字母。
分析发现函数中下图(&v51,5)判断第5位运算结果是否是' - ',和题目要求中是一样的。
还存在10个判断方程,猜测就是判断其余剩下的那10位数字。
因为伪代码中使用了itow_s将运算值取最高位与反回的ASC码比较,根据GetAt()函数和ASC码表排布
那10个判断方程我们可以写成下面约束条件 PS:ord('7')-0x30就是7
((name[0]&1)+5+(((name[1]>>2) & 1 )+1))==ord('7')-0x30 ((((name[0]>>3) & 1)+5)+(((name[1]>>3)&1)+1))==ord('6')-0x30 (((name[0]>>1) & 1)+5+(((name[1]>>4) & 1 )+1))==ord('8')-0x30 (((name[0]>>2) & 1)+5+(((name[1]) & 1 )+1))==ord('7')-0x30 (((name[0]>>4) & 1)+5+(((name[1]>>1) & 1 )+1))==ord('6')-0x30 (((name[2]) & 1)+5+(((name[3]>>2) & 1 )+1))==ord('7')-0x30 (((name[2]>>3) & 1)+5+(((name[3]>>3) & 1 )+1))==ord('7')-0x30 (((name[2]>>1) & 1)+5+(((name[3]>>4) & 1 )+1))==ord('7')-0x30 (((name[2]>>2) & 1)+5+(((name[3]) & 1 )+1))==ord('7')-0x30 (((name[2]>>4) & 1)+5+(((name[3]>>1) & 1 )+1))==ord('6')-0x30
0x4编写获取flag脚本
我们梳理一下我们分析后的内容结合题目提示得:
1.Name由4个字节组成,最后一个为p,其余3个的取值范围为a-z。
2.满足那10个方程运算结果。
然后我们编写脚本:
from z3 import * name= [BitVec('u%d'%i,8) for i in range(0,4)] solver = Solver() #check '76876' '77776' solver.add(((name[0]&1)+5+(((name[1]>>2) & 1 )+1))==ord('7')-0x30) solver.add(((((name[0]>>3) & 1)+5)+(((name[1]>>3)&1)+1))==ord('6')-0x30) solver.add((((name[0]>>1) & 1)+5+(((name[1]>>4) & 1 )+1))==ord('8')-0x30) solver.add((((name[0]>>2) & 1)+5+(((name[1]) & 1 )+1))==ord('7')-0x30) solver.add((((name[0]>>4) & 1)+5+(((name[1]>>1) & 1 )+1))==ord('6')-0x30) solver.add((((name[2]) & 1)+5+(((name[3]>>2) & 1 )+1))==ord('7')-0x30) solver.add((((name[2]>>3) & 1)+5+(((name[3]>>3) & 1 )+1))==ord('7')-0x30) solver.add((((name[2]>>1) & 1)+5+(((name[3]>>4) & 1 )+1))==ord('7')-0x30) solver.add((((name[2]>>2) & 1)+5+(((name[3]) & 1 )+1))==ord('7')-0x30) solver.add((((name[2]>>4) & 1)+5+(((name[3]>>1) & 1 )+1))==ord('6')-0x30) solver.add(name[3] == ord('p')) for i in range(0,4): solver.add(name[i] >= ord('a')) solver.add(name[i] <= ord('z')) solver.check() result = solver.model() flag = '' for i in range(0,4): flag += chr(result[name[i]].as_long().real) print flag
运行结果为 bump我们输入测试一下,成功!!
小结
其实CTF逆向中还有许许多多的小工具或小套路,我们需要在实战中去积累,去学习。在此感谢看雪无名侠提供CTF题目附件和解题思路。
参考资料:https://bbs.pediy.com/thread-224452.htm
关注我们
Tide安全团队正式成立于2019年1月,是新潮信息旗下以互联网攻防技术研究为目标的安全团队,目前聚集了十多位专业的安全攻防技术研究人员,专注于网络攻防、Web安全、移动终端、安全开发、IoT/物联网/工控安全等方向。
想了解更多Tide安全团队,请关注团队官网: http://www.TideSec.com 或长按二维码关注公众号: