【总结】逻辑运算在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://xiahunao.cn/news/3247747.html

如若内容造成侵权/违法违规/事实不符，请联系瞎胡闹网进行投诉反馈，一经查实，立即删除！

相关文章

“论企业集成平台的理解与应用”，软考高级论文，系统架构设计师论文

“论企业集成平台的理解与应用”，软考高级论文，系统架构设计师论文

论文真题 企业集成平台&#xff08;Enterprise Imtcgation Plaform,EIP)是支特企业信息集成的像环境&#xff0c;其主要功能是为企业中的数据、系统和应用等多种对象的协同行提供各种公共服务及运行时的支撑环境。企业集成平台能够根据业务模型的变化快速地进行信息系统的配置…
阅读更多...
linux环境安装mongoDB

linux环境安装mongoDB

一、安装单体mogodb 目标&#xff1a;在Linux中部署一个单机的MongoDB&#xff0c;作为生产环境下使用。 提示&#xff1a;和Windows下操作差不多。 步骤如下&#xff1a; &#xff08;1&#xff09;先到官网下载压缩包 mongod-linux-x86_64-4.0.10.tgz 。 &#xff08;2&…
阅读更多...
node+MySQL+Express实现账户登录,注册，重置之登录篇

node+MySQL+Express实现账户登录,注册，重置之登录篇

nodeMySQLExpress实现账户登录 实现技术开发工具项目结构效果图app.js代码db.jsrouter下的account.jsdb下的account.jslogin.html数据库结构 实现技术 node.js,MySQL5.7(8.0以上版本会报错)&#xff0c;layui(前端框架)&#xff0c;Express notify(消息通知layui插件) 开发工…
阅读更多...
破解反爬虫策略 /_guard/auto.js（二）实战

破解反爬虫策略 /_guard/auto.js（二）实战

这次我们用上篇文章讲到的方法来真正破解一下反爬虫策略&#xff0c;这两个案例是两个不同的网站&#xff0c;一个用的是 /_guard/auto.js&#xff0c;另一个用的是/_guard/delay_jump.js。经过解析发现这两个网站用的反爬虫策略基本是一模一样&#xff0c;只不过在js混淆和生成…
阅读更多...
高通Android 12 设置Global属性为null问题

高通Android 12 设置Global属性为null问题

1、最近在做app调用framework.jar需求&#xff0c;尝试在frameworks/base/packages/SettingsProvider/res/values/defaults.xml增加属性 <integer name"def_xxxxx">1</integer> 2、在frameworks\base\packages\SettingsProvider\src\com\android\provide…
阅读更多...
2024年“数据要素×”大赛宁夏分赛正式启动

2024年“数据要素×”大赛宁夏分赛正式启动

数据赋能 乘数而上 分赛聚焦“数据赋能　乘数而上”主题&#xff0c;对标国家“数据要素”大赛要求&#xff0c;结合宁夏特色优势产业、重点行业发展&#xff0c;设立工业制造、现代农业、金融服务、医疗健康、现代教育、水利应用6个行业赛道和1个通用赛道&#xff0c;围绕22个…
阅读更多...
linux进程——概念理解与PCB

linux进程——概念理解与PCB

前言&#xff1a;本篇讲解Linux进程概念相关内容。 操作系统被称为计算机世界的哲学&#xff0c; 可以见得操作系统的知识并不好理解。 对于这篇进程概念的讲解&#xff0c; 博主认为&#xff0c; 如果没有一些前置知识的话&#xff0c;里面的有些概念并不好理解。 但是如果学习…
阅读更多...
STM32测测速---编码电机读取速度的计算

STM32测测速---编码电机读取速度的计算

1、首先先了解一下计算的公式 速度计算&#xff1a; 轮胎每转一圈的脉冲数取决于编码器的分辨率&#xff0c;可由下面公式进行计算&#xff1a; PPR是电机的线数 以GA25-370电机为例。 图片来源&#xff1a;第四节&#xff1a;STM32定时器&#xff08;4.JGA25-370霍尔编码器…
阅读更多...
navicat15已连接忘记密码

navicat15已连接忘记密码

1.导出链接 2.使用文本打开 connections.ncx UserName"root" PasswordXXXX 3.复制加密密码&#xff0c;在线解密 代码在线运行 - 在线工具 php解密代码 <?php class NavicatPassword {protected $version 0;protected $aesKey libcckeylibcckey;protected…
阅读更多...
vue3 快速入门 (二) : 实现第一个Vue网页，并在手机上浏览

vue3 快速入门 (二) : 实现第一个Vue网页，并在手机上浏览

1. 最简单的一个VUE网页 首先&#xff0c;我们可以看我的这篇文章 : vue3 快速入门 (一) : 环境配置与搭建 完成环境搭建。 接着就可以来实现我们的第一个Vue网页了。 本文环境 Vue版本 : 3.4.29Node.js版本 : v20.15.0系统 : Windows11 64位IDE : VsCode 1.1 基础模板 vu…
阅读更多...
leetcode热题100-技巧-只出现一次的数字

leetcode热题100-技巧-只出现一次的数字

题源 136.只出现一次的数字 题目描述 给你一个 非空 整数数组 nums &#xff0c;除了某个元素只出现一次以外&#xff0c;其余每个元素均出现两次。找出那个只出现了一次的元素。 你必须设计并实现线性时间复杂度的算法来解决此问题&#xff0c;且该算法只使用常量额外空间…
阅读更多...
未来职场：人工智能就业，人类失业

未来职场：人工智能就业，人类失业

未来职场&#xff1a;人工智能就业&#xff0c;人类失业 在当今这个快速发展的时代&#xff0c;人工智能和自动化技术的迅猛进步不仅改变了我们的生活方式&#xff0c;也对各行各业产生了深远的影响。从无人驾驶汽车到自动化建筑技术&#xff0c;从机器翻译到智能法律咨询&…
阅读更多...
[日进斗金系列]用码上飞解决企微开发维修管理系统的需求

[日进斗金系列]用码上飞解决企微开发维修管理系统的需求

前言&#xff1a; 今天跟大家唠唠如何用小money生 大money的方法&#xff0c;首先我们需要准备一个工具。 这个工具叫码上飞CodeFlying&#xff0c;它是目前国内首发的L4级自动化智能软件开发平台。 它可以在短时间内&#xff0c;与AI进行几轮对话就能开发出一个可以解决实际…
阅读更多...
torch学习：均值和方差

torch学习：均值和方差

torch学习&#xff1a;均值和方差 初始化Relu对方差的影响He Kaiming Normal欢迎使用Markdown编辑器新的改变功能快捷键合理的创建标题&#xff0c;有助于目录的生成如何改变文本的样式插入链接与图片如何插入一段漂亮的代码片生成一个适合你的列表创建一个表格设定内容居中、居…
阅读更多...
轨道交通AR交互教学定制公司优选深圳华锐视点

轨道交通AR交互教学定制公司优选深圳华锐视点

在寻找上海AR开发制作公司作为合作伙伴的过程中&#xff0c;选择一家既技术深厚又具备丰富经验的AR开发企业&#xff0c;成为了众多客户与合作伙伴的共同追求。华锐视点上海AR开发制作公司作为业界的佼佼者&#xff0c;凭借其卓越的公司规模、丰富的行业案例以及顶尖的ar增强现…
阅读更多...
usb2.0的同步和自动重传机制

usb2.0的同步和自动重传机制

1. usb2.0主机和设备的时间同步 usb 主机(host) 通过 SOF(Start-of-Frame) 向 device设备 广播时间&#xff0c;用以时间同步。 1.1 SOF(Start-of-Frame) 格式 1.2 SOF的作用 usb2.0 主机(host) 周期性的向 设备(device) 广播 SOF(Start-of-Frame), SOF(Start-of-Frame) 将总…
阅读更多...
N沟道功率高压MOSFET WPH4003-1E 在工业自动化控制中的应用

N沟道功率高压MOSFET WPH4003-1E 在工业自动化控制中的应用

1700V高压MOSFET WPH4003-1E 具有低导通电阻和高速开关&#xff0c;有助于需要高压电源的工业设备相关应用的低功耗和高效率。WPH4003-1E 反激式电路可以通过减少零件数量来实现“简化栅极驱动电路”和“减少基板面积”的“成本效益”和“环保”应用。 其部分参数如下&#xf…
阅读更多...
ubuntu24.04 linux bcm94352hmb 无线网卡（带蓝牙功能）无法连接蓝牙设备的解决办法

ubuntu24.04 linux bcm94352hmb 无线网卡（带蓝牙功能）无法连接蓝牙设备的解决办法

ubuntu24.04 linux bcm94352hmb 无线网卡&#xff08;带蓝牙功能&#xff09;无法连接蓝牙设备的解决办法 问题描述 小本是自己换装的bcm94352hmb&#xff0c;现在跑不动黑苹果了&#xff0c;换装ubuntu&#xff0c;该网卡在黑苹果上和windows上都能正常工作&#xff0c;到了…
阅读更多...
部署运维之二：虚拟化

部署运维之二：虚拟化

摘要&#xff1a; 在21世纪初的曙光中&#xff0c;虚拟化技术悄然萌芽&#xff0c;标志着计算领域的一次革命性飞跃。这一时期&#xff0c;通过引入虚拟化技术&#xff0c;业界实现了在单一物理服务器之上并行运行多个虚拟机的壮举&#xff0c;每个虚拟机均构筑起一个隔离而独…
阅读更多...
牛客 7.13 月赛（留 C逆元 Ddp）

牛客 7.13 月赛（留 C逆元 Ddp）

B-最少剩几个&#xff1f;_牛客小白月赛98 (nowcoder.com) 思路 奇数偶数 奇数&#xff1b;奇数*偶数 奇数 所以在既有奇数又有偶数时&#xff0c;两者结合可以同时删除 先分别统计奇数&#xff0c;偶数个数 若偶个数大于奇个数&#xff0c;答案是偶个数-奇个数 若奇个数…
阅读更多...
最新文章

Copyright @ 2022~2023