网站建设对公司有什么意义,上海网站排名seo公司哪家好,软件开发定制app,墨西哥网站后缀CTF-reverse中有一类题目是通过约束方程求解变量的值#xff0c;然后转化为对应的ASCII码#xff0c;最终获得flag#xff0c;约束方程以及要求解的未知数往往非常多#xff0c;因此手算十分不现实#xff0c;借助python中的z3模块可以很快完成求解#xff01; 下面是某道… CTF-reverse中有一类题目是通过约束方程求解变量的值然后转化为对应的ASCII码最终获得flag约束方程以及要求解的未知数往往非常多因此手算十分不现实借助python中的z3模块可以很快完成求解 下面是某道CTF-reverse原题的反汇编代码可以看到约束方程非常多要求解的未知数也是多达16个因此本篇用于记录z3求解器脚本方便使用 一例题放送 int __cdecl main(int argc, const char **argv, const char **envp)
{char flag[32]; // [rsp20h] [rbp-60h] BYREFint v5; // [rsp40h] [rbp-40h]int v6; // [rsp44h] [rbp-3Ch]int v7; // [rsp48h] [rbp-38h]int v8; // [rsp4Ch] [rbp-34h]int v9; // [rsp50h] [rbp-30h]int v10; // [rsp54h] [rbp-2Ch]int v11; // [rsp58h] [rbp-28h]int v12; // [rsp5Ch] [rbp-24h]int v13; // [rsp60h] [rbp-20h]int v14; // [rsp64h] [rbp-1Ch]int v15; // [rsp68h] [rbp-18h]int v16; // [rsp6Ch] [rbp-14h]int v17; // [rsp70h] [rbp-10h]int v18; // [rsp74h] [rbp-Ch]int v19; // [rsp78h] [rbp-8h]int v20; // [rsp7Ch] [rbp-4h]_main(argc, argv, envp);printf(Please input your flag: );scanf(%s, flag);v20 flag[0];v19 flag[1];v18 flag[2];v17 flag[3];v16 flag[4];v15 flag[5];v14 flag[6];v13 flag[7];v12 flag[8];v11 flag[9];v10 flag[10];v9 flag[11];v8 flag[12];v7 flag[13];v6 flag[14];v5 flag[15];if ( 7 * flag[0] 546 // flag[0]78 2 * v19 166 // v1983 6 * v18 v17 7 * v15 1055 2 * v7 v12 7 * v15 v17 4 * v19 4 * v16 6 * v13 8 * v5 3107 4 * v16 336 // v1684 2 * v19 7 * v15 656 // v1570 2 * v7 3 * v9 3 * v14 6 * v13 v12 5 * v11 16 * v10 6 * v8 8 * v5 5749 6 * v13 606 // v13101 5 * v6 v12 652 // v1252 5 * v11 16 * v10 6 * v8 3213 2 * v7 3 * v9 24 * v10 5 * v11 3 * v14 6 * v13 v12 6 * v8 8 * v5 6717 3 * v9 285 // v995 2 * v12 3 * v14 6 * v13 8 * v10 6 * v8 2 * v7 5 * v6 8 * v5 4573 5 * v6 600 // v6120 v17 6 * v18 4 * v16 7 * v15 2 * v7 1615 v12 7 * v15 2 * v19 6 * v13 8 * v5 2314 )// v5125{puts(Success);system(pause);}else{puts(Wrong);system(pause);}return 0;
} 二解决本题的完整脚本 下面是完整脚本想节省时间不看解释的可以直接取走用 from z3 import *#创建未知数变量
v [Int(fv{i}) for i in range(0, 16)]#创建解释器对象
solver Solver()#创建一个求解器对象#添加约束方程
solver.add(v[0] * 7 546)
solver.add(v[1] * 2 166)
solver.add(v[2] * 6 v[3] * 1 v[5] * 7 1055)
solver.add(v[1] * 4 v[3] v[4] * 4 v[5] * 7 v[7] * 6 v[8] * 1 v[13] * 2 v[15] * 8 3107)
solver.add(v[4] * 4 336)
solver.add(v[1] * 2 v[5] * 7 656)
solver.add(v[6] * 3 v[7] * 6 v[8] v[9] * 5 v[10] * 16 v[11] * 3 v[12] * 6 v[13] * 2 v[15] * 8 5749)
solver.add(v[7] * 6 606)
solver.add(v[8] v[14] * 5 652)
solver.add(v[9] * 5 v[10] * 16 v[12] * 6 3213)
solver.add(v[6] * 3 v[7] * 6 v[8] v[9] * 5 v[10] * 24 v[11] * 3 v[12] * 6 v[13] * 2 v[15] * 8 6717)
solver.add(v[11] * 3 285)
solver.add(v[6] * 3 v[7] * 6 v[8] * 2 v[10] * 8 v[12] * 6 v[13] * 2 v[14] * 5 v[15] * 8 4573)
solver.add(v[14] * 5 600)
solver.add(v[2] * 6 v[3] * 1 v[4] * 4 v[5] * 7 v[13] * 2 1615)
solver.add(v[1] * 2 v[5] * 7 v[7] * 6 v[8] * 1 v[15] * 8 2314)#求解并转化为字符输出得到flag
if solver.check() sat: #check()方法用来判断是否有解sat(即satisify)表示满足有解ans solver.model() #model()方法得到解for i in v:print(chr(ans[i].as_long()), end)
#一般不会无解如果无解八成是未知数变量的类型不符合或约束方程添加错误
else:print(no ans!)三脚本详解 一导入z3库 这步看似就是简简单单的一个倒库操作但也能硬控一大片萌新很长时间比如蒟蒻博主/(ㄒoㄒ)/~~ 因为第一次用z3所以这个库理所当然是不存在的要先下载但是用【pip install z3】命令下载的库是不对的能下载但下载的不对而要用【pip install z3-solver】具体见本篇-Windows下安装z3python3_z3-py3-whl csdn-CSDN博客 而且下载好后也不能用【import z3】这种导入方式而要用下面代码块的这种具体原因未知 from z3 import * 二 创建未知数变量 未知数变量即方程中的未知数必须主动提供给z3求解器如果是比较简单的、只有几个参数的方程可以直接手动列出如下图所示注意逐个列出时使用Int()一次全部列出使用Ints() 如果参数较多则建议使用循环 当然博主建议都用循环直接硬套下面这行代码来创建变量 其中 【for i in range(0, 16)】的含义是产生值为0到15的i 【fv{i}】表示格式化字符串结果显然为[v0, v1, v2 ... v15] 这里最后还有一步操作很关键【Int()】是z3中用于将变量转换为特定类型的一个函数转换后的结果显然为[v0, v1, v2 ... v15]这步转换是不可或缺的只有转为z3中的特定整数类型变量后它们才能作为之后的约束方程中的变量来使用 v [Int(fv{i}) for i in range(0, 16)] 三创建解释器对象 这一步是最好理解的就是实例化了z3中的一个Solver类对象以方便后续调用其成员函数当然如果你没有面向对象程序的经验可能查阅资料需要稍作理解 solver Solver() 四添加约束方程 这一步也很好理解直接调用Solver类的成员函数add()将题目给出的所有约束方程添加即可每个方程都要添加注意不要遗漏 solver.add(v[0] * 7 546)
solver.add(v[1] * 2 166)
solver.add(v[2] * 6 v[3] * 1 v[5] * 7 1055)
solver.add(v[1] * 4 v[3] v[4] * 4 v[5] * 7 v[7] * 6 v[8] * 1 v[13] * 2 v[15] * 8 3107)
solver.add(v[4] * 4 336)
solver.add(v[1] * 2 v[5] * 7 656)
solver.add(v[6] * 3 v[7] * 6 v[8] v[9] * 5 v[10] * 16 v[11] * 3 v[12] * 6 v[13] * 2 v[15] * 8 5749)
solver.add(v[7] * 6 606)
solver.add(v[8] v[14] * 5 652)
solver.add(v[9] * 5 v[10] * 16 v[12] * 6 3213)
solver.add(v[6] * 3 v[7] * 6 v[8] v[9] * 5 v[10] * 24 v[11] * 3 v[12] * 6 v[13] * 2 v[15] * 8 6717)
solver.add(v[11] * 3 285)
solver.add(v[6] * 3 v[7] * 6 v[8] * 2 v[10] * 8 v[12] * 6 v[13] * 2 v[14] * 5 v[15] * 8 4573)
solver.add(v[14] * 5 600)
solver.add(v[2] * 6 v[3] * 1 v[4] * 4 v[5] * 7 v[13] * 2 1615)
solver.add(v[1] * 2 v[5] * 7 v[7] * 6 v[8] * 1 v[15] * 8 2314) 五求解并转化为字符输出得到flag 使用成员函数check()获取返回值判断是否等于satsat是z3模块中的一个常量代表方程组有解 有解情况下使用成员函数model()获取解该函数会返回一个列表列表中的解以键值对的形式存储例如本题的解形式如下 接下来要做的是将解转化为字符但由于该列表中的元素是z3中的特殊类型需要先转换为python中的整数类型才能使用chr()函数转为对应字符 另外需要注意的是该列表求出的解不是按未知参数的名字大小排序的如果直接按列表中的解的顺序转为字符输出flag显然不对 解决办法是循环访问v列表中的[v0, v1, v2 ... v15]将其作为索引去访问ans列表即此处的【ans[i]】然后使用as_long()函数将解的类型转为python中的int类型最后使用chr()函数转为对应字符 if solver.check() sat: #check()方法用来判断是否有解sat(即satisify)表示满足有解ans solver.model() #model()方法得到解for i in v:print(chr(ans[i].as_long()), end)
#一般不会无解如果无解八成是未知数变量的类型不符合或约束方程添加错误
else:print(no ans!)
