Solving CTF challenges with Z3
This is a writeup of 2 challenges from the PlaidCTF 2025 that could be solved using Z3!
The first one is a crypto challenge called excav8. Let’s get started!
Excav8
As the name suggests, it does in fact has something to do with V8.
This is the chall.py file:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
import subprocess
secret = open('secret.txt').read().strip()
secretbits = ''.join(f'{ord(i):08b}' for i in secret)
output = []
for bit in secretbits:
if bit == '0':
output += [float(i) for i in subprocess.check_output('./d8 gen.js', shell=True).decode().split()]
else:
output += [float(i) for i in subprocess.check_output('node gen.js', shell=True).decode().split()]
for i in output:
print(i)
And this is the gen.js file:
1
2
3
for (let i = 0; i < 24; i++) {
console.log(Math.random());
}
As you can see, it reads from the secret.txt file (which in this case would be the flag) and turns every character in a 8-bit representation. After that, it iterates through each bit: If the bit is zero, it uses the d8 binary to generate 24 random numbers. If the bit is one, then it uses node to generate these 24 random numbers.
The thing to note here is that the V8 engine version being used is from Chrome 13.6.1 and Node’s V8 version to generate the random numbers is a bit older.
Random Number Generation
Why is the versions important?
If you take a look at V8’s: https://github.com/v8/v8/blob/13.6.1/src/base/utils/random-number-generator.h#L111
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// Static and exposed for external use.
static inline double ToDouble(uint64_t state0) {
// Get a random [0,2**53) integer value (up to MAX_SAFE_INTEGER) by dropping
// 11 bits of the state.
double random_0_to_2_53 = static_cast<double>(state0 >> 11);
// Map this to [0,1) by division with 2**53.
constexpr double k2_53{static_cast<uint64_t>(1) << 53};
return random_0_to_2_53 / k2_53;
}
// Static and exposed for external use.
static inline void XorShift128(uint64_t* state0, uint64_t* state1) {
uint64_t s1 = *state0;
uint64_t s0 = *state1;
*state0 = s0;
s1 ^= s1 << 23;
s1 ^= s1 >> 17;
s1 ^= s0;
s1 ^= s0 >> 26;
*state1 = s1;
}
And look at Node’s: https://github.com/nodejs/node/blob/main/deps/v8/src/base/utils/random-number-generator.h#L111
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// Static and exposed for external use.
static inline double ToDouble(uint64_t state0) {
// Exponent for double values for [1.0 .. 2.0)
static const uint64_t kExponentBits = uint64_t{0x3FF0000000000000};
uint64_t random = (state0 >> 12) | kExponentBits;
return base::bit_cast<double>(random) - 1;
}
// Static and exposed for external use.
static inline void XorShift128(uint64_t* state0, uint64_t* state1) {
uint64_t s1 = *state0;
uint64_t s0 = *state1;
*state0 = s0;
s1 ^= s1 << 23;
s1 ^= s1 >> 17;
s1 ^= s0;
s1 ^= s0 >> 26;
*state1 = s1;
}
The way it converts to a floating-point number is different!
This is super important, because using the fact that they are different we can figure out which one was used to generate the numbers!
Using Z3
Z3 is a SMT prover. You can basically give it some constraints and ask it to find a solution that satisfies the given constraints.
This is perfect for this! The way a random number is generated using the Math.random() is exactly it.
So we can basically make a Z3 model that tries to solve for Node’s random number generations (which you can find a lot of models on the internet) and see if it solves it. If we can give it the 24 numbers generated and the given constraints and ask it to solve (basically finding the internal state) and it does in fact solve it, then the bit is a 1!
If we can’t find any solutions, then this must mean the numbers weren’t generated with the given constraints (which means they were generated by the new implementation of V8) and therefore the bit is a 0!
This way we can retrieve all of the bits of the flag and see what it was :)
This is my solve:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
#!/usr/bin/python3
import z3
import struct
import sys
def read_numbers(filename):
with open(filename, 'r') as f:
return [float(line.strip()) for line in f if line.strip()]
def check_batch(reversed_batch):
solver = z3.Solver()
se_state0, se_state1 = z3.BitVecs("se_state0 se_state1", 64)
current_s0, current_s1 = se_state0, se_state1
for num in reversed_batch:
new_s0 = current_s1
s1 = current_s0
s1 ^= s1 << 23
s1 ^= z3.LShR(s1, 17)
s1 ^= new_s0
s1 ^= z3.LShR(new_s0, 26)
new_s1 = s1
float_plus_1 = num + 1
packed = struct.pack('d', float_plus_1)
ulong = struct.unpack('<Q', packed)[0]
mantissa = ulong & ((1 << 52) - 1)
solver.add(z3.LShR(new_s0, 12) == mantissa)
current_s0, current_s1 = new_s0, new_s1
return solver.check() == z3.sat
def main():
numbers = read_numbers('output.txt')
batch_size = 24
batches = [numbers[i:i+batch_size] for i in range(0, len(numbers), batch_size)]
result_bits = []
for batch in batches:
if len(batch) != batch_size:
continue
reversed_batch = batch[::-1]
valid = check_batch(reversed_batch)
result_bits.append('1' if valid else '0')
print('1' if valid else '0')
print(''.join(result_bits))
if __name__ == "__main__":
main()
You must take notice that V8 uses a LIFO cache to generate the numbers. Whenever you ask it to generate a single random number, in fact it generates a lot more and save them on a bucket. This means you basically need to provide the batch of numbers in a reverse order.
This is the result:
1
011001100110110001100001011001110011101000100000010100000100001101010100010001100111101101000010011101010110100101101100010001000011000101101110010001110101111101110110001110000101111101101001001101010101111101010011011101010100001101101000010111110011010001011111011100000110000100110001010011100010111000101110001011100111110100001010011100000110000101110011011100110111011101101111011100100110010000100000011101000110111100100000011100000110000101110010011101000010000000110010001110100010000001101111011000010111000100110001010011010100010000111001001100100110010101110110010100100111001101000100010110100111011001001000
Converting it:
1
2
flag: PCTF{BuilD1nG_v8_i5_SuCh_4_pa1N...}
password to part 2: oaq1MD92evRsDZvH
You can find other implementations of a V8’s random number cracker using Z3 on this YouTube video. This is a great resource and really helped me solving the challenge! You should take a look at it.
Fool’s Gulch
This one is a bit weird. It is a reverse challenge with a aarch64 binary.
The setup
I am on a x86-64 architecture, so this could be a little tricky.
The thing I did to run the binary was the following:
Install the aarch64 libraries on your system
Copy the ld to your chall folder (or anywhere, really).
In my case, it was on /usr/aarch64-linux-gnu/lib/ld-linux-aarch64.so.1.
So I just: cp /usr/aarch64-linux-gnu/lib/ld-linux-aarch64.so.1 aarch64-libs/lib it.
Do the same for the libc:
cp /usr/aarch64-linux-gnu/lib/libc.so.6 aarch64-libs/lib.Now use qemu to emulate the library and pass the libraries location as an argument:
qemu-aarch64 -g 1234 -L aarch64-libs ./prospectors_claim.
You can also add the -g 1234 for debug purposes. On this case, run gdb-multiarch on the binary and connect it to the port 1234 to debug it. Notice that if you do the -g 1234 command, the binary won’t run until you attach gdb to it.
Decompiling it
When you decompile it (I used Ghidra), you will get a HUGE file with a LOT of if conditions:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
undefined8 main(void)
{
byte local_55;
byte local_54;
byte local_53;
byte local_52;
byte local_51;
byte local_50;
byte local_4f;
byte local_4e;
byte local_4d;
byte local_4c;
byte local_4b;
byte local_4a;
byte local_49;
byte local_48;
byte local_47;
byte local_46;
byte local_45;
byte local_44;
byte local_43;
byte local_42;
byte local_41;
byte local_40;
byte local_3f;
byte local_3e;
byte local_3d;
byte local_3c;
byte local_3b;
byte local_3a;
byte local_39;
byte local_38;
byte local_37;
byte local_36;
byte local_35;
byte local_34;
byte local_33;
byte local_32;
char local_31;
byte local_30;
byte local_2f;
char local_2e;
byte local_2d;
byte local_2c;
byte local_2b;
byte local_2a;
byte local_29;
byte local_28;
byte local_27;
byte local_26;
byte local_25;
byte local_24;
byte local_23;
byte local_22;
byte local_21;
byte local_20;
byte local_1f;
byte local_1e;
byte local_1d;
byte local_1c;
byte local_1b;
byte local_1a;
byte local_19;
byte local_18;
byte local_17;
byte local_16;
undefined4 local_14;
local_14 = 0;
setvbuf(_stdout,(char *)0x0,2,0);
printf("=== The Prospector\'s Claim ===\n");
printf("Old Man Jenkins\' map to his modest gold claim has been floating around\n");
printf("Fool\'s Gulch for years. Most folks think it\'s worthless, but you\'ve\n");
printf("noticed something peculiar in the worn-out corners...\n\n");
printf("Enter the claim sequence: ");
fgets((char *)&local_55,0x41,_stdin);
if (local_3a == 0x32) {
bump(&score);
}
if ((local_36 ^ local_3d) == 0xaa) {
bump(&score);
}
if ((byte)(local_36 + local_27) == -0x70) {
bump(&score);
}
if ((byte)(local_1a + local_31) == -0x7f) {
bump(&score);
}
if (local_48 == 0xbe) {
bump(&score);
}
if (local_35 == 100) {
bump(&score);
}
if (local_3b == 0x31) {
bump(&score);
}
if (local_2b == 0x39) {
bump(&score);
}
if ((byte)(local_28 + local_16) == -0x6d) {
bump(&score);
}
if (local_23 == 0x31) {
bump(&score);
}
if ((byte)(local_54 + local_46) == '8') {
bump(&score);
}
if ((local_48 ^ local_32) == 0x8e) {
bump(&score);
}
if ((local_54 ^ local_27) == 0x71) {
bump(&score);
}
if (local_2b == 0xb4) {
bump(&score);
}
if (local_42 == 0x36) {
bump(&score);
}
if (local_39 == local_25) {
bump(&score);
}
if ((local_4b ^ local_34) == 3) {
bump(&score);
}
if (local_37 == 0x76) {
bump(&score);
}
if (local_50 == 0x32) {
bump(&score);
}
if ((local_54 ^ local_25) == 0x85) {
bump(&score);
}
if (local_53 == 0x54) {
bump(&score);
}
if (local_3e == 0xe1) {
bump(&score);
}
if ((local_4c ^ local_1f) == 0x81) {
bump(&score);
}
if ((byte)(local_20 + local_3b) == 'a') {
bump(&score);
}
if ((local_43 ^ local_1c) == 7) {
bump(&score);
}
if ((local_43 ^ local_50) == 0x56) {
bump(&score);
}
if ((byte)(local_47 + local_20) == 'f') {
bump(&score);
}
if ((local_25 ^ local_1d) == 0x54) {
bump(&score);
}
if (local_21 == 0xe5) {
bump(&score);
}
if (local_31 == 'o') {
bump(&score);
}
if ((byte)(local_30 + local_37) == 'f') {
bump(&score);
}
if (local_23 == 0x31) {
bump(&score);
}
if (local_3e == 0x38) {
bump(&score);
}
if (local_2e == '4') {
bump(&score);
}
if ((byte)(local_1d + local_42) == -0x69) {
bump(&score);
}
[...]
if ((local_30 ^ local_53) == 0x67) {
bump(&score);
}
if ((local_1f ^ local_45) == 0x7b) {
bump(&score);
}
if ((local_28 ^ local_43) == 0x91) {
bump(&score);
}
if (local_43 == 100) {
bump(&score);
}
if (score < 0x119) {
if (score < 0xFC) {
if (score < 0x8C) {
printf("\nThat claim\'s as empty as a desert well in August.\n",
printf("Not a speck of gold to be found. Try another spot, prospector!\n");
}
else {
printf("The saloon erupts in laughter as you show off your \'treasure\'.\n");
printf("Keep prospecting - or take up farming instead!\n");
}
}
else {
printf("The assayer laughs you out of his office. \"Come back when you\'ve got\n");
printf("something worth my time, greenhorn!\"\n");
}
}
else {
printf("You\'ve struck a rich vein of gold! Your claim is officially recorded\n");
printf("at the assayer\'s office, and the flag is yours: %s\n",&local_55);
}
return 0;
}
You can change the byte declarations to a char[65] so that things will become much cleaner.
Using Z3
This looks exactly like a Z3 case, right?!
There are lots of constraints and we want to find a solution that satisfies them.
But if you take a closer look, you don’t really need to solve every single one of them. In fact, it is actually impossible to solve them all.
So this basically mean that we want to find a solution good enough to let the score reach something higher than 0x119.
We can do it with Z3!
Optimizing
Z3 also has a really cool way of doing things: Optimizing solutions!
We basically want to get all these if conditions and write them on a Z3 format. We will also make it so that if a condition is satisfied, the score increases. If we can optimize it and get a result higher than 0x119, we solve the problem!
To solve it, I parsed the decompiled file and generated python Z3 conditions in another file like this:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
import re
def generate_conditions(input_file, output_file):
pattern = re.compile(r'if\s*\((.*?)\)\s*{\s*bump\(&score\);', re.DOTALL)
var_pattern = re.compile(r'local_([0-9a-fA-F]{2})')
byte_cast_pattern = re.compile(r'\(byte\)\s*\((.*?)\)')
hex_pattern = re.compile(r'-0x([0-9a-fA-F]+)')
with open(input_file, 'r') as f:
code = f.read()
conditions = pattern.findall(code)
with open(output_file, 'w') as out:
for i, cond in enumerate(conditions, 1):
def var_replacer(match):
offset = int(match.group(1), 16)
index = 0x55 - offset
return f'flag[{index}]'
cond = var_pattern.sub(var_replacer, cond)
cond = byte_cast_pattern.sub(r'(\1 & 0xFF)', cond)
def hex_replacer(match):
val = int(match.group(1), 16)
return f'0x{(0x100 - val):02x}'
cond = hex_pattern.sub(hex_replacer, cond)
out.write(f' # Condition {i}\n')
out.write(f' cond{i} = ({cond})\n')
out.write(f' score += If(cond{i}, 1, 0)\n\n')
if __name__ == '__main__':
generate_conditions('original.c', 'z3_conditions.txt')
This generated a huge file with 400 conditions:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
# Condition 1
cond1 = (flag[27] == 0x32)
score += If(cond1, 1, 0)
# Condition 2
cond2 = ((flag[31] ^ flag[24]) == 0xaa)
score += If(cond2, 1, 0)
# Condition 3
cond3 = ((flag[31] + flag[46] & 0xFF) == 0x90)
score += If(cond3, 1, 0)
# Condition 4
cond4 = ((flag[59] + flag[36] & 0xFF) == 0x81)
score += If(cond4, 1, 0)
# Condition 5
cond5 = (flag[13] == 0xbe)
score += If(cond5, 1, 0)
# Condition 6
cond6 = (flag[32] == 100)
score += If(cond6, 1, 0)
# Condition 7
cond7 = (flag[26] == 0x31)
score += If(cond7, 1, 0)
[...]
# Condition 392
cond392 = (flag[46] == flag[38])
score += If(cond392, 1, 0)
# Condition 393
cond393 = ((flag[48] ^ flag[61]) == 5)
score += If(cond393, 1, 0)
# Condition 394
cond394 = (flag[12] == 0x56)
score += If(cond394, 1, 0)
# Condition 395
cond395 = ((flag[44] ^ flag[28]) == 0x51)
score += If(cond395, 1, 0)
# Condition 396
cond396 = (flag[45] == 0x37)
score += If(cond396, 1, 0)
# Condition 397
cond397 = ((flag[37] ^ flag[2]) == 0x67)
score += If(cond397, 1, 0)
# Condition 398
cond398 = ((flag[54] ^ flag[16]) == 0x7b)
score += If(cond398, 1, 0)
# Condition 399
cond399 = ((flag[45] ^ flag[18]) == 0x91)
score += If(cond399, 1, 0)
# Condition 400
cond400 = (flag[18] == 100)
score += If(cond400, 1, 0)
We can just write the solve now and paste it there. I also added some constraints that tell it that the first 5 characters are “PCTF{“ and the last one is a “}”:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
from z3 import *
def solve_flag():
opt = Optimize()
flag = [BitVec(f'flag_{i}', 8) for i in range(0x41)]
opt.add(flag[0] == ord('P'))
opt.add(flag[1] == ord('C'))
opt.add(flag[2] == ord('T'))
opt.add(flag[3] == ord('F'))
opt.add(flag[4] == ord('{'))
opt.add(flag[0x40] == ord('}'))
for c in flag:
opt.add(Or(And(c >= ord(' '), c <= ord('~')), c == 0))
score = 0
# LOL
# Condition 1
cond1 = (flag[27] == 0x32)
score += If(cond1, 1, 0)
# Condition 2
cond2 = ((flag[31] ^ flag[24]) == 0xaa)
score += If(cond2, 1, 0)
# Condition 3
cond3 = ((flag[31] + flag[46] & 0xFF) == 0x90)
score += If(cond3, 1, 0)
# Condition 4
cond4 = ((flag[59] + flag[36] & 0xFF) == 0x81)
score += If(cond4, 1, 0)
# Condition 5
cond5 = (flag[13] == 0xbe)
score += If(cond5, 1, 0)
# Condition 6
cond6 = (flag[32] == 100)
score += If(cond6, 1, 0)
# Condition 7
cond7 = (flag[26] == 0x31)
score += If(cond7, 1, 0)
# Condition 8
cond8 = (flag[42] == 0x39)
score += If(cond8, 1, 0)
# Condition 9
cond9 = ((flag[45] + flag[63] & 0xFF) == 0x93)
score += If(cond9, 1, 0)
# Condition 10
cond10 = (flag[50] == 0x31)
score += If(cond10, 1, 0)
[...]
# Condition 398
cond398 = ((flag[54] ^ flag[16]) == 0x7b)
score += If(cond398, 1, 0)
# Condition 399
cond399 = ((flag[45] ^ flag[18]) == 0x91)
score += If(cond399, 1, 0)
# Condition 400
cond400 = (flag[18] == 100)
score += If(cond400, 1, 0)
opt.maximize(score)
if opt.check() == sat:
model = opt.model()
solution = ''.join([chr(model.eval(flag[i]).as_long()) for i in range(0x41)])
print(f"Found flag: {solution}")
else:
print("No solution found")
if __name__ == "__main__":
solve_flag()
Just like that, we get the flag: Found flag: PCTF{24d16126d6739d6ada82b125534d2ae2324b39ed72e5a1200c5ac96200}
Let’s try it on the binary:
1
2
3
4
5
6
7
8
9
10
11
$ qemu-aarch64 -L aarch64-libs ./prospectors_claim
=== The Prospector's Claim ===
Old Man Jenkins' map to his modest gold claim has been floating around
Fool's Gulch for years. Most folks think it's worthless, but you've
noticed something peculiar in the worn-out corners...
Enter the claim sequence: PCTF{24d16126d6739d6ada82b125534d2ae2324b39ed72e5a1200c5ac96200}
🌟 PAYDIRT! 🌟
You've struck a rich vein of gold! Your claim is officially recorded
at the assayer's office, and the flag is yours: PCTF{24d16126d6739d6ada82b125534d2ae2324b39ed72e5a1200c5ac96200}
We solved it!
Thanks for reading until here :)