【总结】逻辑运算在Z3中运用+CTF习题

国际赛IrisCTF在前几天举办，遇到了一道有意思的题目，特来总结。

题目

附件如下：📎babyrevjohnson.tar

解题过程

关键main函数分析如下：

int __fastcall main(int argc, const char **argv, const char**envp){int v4; // [rsp+4h] [rbp-7Ch]int v5; // [rsp+4h] [rbp-7Ch]int v6; // [rsp+8h] [rbp-78h]int v7; // [rsp+Ch] [rbp-74h]char input[104]; // [rsp+10h] [rbp-70h] BYREFunsigned __int64 v9; // [rsp+78h] [rbp-8h]v9 = __readfsqword(0x28u);puts("Welcome to the Johnson's family!");puts("You have gotten to know each person decently well, so let's seeif you remember all of the facts.");puts("(Remember that each of the members like different things fromeach other.)");v4 = 0;while ( v4 <= 3 ) // 在提供的颜色中，选择4种{printf("Please choose %s's favorite color: ", (&names)[v4]);//4个人__isoc99_scanf("%99s", input);if ( !strcmp(input, colors) ){v6 = 1; // redgoto LABEL_11;}if ( !strcmp(input, s2) ){v6 = 2; // bluegoto LABEL_11;}if ( !strcmp(input, off_4050) ){v6 = 3; // greengoto LABEL_11;}if ( !strcmp(input, off_4058) ){v6 = 4; // yellowLABEL_11:if ( v6 == chosenColors[0] || v6 == dword_4094 || v6 ==dword_4098 || v6 == dword_409C )// 选择4个颜色，然后顺序不能一样puts("That option was already chosen!");elsechosenColors[v4++] = v6; // 存储选择的颜色（已经转换成了数字）}else{puts("Invalid color!");}}v5 = 0;while ( v5 <= 3 ){printf("Please choose %s's favorite food: ", (&names)[v5]);//4个人最喜欢的食物__isoc99_scanf("%99s", input);if ( !strcmp(input, foods) ){v7 = 1; // pizzagoto LABEL_28;}if ( !strcmp(input, off_4068) ){v7 = 2; // pastagoto LABEL_28;}if ( !strcmp(input, off_4070) ){v7 = 3; // steakgoto LABEL_28;}if ( !strcmp(input, off_4078) ){v7 = 4; // chickenLABEL_28:if ( v7 == chosenFoods[0] || v7 == dword_40A4 || v7 == dword_40A8|| v7 == dword_40AC )puts("That option was already chosen!");elsechosenFoods[v5++] = v7;}else{puts("Invalid food!");}}check(); // 开始check，检测我们输入的颜色和食物是否正确return 0;}-----------------------------------------------------------------------

将check提取出来，我们方便分析

其实到这里已经可以得到结果了，国外的题目确实很讲究趣味性，用颜色和食物作为导向，引导一步一步分析

笔者使用静态分析的方法，一步一步跟踪

C++

 int check(){bool v0; // dl_BOOL4 v1; // eax_BOOL4 v2; // edxv0 = dword_40A8 != 2 && dword_40AC != 2;v1 = v0 && dword_4094 != 1;v2 = chosenColors[0] != 3 && dword_4094 != 3;if ( !v2 || !v1 || chosenFoods[0] != 4 || dword_40AC == 3 ||dword_4098 == 4 || dword_409C != 2 )return puts("Incorrect.");puts("Correct!");return system("cat flag.txt"); // 执行cat flag的命令}-----------------------------------------------------------------------

对应的输入值地址如下：

我们将颜色color数组用x系列表示，将食物用food数组y系列表示

化简如下：

 C++v0 = y3 != 2 && y4 != 2;v1 = v0 && x2 != 1;v2 = x1 != 3 && x2 != 3;if ( !v2 || !v1 || y1 != 4 || y4 == 3 || x3 == 4 || x4 != 2){//错误}else{//成功}-----------------------------------------------------------------------

思路1:简单粗暴的爆破，但不是学习的目的，因此并不采用

思路2:锻炼写脚本能力，使用z3解题可以锻炼写脚本的能力，因此采用

Python

  from z3 import *# 创建变量x1, x2, x3, x4 = Ints('x1 x2 x3 x4')y1, y2, y3, y4 = Ints('y1 y2 y3 y4')# 创建约束条件v0 = And(y3 != 2, y4 != 2)v1 = And(v0, x2 != 1)v2 = And(x1 != 3, x2 != 3)# 创建条件语句cond = Or(Not(v2), Not(v1), y1 != 4, y4 == 3, x3 == 4, x4 != 2)cond1 = Not(cond)#正常来说，cond的值要为false的，但是z3的add添加的条件必须为1才行，因此要进行取反操作# 创建求解器solver = Solver()# 添加约束条件和条件语句到求解器solver.add(cond1)#这里添加的条件必须为true，所以最后使用了 not 进行取反操作# 求解if solver.check() == sat:# 如果有解，则获取解model = solver.model()# 打印解print("成功:")print("x1 =", model[x1])print("x2 =", model[x2])print("x3 =", model[x3])print("x4 =", model[x4])print("y1 =", model[y1])print("y2 =", model[y2])print("y3 =", model[y3])print("y4 =", model[y4])else:print("无解")---------------------------------------------------------------------------------------

得到结果

Python

  成功:x1 = 4x2 = 0x3 = 5x4 = 2y1 = 4y2 = Noney3 = 3y4 = 0-----------------------------------------------------------------------

其实有经验的师傅发现了，这是有多解的，因为没有为约束变量添加范围约束

帮助网安学习，全套资料S信免费领取：
① 网安学习成长路径思维导图
② 60+网安经典常用工具包
③ 100+SRC分析报告
④ 150+网安攻防实战技术电子书
⑤ 最权威CISSP 认证考试指南+题库
⑥ 超1800页CTF实战技巧手册
⑦ 最新网安大厂面试题合集（含答案）
⑧ APP客户端安全检测指南（安卓+IOS）

改进之后的代码如下：

Python

  from z3 import *# 创建变量x1, x2, x3, x4 = Ints('x1 x2 x3 x4')y1, y2, y3, y4 = Ints('y1 y2 y3 y4')# 创建约束条件v0 = And(y3 != 2, y4 != 2)v1 = And(v0, x2 != 1)v2 = And(x1 != 3, x2 != 3)range_constraint = And(x1 >= 1, x1 <= 4, x2 >= 1, x2 <= 4, x3 >= 1, x3 <= 4, x4>= 1, x4 <= 4,y1 >= 1, y1 <= 4, y2 >= 1, y2 <= 4, y3 >= 1, y3 <= 4, y4 >= 1, y4 <= 4)# 创建条件语句cond = Or(Not(v2), Not(v1), y1 != 4, y4 == 3, x3 == 4, x4 != 2)cond1 = Not(cond)#正常来说，cond的值要为false的，但是z3的add添加的条件必须为1才行，因此要进行取反操作# 创建求解器solver = Solver()# 添加约束条件和条件语句到求解器solver.add(cond1)#这里添加的条件必须为true，所以最后使用了 not 进行取反操作solver.add(range_constraint)# 求解if solver.check() == sat:# 如果有解，则获取解model = solver.model()# 打印解print("成功:")print("x1 =", model[x1])print("x2 =", model[x2])print("x3 =", model[x3])print("x4 =", model[x4])print("y1 =", model[y1])print("y2 =", model[y2])print("y3 =", model[y3])print("y4 =", model[y4])else:print("无解")------------------------------------------------------------------------------------------------------------------------------------------------------------------------------得到结果：-----------------------------------------------------------------------Python成功:x1 = 1x2 = 4x3 = 1x4 = 2y1 = 4y2 = 1y3 = 3y4 = 4-----------------------------------------------------------------------

发现x1和x3重复了，因此还要添加值不重复约束

 Pythonfrom z3 import *# 创建变量x1, x2, x3, x4 = Ints('x1 x2 x3 x4')y1, y2, y3, y4 = Ints('y1 y2 y3 y4')# 创建约束条件v0 = And(y3 != 2, y4 != 2)v1 = And(v0, x2 != 1)v2 = And(x1 != 3, x2 != 3)#值范围约束range_constraint = And(x1 >= 1, x1 <= 4, x2 >= 1, x2 <= 4, x3 >= 1, x3 <= 4, x4>= 1, x4 <= 4,y1 >= 1, y1 <= 4, y2 >= 1, y2 <= 4, y3 >= 1, y3 <= 4, y4 >= 1, y4 <= 4)#非重复值约束distinct_x=Distinct(x1,x2,x3,x4)distinct_y=Distinct(y1,y2,y3,y4)# 创建条件语句cond = Or(Not(v2), Not(v1), y1 != 4, y4 == 3, x3 == 4, x4 != 2)cond1 = Not(cond)#正常来说，cond的值要为false的，但是z3的add添加的条件必须为1才行，因此要进行取反操作# 创建求解器solver = Solver()# 添加约束条件和条件语句到求解器solver.add(cond1)#这里添加的条件必须为true，所以最后使用了 not 进行取反操作solver.add(range_constraint)solver.add(distinct_y)solver.add(distinct_x)# 求解if solver.check() == sat:# 如果有解，则获取解model = solver.model()# 打印解print("成功:")print("x1 =", model[x1])print("x2 =", model[x2])print("x3 =", model[x3])print("x4 =", model[x4])print("y1 =", model[y1])print("y2 =", model[y2])print("y3 =", model[y3])print("y4 =", model[y4])else:print("无解")---------------------------------------------------------------------------------------

最终得到正确的结果

Python
成功:
x1 = 1
x2 = 4
x3 = 3
x4 = 2
y1 = 4
y2 = 2
y3 = 3

y4 = 1

x1-x4= 1 4 3 2

y1-y4= 4 2 3 1

按照这样的顺序输入即可：

得到了flag

irisctf{m0r3_th4n_0n3_l0g1c_puzzl3_h3r3}

总结

题目并不是很难，没有复杂的ollvm混淆也没有复杂的加密。但是却一步一步引导我们去学习和总结。z3解题的过程中，会有很多误解，然后经过自己的思考总结，发现了漏掉的东西，再进行补充，最终写出正确的脚本。

国外的题还是很值得学习的，不单单为了出题而出题。这就是逻辑运算在z3的运用以及如何增加约束，让z3求解出我们需要的key

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

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

相关文章

关于adcoder和codeforce 如何安装翻译插件

关于adcoder和codeforce 如何安装翻译插件

首先在扩展当中下载插件篡改猴 其次&#xff0c;点击获取新的脚本 最后搜索 atcoder better 和 codeforce better 安装即可
阅读更多...
【Spring Boot】网页五子棋项目实现，手把手带你全盘解析（长达两万3千字的干货，坐好了，要发车了......）

【Spring Boot】网页五子棋项目实现，手把手带你全盘解析（长达两万3千字的干货，坐好了，要发车了......）

目录 网页五子棋项目一、项目核心流程二、 登录模块2.1 前端输入用户信息2.2 后端进行数据库查询用户信息 三、 游戏大厅模块3.1 前端通过Ajax请求用户数据&#xff0c;后端从Session中拿取并从数据库中查询后返回3.2 前后端建立WebSocket连接&#xff0c;并进行判断&#xff0…
阅读更多...
如何处理 PostgreSQL 中死锁的情况？

如何处理 PostgreSQL 中死锁的情况？

&#x1f345;关注博主&#x1f397;️ 带你畅游技术世界&#xff0c;不错过每一次成长机会&#xff01;&#x1f4da;领书&#xff1a;PostgreSQL 入门到精通.pdf 文章目录 如何处理 PostgreSQL 中死锁的情况&#xff1f;一、认识死锁二、死锁的症状三、死锁的检测四、预防死锁…
阅读更多...
【MySQL】：想学好数据库，不知道这些还想咋学

【MySQL】：想学好数据库，不知道这些还想咋学

客户端—服务器 客户端是一个“客户端—服务器”结构的程序 C&#xff08;client&#xff09;—S&#xff08;server&#xff09; 客户端和服务器是两个独立的程序&#xff0c;这两个程序之间通过“网络”进行通信&#xff08;相当于是两种角色&#xff09; 客户端 主动发起网…
阅读更多...
Java语言程序设计——篇六(1)

Java语言程序设计——篇六(1)

字符串 概述创建String类对象     字符串基本操作实战演练 字符串查找字符串转换为数组字符串比较实战演练 字符串的拆分与组合 概述 字符串 用一对双引号“”括起来的字符序列。Java语言中&#xff0c;字符串常量或变量均用类实现。 字符串有两大类&#xff1a; 1&…
阅读更多...
设计模式学习[2]---策略模式+简单工厂回顾

设计模式学习[2]---策略模式+简单工厂回顾

文章目录 前言1.简单工厂模式回顾2.策略模式3.策略模式简单工厂的结合总结 前言 上一篇讲到简单工厂模式。 在我的理解中工厂的存在就是&#xff0c;为了实例化对象。根据不同条件实例化不同的对象的作用。 这篇博客写的策略模式&#xff0c;可以说是把这个根据不同情况实例化…
阅读更多...
pyinstaller 打包基于PyQt5和PaddleOCR的项目为.exe

pyinstaller 打包基于PyQt5和PaddleOCR的项目为.exe

简介&#xff1a; 最近做了一个小项目&#xff0c;是基于PyQt5和PaddleOCR的。需要将其打包为.exe&#xff0c;然后打包过程中遇到了很多问题&#xff0c;也看了很多教程&#xff0c;方法千奇百怪的&#xff0c;最后也是一步一步给试出来了。记录一下&#xff0c;防止以后忘记…
阅读更多...
华为路由器SSH登录实验

华为路由器SSH登录实验

概念 SSH全称安全外壳&#xff08;Secure Shell&#xff09;协议&#xff0c;这个协议的目的就是为了取代缺乏机密性保障的远程管理协议&#xff0c;SSH基于TCP协议的加密通道&#xff0c;让客户端使用服务器的RSA公钥来验证SSHv2服务器的身份。 创建密钥对 在充当SSH服务器的…
阅读更多...
C语言随机数的生成相关案例

C语言随机数的生成相关案例

随机数的方式&#xff1a; 1、设置种子&#xff1a;srand(初始值) 2、获取随机数&#xff1a;rand(); 引导案例&#xff1a; 通过for循环简单生成10个随机数 #include<stdio.h> #include<stdlib.h> //添加包含随机数的库函数 int main() {srand(1); …
阅读更多...
嵌入式人工智能（15-基于树莓派4B的电机控制-直流电机TB6612）

嵌入式人工智能（15-基于树莓派4B的电机控制-直流电机TB6612）

电机是传动以及控制系统的重要组成部分&#xff0c;现在的电机已从过去简单的传动向复杂的控制转移&#xff0c;尤其是对电机的速度、位置、转矩的精确控制&#xff0c;本系列将介绍如何使用树莓派驱动并控制3种最为常见的控制电机&#xff1a;直流电机&#xff08;风扇&#x…
阅读更多...
大语言模型推理优化--键值缓存--Key-value Cache

大语言模型推理优化--键值缓存--Key-value Cache

文章目录 一、生成式预训练语言模型 GPT 模型结构二、FastServe 框架三、Key-value Cache1.大模型推理的冗余计算2.Self Attention3.KV Cache 一、生成式预训练语言模型 GPT 模型结构 目前&#xff0c;深度神经网络推理服务系统已经有一些工作针对生成式预训练语言模型 GPT 的独…
阅读更多...
安全防御---防火墙综合实验3

安全防御---防火墙综合实验3

安全防御—防火墙综合实验3 一、实验拓扑图 二、实验要求 12&#xff0c;对现有网络进行改造升级&#xff0c;将当个防火墙组网改成双机热备的组网形式&#xff0c;做负载分担模式&#xff0c;游客区和DMZ区走FW3&#xff0c;生产区和办公区的流量走FW1 13&#xff0c;办公区…
阅读更多...
Ubuntu22.04安装OMNeT++

Ubuntu22.04安装OMNeT++

一、官网地址及安装指南 官网地址&#xff1a;OMNeT Discrete Event Simulator 官网安装指南&#xff08;V6.0.3&#xff09;&#xff1a;https://doc.omnetpp.org/omnetpp/InstallGuide.pdf 官网下载地址&#xff1a;OMNeT Downloads 旧版本下载地址&#xff1a;OMNeT Old…
阅读更多...
【动态规划】整数拆分

【动态规划】整数拆分

整数拆分&#xff08;难度&#xff1a;中等&#xff09; 该题对应力扣网址 AC代码 class Solution { public:int integerBreak(int n) {//动态规划//感觉这个题和零钱兑换有点像&#xff0c;只是零钱兑换提供了coin列表vector <int> dp(n1,0);//1、定义子问题//将原问题…
阅读更多...
PolarisMesh源码系列--Polaris-Go注册发现流程

PolarisMesh源码系列--Polaris-Go注册发现流程

导语 北极星是腾讯开源的一款服务治理平台&#xff0c;用来解决分布式和微服务架构中的服务管理、流量管理、配置管理、故障容错和可观测性问题。在分布式和微服务架构的治理领域&#xff0c;目前国内比较流行的还包括 Spring Cloud&#xff0c;Apache Dubbo 等。在 Kubernete…
阅读更多...
错误：PHP：Deprecated: Required parameter $xxx follows optional parameter $yyy

错误：PHP：Deprecated: Required parameter $xxx follows optional parameter $yyy

前言 略 错误 Deprecated: Required parameter $xxx follows optional parameter $yyy 解决办法 设置 error_reporting E_ALL & ~E_DEPRECATED & ~E_STRICT 参考 https://blog.csdn.net/lxw1844912514/article/details/100028023
阅读更多...
创建自己的 app： html网页直接打包成app；在线网页打包app工具fusionapp、pake

创建自己的 app： html网页直接打包成app；在线网页打包app工具fusionapp、pake

1、html网页直接打包成app 主要通过hbuilderx框架工具来进行打包 https://www.dcloud.io/hbuilderx.html 参考&#xff1a; https://www.bilibili.com/video/BV1XG411r7QZ/ https://www.bilibili.com/video/BV1ZJ411W7Na 1&#xff09;网页制作 这里做的工具是TodoList 页面&a…
阅读更多...
【数据结构--查找】

【数据结构--查找】

目录 一、查找&#xff08;Searching&#xff09;的概念1.1、基本概念1.2、算法的评价指标 二、顺序查找2.1、算法思想2.2、算法实现2.2.1、常规顺序查找2.2.2、带哨兵的顺序查找 2.3、效率分析2.4、优化2.4.1、针对有序表2.4.2、被查效率不相等 三、折半查找3.1、算法思想3.2、…
阅读更多...
C语言项目篇：二、课程管理系统

C语言项目篇：二、课程管理系统

为加强对于C语言的巩固和复习&#xff0c;以实战项目为导向&#xff0c;串起所有C语言的语法&#xff0c;达到活学活用的目的&#xff0c;本篇博客&#xff0c;详细总结利用C语言编码简单编码实现生活中的课程管理系统后台开发的整个过程&#xff0c;学习多文件编程和调试&…
阅读更多...
Internet 控制报文协议 —— ICMPv4 和 ICMPv6 详解

Internet 控制报文协议 —— ICMPv4 和 ICMPv6 详解

ICMP 是一种面向无连接的协议&#xff0c;负责传递可能需要注意的差错和控制报文&#xff0c;差错指示通信网络是否存在错误 (如目的主机无法到达、IP 路由器无法正常传输数据包等。注意&#xff0c;路由器缓冲区溢出导致的丢包不包括在 ICMP 响应范围内&#xff0c;在 TCP 负责…
阅读更多...
推荐文章
最新文章

Copyright @ 2022~2023