z3求解器

简介

Z3是一个微软出品的开源约束求解器，能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题（可以简单理解为解方程的感觉，虽然这么比喻其实还差距甚远，请勿吐槽），功能强大且易于使用。
Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外，著名的二进制分析框架 angr 也内置了一个修改版的 Z3。

安装

这里我用的是angr里面的z3，安装教程。

测试

from z3 import *

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

上面的例子中，定义了两个变量：x 和 y。类型为 Int（注意这里的 Int 可不是 C/C++ 里面包含上下界的 int，Z3 中的 Int 对应的就是数学中的整数，Z3 中的 BitVector 才对应到 C/C++ 中的 int）。

然后就调用了 solve 函数求解三个条件下的满足模型，这三个条件分别是 x 大于 2，y 小于 10，并且 x 加 2 个 y 等于 7。

运行一下结果：

1 2	(angr) angr@36aeab92fea7:~/z3$ python test.py [y = 0, x = 7]

ctf实例

某比赛中的逆向题

首先我们利用IDA去打开该文件，定位到关键点，发现关键函数如下：

signed __int64 sub_400766()
{
  if ( strlen((const char *)&stru_6020A0) != 32 )
    return 0LL;
  v3 = stru_6020A0.y1;
  v4 = stru_6020A0.y2;
  v5 = stru_6020A0.y3;
  v6 = stru_6020A0.y4;
  if ( stru_6020A0.x2 * (signed __int64)stru_6020A0.x1 - stru_6020A0.x4 * (signed __int64)stru_6020A0.x3 != 0x24CDF2E7C953DA56LL )
    goto LABEL_15;
  if ( 3LL * stru_6020A0.x3 + 4LL * stru_6020A0.x4 - stru_6020A0.x2 - 2LL * stru_6020A0.x1 != 0x17B85F06 )
    goto LABEL_15;
  if ( 3 * stru_6020A0.x1 * (signed __int64)stru_6020A0.x4 - stru_6020A0.x3 * (signed __int64)stru_6020A0.x2 != 0x2E6E497E6415CF3ELL )
    goto LABEL_15;
  if ( 27LL * stru_6020A0.x2 + stru_6020A0.x1 - 11LL * stru_6020A0.x4 - stru_6020A0.x3 != 0x95AE13337LL )
    goto LABEL_15;
  srand(stru_6020A0.x3 ^ stru_6020A0.x2 ^ stru_6020A0.x1 ^ stru_6020A0.x4);
  v1 = rand() % 50;
  v2 = rand() % 50;
  v7 = rand() % 50;
  v8 = rand() % 50;
  v9 = rand() % 50;
  v10 = rand() % 50;
  v11 = rand() % 50;
  v12 = rand() % 50;
  if ( v6 * v2 + v3 * v1 - v4 - v5 != 0xE638C96D3LL
    || v6 + v3 + v5 * v8 - v4 * v7 != 0xB59F2D0CBLL
    || v3 * v9 + v4 * v10 - v5 - v6 != 0xDCFE88C6DLL
    || v5 * v12 + v3 - v4 - v6 * v11 != 0xC076D98BBLL )
  {
LABEL_15:
    result = 0LL;
  }
  else
  {
    result = 1LL;
  }
  return result;
}

可以看得出来这个题目的目的就是找出满足方程的flag。我们可以很方便的把方程式列出来，但是求解对于一些数学不是很好的人来说简直就是噩梦，这时候Z3求解器就可以很方便的给我们帮助。我们按照题目的意思一步一步利用Z3求解器来求解：

from z3 import *
x1 = Int('x1')
x2 = Int('x2')
x3 = Int('x3')
x4 = Int('x4')
s = Solver()  #创建一个通用求解器
s.add( x2*x1-x4*x3 == 0x24CDF2E7C953DA56)  #添加约束条件
s.add( 3*x3+4*x4-x2-2*x1 == 0x17B85F06)
s.add( 3*x1*x4-x3*x2 == 0x2E6E497E6415CF3E)
s.add( 27*x2+x1-11*x4 - x3 == 0x95AE13337)
print s.check()   #检查是否有解，sat结果表示找到某个合适的解，unsat结果表示没有解
m = s.model()    #得到一组解，m为字典类型
print m
print "traversing model..."
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])

第八届极客大挑战的REConvolution

我们打开文件，也是比较直观的看到约束条件，我试着逆向了这个过程，花费了挺多的时间才得到答案，但是如果我们使用Z3Py来求解的话就会非常的快。

函数关键部分如下：

int __cdecl main(int argc, const char **argv, const char **envp)
{
  unsigned int ii; // esi
  unsigned int v4; // kr00_4
  char flag_i; // bl
  unsigned int jj; // eax
  char *v7; // edx
  char v8; // cl
  int v9; // eax
  char xor_result[80]; // [esp+8h] [ebp-A4h]
  char flag[80]; // [esp+58h] [ebp-54h]
  sub_DC1020("Please input your flag: ");
  sub_DC1050("%40s", flag);
  memset(xor_result, 0, 0x50u);
  ii = 0;
  v4 = strlen(flag);
  if ( v4 )
  {
    do
    {
      flag_i = flag[ii];
      jj = 0;
      do
      {
        v7 = &xor_result[jj + ii];
        v8 = flag_i ^ data1[jj++];
        *v7 += v8;
      }
      while ( jj < 0x20 );
      ++ii;
    }
    while ( ii < v4 );
  }
  v9 = strcmp(xor_result, (const char *)&data2);
  if ( v9 )
    v9 = -(v9 < 0) | 1;
  if ( v9 )
    puts("No, it isn't.");
  else
    puts("Yes, it is.");
  return 0;
}

我们利用Z3Py来进行变量的声明和约束的增加并进行求解

#! /usr/bin/env python2
#coding=utf-8
from z3 import *
s = Solver()
X =  [BitVec(('x%s' % i),8) for i in range(0x22) ]   #生成34个8比特的数
print X
data1 =  [0x21,0x22,0x23,0x24,0x25,0x26,0x27,0x28,0x29,0x2A,0x2B,0x2C,0x2D,0x2E,0x2F,0x3A,
0x3B,0x3C,0x3D,0x3E,0x3F,0x40,0x5B,0x5C,0x5D,0x5E,0x5F,0x60,0x7B,0x7C,0x7D,0x7E]
data2 = [0x72,0xE9,0x4D,0xAC,0xC1,0xD0,0x24,0x6B,0xB2,0xF5,0xFD,0x45,0x49,0x94,0xDC,0x10,
0x10,0x6B,0xA3,0xFB,0x5C,0x13,0x17,0xE4,0x67,0xFE,0x72,0xA1,0xC7,0x04,0x2B,0xC2,
0x9D,0x3F,0xA7,0x6C,0xE7,0xD0,0x90,0x71,0x36,0xB3,0xAB,0x67,0xBF,0x60,0x30,0x3E,
0x78,0xCD,0x6D,0x35,0xC8,0x55,0xFF,0xC0,0x95,0x62,0xE6,0xBB,0x57,0x34,0x29,0x0E,3]
xor_result = [0]*0x41
for m in range(0,0x22):
    for n in range(0,0x20):
        xor_result[n+m] += X[m] ^ data1[n]
for o in range(0,0x41):          #循环添加约束条件
    s.add(xor_result[o] == data2[o])   
print s.check()
m = s.model()
print "traversing model..."
flag=''
for i in range(0,0x22):
    flag+=chr(int("%s" % (m[X[i]])))
print flag

执行脚本如下:

(angr) angr@36aeab92fea7:~/z3$ python exp2.py 
[x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33]
sat
traversing model...
SYC{4+mile+b3gin+with+sing1e+step}