z3¶

Warning

The current page still doesn't have a translation for this language.

You can read it through Google Translate.

Besides, you can also help to translate it: Contributing.

简介¶

Z3 solver 是由微软开发的 可满足性模理论求解器（Satisfiability Modulo Theory solver，即 SMT solver），用于检查逻辑表达式的可满足性，并可以找到一组约束中的其中一个可行解（无法找出所有的可行解）。

在 CTF 逆向题中，我们有的时候会遇到一些较为复杂的约束条件，此时可以使用 z3 来辅助求解。

安装¶

Z3 提供了多种语言的接口，方便起见我们使用 Python 版本，我们可以直接通过 pip 进行安装（注意这里应当为 z3-solver 而非 z3）：

$ pip3 install z3-solver

基本用法¶

本节仅介绍 z3 最基本的用法，更多高级用法参见官方文档

变量表示¶

一阶命题逻辑公式由项（变量或常量）与扩展布尔结构组成，在 z3 当中我们可以通过如下方式创建变量实例：

整型（integer，长度不限）

>>> import z3
>>> x = z3.Int(name = 'x') # x is an integer

实数类型（real number，长度不限）

>>> y = z3.Real(name = 'y') # y is a real number

位向量（bit vector，长度需在创建时指定）

>>> z = z3.BitVec(name = 'z', bv = 32) # z is a 32-bit vector

布尔类型（bool）

>>> p = z3.Bool(name = 'p')

整型与实数类型变量之间可以互相进行转换：

>>> z3.ToReal(x)
ToReal(x)
>>> z3.ToInt(y)
ToInt(y)

常量表示¶

除了 Python 原有的常量数据类型外，我们也可以使用 z3 自带的常量类型参与运算：

>>> z3.IntVal(val = 114514) # integer
114514
>>> z3.RealVal(val = 1919810) # real number
1919810
>>> z3.BitVecVal(val = 1145141919810, bv = 32) # bit vector，自动截断
2680619074
>>> z3.BitVecVal(val = 1145141919810, bv = 64) # bit vector
1145141919810

求解器¶

在使用 z3 进行约束求解之前我们首先需要获得一个 求解器 类实例，本质上其实就是一组约束的集合：

>>> s = z3.Solver()

添加约束¶

我们可以通过求解器的 add() 方法为指定求解器添加约束条件，约束条件可以直接通过 z3 变量组成的式子进行表示：

>>> s.add(x * 5 == 10)
>>> s.add(y * 1/2 == x)

对于布尔类型的式子而言，我们可以使用 z3 内置的 And()、Or()、Not()、Implies() 等方法进行布尔逻辑运算：

>>> s.add(z3.Implies(p, q))
>>> s.add(r == z3.Not(q))
>>> s.add(z3.Or(z3.Not(p), r))

约束求解¶

当我们向求解器中添加约束条件之后，我们可以使用 check() 方法检查约束是否是可满足的（satisfiable，即 z3 是否能够帮我们找到一组解）：

z3.sat：约束可以被满足
z3.unsat：约束无法被满足

>>> s.check()
sat

若约束可以被满足，则我们可以通过 model() 方法获取到一组解：

>>> s.model()
[q = True, p = False, x = 2, y = 4, r = False]

对于约束条件比较少的情况，我们也可以无需创建求解器，直接通过 solve() 方法进行求解：

>>> z3.solve(z3.Implies(p, q), r == z3.Not(q), z3.Or(z3.Not(p), r))
[q = True, p = False, r = False]

例题：GWCTF 2019 - xxor¶

逆向分析¶

首先惯例拖入 IDA 中，main() 函数整体逻辑比较简单，首先会读入 6 个整型到栈上，接下来对前三个整型调用三次 sub_400686() 函数进行处理并将结果存到 v7 中，最后调用 sub_400770() 进行检查：

__int64 __fastcall main(int a1, char **a2, char **a3)
{
  int i; // [rsp+8h] [rbp-68h]
  int j; // [rsp+Ch] [rbp-64h]
  __int64 v6[6]; // [rsp+10h] [rbp-60h] BYREF
  __int64 v7[6]; // [rsp+40h] [rbp-30h] BYREF

  v7[5] = __readfsqword(0x28u);
  puts("Let us play a game?");
  puts("you have six chances to input");
  puts("Come on!");
  v6[0] = 0LL;
  v6[1] = 0LL;
  v6[2] = 0LL;
  v6[3] = 0LL;
  v6[4] = 0LL;
  for ( i = 0; i <= 5; ++i )
  {
    printf("%s", "input: ");
    a2 = (char **)((char *)v6 + 4 * i);
    __isoc99_scanf("%d", a2);
  }
  v7[0] = 0LL;
  v7[1] = 0LL;
  v7[2] = 0LL;
  v7[3] = 0LL;
  v7[4] = 0LL;
  for ( j = 0; j <= 2; ++j )
  {
    dword_601078 = v6[j];
    dword_60107C = HIDWORD(v6[j]);
    a2 = (char **)&unk_601060;
    sub_400686(&dword_601078, &unk_601060);
    LODWORD(v7[j]) = dword_601078;
    HIDWORD(v7[j]) = dword_60107C;
  }
  if ( (unsigned int)sub_400770(v7, a2) != 1 )
  {
    puts("NO NO NO~ ");
    exit(0);
  }
  puts("Congratulation!\n");
  puts("You seccess half\n");
  puts("Do not forget to change input to hex and combine~\n");
  puts("ByeBye");
  return 0LL;
}

sub_400686() 有点类似于魔改的 TEA 加密：

__int64 __fastcall sub_400686(unsigned int *a1, _DWORD *a2)
{
  __int64 result; // rax
  unsigned int v3; // [rsp+1Ch] [rbp-24h]
  unsigned int v4; // [rsp+20h] [rbp-20h]
  int v5; // [rsp+24h] [rbp-1Ch]
  unsigned int i; // [rsp+28h] [rbp-18h]

  v3 = *a1;
  v4 = a1[1];
  v5 = 0;
  for ( i = 0; i <= 0x3F; ++i )
  {
    v5 += 1166789954;
    v3 += (v4 + v5 + 11) ^ ((v4 << 6) + *a2) ^ ((v4 >> 9) + a2[1]) ^ 0x20;
    v4 += (v3 + v5 + 20) ^ ((v3 << 6) + a2[2]) ^ ((v3 >> 9) + a2[3]) ^ 0x10;
  }
  *a1 = v3;
  result = v4;
  a1[1] = v4;
  return result;
}

这里的参数 a1 为我们的输入，而 a2 则为四个 int32：

.data:0000000000601060 dword_601060    dd 2                    ; DATA XREF: main+FE↑o
.data:0000000000601064                 dd 2
.data:0000000000601068                 dd 3
.data:000000000060106C                 dd 4

而 sub_400770() 会对处理过后的输入进行检查：

__int64 __fastcall sub_400770(_DWORD *a1)
{
  __int64 result; // rax

  if ( a1[2] - a1[3] == 2225223423LL
    && a1[3] + a1[4] == 4201428739LL
    && a1[2] - a1[4] == 1121399208LL
    && *a1 == -548868226
    && a1[5] == -2064448480
    && a1[1] == 550153460 )
  {
    puts("good!");
    result = 1LL;
  }
  else
  {
    puts("Wrong!");
    result = 0LL;
  }
  return result;
}

求解¶

我们首先使用 z3 来求解 sub_400686() 运算后的结果：

import z3

x = [0] * 6
for i in range(6):
    x[i] = z3.Int('x[' + str(i) + ']')

s = z3.Solver()
s.add(x[0] == 0xDF48EF7E)
s.add(x[5] == 0x84F30420)
s.add(x[1] == 0x20CAACF4)
s.add(x[2]-x[3] == 0x84A236FF)
s.add(x[3]+x[4] == 0xFA6CB703)
s.add(x[2]-x[4] == 0x42D731A8)

if s.check() == z3.sat:
    print(s.model())
else:
    raise Exception("NO SOLUTION!")

结果如下：

$ python3 solve.py 
[x[2] = 3774025685,
 x[3] = 1548802262,
 x[4] = 2652626477,
 x[1] = 550153460,
 x[5] = 2230518816,
 x[0] = 3746099070]

接下来我们逆着 sub_400686() 的逻辑写出解密程序即可：

#include <stdio.h>
#include <stdint.h>

void decrypt(uint32_t sum, uint32_t *v, uint32_t *k)
{
    uint32_t v0, v1;

    v0 = v[0];
    v1 = v[1];

    for (int i = 0; i < 0x40; i++) {
        v1 -= (v0 + sum + 20) ^ ((v0 << 6) + k[2]) ^ ((v0 >> 9) + k[3]) ^ 0x10;
        v0 -= (v1 + sum + 11) ^ ((v1 << 6) + k[0]) ^ ((v1 >> 9) + k[1]) ^ 0x20;
        sum -= 0x458BCD42;
    }

    v[0] = v0;
    v[1] = v1;
}

int main(int argc, char **argv, char **envp)
{
    uint32_t data[] = {
        3746099070, 550153460, 3774025685, 1548802262, 2652626477, 2230518816
    };
    uint32_t sum = 0;
    uint32_t k[] = {
        2, 2, 3, 4
    };

    for (int i = 0; i < 0x40; i++) {
        sum += 0x458BCD42;
    }

    for (int i = 0; i < 3; i++) {
        decrypt(sum, &data[i * 2], k);
        printf("%4x%4x", data[i * 2], data[i * 2 + 1]);
    }

    puts("");

    return 0;
}

结果如下：

$ ./solve 
666c61677b72655f69735f6772656174217d

接下来就是快乐的拿 flag 时间了：

s = '666c61677b72655f69735f6772656174217d'
while len(s) != 0:
    print(chr(int(s[:2], 16)), end = '')
    s = s[2:]
print('')
# flag{re_is_great!}