z3约束求解器使用_plz input your flag-程序员宅基地
Z3的使用
z3作为一种约束求解器，在CTF中可以用来解一些密码学，二进制逆向等问题。本文简单的介绍了z3的安装，用法，并且通过一个逆向题目来具体实践一下。
安装
pip install z3-solver
用法
1.声明变量
z3中有3中类型的变量，分别是整型(Int),实型(Real)和向量(BitVec)
Int-整数型
from z3 import *
a = Int('a')#声明单个整型变量
a,b = Ints('a b')#声明多个整型变量
Real-实数型
from z3 import *
a = Real('a')#声明单个实型变量
a,b = Reals('a b')#声明多个实型变量
BitVec-向量
from z3 import *
a = BitVec('a',8) #声明单个8位的变量
a, b = BitVec('a b',8)#声明多个8位的变量
2.常规使用
from z3 import *
a,b = Ints('a b')
solve(a>3,b<8,2*a+b==16)
#结果 [a = 5, b = 6]
3.约束求解器
在解决问题是很多情况下是有多个约束条件的。这个时候可以先生成一个求解器对象(Solver())，然后就可以方便的向其中添加更多的约束条件。
#!/usr/bin/python3
#-*- coding=utf-8 -*-
from z3 import *
a,b = Ints('a b')
solver = Solver()#创建一个求解器对象
solver.add(a+b==10)#用add方法添加约束条件
solver.add(a-b==6)
if solver.check() == sat: #check()方法用来判断是否有解，sat(satisify)表示满足有解
ans = solver.model() #model()方法得到解
print(ans)
#也可以用变量名作为下标得到解
print(ans[a])
else:
print("no ans!")
更多用法参考官方文档：
https://rise4fun.com/z3/tutorialcontent/guide
实例
这是第十三届全国大学生网络安全预选赛的一道逆向题，题目链接如下：
链接：https://pan.baidu.com/s/1srNNrt8l3qsMt4cP1OM11Q
提取码：j6c9
用IDA打开：
选中main函数，按F5反汇编，得到如下反汇编代码：
// local variable allocation has failed, the output may be wrong!
int __cdecl main(int argc, const char **argv, const char **envp)
{
......
_main(*(_QWORD *)&argc, argv, envp);
memcpy(Dst, &unk_404020, 0xA8ui64);
printf("plz input your flag:");
scanf("%42s", &v46);
v4 = 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52;
v5 = 27 * v50 + 73 * v49 + 12 * v48 + 83 * v46 + 85 * v47 + 96 * v51 + 52 * v52;
v6 = 24 * v48 + 78 * v46 + 53 * v47 + 36 * v49 + 86 * v50 + 25 * v51 + 46 * v52;
v7 = 78 * v47 + 39 * v46 + 52 * v48 + 9 * v49 + 62 * v50 + 37 * v51 + 84 * v52;
v8 = 48 * v50 + 14 * v48 + 23 * v46 + 6 * v47 + 74 * v49 + 12 * v51 + 83 * v52;
v9 = 15 * v51 + 48 * v50 + 92 * v48 + 85 * v47 + 27 * v46 + 42 * v49 + 72 * v52;
v10 = 26 * v51 + 67 * v49 + 6 * v47 + 4 * v46 + 3 * v48 + 68 * v52;
v11 = 34 * v56 + 12 * v53 + 53 * v54 + 6 * v55 + 58 * v57 + 36 * v58 + v59;
v12 = 27 * v57 + 73 * v56 + 12 * v55 + 83 * v53 + 85 * v54 + 96 * v58 + 52 * v59;
v13 = 24 * v55 + 78 * v53 + 53 * v54 + 36 * v56 + 86 * v57 + 25 * v58 + 46 * v59;
v14 = 78 * v54 + 39 * v53 + 52 * v55 + 9 * v56 + 62 * v57 + 37 * v58 + 84 * v59;
v15 = 48 * v57 + 14 * v55 + 23 * v53 + 6 * v54 + 74 * v56 + 12 * v58 + 83 * v59;
v16 = 15 * v58 + 48 * v57 + 92 * v55 + 85 * v54 + 27 * v53 + 42 * v56 + 72 * v59;
v17 = 26 * v58 + 67 * v56 + 6 * v54 + 4 * v53 + 3 * v55 + 68 * v59;
v18 = 34 * v63 + 12 * v60 + 53 * v61 + 6 * v62 + 58 * v64 + 36 * v65 + v66;
v19 = 27 * v64 + 73 * v63 + 12 * v62 + 83 * v60 + 85 * v61 + 96 * v65 + 52 * v66;
v20 = 24 * v62 + 78 * v60 + 53 * v61 + 36 * v63 + 86 * v64 + 25 * v65 + 46 * v66;
v21 = 78 * v61 + 39 * v60 + 52 * v62 + 9 * v63 + 62 * v64 + 37 * v65 + 84 * v66;
v22 = 48 * v64 + 14 * v62 + 23 * v60 + 6 * v61 + 74 * v63 + 12 * v65 + 83 * v66;
v23 = 15 * v65 + 48 * v64 + 92 * v62 + 85 * v61 + 27 * v60 + 42 * v63 + 72 * v66;
v24 = 26 * v65 + 67 * v63 + 6 * v61 + 4 * v60 + 3 * v62 + 68 * v66;
v25 = 34 * v70 + 12 * v67 + 53 * v68 + 6 * v69 + 58 * v71 + 36 * v72 + v73;
v26 = 27 * v71 + 73 * v70 + 12 * v69 + 83 * v67 + 85 * v68 + 96 * v72 + 52 * v73;
v27 = 24 * v69 + 78 * v67 + 53 * v68 + 36 * v70 + 86 * v71 + 25 * v72 + 46 * v73;
v28 = 78 * v68 + 39 * v67 + 52 * v69 + 9 * v70 + 62 * v71 + 37 * v72 + 84 * v73;
v29 = 48 * v71 + 14 * v69 + 23 * v67 + 6 * v68 + 74 * v70 + 12 * v72 + 83 * v73;
v30 = 15 * v72 + 48 * v71 + 92 * v69 + 85 * v68 + 27 * v67 + 42 * v70 + 72 * v73;
v31 = 26 * v72 + 67 * v70 + 6 * v68 + 4 * v67 + 3 * v69 + 68 * v73;
v32 = 34 * v77 + 12 * v74 + 53 * v75 + 6 * v76 + 58 * v78 + 36 * v79 + v80;
v33 = 27 * v78 + 73 * v77 + 12 * v76 + 83 * v74 + 85 * v75 + 96 * v79 + 52 * v80;
v34 = 24 * v76 + 78 * v74 + 53 * v75 + 36 * v77 + 86 * v78 + 25 * v79 + 46 * v80;
v35 = 78 * v75 + 39 * v74 + 52 * v76 + 9 * v77 + 62 * v78 + 37 * v79 + 84 * v80;
v36 = 48 * v78 + 14 * v76 + 23 * v74 + 6 * v75 + 74 * v77 + 12 * v79 + 83 * v80;
v37 = 15 * v79 + 48 * v78 + 92 * v76 + 85 * v75 + 27 * v74 + 42 * v77 + 72 * v80;
v38 = 26 * v79 + 67 * v77 + 6 * v75 + 4 * v74 + 3 * v76 + 68 * v80;
v39 = 34 * v84 + 12 * v81 + 53 * v82 + 6 * v83 + 58 * v85 + 36 * v86 + v87;
v40 = 27 * v85 + 73 * v84 + 12 * v83 + 83 * v81 + 85 * v82 + 96 * v86 + 52 * v87;
v41 = 24 * v83 + 78 * v81 + 53 * v82 + 36 * v84 + 86 * v85 + 25 * v86 + 46 * v87;
v42 = 78 * v82 + 39 * v81 + 52 * v83 + 9 * v84 + 62 * v85 + 37 * v86 + 84 * v87;
v43 = 48 * v85 + 14 * v83 + 23 * v81 + 6 * v82 + 74 * v84 + 12 * v86 + 83 * v87;
v44 = 15 * v86 + 48 * v85 + 92 * v83 + 85 * v82 + 27 * v81 + 42 * v84 + 72 * v87;
v45 = 26 * v86 + 67 * v84 + 6 * v82 + 4 * v81 + 3 * v83 + 68 * v87;
for ( i = 0; i <= 41; ++i )
{
if ( *(&v4 + i) != Dst[i] )
{
printf("error");
exit(0);
}
}
printf("win");
return 0;
}
分析程序可知输入的就是flag,并且flag是42个字符。这里关键点是看for循化中的if比较条件。可以发现需要v4-v45的值要分别和Dst[0]~Dst[41]的值分别相等，才能够得到正确答案。
这里需要注意源码中的：
memcpy(Dst, &unk_404020, 0xA8ui64);
memcpy函数的原型是 ：void *memcpy(void *str1, const void *str2, size_t n)
将str指向的数据复制大小为n个字节到目标数组str1中。在ida中跟进&unk_404020,可以发现对应的Dst[i]中的值：
(注意：这里数组类型是int型，对于64位的程序，也就是占4个字节。又因为是小端存储，因此Dst[0]的值应该是0x4F17,后面依次类推，可以得到完整的Dst数组)。然后可以写对应的脚本：
#!/usr/bin/env python3
#-*- coding=utf-8 -*-
from z3 import *
s = Solver()
v46,v47,v48,v49,v50,v51,v52,v53,v54 = Ints("v46 v47 v48 v49 v50 v51 v52 v53 v54")
v55,v56,v57,v58,v59,v60,v61,v62,v63 = Ints("v55 v56 v57 v58 v59 v60 v61 v62 v63")
v64,v65,v66,v67,v68,v69,v70,v71,v72 = Ints("v64 v65 v66 v67 v68 v69 v70 v71 v72")
v73,v74,v75,v76,v77,v78,v79,v80,v81 = Ints("v73 v74 v75 v76 v77 v78 v79 v80 v81")
v82,v83,v84,v85,v86,v87 = Ints("v82 v83 v84 v85 v86 v87")
s.add(0x4F17 == 34*v49+12*v46+53*v47+6*v48+58*v50+36*v51+v52)
s.add(0x9CF6 == 27*v50+73*v49+12*v48+83*v46+85*v47+96*v51+52*v52)
s.add(0x8DDB == 24*v48+78*v46+53*v47+36*v49+86*v50+25*v51+46*v52)
s.add(0x8EA6 == 78*v47+39*v46+52*v48+9*v49+62*v50+37*v51+84*v52)
s.add(0x6929 == 48*v50+14*v48+23*v46+6*v47+74*v49+12*v51+83*v52)
s.add(0x9911 == 15*v51+48*v50+92*v48+85*v47+27*v46+42*v49+72*v52)
s.add(0x40A2 == 26*v51+67*v49+6*v47+4*v46+3*v48+68*v52)
s.add(0x2F3E == 34*v56+12*v53+53*v54+6*v55+58*v57+36*v58+v59)
s.add(0x62B6 == 27*v57+73*v56+12*v55+83*v53+85*v54+96*v58+52*v59)
s.add(0x4B82 == 24*v55+78*v53+53*v54+36*v56+86*v57+25*v58+46*v59)
s.add(0x486C == 78*v54+39*v53+52*v55+9*v56+62*v57+37*v58+84*v59)
s.add(0x4002 == 48*v57+14*v55+23*v53+6*v54+74*v56+12*v58+83*v59)
s.add(0x52D7 == 15*v58+48*v57+92*v55+85*v54+27*v53+42*v56+72*v59)
s.add(0x2DEF == 26*v58+67*v56+6*v54+4*v53+3*v55+68*v59)
s.add(0x28DC == 34*v63+12*v60+53*v61+6*v62+58*v64+36*v65+v66)
s.add(0x640D == 27*v64+73*v63+12*v62+83*v60+85*v61+96*v65+52*v66)
s.add(0x528F == 24*v62+78*v60+53*v61+36*v63+86*v64+25*v65+46*v66)
s.add(0x613B == 78*v61+39*v60+52*v62+9*v63+62*v64+37*v65+84*v66)
s.add(0x4781 == 48*v64+14*v62+23*v60+6*v61+74*v63+12*v65+83*v66)
s.add(0x6B17 == 15*v65+48*v64+92*v62+85*v61+27*v60+42*v63+72*v66)
s.add(0x3237 == 26*v65+67*v63+6*v61+4*v60+3*v62+68*v66)
s.add(0x2A93 == 34*v70+12*v67+53*v68+6*v69+58*v71+36*v72+v73)
s.add(0x615F == 27*v71+73*v70+12*v69+83*v67+85*v68+96*v72+52*v73)
s.add(0x50BE == 24*v69+78*v67+53*v68+36*v70+86*v71+25*v72+46*v73)
s.add(0x598E == 78*v68+39*v67+52*v69+9*v70+62*v71+37*v72+84*v73)
s.add(0x4656 == 48*v71+14*v69+23*v67+6*v68+74*v70+12*v72+83*v73)
s.add(0x5B31 == 15*v72+48*v71+92*v69+85*v68+27*v67+42*v70+72*v73)
s.add(0x313A == 26*v72+67*v70+6*v68+4*v67+3*v69+68*v73)
s.add(0x3010 == 34*v77+12*v74+53*v75+6*v76+58*v78+36*v79+v80)
s.add(0x67FE == 27*v78+73*v77+12*v76+83*v74+85*v75+96*v79+52*v80)
s.add(0x4D5F == 24*v76+78*v74+53*v75+36*v77+86*v78+25*v79+46*v80)
s.add(0x58DB == 78*v75+39*v74+52*v76+9*v77+62*v78+37*v79+84*v80)
s.add(0x3799 == 48*v78+14*v76+23*v74+6*v75+74*v77+12*v79+83*v80)
s.add(0x60A0 == 15*v79+48*v78+92*v76+85*v75+27*v74+42*v77+72*v80)
s.add(0x2750 == 26*v79+67*v77+6*v75+4*v74+3*v76+68*v80)
s.add(0x3759 == 34*v84+12*v81+53*v82+6*v83+58*v85+36*v86+v87)
s.add(0x8953 == 27*v85+73*v84+12*v83+83*v81+85*v82+96*v86+52*v87)
s.add(0x7122 == 24*v83+78*v81+53*v82+36*v84+86*v85+25*v86+46*v87)
s.add(0x81F9 == 78*v82+39*v81+52*v83+9*v84+62*v85+37*v86+84*v87)
s.add(0x5524 == 48*v85+14*v83+23*v81+6*v82+74*v84+12*v86+83*v87)
s.add(0x8971 == 15*v86+48*v85+92*v83+85*v82+27*v81+42*v84+72*v87)
s.add(0x3A1D == 26*v86+67*v84+6*v82+4*v81+3*v83+68*v87)
flag = []
if s.check() == sat:
ans = s.model()
flag.append(ans[v46])
flag.append(ans[v47])
flag.append(ans[v48])
flag.append(ans[v49])
flag.append(ans[v50])
flag.append(ans[v51])
flag.append(ans[v52])
flag.append(ans[v53])
flag.append(ans[v54])
flag.append(ans[v55])
flag.append(ans[v56])
flag.append(ans[v57])
flag.append(ans[v58])
flag.append(ans[v59])
flag.append(ans[v60])
flag.append(ans[v61])
flag.append(ans[v62])
flag.append(ans[v63])
flag.append(ans[v64])
flag.append(ans[v65])
flag.append(ans[v66])
flag.append(ans[v67])
flag.append(ans[v68])
flag.append(ans[v69])
flag.append(ans[v70])
flag.append(ans[v71])
flag.append(ans[v72])
flag.append(ans[v73])
flag.append(ans[v74])
flag.append(ans[v75])
flag.append(ans[v76])
flag.append(ans[v77])
flag.append(ans[v78])
flag.append(ans[v79])
flag.append(ans[v80])
flag.append(ans[v81])
flag.append(ans[v82])
flag.append(ans[v83])
flag.append(ans[v84])
flag.append(ans[v85])
flag.append(ans[v86])
flag.append(ans[v87])
for x in flag:
print(x,end=",")
得到的结果如下：
102,108,97,103,123,55,101,49,55,49,100,52,51,45,54,51,98,57,45,52,101,49,56,45,57,57,48,101,45,54,101,49,52,99,50,97,102,101,54,52,56,125
然后转为ascii编码即可：
#!/usr/bin/python3
s=[102,108,97,103,123,55,101,49,55,49,100,52,51,45,54,51,98,57,45,52,101,49,56,45,57,57,48,101,45,54,101,49,52,99,50,97,102,101,54,52,56,125]
for x in s:
print(chr(x),end="")
#flag{7e171d43-63b9-4e18-990e-6e14c2afe648}
智能推荐
攻防世界_难度8_happy_puzzle_攻防世界困难模式攻略图文-程序员宅基地
文章浏览阅读645次。这个肯定是末尾的IDAT了，因为IDAT必须要满了才会开始一下个IDAT，这个明显就是末尾的IDAT了。，对应下面的create_head()代码。，对应下面的create_tail()代码。不要考虑爆破，我已经试了一下，太多情况了。题目来源：UNCTF。_攻防世界困难模式攻略图文
达梦数据库的导出（备份）、导入_达梦数据库导入导出-程序员宅基地
文章浏览阅读2.9k次，点赞3次，收藏10次。偶尔会用到，记录、分享。1. 数据库导出1.1 切换到dmdba用户su - dmdba1.2 进入达梦数据库安装路径的bin目录，执行导库操作 导出语句：./dexp cwy_init/[email protected]:5236 file=cwy_init.dmp log=cwy_init_exp.log 注释： cwy_init/init_123..._达梦数据库导入导出
js引入kindeditor富文本编辑器的使用_kindeditor.js-程序员宅基地
文章浏览阅读1.9k次。1. 在官网上下载KindEditor文件，可以删掉不需要要到的jsp，asp，asp.net和php文件夹。接着把文件夹放到项目文件目录下。2. 修改html文件，在页面引入js文件：<script type="text/javascript" src="./kindeditor/kindeditor-all.js"></script><script type="text/javascript" src="./kindeditor/lang/zh-CN.js"_kindeditor.js
STM32学习过程记录11——基于STM32G431CBU6硬件SPI+DMA的高效WS2812B控制方法-程序员宅基地
文章浏览阅读2.3k次，点赞6次，收藏14次。SPI的详情简介不必赘述。假设我们通过SPI发送0xAA，我们的数据线就会变为10101010，通过修改不同的内容，即可修改SPI中0和1的持续时间。比如0xF0即为前半周期为高电平，后半周期为低电平的状态。在SPI的通信模式中，CPHA配置会影响该实验，下图展示了不同采样位置的SPI时序图[1]。CPOL = 0，CPHA = 1：CLK空闲状态 = 低电平，数据在下降沿采样，并在上升沿移出CPOL = 0，CPHA = 0：CLK空闲状态 = 低电平，数据在上升沿采样，并在下降沿移出。_stm32g431cbu6
计算机网络-数据链路层_接收方收到链路层数据后,使用crc检验后,余数为0,说明链路层的传输时可靠传输-程序员宅基地
文章浏览阅读1.2k次，点赞2次，收藏8次。数据链路层习题自测问题1.数据链路(即逻辑链路)与链路(即物理链路)有何区别?“电路接通了”与”数据链路接通了”的区别何在?2.数据链路层中的链路控制包括哪些功能?试讨论数据链路层做成可靠的链路层有哪些优点和缺点。3.网络适配器的作用是什么?网络适配器工作在哪一层?4.数据链路层的三个基本问题(帧定界、透明传输和差错检测)为什么都必须加以解决？5.如果在数据链路层不进行帧定界，会发生什么问题？6.PPP协议的主要特点是什么？为什么PPP不使用帧的编号？PPP适用于什么情况？为什么PPP协议不_接收方收到链路层数据后,使用crc检验后,余数为0,说明链路层的传输时可靠传输
软件测试工程师移民加拿大_无证移民，未受过软件工程师的教育（第1部分）-程序员宅基地
文章浏览阅读587次。软件测试工程师移民加拿大 无证移民，未受过软件工程师的教育(第1部分) (Undocumented Immigrant With No Education to Software Engineer(Part 1))Before I start, I want you to please bear with me on the way I write, I have very little gen...
随便推点
Thinkpad X250 secure boot failed 启动失败问题解决_安装完系统提示secureboot failure-程序员宅基地
文章浏览阅读304次。Thinkpad X250笔记本电脑，装的是FreeBSD，进入BIOS修改虚拟化配置（其后可能是误设置了安全开机），保存退出后系统无法启动，显示：secure boot failed ，把自己惊出一身冷汗，因为这台笔记本刚好还没开始做备份.....根据错误提示，到bios里面去找相关配置，在Security里面找到了Secure Boot选项，发现果然被设置为Enabled，将其修改为Disabled ，再开机，终于正常启动了。_安装完系统提示secureboot failure
C++如何做字符串分割（5种方法）_c++ 字符串分割-程序员宅基地
文章浏览阅读10w+次，点赞93次，收藏352次。1、用strtok函数进行字符串分割原型： char *strtok(char *str, const char *delim);功能：分解字符串为一组字符串。参数说明：str为要分解的字符串，delim为分隔符字符串。返回值：从str开头开始的一个个被分割的串。当没有被分割的串时则返回NULL。其它：strtok函数线程不安全，可以使用strtok_r替代。示例：//借助strtok实现split#include <string.h>#include <stdio.h&_c++ 字符串分割
2013第四届蓝桥杯 C/C++本科A组 真题答案解析_2013年第四届c a组蓝桥杯省赛真题解答-程序员宅基地
文章浏览阅读2.3k次。1 .高斯日记 大数学家高斯有个好习惯：无论如何都要记日记。他的日记有个与众不同的地方，他从不注明年月日，而是用一个整数代替，比如：4210后来人们知道，那个整数就是日期，它表示那一天是高斯出生后的第几天。这或许也是个好习惯，它时时刻刻提醒着主人：日子又过去一天，还有多少时光可以用于浪费呢？高斯出生于：1777年4月30日。在高斯发现的一个重要定理的日记_2013年第四届c a组蓝桥杯省赛真题解答
基于供需算法优化的核极限学习机(KELM)分类算法-程序员宅基地
文章浏览阅读851次，点赞17次，收藏22次。摘要：本文利用供需算法对核极限学习机(KELM)进行优化，并用于分类。
metasploitable2渗透测试_metasploitable2怎么进入-程序员宅基地
文章浏览阅读1.1k次。一、系统弱密码登录1、在kali上执行命令行telnet 192.168.26.1292、Login和password都输入msfadmin3、登录成功，进入系统4、测试如下：二、MySQL弱密码登录：1、在kali上执行mysql –h 192.168.26.129 –u root2、登录成功，进入MySQL系统3、测试效果：三、PostgreSQL弱密码登录1、在Kali上执行psql -h 192.168.26.129 –U post..._metasploitable2怎么进入
Python学习之路：从入门到精通的指南_python人工智能开发从入门到精通pdf-程序员宅基地
文章浏览阅读257次。本文将为初学者提供Python学习的详细指南，从Python的历史、基础语法和数据类型到面向对象编程、模块和库的使用。通过本文，您将能够掌握Python编程的核心概念，为今后的编程学习和实践打下坚实基础。_python人工智能开发从入门到精通pdf