当前位置：首页 > news >正文

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

news 来源：原创 2024/9/20 6:28:55

国际赛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("无解")---------------------------------------------------------------------------------------