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

news2024/9/22 1:33:37

国际赛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] BYREF
  unsigned __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 see
  if you remember all of the facts.");
  puts("(Remember that each of the members like different things from
  each 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; // red
  goto LABEL_11;
  }
  if ( !strcmp(input, s2) )
  {
  v6 = 2; // blue
  goto LABEL_11;
  }
  if ( !strcmp(input, off_4050) )
  {
  v6 = 3; // green
  goto LABEL_11;
  }
  if ( !strcmp(input, off_4058) )
  {
  v6 = 4; // yellow
  LABEL_11:
  if ( v6 == chosenColors[0] || v6 == dword_4094 || v6 ==
  dword_4098 || v6 == dword_409C )// 选择4个颜色，然后顺序不能一样
  puts("That option was already chosen!");
  else
  chosenColors[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; // pizza
  goto LABEL_28;
  }
  if ( !strcmp(input, off_4068) )
  {
  v7 = 2; // pasta
  goto LABEL_28;
  }
  if ( !strcmp(input, off_4070) )
  {
  v7 = 3; // steak
  goto LABEL_28;
  }
  if ( !strcmp(input, off_4078) )
  {
  v7 = 4; // chicken
  LABEL_28:
  if ( v7 == chosenFoods[0] || v7 == dword_40A4 || v7 == dword_40A8
  || v7 == dword_40AC )
  puts("That option was already chosen!");
  else
  chosenFoods[v5++] = v7;
  }
  else
  {
  puts("Invalid food!");
  }
  }
  check(); // 开始check，检测我们输入的颜色和食物是否正确
  return 0;

  }
  -----------------------------------------------------------------------

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

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

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

C++

 int check()
  {
  bool v0; // dl
  _BOOL4 v1; // eax
  _BOOL4 v2; // edx
  v0 = 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 = 4
  x2 = 0
  x3 = 5
  x4 = 2
  y1 = 4
  y2 = None
  y3 = 3

  y4 = 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 = 1
  x2 = 4
  x3 = 1
  x4 = 2
  y1 = 4
  y2 = 1
  y3 = 3

  y4 = 4
  -----------------------------------------------------------------------

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

 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)
  #非重复值约束
  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.coloradmin.cn/o/1933047.html

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

相关文章

Golang | Leetcode Golang题解之第236题二叉树的最近公共祖先

Golang | Leetcode Golang题解之第236题二叉树的最近公共祖先

题目&#xff1a; 题解&#xff1a; func lowestCommonAncestor(root, p, q *TreeNode) *TreeNode {parent : map[int]*TreeNode{}visited : map[int]bool{}var dfs func(*TreeNode)dfs func(r *TreeNode) {if r nil {return}if r.Left ! nil {parent[r.Left.Val] rdfs(r.L…
阅读更多...
用 WireShark 抓住 TCP

用 WireShark 抓住 TCP

Wireshark 是帮助我们分析网络请求的利器&#xff0c;建议每个同学都装一个。我们先用 Wireshark 抓取一个完整的连接建立、发送数据、断开连接的过程。 简单的介绍一下操作流程。 1、首先打开 Wireshark&#xff0c;在欢迎界面会列出当前机器上的所有网口、虚机网口等可以抓取…
阅读更多...
气膜体育馆进校园：政策支持与市场前景—轻空间

气膜体育馆进校园：政策支持与市场前景—轻空间

过去20多年&#xff0c;气膜建筑、场馆相关项目在国内落地众多&#xff0c;展现出强大的市场潜力。2022年8月&#xff0c;《北京晚报》粗略统计&#xff0c;北京全市已建有气膜馆百余座&#xff0c;且数量还在不断增加。这一发展趋势不仅仅体现在北京&#xff0c;全国范围内也都…
阅读更多...
微软GraphRAG +本地模型+Gradio 简单测试笔记

微软GraphRAG +本地模型+Gradio 简单测试笔记

安装 pip install graphragmkdir -p ./ragtest/input#将文档拷贝至 ./ragtest/input/ 下python -m graphrag.index --init --root ./ragtest修改settings.yaml encoding_model: cl100k_base skip_workflows: [] llm:api_key: ${GRAPHRAG_API_KEY}type: openai_chat # or azu…
阅读更多...
如何通过企业微信会话存档保护企业利益？

如何通过企业微信会话存档保护企业利益？

赵总: 张经理&#xff0c;最近行业内频发数据泄露事件&#xff0c;我们的客户资料和内部沟通记录安全吗&#xff1f; 张经理: 赵总&#xff0c;我们已经采取了一系列措施来加强数据安全。特别是针对企业微信的沟通记录&#xff0c;我们最近引入了安企神软件&#xff0c;它能很…
阅读更多...
【BUG】已解决：AttributeError: ‘NoneType‘ object has no attribute ‘split‘

【BUG】已解决：AttributeError: ‘NoneType‘ object has no attribute ‘split‘

已解决&#xff1a;AttributeError: ‘NoneType‘ object has no attribute ‘split‘ 英杰社区https://bbs.csdn.net/topics/617804998 欢迎来到我的主页&#xff0c;我是博主英杰&#xff0c;211科班出身&#xff0c;就职于医疗科技公司&#xff0c;热衷分享知识&#xff0c;…
阅读更多...
通用图形处理器设计GPGPU基础与架构（四）

通用图形处理器设计GPGPU基础与架构（四）

一、前言 本文将介绍GPGPU中线程束的调度方案、记分牌方案和线程块的分配与调度方案。 二、线程束调度 在计算机中有很多资源&#xff0c;既可以是虚拟的计算资源&#xff0c;如线程、进程或数据流&#xff0c;也可以是硬件资源&#xff0c;如处理器、网络连接或 ALU 单元。调…
阅读更多...
大数据平台之Kafka

大数据平台之Kafka

Apache Kafka 是一个分布式流处理平台&#xff0c;最初由 LinkedIn 开发&#xff0c;并在 2011 年开源成为 Apache 项目。Kafka 主要用于构建实时数据管道和流应用&#xff0c;具有高吞吐量、低延迟、容错性强等特点。以下是对 Kafka 的详细介绍&#xff1a; 核心概念 1. Prod…
阅读更多...
爬虫瑞数5案例：某大学总医院

爬虫瑞数5案例：某大学总医院

声明： 该文章为学习使用，严禁用于商业用途和非法用途，违者后果自负，由此产生的一切后果均与作者无关 一、瑞数简介 瑞数动态安全 Botgate（机器人防火墙）以“动态安全”技术为核心，通过动态封装、动态验证、动态混淆、动态令牌等技术对服务器网页底层代码持续动态变换，…
阅读更多...
【 LCD1602显示屏】使用STC89C51控制1602显示、读写操作时序

【 LCD1602显示屏】使用STC89C51控制1602显示、读写操作时序

文章目录 LCD1602显示概述&#xff1a;引脚说明控制指令接线 控制思路步骤 代码示例总结对databuffer dataShow;的理解 LCD1602显示 概述&#xff1a; LCD1602&#xff08;Liquid Crystal Display&#xff09;是一种工业字符型液晶&#xff0c;能够同时显示 1602 即 32 字符…
阅读更多...
深入理解Android中的缓存与文件存储目录

深入理解Android中的缓存与文件存储目录

&#x1f31f; 引言 在Android应用开发中&#xff0c;合理管理应用的数据存储至关重要。应用可能需要保存各种类型的数据&#xff0c;从简单的配置信息到多媒体文件&#xff0c;甚至是缓存数据以提高性能和用户体验。Android提供了多个内置目录来满足这些需求&#xff0c;但它…
阅读更多...
探索Facebook的最新更新：社交体验的新高度

探索Facebook的最新更新：社交体验的新高度

Facebook作为全球领先的社交媒体平台&#xff0c;一直致力于不断创新和改进&#xff0c;以提供更优质的用户体验。近期&#xff0c;Facebook推出了一系列新的更新&#xff0c;旨在提升用户的社交互动体验和平台功能。本文将详细探讨这些最新更新&#xff0c;分析其对用户和社交…
阅读更多...
模拟string(一)详解

模拟string(一)详解

目录 string()构造函数无参初始化错误写法代码 string(const char* str)构造函数有参初始化错误写法代码 string(const char* str "")合并无参和有参的构造函数代码错误写法代码 拷贝构造函数浅拷贝深拷贝方法一string(const string& s)方法二string& opera…
阅读更多...
Hadoop-35 HBase 集群配置和启动 3节点云服务器 集群效果测试 Shell测试

Hadoop-35 HBase 集群配置和启动 3节点云服务器 集群效果测试 Shell测试

点一下关注吧&#xff01;&#xff01;&#xff01;非常感谢&#xff01;&#xff01;持续更新&#xff01;&#xff01;&#xff01; 目前已经更新到了&#xff1a; HadoopHDFSMapReduceHiveFlumeSqoopZookeeperHBase 正在 章节内容 上一节我们完成了&#xff1a; HBase …
阅读更多...
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&…
阅读更多...
设计模式：真正的建造者模式

设计模式：真正的建造者模式

又臭又长的set方法 经常进行Java项目开发使用各类starter的你一定见过这种代码&#xff1a; public class SwaggerConfig {Beanpublic Docket api() {return new Docket(DocumentationType.SWAGGER_2).select().apis(RequestHandlerSelectors.any()).paths(PathSelectors.any…
阅读更多...
文章解读与仿真程序复现思路——电力自动化设备EI\CSCD\北大核心《考虑光热集热单元的氢储能热电联供综合能源系统容量优化配置》

文章解读与仿真程序复现思路——电力自动化设备EI\CSCD\北大核心《考虑光热集热单元的氢储能热电联供综合能源系统容量优化配置》

本专栏栏目提供文章与程序复现思路&#xff0c;具体已有的论文与论文源程序可翻阅本博主免费的专栏栏目《论文与完整程序》 论文与完整源程序_电网论文源程序的博客-CSDN博客https://blog.csdn.net/liang674027206/category_12531414.html 电网论文源程序-CSDN博客电网论文源…
阅读更多...
【Access、Trunk和Hybrid】

【Access、Trunk和Hybrid】

概述 Access类型的端口只能属于1个VLAN&#xff0c;一般用于连接计算机的端口&#xff1b;Trunk类型的端口可以允许多个VLAN通过&#xff0c;可以接收和发送多个VLAN的报文&#xff0c;一般用于交换机之间连接的端口&#xff1b;Hybrid类型的端口可以允许多个VLAN通过&#xf…
阅读更多...
Java中的迭代器（Iterator）

Java中的迭代器（Iterator）

Java中的迭代器&#xff08;Iterator&#xff09; 1、 迭代器的基本方法2、 迭代器的使用示例3、注意事项4、克隆与序列化5、结论 &#x1f496;The Begin&#x1f496;点点关注&#xff0c;收藏不迷路&#x1f496; 在Java中&#xff0c;迭代器&#xff08;Iterator&#xff0…
阅读更多...
1w字图文带你了解sqlmap，从0到1，WAF绕过，高级用法一文通透

1w字图文带你了解sqlmap，从0到1，WAF绕过，高级用法一文通透

前言 在信息安全领域&#xff0c;SQL注入攻击是一种极为常见且危害严重的安全漏洞。攻击者利用Web应用程序对SQL查询的不当处理&#xff0c;通过注入恶意SQL代码&#xff0c;从而绕过安全措施&#xff0c;非法访问或篡改数据库中的数据。随着网络安全威胁的日益严峻&#xff0…
阅读更多...
推荐文章
最新文章

Copyright @ 2022~2023