Insomni'hack 2022 - GDBUG

Simple serial check algorithm solved with Z3 solver.

Description

Download

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

$ 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