# Insomni'hack 2022 - GDBUG

Simple serial check algorithm solved with Z3 solver.

### Details

Points: 120

Category: reverse

### Solution

The file is a standard x86-64 binary:

$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: $  ./GDBug
_/_/_/  _/_/_/    _/_/_/
_/        _/    _/  _/    _/  _/    _/    _/_/_/
_/  _/_/  _/    _/  _/_/_/    _/    _/  _/    _/
_/    _/  _/    _/  _/    _/  _/    _/  _/    _/
_/_/_/  _/_/_/    _/_/_/      _/_/_/    _/_/_/
_/
_/_/

Usage: ./GDBug <serial>



I opened it in 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:

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)
else:

sum =  0x539 + sum([i for i in serial])

if s.check():
m = s.model()
for i in range(length):
print(chr(m[serial[i]].as_long()), end = "")
print()


It outputs a serial:

$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.

Written on February 21, 2022