z3¶

Introduction¶

Z3 solver is a Satisfiability Modulo Theory solver (SMT solver) developed by Microsoft, used to check the satisfiability of logical expressions and to find a feasible solution within a set of constraints (it cannot find all feasible solutions).

In CTF reverse engineering challenges, we sometimes encounter relatively complex constraint conditions, in which case we can use z3 to assist with solving.

Installation¶

Z3 provides interfaces for multiple languages. For convenience, we use the Python version, which can be installed directly via pip (note that the package name should be z3-solver, not z3):

$ pip3 install z3-solver

Basic Usage¶

This section only covers the most basic usage of z3. For more advanced usage, refer to the official documentation.

Variable Representation¶

First-order propositional logic formulas consist of terms (variables or constants) and extended Boolean structures. In z3, we can create variable instances in the following ways:

Integer (unlimited length)

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

Real number (unlimited length)

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

Bit vector (length must be specified at creation time)

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

Boolean

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

Integer and real number type variables can be converted to each other:

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

Constant Representation¶

In addition to Python's native constant data types, we can also use z3's built-in constant types for computations:

>>> z3.IntVal(val = 114514) # integer
114514
>>> z3.RealVal(val = 1919810) # real number
1919810
>>> z3.BitVecVal(val = 1145141919810, bv = 32) # bit vector, automatically truncated
2680619074
>>> z3.BitVecVal(val = 1145141919810, bv = 64) # bit vector
1145141919810

Solver¶

Before using z3 for constraint solving, we first need to obtain a solver class instance, which is essentially a collection of constraints:

>>> s = z3.Solver()

Adding Constraints¶

We can add constraint conditions to a specified solver using the solver's add() method. Constraints can be expressed directly through expressions composed of z3 variables:

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

For Boolean expressions, we can use z3's built-in methods such as And(), Or(), Not(), and Implies() for Boolean logic operations:

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

Solving Constraints¶

After adding constraint conditions to the solver, we can use the check() method to check whether the constraints are satisfiable (i.e., whether z3 can find a solution for us):

z3.sat: the constraints can be satisfied
z3.unsat: the constraints cannot be satisfied

>>> s.check()
sat

If the constraints can be satisfied, we can obtain a solution using the model() method:

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

For cases with fewer constraints, we can also solve directly using the solve() method without creating a solver:

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

Example: GWCTF 2019 - xxor¶

Reverse Analysis¶

As usual, we first load it into IDA. The overall logic of the main() function is fairly simple: it first reads 6 integers onto the stack, then calls the sub_400686() function three times on the first three integers to process them, storing the results in v7, and finally calls sub_400770() to perform the check:

__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() resembles a modified TEA encryption:

__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;
}

Here, parameter a1 is our input, and a2 consists of four int32 values:

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

Meanwhile, sub_400770() checks the processed input:

__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;
}

Solving¶

We first use z3 to solve for the results after the sub_400686() computation:

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!")

The result is as follows:

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

Next, we write a decryption program by reversing the logic of 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;
}

The result is as follows:

$ ./solve 
666c61677b72655f69735f6772656174217d

Now it's time to happily grab the flag:

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