Writeup: Sharky CTF 2020 - Z3 Robot

Information

  • category : reverse
  • points : 188

Description

I made a robot that can only communicate with “z3”. He locked himself and now he is asking me for a password !

1 file: z3_robot

Writeup

We’re given a file named z3_robot.

1
2
3
$ file z3_robot 
z3_robot: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2,
for GNU/Linux 3.2.0, BuildID[sha1]=bce2975b632a64a4c4af2009a81f41f43619dad1, not stripped

So it’s an ELF binary, 64 bit not stripped. If we run it we get the following message:

1
2
3
4
5
6
7
8
9
      \_/
(* *)
__)#(__
( )...( )(_)
|| |_| ||//
>==() | | ()/
_(___)_
[-] [-] Z3 robot says :z3 Z3Z3z3 Zz3 zz33 3Z Passz3rd? Zz3 zZ3 3Z Z3Z3z
-> # WAITING FOR INPUT HERE

So I opened it with Cutter and I started analyzing main:

The main read our input with fgets and then pass it as argument to check_flag.
If check_flag function returns 1, the challenge is solved.

The graph overview of check_flag is the following (not very short):

Now let’s see the decompiled of check_flag (with r2ghidra-dec):

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
// Cleaned version
undefined8 check_flag(int64_t arg1)
{
undefined8 uVar1;
uint8_t uVar2;
int64_t var_8h;
if (((((*(arg1 + 0x14) ^ 0x2b) == *(arg1 + 7)) &&
(*(arg1 + 0x15) - *(arg1 + 3) == -0x14)) &&
(*(arg1 + 2) >> 6 == '\0')) &&
((*(arg1 + 0xd) == 't' && ((*(arg1 + 0xb) & 0x3fffffffU) == 0x5f)))) &&
((uVar2 = (*(arg1 + 0x11) >> 7) >> 5,
*(arg1 + 7) >> ((*(arg1 + 0x11) + uVar2 & 7) - uVar2 & 0x1f) == 5 &&
(((*(arg1 + 6) ^ 0x53) == *(arg1 + 0xe) && (*(arg1 + 8) == 'z')))))) &&
((uVar2 = (*(arg1 + 9) >> 7) >> 5,
*(arg1 + 5) << ((*(arg1 + 9) + uVar2 & 7) - uVar2 & 0x1f) == 0x188 &&
((((*(arg1 + 0x10) - *(arg1 + 7) == 0x14 &&
(uVar2 = (*(arg1 + 0x17) >> 7) >> 5,
*(arg1 + 7) << ((*(arg1 + 0x17) + uVar2 & 7) - uVar2 & 0x1f) == 0xbe)) &&

// MANY MORE LINES OF CONSTRAINTS

(uVar2 = (*(arg1 + 0x16) >> 7) >> 5,
*(arg1 + 7) << ((*(arg1 + 0x16) + uVar2 & 7) - uVar2 & 0x1f) == 0x17c)) &&
(*(arg1 + 0x16) == ':')) &&
((*(arg1 + 0x10) == 's' && ((*(arg1 + 0x17) ^ 0x1d) == *(arg1 + 0x12)))))))))
)))) && (((*(arg1 + 0xe) + *(arg1 + 0x17) == 0x59 &&
(((*(arg1 + 2) & *(arg1 + 5)) == 0x30 &&
((*(arg1 + 0xf) & 0x9fU) == 0x1f)))) &&
((*(arg1 + 4) == 's' &&
(((*(arg1 + 0x17) ^ 0x4a) == *arg1 &&
((*(arg1 + 6) ^ 0x3c) == *(arg1 + 0xb))))) {
uVar1 = 1;
} else {
uVar1 = 0;
}
return uVar1;
}

To solve the challenge we have to make all the constraints inside the if true.

There are two possible ways to solve those constraints:

  1. angr
  2. z3

Angr Solution

The main issues an fgets of 0x19 (25) bytes, so our input must be of that dimension.

1
2
3
4
5
proj = angr.Project("z3_robot",load_options={"auto_load_libs": False},
main_opts={"base_addr": 0})
flag = [claripy.BVS(f"c_{i}", 8) for i in range(0x19)]
flag_ast = claripy.Concat(*flag)
state = proj.factory.entry_state(stdin=flag_ast)

We add the constraints that makes the flag readable:

1
2
3
for f in flag:
state.solver.add(f >= 0x20)
state.solver.add(f < 0x7f)

Then we launch the exploration to find in the stdout the string “Well done”:

1
2
3
simgr = proj.factory.simulation_manager(state)
print("start exploring")
simgr.explore(find=lambda s: b"Well" in s.posix.dumps(1))

And finally:

1
2
3
found = simgr.found[0]
valid_flag = found.solver.eval(flag_ast, cast_to=bytes)
print(valid_flag)

The final exploit is:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
#!/usr/bin/env python3

import angr
import claripy

proj = angr.Project("z3_robot",load_options={"auto_load_libs": False},
main_opts={"base_addr": 0})
flag = [claripy.BVS(f"c_{i}", 8) for i in range(0x19)]
flag_ast = claripy.Concat(*flag)
state = proj.factory.entry_state(stdin=flag_ast)
for f in flag:
state.solver.add(f >= 0x20)
state.solver.add(f < 0x7f)

simgr = proj.factory.simulation_manager(state)
print("start exploring")
simgr.explore(find=lambda s: b"Well" in s.posix.dumps(1))

if len(simgr.found) > 0:
found = simgr.found[0]
valid_flag = found.solver.eval(flag_ast, cast_to=bytes)
print(valid_flag)
else:
print("unlucky")

Z3 Solution

Another way to solve the challenge is to use z3.

Since the ghidra’s decompiled of check_flag is a bit messy we can use the IDA’s one, which is more polished:

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
return ((unsigned __int8)a1[20] ^ 0x2B) == a1[7]
&& a1[21] - a1[3] == -20
&& !(a1[2] >> 6)
&& a1[13] == 116
&& 4 * a1[11] == 380
&& a1[7] >> (a1[17] % 8) == 5
&& ((unsigned __int8)a1[6] ^ 0x53) == a1[14]
&& a1[8] == 122
&& a1[5] << (a1[9] % 8) == 392
&& a1[16] - a1[7] == 20
&& a1[7] << (a1[23] % 8) == 190
&& a1[2] - a1[7] == -43
&& a1[21] == 95
&& ((unsigned __int8)a1[2] ^ 0x47) == a1[3]
&& *a1 == 99
&& a1[13] == 116
&& (a1[20] & 0x45) == 68
&& (a1[8] & 0x15) == 16
&& a1[12] == 95
&& a1[4] >> 4 == 7
&& a1[13] == 116
&& *a1 >> (*a1 % 8) == 12
&& a1[10] == 95
&& (a1[8] & 0xAC) == 40
&& a1[16] == 115
&& (a1[22] & 0x1D) == 24
&& a1[9] == 51
&& a1[5] == 49
&& 4 * a1[19] == 456
&& a1[20] >> 6 == 1
&& a1[7] >> 1 == 47
&& a1[1] == 108
&& a1[3] >> 4 == 7
&& (a1[19] & 0x49) == 64
&& a1[4] == 115
&& ((unsigned __int8)a1[2] & (unsigned __int8)a1[11]) == 20
&& *a1 == 99
&& a1[4] + a1[5] == 164
&& a1[15] << 6 == 6080
&& ((unsigned __int8)a1[10] ^ 0x2B) == a1[17]
&& ((unsigned __int8)a1[12] ^ 0x2C) == a1[4]
&& a1[19] - a1[21] == 19
&& a1[12] == 95
&& a1[15] >> 1 == 47
&& a1[19] == 114
&& a1[17] + a1[18] == 168
&& a1[22] == 58
&& ((unsigned __int8)a1[23] & (unsigned __int8)a1[21]) == 9
&& a1[6] << (a1[19] % 8) == 396
&& a1[3] + a1[7] == 210
&& (a1[22] & 0xED) == 40
&& (a1[12] & 0xAC) == 12
&& ((unsigned __int8)a1[18] ^ 0x6B) == a1[15]
&& (a1[16] & 0x7A) == 114
&& (*a1 & 0x39) == 33
&& ((unsigned __int8)a1[6] ^ 0x3C) == a1[21]
&& a1[20] == 116
&& a1[19] == 114
&& a1[12] == 95
&& a1[2] == 52
&& a1[23] == 41
&& a1[10] == 95
&& ((unsigned __int8)a1[22] & (unsigned __int8)a1[9]) == 50
&& a1[3] + a1[2] == 167
&& a1[17] - a1[14] == 68
&& a1[21] == 95
&& ((unsigned __int8)a1[19] ^ 0x2D) == a1[10]
&& 4 * a1[12] == 380
&& a1[6] & 0x40
&& ((unsigned __int8)a1[12] & (unsigned __int8)a1[22]) == 26
&& a1[7] << (a1[19] % 8) == 380
&& ((unsigned __int8)a1[20] ^ 0x4E) == a1[22]
&& a1[6] == 99
&& a1[12] == a1[7]
&& a1[19] - a1[13] == -2
&& a1[14] >> 4 == 3
&& (a1[12] & 0x38) == 24
&& a1[8] << (a1[10] % 8) == 15616
&& a1[20] == 116
&& a1[6] >> (a1[22] % 8) == 24
&& a1[22] - a1[5] == 9
&& a1[7] << (a1[22] % 8) == 380
&& a1[22] == 58
&& a1[16] == 115
&& ((unsigned __int8)a1[23] ^ 0x1D) == a1[18]
&& a1[23] + a1[14] == 89
&& ((unsigned __int8)a1[5] & (unsigned __int8)a1[2]) == 48
&& (a1[15] & 0x9F) == 31
&& a1[4] == 115
&& ((unsigned __int8)a1[23] ^ 0x4A) == *a1
&& ((unsigned __int8)a1[6] ^ 0x3C) == a1[11];

What we need to do is:

  • remove the casting to (unsigned __int8).
  • change the pointer to the first element of the array *a1 to a1[0].
  • need to adapts the bit a bit operations a bit (:D).

Final exploit:

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
#!/usr/bin/env python3

from z3 import *

# List of BitVec
a1 = [BitVec(f'{i}', 8) for i in range(0x19)]
s = Solver()

# Constraints
s.add((a1[20] ^ 0x2B) == a1[7])
s.add(a1[21] - a1[3] == -20)
s.add((a1[2] >> 6) == 0)
s.add(a1[13] == 116)
s.add(4 * a1[11] == 380)
s.add(a1[7] >> (a1[17] % 8) == 5)
s.add((a1[6] ^ 0x53) == a1[14])
s.add(a1[8] == 122)
s.add(a1[5] << (a1[9] % 8) == 392)
s.add(a1[16] - a1[7] == 20)
s.add(a1[7] << (a1[23] % 8) == 190)
s.add(a1[2] - a1[7] == -43)
s.add(a1[21] == 95)
s.add((a1[2] ^ 0x47) == a1[3])
s.add(a1[0] == 99)
s.add(a1[13] == 116)
s.add((a1[20] & 0x45) == 68)
s.add((a1[8] & 0x15) == 16)
s.add(a1[12] == 95)
s.add(a1[4] >> 4 == 7)
s.add(a1[13] == 116)
s.add(a1[0] >> (a1[0] % 8) == 12)
s.add(a1[10] == 95)
s.add((a1[8] & 0xAC) == 40)
s.add(a1[16] == 115)
s.add((a1[22] & 0x1D) == 24)
s.add(a1[9] == 51)
s.add(a1[5] == 49)
s.add(4 * a1[19] == 456)
s.add(a1[20] >> 6 == 1)
s.add(a1[7] >> 1 == 47)
s.add(a1[1] == 108)
s.add(a1[3] >> 4 == 7)
s.add((a1[19] & 0x49) == 64)
s.add(a1[4] == 115)
s.add(a1[2] & a1[11] == 20)
s.add(a1[0] == 99)
s.add(a1[4] + a1[5] == 164)
s.add(a1[15] << 6 == 6080)
s.add(a1[10] ^ 0x2B == a1[17])
s.add(a1[12] ^ 0x2C == a1[4])
s.add(a1[19] - a1[21] == 19)
s.add(a1[12] == 95)
s.add(a1[15] >> 1 == 47)
s.add(a1[19] == 114)
s.add(a1[17] + a1[18] == 168)
s.add(a1[22] == 58)
s.add(a1[23] & a1[21] == 9)
s.add(a1[6] << (a1[19] % 8) == 396)
s.add(a1[3] + a1[7] == 210)
s.add((a1[22] & 0xED) == 40)
s.add((a1[12] & 0xAC) == 12)
s.add((a1[18] ^ 0x6B) == a1[15])
s.add((a1[16] & 0x7A) == 114)
s.add((a1[0] & 0x39) == 33)
s.add((a1[6] ^ 0x3C) == a1[21])
s.add(a1[20] == 116)
s.add(a1[19] == 114)
s.add(a1[12] == 95)
s.add(a1[2] == 52)
s.add(a1[23] == 41)
s.add(a1[10] == 95)
s.add((a1[22] & a1[9]) == 50)
s.add(a1[3] + a1[2] == 167)
s.add(a1[17] - a1[14] == 68)
s.add(a1[21] == 95)
s.add((a1[19] ^ 0x2D) == a1[10])
s.add(4 * a1[12] == 380)
s.add(a1[6] & 0x40 >= 1)
s.add((a1[12] & a1[22]) == 26)
s.add(a1[7] << (a1[19] % 8) == 380)
s.add((a1[20] ^ 0x4E) == a1[22])
s.add(a1[6] == 99)
s.add(a1[12] == a1[7])
s.add(a1[19] - a1[13] == -2)
s.add(a1[14] >> 4 == 3)
s.add((a1[12] & 0x38) == 24)
s.add(a1[8] << (a1[10] % 8) == 15616)
s.add(a1[20] == 116)
s.add(a1[6] >> (a1[22] % 8) == 24)
s.add(a1[22] - a1[5] == 9)
s.add(a1[7] << (a1[22] % 8) == 380)
s.add(a1[22] == 58)
s.add(a1[16] == 115)
s.add((a1[23] ^ 0x1D) == a1[18])
s.add(a1[23] + a1[14] == 89)
s.add((a1[5] & a1[2]) == 48)
s.add((a1[15] & 0x9F) == 31)
s.add(a1[4] == 115)
s.add((a1[23] ^ 0x4A) == a1[0])
s.add((a1[6] ^ 0x3C) == a1[11])

print(s.check())
model = s.model()
flag = ''.join([chr(int(str(model[a1[i]]))) for i in range(len(model))])
print(flag)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
$ ./z3_robot 
\_/
(* *)
__)#(__
( )...( )(_)
|| |_| ||//
>==() | | ()/
_(___)_
[-] [-] Z3 robot says :z3 Z3Z3z3 Zz3 zz33 3Z Passz3rd? Zz3 zZ3 3Z Z3Z3z
-> cl4ss1c_z3___t0_st4rt_:)
\_/
(* *)
__)#(__
( )...( )(_)
|| |_| ||//
>==() | | ()/
_(___)_
[-] [-] Z3 robot says :
Well done, valdiate with shkCTF{cl4ss1c_z3___t0_st4rt_:)}

Flag

shkCTF{cl4ss1c_z3___t0_st4rt_:)}