This is the solution of the challenge “GDBUG” given during the Insomni’hack 2022 CTF . It was a simple serial check algorithm solved with Z3 solver.
Description
Download
Details
Points: 120
Category: reverse
Solution
The file is a standard x86-64 binary:
1
2
$ file reee
GDBug: ELF 64-bit LSB pie executable, x86-64, version 1 ( SYSV) , dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[ sha1]= f78a32c0f9b8933b44dc1ab0b966e22bfa343a93, for GNU/Linux 3.2.0, not stripped
And it’s waiting an argument:
1
2
3
4
5
6
7
8
9
10
$ ./GDBug
_/_/_/ _/_/_/ _/_/_/
_/ _/ _/ _/ _/ _/ _/ _/_/_/
_/ _/_/ _/ _/ _/_/_/ _/ _/ _/ _/
_/ _/ _/ _/ _/ _/ _/ _/ _/ _/
_/_/_/ _/_/_/ _/_/_/ _/_/_/ _/_/_/
_/
_/_/
Usage: ./GDBug <serial>
I opened it in ghidra:
ghidra
There is anti-debug mechanisms but the computation of the serial was straight forward. The serial has the for XXXX-XXXX-XXXX-XXXX . The sum of all the characters added to 0x539 should give 0xb38. Thus, for this challenge I decided to give z3 a chance:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
from z3 import IntVector , Solver , Or , And
length = 24
serial = IntVector ( "a" , length )
s = Solver ()
for i in range ( length ):
if i != 4 and i != 9 and i != 14 and i != 19 :
digits = And ( serial [ i ] > 47 , serial [ i ] < 58 )
lower = And ( serial [ i ] > 96 , serial [ i ] < 123 )
upper = And ( serial [ i ] > 64 , serial [ i ] < 91 )
s . add ( Or ( digits , lower , upper ))
else :
s . add ( serial [ i ] == ord ( "-" ))
sum = 0x539 + sum ([ i for i in serial ])
s . add ( sum == 0xb38 )
if s . check ():
m = s . model ()
for i in range ( length ):
print ( chr ( m [ serial [ i ]] . as_long ()), end = "" )
print ()
It outputs a serial:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
$ python3 solve-z3.py
ZAAA-AAAA-AAAA-AAAA-AFZA
$ ./GDBug ZAAA-AAAA-AAAA-AAAA-AFZA
_/_/_/ _/_/_/ _/_/_/
_/ _/ _/ _/ _/ _/ _/ _/_/_/
_/ _/_/ _/ _/ _/_/_/ _/ _/ _/ _/
_/ _/ _/ _/ _/ _/ _/ _/ _/ _/
_/_/_/ _/_/_/ _/_/_/ _/_/_/ _/_/_/
_/
_/_/
[ +] Checking serial ZAAA-AAAA-AAAA-AAAA-AFZA
[ -] Registration successful
[ -] Your flag is INS{ ZAAA-AAAA-AAAA-AAAA-AFZA}
There were a lot of possible solutions, each one works.