z3约束求解器使用

Bertha 。 2021-09-21 11:08 660阅读 0赞

### Z3约束求解器 ###

*  Z3的使用
 *   *  安装
     *  用法
     *  实例

# Z3的使用 #

> z3作为一种约束求解器，在CTF中可以用来解一些密码学，二进制逆向等问题。本文简单的介绍了z3的安装，用法，并且通过一个逆向题目来具体实践一下。

## 安装 ##

pip install z3-solver

## 用法 ##

**1.声明变量**

z3中有3中类型的变量，分别是**整型(Int)**,**实型(Real)和向量(BitVec)**

**Int-整数型**

from z3 import *
    a = Int('a')#声明单个整型变量
    a,b = Ints('a b')#声明多个整型变量

**Real-实数型**

from z3 import *
    a = Real('a')#声明单个实型变量
    a,b = Real('a b')#声明多个实型变量

**BitVec-向量**

from z3 import *
    a = BitVec('a',8) #声明单个8位的变量
    a, b = BitVec('a b',8)#声明多个8位的变量

**2.常规使用**

from z3 import *
    a,b = Ints('a b')
    solve(a>3,b<8,2*a+b==16)
    #结果 [a = 5, b = 6]

**3.约束求解器**

在解决问题是很多情况下是有多个约束条件的。这个时候可以先生成一个求解器对象(**Solver()**)，然后就可以方便的向其中添加更多的约束条件。

#!/usr/bin/python3
    #-*- coding=utf-8 -*-
    from z3 import *
    a,b = Ints('a b')
    solver = Solver()#创建一个求解器对象
    solver.add(a+b==10)#用add方法添加约束条件
    solver.add(a-b==6)
    if solver.check() == sat: #check()方法用来判断是否有解，sat(satisify)表示满足有解
        ans = solver.model() #model()方法得到解
        print(ans)
        #也可以用变量名作为下标得到解
        print(ans[a])
    else:
        print("no ans!")

更多用法参考官方文档：

https://rise4fun.com/z3/tutorialcontent/guide

## 实例 ##

这是第十三届全国大学生网络安全预选赛的一道逆向题，题目链接如下：

> 链接：https://pan.baidu.com/s/1srNNrt8l3qsMt4cP1OM11Q  
> 提取码：j6c9

用IDA打开：

选中**main**函数，按F5反汇编，得到如下反汇编代码：

// local variable allocation has failed, the output may be wrong!
    int __cdecl main(int argc, const char **argv, const char **envp)
    { 
      ......
      _main(*(_QWORD *)&argc, argv, envp);
      memcpy(Dst, &unk_404020, 0xA8ui64);
      printf("plz input your flag:");
      scanf("%42s", &v46);
      v4 = 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52;
      v5 = 27 * v50 + 73 * v49 + 12 * v48 + 83 * v46 + 85 * v47 + 96 * v51 + 52 * v52;
      v6 = 24 * v48 + 78 * v46 + 53 * v47 + 36 * v49 + 86 * v50 + 25 * v51 + 46 * v52;
      v7 = 78 * v47 + 39 * v46 + 52 * v48 + 9 * v49 + 62 * v50 + 37 * v51 + 84 * v52;
      v8 = 48 * v50 + 14 * v48 + 23 * v46 + 6 * v47 + 74 * v49 + 12 * v51 + 83 * v52;
      v9 = 15 * v51 + 48 * v50 + 92 * v48 + 85 * v47 + 27 * v46 + 42 * v49 + 72 * v52;
      v10 = 26 * v51 + 67 * v49 + 6 * v47 + 4 * v46 + 3 * v48 + 68 * v52;
      v11 = 34 * v56 + 12 * v53 + 53 * v54 + 6 * v55 + 58 * v57 + 36 * v58 + v59;
      v12 = 27 * v57 + 73 * v56 + 12 * v55 + 83 * v53 + 85 * v54 + 96 * v58 + 52 * v59;
      v13 = 24 * v55 + 78 * v53 + 53 * v54 + 36 * v56 + 86 * v57 + 25 * v58 + 46 * v59;
      v14 = 78 * v54 + 39 * v53 + 52 * v55 + 9 * v56 + 62 * v57 + 37 * v58 + 84 * v59;
      v15 = 48 * v57 + 14 * v55 + 23 * v53 + 6 * v54 + 74 * v56 + 12 * v58 + 83 * v59;
      v16 = 15 * v58 + 48 * v57 + 92 * v55 + 85 * v54 + 27 * v53 + 42 * v56 + 72 * v59;
      v17 = 26 * v58 + 67 * v56 + 6 * v54 + 4 * v53 + 3 * v55 + 68 * v59;
      v18 = 34 * v63 + 12 * v60 + 53 * v61 + 6 * v62 + 58 * v64 + 36 * v65 + v66;
      v19 = 27 * v64 + 73 * v63 + 12 * v62 + 83 * v60 + 85 * v61 + 96 * v65 + 52 * v66;
      v20 = 24 * v62 + 78 * v60 + 53 * v61 + 36 * v63 + 86 * v64 + 25 * v65 + 46 * v66;
      v21 = 78 * v61 + 39 * v60 + 52 * v62 + 9 * v63 + 62 * v64 + 37 * v65 + 84 * v66;
      v22 = 48 * v64 + 14 * v62 + 23 * v60 + 6 * v61 + 74 * v63 + 12 * v65 + 83 * v66;
      v23 = 15 * v65 + 48 * v64 + 92 * v62 + 85 * v61 + 27 * v60 + 42 * v63 + 72 * v66;
      v24 = 26 * v65 + 67 * v63 + 6 * v61 + 4 * v60 + 3 * v62 + 68 * v66;
      v25 = 34 * v70 + 12 * v67 + 53 * v68 + 6 * v69 + 58 * v71 + 36 * v72 + v73;
      v26 = 27 * v71 + 73 * v70 + 12 * v69 + 83 * v67 + 85 * v68 + 96 * v72 + 52 * v73;
      v27 = 24 * v69 + 78 * v67 + 53 * v68 + 36 * v70 + 86 * v71 + 25 * v72 + 46 * v73;
      v28 = 78 * v68 + 39 * v67 + 52 * v69 + 9 * v70 + 62 * v71 + 37 * v72 + 84 * v73;
      v29 = 48 * v71 + 14 * v69 + 23 * v67 + 6 * v68 + 74 * v70 + 12 * v72 + 83 * v73;
      v30 = 15 * v72 + 48 * v71 + 92 * v69 + 85 * v68 + 27 * v67 + 42 * v70 + 72 * v73;
      v31 = 26 * v72 + 67 * v70 + 6 * v68 + 4 * v67 + 3 * v69 + 68 * v73;
      v32 = 34 * v77 + 12 * v74 + 53 * v75 + 6 * v76 + 58 * v78 + 36 * v79 + v80;
      v33 = 27 * v78 + 73 * v77 + 12 * v76 + 83 * v74 + 85 * v75 + 96 * v79 + 52 * v80;
      v34 = 24 * v76 + 78 * v74 + 53 * v75 + 36 * v77 + 86 * v78 + 25 * v79 + 46 * v80;
      v35 = 78 * v75 + 39 * v74 + 52 * v76 + 9 * v77 + 62 * v78 + 37 * v79 + 84 * v80;
      v36 = 48 * v78 + 14 * v76 + 23 * v74 + 6 * v75 + 74 * v77 + 12 * v79 + 83 * v80;
      v37 = 15 * v79 + 48 * v78 + 92 * v76 + 85 * v75 + 27 * v74 + 42 * v77 + 72 * v80;
      v38 = 26 * v79 + 67 * v77 + 6 * v75 + 4 * v74 + 3 * v76 + 68 * v80;
      v39 = 34 * v84 + 12 * v81 + 53 * v82 + 6 * v83 + 58 * v85 + 36 * v86 + v87;
      v40 = 27 * v85 + 73 * v84 + 12 * v83 + 83 * v81 + 85 * v82 + 96 * v86 + 52 * v87;
      v41 = 24 * v83 + 78 * v81 + 53 * v82 + 36 * v84 + 86 * v85 + 25 * v86 + 46 * v87;
      v42 = 78 * v82 + 39 * v81 + 52 * v83 + 9 * v84 + 62 * v85 + 37 * v86 + 84 * v87;
      v43 = 48 * v85 + 14 * v83 + 23 * v81 + 6 * v82 + 74 * v84 + 12 * v86 + 83 * v87;
      v44 = 15 * v86 + 48 * v85 + 92 * v83 + 85 * v82 + 27 * v81 + 42 * v84 + 72 * v87;
      v45 = 26 * v86 + 67 * v84 + 6 * v82 + 4 * v81 + 3 * v83 + 68 * v87;
      for ( i = 0; i <= 41; ++i )
      { 
        if ( *(&v4 + i) != Dst[i] )
        { 
          printf("error");
          exit(0);
        }
      }
      printf("win");
      return 0;
    }

分析程序可知输入的就是flag,并且flag是42个字符。这里关键点是看for循化中的if比较条件。可以发现需要v4-v45的值要分别和Dst\[0\]~Dst\[41\]的值分别相等，才能够得到正确答案。

这里需要注意源码中的：

memcpy(Dst, &unk_404020, 0xA8ui64);

memcpy函数的原型是 ：`void *memcpy(void *str1, const void *str2, size_t n)`

将str指向的数据复制大小为n个字节到目标数组str1中。在ida中跟进&unk\_404020,可以发现对应的Dst\[i\]中的值：

![在这里插入图片描述][watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2ljemZ5NTg1_size_16_color_FFFFFF_t_70_pic_center]

(注意：这里数组类型是int型，对于64位的程序，也就是占4个字节。又因为是小端存储，因此Dst\[0\]的值应该是**0x4F17**,后面依次类推，可以得到完整的Dst数组)。然后可以写对应的脚本：

#!/usr/bin/env python3
    #-*- coding=utf-8 -*-
    from z3 import *
    s = Solver()
    v46,v47,v48,v49,v50,v51,v52,v53,v54 = Ints("v46 v47 v48 v49 v50 v51 v52 v53 v54")
    v55,v56,v57,v58,v59,v60,v61,v62,v63 = Ints("v55 v56 v57 v58 v59 v60 v61 v62 v63")
    v64,v65,v66,v67,v68,v69,v70,v71,v72 = Ints("v64 v65 v66 v67 v68 v69 v70 v71 v72")
    v73,v74,v75,v76,v77,v78,v79,v80,v81 = Ints("v73 v74 v75 v76 v77 v78 v79 v80 v81")
    v82,v83,v84,v85,v86,v87 = Ints("v82 v83 v84 v85 v86 v87")
    s.add(0x4F17 == 34*v49+12*v46+53*v47+6*v48+58*v50+36*v51+v52)
    s.add(0x9CF6 == 27*v50+73*v49+12*v48+83*v46+85*v47+96*v51+52*v52)
    s.add(0x8DDB == 24*v48+78*v46+53*v47+36*v49+86*v50+25*v51+46*v52)
    s.add(0x8EA6 == 78*v47+39*v46+52*v48+9*v49+62*v50+37*v51+84*v52)
    s.add(0x6929 == 48*v50+14*v48+23*v46+6*v47+74*v49+12*v51+83*v52)
    s.add(0x9911 == 15*v51+48*v50+92*v48+85*v47+27*v46+42*v49+72*v52)
    s.add(0x40A2 == 26*v51+67*v49+6*v47+4*v46+3*v48+68*v52)
    s.add(0x2F3E == 34*v56+12*v53+53*v54+6*v55+58*v57+36*v58+v59)
    s.add(0x62B6 == 27*v57+73*v56+12*v55+83*v53+85*v54+96*v58+52*v59)
    s.add(0x4B82 == 24*v55+78*v53+53*v54+36*v56+86*v57+25*v58+46*v59)
    s.add(0x486C == 78*v54+39*v53+52*v55+9*v56+62*v57+37*v58+84*v59)
    s.add(0x4002 == 48*v57+14*v55+23*v53+6*v54+74*v56+12*v58+83*v59)
    s.add(0x52D7 == 15*v58+48*v57+92*v55+85*v54+27*v53+42*v56+72*v59)
    s.add(0x2DEF == 26*v58+67*v56+6*v54+4*v53+3*v55+68*v59)
    s.add(0x28DC == 34*v63+12*v60+53*v61+6*v62+58*v64+36*v65+v66)
    s.add(0x640D == 27*v64+73*v63+12*v62+83*v60+85*v61+96*v65+52*v66)
    s.add(0x528F == 24*v62+78*v60+53*v61+36*v63+86*v64+25*v65+46*v66)
    s.add(0x613B == 78*v61+39*v60+52*v62+9*v63+62*v64+37*v65+84*v66)
    s.add(0x4781 == 48*v64+14*v62+23*v60+6*v61+74*v63+12*v65+83*v66)
    s.add(0x6B17 == 15*v65+48*v64+92*v62+85*v61+27*v60+42*v63+72*v66)
    s.add(0x3237 == 26*v65+67*v63+6*v61+4*v60+3*v62+68*v66)
    s.add(0x2A93 == 34*v70+12*v67+53*v68+6*v69+58*v71+36*v72+v73)
    s.add(0x615F == 27*v71+73*v70+12*v69+83*v67+85*v68+96*v72+52*v73)
    s.add(0x50BE == 24*v69+78*v67+53*v68+36*v70+86*v71+25*v72+46*v73)
    s.add(0x598E == 78*v68+39*v67+52*v69+9*v70+62*v71+37*v72+84*v73)
    s.add(0x4656 == 48*v71+14*v69+23*v67+6*v68+74*v70+12*v72+83*v73)
    s.add(0x5B31 == 15*v72+48*v71+92*v69+85*v68+27*v67+42*v70+72*v73)
    s.add(0x313A == 26*v72+67*v70+6*v68+4*v67+3*v69+68*v73)
    s.add(0x3010 == 34*v77+12*v74+53*v75+6*v76+58*v78+36*v79+v80)
    s.add(0x67FE == 27*v78+73*v77+12*v76+83*v74+85*v75+96*v79+52*v80)
    s.add(0x4D5F == 24*v76+78*v74+53*v75+36*v77+86*v78+25*v79+46*v80)
    s.add(0x58DB == 78*v75+39*v74+52*v76+9*v77+62*v78+37*v79+84*v80)
    s.add(0x3799 == 48*v78+14*v76+23*v74+6*v75+74*v77+12*v79+83*v80)
    s.add(0x60A0 == 15*v79+48*v78+92*v76+85*v75+27*v74+42*v77+72*v80)
    s.add(0x2750 == 26*v79+67*v77+6*v75+4*v74+3*v76+68*v80)
    s.add(0x3759 == 34*v84+12*v81+53*v82+6*v83+58*v85+36*v86+v87)
    s.add(0x8953 == 27*v85+73*v84+12*v83+83*v81+85*v82+96*v86+52*v87)
    s.add(0x7122 == 24*v83+78*v81+53*v82+36*v84+86*v85+25*v86+46*v87)
    s.add(0x81F9 == 78*v82+39*v81+52*v83+9*v84+62*v85+37*v86+84*v87)
    s.add(0x5524 == 48*v85+14*v83+23*v81+6*v82+74*v84+12*v86+83*v87)
    s.add(0x8971 == 15*v86+48*v85+92*v83+85*v82+27*v81+42*v84+72*v87)
    s.add(0x3A1D == 26*v86+67*v84+6*v82+4*v81+3*v83+68*v87)
    flag = []
    if s.check() == sat:
    	ans = s.model()
    	flag.append(ans[v46])
    	flag.append(ans[v47])
    	flag.append(ans[v48])
    	flag.append(ans[v49])
    	flag.append(ans[v50])
    	flag.append(ans[v51])
    	flag.append(ans[v52])
    	flag.append(ans[v53])
    	flag.append(ans[v54])
    	flag.append(ans[v55])
    	flag.append(ans[v56])
    	flag.append(ans[v57])
    	flag.append(ans[v58])
    	flag.append(ans[v59])
    	flag.append(ans[v60])
    	flag.append(ans[v61])
    	flag.append(ans[v62])
    	flag.append(ans[v63])
    	flag.append(ans[v64])
    	flag.append(ans[v65])
    	flag.append(ans[v66])
    	flag.append(ans[v67])
    	flag.append(ans[v68])
    	flag.append(ans[v69])
    	flag.append(ans[v70])
    	flag.append(ans[v71])
    	flag.append(ans[v72])
    	flag.append(ans[v73])
    	flag.append(ans[v74])
    	flag.append(ans[v75])
    	flag.append(ans[v76])
    	flag.append(ans[v77])
    	flag.append(ans[v78])
    	flag.append(ans[v79])
    	flag.append(ans[v80])
    	flag.append(ans[v81])
    	flag.append(ans[v82])
    	flag.append(ans[v83])
    	flag.append(ans[v84])
    	flag.append(ans[v85])
    	flag.append(ans[v86])
    	flag.append(ans[v87])
    for x in flag:
    	print(x,end=",")

得到的结果如下：

102,108,97,103,123,55,101,49,55,49,100,52,51,45,54,51,98,57,45,52,101,49,56,45,57,57,48,101,45,54,101,49,52,99,50,97,102,101,54,52,56,125

然后转为ascii编码即可：

#!/usr/bin/python3
    s=[102,108,97,103,123,55,101,49,55,49,100,52,51,45,54,51,98,57,45,52,101,49,56,45,57,57,48,101,45,54,101,49,52,99,50,97,102,101,54,52,56,125]
    for x in s:
        print(chr(x),end="")
    #flag{7e171d43-63b9-4e18-990e-6e14c2afe648}

[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2ljemZ5NTg1_size_16_color_FFFFFF_t_70_pic_center]: /images/20210920/9ddae899f3bd41d884d24eb21657c836.png