z3求解器脚本(CTF-reverse必备)

CTF-reverse中有一类题目是通过约束方程求解变量的值,然后转化为对应的ASCII码,最终获得flag,约束方程以及要求解的未知数往往非常多,因此手算十分不现实,借助python中的z3模块可以很快完成求解!

下面是某道CTF-reverse原题的反汇编代码,可以看到约束方程非常多,要求解的未知数也是多达16个,因此本篇用于记录z3求解器脚本方便使用

一,例题放送

int __cdecl main(int argc, const char **argv, const char **envp)
{char flag[32]; // [rsp+20h] [rbp-60h] BYREFint v5; // [rsp+40h] [rbp-40h]int v6; // [rsp+44h] [rbp-3Ch]int v7; // [rsp+48h] [rbp-38h]int v8; // [rsp+4Ch] [rbp-34h]int v9; // [rsp+50h] [rbp-30h]int v10; // [rsp+54h] [rbp-2Ch]int v11; // [rsp+58h] [rbp-28h]int v12; // [rsp+5Ch] [rbp-24h]int v13; // [rsp+60h] [rbp-20h]int v14; // [rsp+64h] [rbp-1Ch]int v15; // [rsp+68h] [rbp-18h]int v16; // [rsp+6Ch] [rbp-14h]int v17; // [rsp+70h] [rbp-10h]int v18; // [rsp+74h] [rbp-Ch]int v19; // [rsp+78h] [rbp-8h]int v20; // [rsp+7Ch] [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                           // v19=83&& 6 * v18 + v17 + 7 * v15 == 1055&& 2 * v7 + v12 + 7 * v15 + v17 + 4 * v19 + 4 * v16 + 6 * v13 + 8 * v5 == 3107&& 4 * v16 == 336                           // v16=84&& 2 * v19 + 7 * v15 == 656                 // v15=70&& 2 * v7 + 3 * v9 + 3 * v14 + 6 * v13 + v12 + 5 * v11 + 16 * v10 + 6 * v8 + 8 * v5 == 5749&& 6 * v13 == 606                           // v13=101&& 5 * v6 + v12 == 652                      // v12=52&& 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                            // v9=95&& 2 * v12 + 3 * v14 + 6 * v13 + 8 * v10 + 6 * v8 + 2 * v7 + 5 * v6 + 8 * v5 == 4573&& 5 * v6 == 600                            // v6=120&& v17 + 6 * v18 + 4 * v16 + 7 * v15 + 2 * v7 == 1615&& v12 + 7 * v15 + 2 * v19 + 6 * v13 + 8 * v5 == 2314 )// v5=125{puts("Success");system("pause");}else{puts("Wrong");system("pause");}return 0;
}


二,解决本题的完整脚本

下面是完整脚本,想节省时间不看解释的可以直接取走用

from z3 import *#创建未知数变量
v = [Int(f'v{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下安装z3(python3_z3-py3-whl csdn-CSDN博客

而且下载好后也不能用【import z3】这种导入方式,而要用下面代码块的这种,具体原因未知

from z3 import *

(二) 创建未知数变量

未知数变量即方程中的未知数,必须主动提供给z3求解器,如果是比较简单的、只有几个参数的方程,可以直接手动列出,如下图所示(注意逐个列出时使用Int(),一次全部列出使用Ints())

如果参数较多,则建议使用循环

当然,博主建议都用循环,直接硬套下面这行代码来创建变量

其中

for i in range(0, 16)】的含义是产生值为0到15的i

f'v{i}'】表示格式化字符串,结果显然为['v0', 'v1', 'v2' ... 'v15']

这里最后还有一步操作很关键,【Int()】是z3中用于将变量转换为特定类型的一个函数,转换后的结果显然为[v0, v1, v2 ... v15],这步转换是不可或缺的,只有转为z3中的特定整数类型变量后,它们才能作为之后的约束方程中的变量来使用

v = [Int(f'v{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()获取返回值,判断是否等于sat(sat是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!")

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.mzph.cn/news/827105.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

开始Java之旅

1.Java语言 java是一门优秀的程序设计语言,并且是一种半编译型,半解释型语言。 Java 语言源于 1991 年 4 月,Sun 公司 James Gosling博士 领导的绿色计划(Green Project) 开始启动,此计划最初的目标是开发一种能够在各种消费性电…

递归的题目

1.一个递归算法必须包括(B)。 A.递归部分 B.终止条件和递归部分 C.循环部分 D.终止条件和循环部分 2.阶乘的递归代码: int func(int i) {if (i > 1)return i * func(i - 1);elsereturn 1; } 求和的递归代码: int f(int n…

【分治算法】Hanoi塔问题Python实现

文章目录 [toc]问题描述Python实现 个人主页:丷从心 系列专栏:Python基础 学习指南:Python学习指南 问题描述 设 a a a、 b b b、 c c c是三个塔座,开始时,在塔座 a a a上有一叠共 n n n个圆盘,这些圆盘…

最新免费 ChatGPT、GPTs、AI换脸(Suno-AI音乐生成大模型)

🔥博客主页:只恨天高 ❤️感谢大家点赞👍收藏⭐评论✍️ ChatGPT3.5、GPT4.0、GPTs、AI绘画相信对大家应该不感到陌生吧?简单来说,GPT-4技术比之前的GPT-3.5相对来说更加智能,会根据用户的要求生成多种内容…

虚良SEO怎么有效的对百度蜘蛛权重优化?

人们交换链接通常首先要问的是你BR值是多少?国内搜索引擎来说以百度马首是瞻,无论seo还是竞价都看重的是百度,那么针对百度权重的优化就特别重要了。其实,百度权重是民间的一种说法,百度官方并没有认同这个数值&#x…

mkdir: ‘/opt/hdfsDep‘: Input/output error

执行hdfs dfs -mkdir -p /opt/hdfsDepo时,报错:mkdir: /opt/hdfsDep: Input/output error,应该是配置文件的问题。 参考文章Spark Standalone模式部署-CSDN博客第三章,安装配置好hadoop,并启动,再次执行上…

(回溯)记忆化搜索和dp

动态规划的核心就是 状态的定义和状态的转移 灵神 的 回溯改递归思路 首先很多动态规划问题都可以采用 回溯 的思想 回溯主要思想就是把 一个大问题分解成小问题 比如 采用子集类回溯问题中的核心思想-> 选或不选 或者 选哪个 记忆化搜索之后 我们可以发现 每个新节点依…

Oracle故障处理:ORA-00600错误处理思路

提前说明: 该故障,我只是旁观者。 但处理该故障的DBA工程师,思路很清晰,我非常受教!在此也将经验分享。 目录 项目场景 问题分析 优化建议 项目场景 在某项目数据库运维群,有现场同事发了张报错截图如下…

代码学习记录49---单调栈

随想录日记part49 t i m e : time: time: 2024.04.20 主要内容:今天开始要学习单调栈的相关知识了,今天的内容主要涉及:柱状图中最大的矩形 84.柱状图中最大的矩形 Topic184.柱状图中最大的矩形 题目&…

SQL EXPLAIN select_type 为DERIVED啥意思

在 MySQL 中,当你使用 EXPLAIN 命令来查看查询执行计划时,select_type 字段的取值为 DERIVED 时表示子查询或派生表。 具体来说,select_type 的取值有多种,常见的包括: SIMPLE:简单的 SELECT 查询&#x…

Scikit-Learn支持向量机分类

Scikit-Learn 支持向量机分类 1、支持向量机(SVM)1.1、SVM概述1.2、SVM原理1.3、SVM的损失函数1.4、支持向量机分类的优缺点 2、Scikit-Learn支持向量机分类2.1、Scikit-Learn支持向量机分类API2.2、支持向量机分类初体验(手写数字识别&#…

openFeign拦截器(微服务调用feign接口会造成请求头缺失望周知)

在学习商品甄选项目的时候,当时我的解决方案是在登录的时候存入用户数据 由于懒得看视频 最后才发现 文档最后才给了这个解决方案。。。。 问题说明 在测试的时候,那么service-cart微服务会报错,如下所示: java.lang.NullPoint…

四川易点慧电子商务抖音小店:安全正规,购物新选择

在当今互联网高速发展的时代,电子商务已经成为人们日常购物的重要组成部分。四川易点慧电子商务抖音小店作为新兴的电商平台,凭借其安全正规的经营理念和便捷高效的购物体验,正逐渐赢得消费者的信赖和喜爱。 一、平台背景实力雄厚 四川易点慧…

百钱买百鸡

百钱买百鸡问题可以使用穷举法解决。我们可以使用三重循环来遍历所有可能的公鸡、母鸡和小鸡的数量,然后判断是否满足题目条件,即总花费不超过100元,并且买到100只鸡。(公鸡5元一只,母鸡3元一只,小鸡一元三…

Windows11+Ubuntu20.04系统重装(升级为Ubuntu22.04)

事情起因是标题所对应的双系统中,Ubuntu老自动断电关机,一开始是跑大型程序才会关机,这两天愈演愈烈变成运行一个远程控制或者VSCode就会关机。一怒之下找了Dell在线客服,在对方引导下检测了硬件系统,发现没有明显故障…

Java可变参数和不可变参数

可变参数 Java可变参数允许在方法中传递不定数量的参数。 可变参数是Java 5引入的一项功能,它极大地提高了代码的灵活性和易用性。使用可变参数时,你可以在调用方法时传递任意数量的参数,而这些参数在方法内部被当作数组处理。这意味着你可…

A29 STM32_HAL库函数 之 IWDG通用驱动 所有函数的介绍及使用

A29 STM32_HAL库函数 之 IWDG通用驱动 所有函数的介绍及使用 1 该驱动函数预览1.1 HAL_IWDG_Init1.2 HAL_IWDG_Refresh 该文档修改记录:总结 1 该驱动函数预览 序号函数名描述1HAL_IWDG_Init()初始化独立看门狗(IWDG)。2HAL_IWDG_Refresh()刷新独立看门狗(IWDG)的计…

STM32单片机C语言模块化编程实战:按键控制LED灯详解与示例

一、开发环境 硬件:正点原子探索者 V3 STM32F407 开发板 单片机:STM32F407ZGT6 Keil版本:5.32 STM32CubeMX版本:6.9.2 STM32Cube MCU Packges版本:STM32F4 V1.27.1 之前介绍了很多关于点灯的方法,比如…

4.20 IO流

IO流结构 InputStream(字节输入流) public static void main(String[] args) {// byteInputStream();// byteInputStream1();// byteInputStream2();byteInputStream3();}// 使用字节流时对于中文汉字基本都会出现乱码问题,因此对中文乱码问…

mininet+odl安装

安装环境 ubuntu-18.04.2-desktop-amd64 Java version: 1.8.0_362 Apache Maven 3.6.0 opendaylight: distribution-karaf-0.6.0-Carbon(csdn中应该是已有资源,不让上传) opendaylight的官网下载链接一直打开失败,我使用的是别人的Carbon版本。 在安…