Step One: How2 Z3

Apr 4, 2025

8 mins read

Z3 Reverse Engineering
Z3 Reverse engineering

This article is a long time coming. z3, the constraint solver, is commonly used in crackmes and CTF challenges. Wherever possible, I just lift to angr for symbolic execution and bruteforce that way, since z3 is basically math bruteforce anyways. Regardless:

I don’t remember where I got this bin. I think it’s a HackTheBox Challenge?

01e9a95f1ebf227ed63e9ac9b5d1df59  spookylicence

The main is straightforward, provide a license as an arg, there’s a bunch of checks, it either passes or not.

int32_t main(int32_t argc, char** argv, char** envp)

    if (argc != 2)
        puts(str: "./spookylicence <license>")
        return -1
    
    if (strlen(argv[1]) != 0x20)
        puts(str: "Invalid License Format")
        return -1
    
    char* rax_6 = argv[1]
    
    if (rax_6[0x1d] != rax_6[5] - rax_6[3] + 0x46 || rax_6[2] + rax_6[0x16] != rax_6[0xd] + 0x7b || rax_6[0xc] + rax_6[4] != rax_6[5] + 0x1c || rax_6[0x19] * rax_6[0x17] != *rax_6 + rax_6[0x11] + 0x17 || rax_6[0x1b] * rax_6[1] != rax_6[5] + rax_6[0x16] - 0x15 || rax_6[9] * rax_6[0xd] != rax_6[0x1c] * rax_6[3] - 9 || rax_6[9] != 0x70 || rax_6[0x13] + rax_6[0x15] != rax_6[6] - 0x80 || rax_6[0x10] != rax_6[0xf] - rax_6[0xb] + 0x30 || rax_6[7] * rax_6[0x1b] != rax_6[1] * rax_6[0xd] + 0x2d || rax_6[0xd] != rax_6[0x12] + rax_6[0xd] - 0x65 || rax_6[0x14] - rax_6[8] != rax_6[9] + 0x7c || rax_6[0x1f] != rax_6[8] - rax_6[0x1f] - 0x79 || rax_6[0x14] * rax_6[0x1f] != rax_6[0x14] + 4 || rax_6[0x18] - rax_6[0x11] != rax_6[0x15] + rax_6[8] - 0x17 || rax_6[7] + rax_6[5] != rax_6[5] + rax_6[0x1d] + 0x2c || rax_6[0xc] * rax_6[0xa] != rax_6[1] - rax_6[0xb] - 0x24 || rax_6[0x1f] * *rax_6 != rax_6[0x1a] - 0x1b || rax_6[1] + rax_6[0x14] != rax_6[0xa] - 0x7d || rax_6[0x12] != rax_6[0x1b] + rax_6[0xe] + 2 || rax_6[0x1e] * rax_6[0xb] != rax_6[0x15] + 0x44 || rax_6[5] * rax_6[0x13] != rax_6[1] - 0x2c || rax_6[0xd] - rax_6[0x1a] != rax_6[0x15] - 0x7f || rax_6[0x17] != rax_6[0x1d] - *rax_6 + 0x58 || rax_6[0x13] != rax_6[8] * rax_6[0xd] - 0x17 || rax_6[6] + rax_6[0x16] != rax_6[3] + 0x53 || rax_6[0xc] != rax_6[0x1a] + rax_6[7] - 0x72 || rax_6[0x10] != rax_6[0x12] - rax_6[5] + 0x33 || rax_6[0x1e] - rax_6[8] != rax_6[0x1d] - 0x4d || rax_6[0x14] - rax_6[0xb] != rax_6[3] - 0x4c || rax_6[0x10] - rax_6[7] != rax_6[0x11] + 0x66 || rax_6[1] + rax_6[0x15] != rax_6[0xb] + rax_6[0x12] + 0x2b)
        puts(str: "License Invalid")
        return -1
    
    puts(str: "License Correct")
    return 0

Absolutely disgusting. We know the license is 0x20 in length, and various checks are done on byte offsets with OR || in binary ninja HLIL.

Extract it out, split on ||.

rax_6[0x1d] != rax_6[5] - rax_6[3] + 0x46 
rax_6[2] + rax_6[0x16] != rax_6[0xd] + 0x7b 
rax_6[0xc] + rax_6[4] != rax_6[5] + 0x1c 
rax_6[0x19] * rax_6[0x17] != *rax_6 + rax_6[0x11] + 0x17 
rax_6[0x1b] * rax_6[1] != rax_6[5] + rax_6[0x16] - 0x15 
rax_6[9] * rax_6[0xd] != rax_6[0x1c] * rax_6[3] - 9 
rax_6[9] != 0x70 
rax_6[0x13] + rax_6[0x15] != rax_6[6] - 0x80 
rax_6[0x10] != rax_6[0xf] - rax_6[0xb] + 0x30 
rax_6[7] * rax_6[0x1b] != rax_6[1] * rax_6[0xd] + 0x2d 
rax_6[0xd] != rax_6[0x12] + rax_6[0xd] - 0x65 
rax_6[0x14] - rax_6[8] != rax_6[9] + 0x7c 
rax_6[0x1f] != rax_6[8] - rax_6[0x1f] - 0x79 
rax_6[0x14] * rax_6[0x1f] != rax_6[0x14] + 4 
rax_6[0x18] - rax_6[0x11] != rax_6[0x15] + rax_6[8] - 0x17 
rax_6[7] + rax_6[5] != rax_6[5] + rax_6[0x1d] + 0x2c 
rax_6[0xc] * rax_6[0xa] != rax_6[1] - rax_6[0xb] - 0x24 
rax_6[0x1f] * *rax_6 != rax_6[0x1a] - 0x1b 
rax_6[1] + rax_6[0x14] != rax_6[0xa] - 0x7d 
rax_6[0x12] != rax_6[0x1b] + rax_6[0xe] + 2 
rax_6[0x1e] * rax_6[0xb] != rax_6[0x15] + 0x44 
rax_6[5] * rax_6[0x13] != rax_6[1] - 0x2c 
rax_6[0xd] - rax_6[0x1a] != rax_6[0x15] - 0x7f 
rax_6[0x17] != rax_6[0x1d] - *rax_6 + 0x58 
rax_6[0x13] != rax_6[8] * rax_6[0xd] - 0x17 
rax_6[6] + rax_6[0x16] != rax_6[3] + 0x53 
rax_6[0xc] != rax_6[0x1a] + rax_6[7] - 0x72 
rax_6[0x10] != rax_6[0x12] - rax_6[5] + 0x33 
rax_6[0x1e] - rax_6[8] != rax_6[0x1d] - 0x4d 
rax_6[0x14] - rax_6[0xb] != rax_6[3] - 0x4c 
rax_6[0x10] - rax_6[7] != rax_6[0x11] + 0x66 
rax_6[1] + rax_6[0x15] != rax_6[0xb] + rax_6[0x12] + 0x2b

Setup z3 in python. There’s often easier ways to use z3, but everything always can be represented as a BitVector, so that’s what I use as a template.

from z3 import *

# Valid license is a BitVec with length of 0x20
licensePtr = [BitVec("x_%s" % (i), 8) for i in range(0x20)]
s = Solver()

Draw the rest of the owl, don’t forget to invert logic because the validations we’ve extracted trigger an “invalid license”. IE: != should be inverted to ==.

#rax_6[0x1d] != rax_6[5] - rax_6[3] + 0x46 
s.add(licensePtr[0x1d] == licensePtr[5] - licensePtr[3] + 0x46)
#rax_6[2] + rax_6[0x16] != rax_6[0xd] + 0x7b 
s.add(licensePtr[2] + licensePtr[0x16] == licensePtr[0xd] + 0x7b)
#rax_6[0xc] + rax_6[4] != rax_6[5] + 0x1c 
s.add(licensePtr[0xc] + licensePtr[4] == licensePtr[5] + 0x1c)
#rax_6[0x19] * rax_6[0x17] != *rax_6 + rax_6[0x11] + 0x17 
s.add(licensePtr[0x19] * licensePtr[0x17] == licensePtr[0] + licensePtr[0x11] + 0x17)
#rax_6[0x1b] * rax_6[1] != rax_6[5] + rax_6[0x16] - 0x15 
s.add(licensePtr[0x1b] * licensePtr[1] == licensePtr[5] + licensePtr[0x16] - 0x15)
#rax_6[9] * rax_6[0xd] != rax_6[0x1c] * rax_6[3] - 9 
s.add(licensePtr[9] * licensePtr[0xd] == licensePtr[0x1c] * licensePtr[3] - 9)
#rax_6[9] != 0x70 
s.add(licensePtr[9] == 0x70)
#rax_6[0x13] + rax_6[0x15] != rax_6[6] - 0x80 
s.add(licensePtr[0x13] + licensePtr[0x15] == licensePtr[6] - 0x80)
#rax_6[0x10] != rax_6[0xf] - rax_6[0xb] + 0x30 
s.add(licensePtr[0x10] == licensePtr[0xf] - licensePtr[0xb] + 0x30)
#rax_6[7] * rax_6[0x1b] != rax_6[1] * rax_6[0xd] + 0x2d 
s.add(licensePtr[7] * licensePtr[0x1b] == licensePtr[1] * licensePtr[0xd] + 0x2d)
#rax_6[0xd] != rax_6[0x12] + rax_6[0xd] - 0x65 
s.add(licensePtr[0xd] == licensePtr[0x12] + licensePtr[0xd] - 0x65)
#rax_6[0x14] - rax_6[8] != rax_6[9] + 0x7c 
s.add(licensePtr[0x14] - licensePtr[8] == licensePtr[9] + 0x7c)
#rax_6[0x1f] != rax_6[8] - rax_6[0x1f] - 0x79 
s.add(licensePtr[0x1f] == licensePtr[8] - licensePtr[0x1f] - 0x79)
#rax_6[0x14] * rax_6[0x1f] != rax_6[0x14] + 4 
s.add(licensePtr[0x14] * licensePtr[0x1f] == licensePtr[0x14] + 4)
#rax_6[0x18] - rax_6[0x11] != rax_6[0x15] + rax_6[8] - 0x17 
s.add(licensePtr[0x18] - licensePtr[0x11] == licensePtr[0x15] + licensePtr[8] - 0x17)
#rax_6[7] + rax_6[5] != rax_6[5] + rax_6[0x1d] + 0x2c 
s.add(licensePtr[7] + licensePtr[5] == licensePtr[5] + licensePtr[0x1d] + 0x2c)
#rax_6[0xc] * rax_6[0xa] != rax_6[1] - rax_6[0xb] - 0x24 
s.add(licensePtr[0xc] * licensePtr[0xa] == licensePtr[1] - licensePtr[0xb] - 0x24)
#rax_6[0x1f] * *rax_6 != rax_6[0x1a] - 0x1b 
s.add(licensePtr[0x1f] * licensePtr[0] == licensePtr[0x1a] - 0x1b)
#rax_6[1] + rax_6[0x14] != rax_6[0xa] - 0x7d 
s.add(licensePtr[1] + licensePtr[0x14] == licensePtr[0xa] - 0x7d)
#rax_6[0x12] != rax_6[0x1b] + rax_6[0xe] + 2 
s.add(licensePtr[0x12] == licensePtr[0x1b] + licensePtr[0xe] + 2)
#rax_6[0x1e] * rax_6[0xb] != rax_6[0x15] + 0x44 
s.add(licensePtr[0x1e] * licensePtr[0xb] == licensePtr[0x15] + 0x44)
#rax_6[5] * rax_6[0x13] != rax_6[1] - 0x2c 
s.add(licensePtr[5] * licensePtr[0x13] == licensePtr[1] - 0x2c)
#rax_6[0xd] - rax_6[0x1a] != rax_6[0x15] - 0x7f 
s.add(licensePtr[0xd] - licensePtr[0x1a] == licensePtr[0x15] - 0x7f)
#rax_6[0x17] != rax_6[0x1d] - *rax_6 + 0x58 
s.add(licensePtr[0x17] == licensePtr[0x1d] - licensePtr[0] + 0x58)
#rax_6[0x13] != rax_6[8] * rax_6[0xd] - 0x17 
s.add(licensePtr[0x13] == licensePtr[8] * licensePtr[0xd] - 0x17)
#rax_6[6] + rax_6[0x16] != rax_6[3] + 0x53 
s.add(licensePtr[6] + licensePtr[0x16] == licensePtr[3] + 0x53)
#rax_6[0xc] != rax_6[0x1a] + rax_6[7] - 0x72 
s.add(licensePtr[0xc] == licensePtr[0x1a] + licensePtr[7] - 0x72)
#rax_6[0x10] != rax_6[0x12] - rax_6[5] + 0x33 
s.add(licensePtr[0x10] == licensePtr[0x12] - licensePtr[5] + 0x33)
#rax_6[0x1e] - rax_6[8] != rax_6[0x1d] - 0x4d 
s.add(licensePtr[0x1e] - licensePtr[8] == licensePtr[0x1d] - 0x4d)
#rax_6[0x14] - rax_6[0xb] != rax_6[3] - 0x4c 
s.add(licensePtr[0x14] - licensePtr[0xb] == licensePtr[3] - 0x4c)
#rax_6[0x10] - rax_6[7] != rax_6[0x11] + 0x66 
s.add(licensePtr[0x10] - licensePtr[7] == licensePtr[0x11] + 0x66)
#rax_6[1] + rax_6[0x15] != rax_6[0xb] + rax_6[0x12] + 0x2b
s.add(licensePtr[1] + licensePtr[0x15] == licensePtr[0xb] + licensePtr[0x12] + 0x2b)

Finally, print asseertions, check the model, reorder the solved constraints on completion, and retrieve the values. This is in part a nasty side effect of always using BitVector, but as stated before, I use it because anything can be represented as a bitvector.

for c in s.assertions():
    print(c)

print(s.check())
m = s.model()
sortSolve = sorted ([(d, m[d]) for d in m], key = lambda x: int(str(x[0]).split('_')[1]))
out = ""
for i in sortSolve:
    out += chr(i[1].as_long())
print(out)

Run it and:

x_29 == x_5 - x_3 + 70
x_2 + x_22 == x_13 + 123
x_12 + x_4 == x_5 + 28
x_25*x_23 == x_0 + x_17 + 23
x_27*x_1 == x_5 + x_22 - 21
x_9*x_13 == x_28*x_3 - 9
x_9 == 112
x_19 + x_21 == x_6 - 128
x_16 == x_15 - x_11 + 48
x_7*x_27 == x_1*x_13 + 45
x_13 == x_18 + x_13 - 101
x_20 - x_8 == x_9 + 124
x_31 == x_8 - x_31 - 121
x_20*x_31 == x_20 + 4
x_24 - x_17 == x_21 + x_8 - 23
x_7 + x_5 == x_5 + x_29 + 44
x_12*x_10 == x_1 - x_11 - 36
x_31*x_0 == x_26 - 27
x_1 + x_20 == x_10 - 125
x_18 == x_27 + x_14 + 2
x_30*x_11 == x_21 + 68
x_5*x_19 == x_1 - 44
x_13 - x_26 == x_21 - 127
x_23 == x_29 - x_0 + 88
x_19 == x_8*x_13 - 23
x_6 + x_22 == x_3 + 83
x_12 == x_26 + x_7 - 114
x_16 == x_18 - x_5 + 51
x_30 - x_8 == x_29 - 77
x_20 - x_11 == x_3 - 76
x_16 - x_7 == x_17 + 102
x_1 + x_21 == x_11 + x_18 + 43
sat
HTB{<redactedddddddddddddddddddddddddddddd>}

Sharing is caring!