Spooky License

4 minutes to read

We are given a binary called spookylicense:

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

Reverse engineering

If we use Ghidra, we will see this main function:

int main(int argc, char **argv) {
  int ret;
  size_t length;
  char *data;

  if (argc == 2) {
    length = strlen(argv[1]);

    if (length == 32) {
      data = argv[1];

      if ((((((((data[0x1d] == (char) ((data[5] - data[3]) + 0x46)) &&
               ((char) (data[2] + data[0x16]) == (char) (data[0xd] + 0x7b))) &&
              ((char) (data[0xc] + data[4]) == (char) (data[5] + 0x1c))) &&
             ((((char) (data[0x19] * data[0x17]) == (char) (*data + data[0x11] + 0x17) &&
               ((char) (data[0x1b] * data[1]) == (char) (data[5] + data[0x16] - 0x15))) &&
              (((char) (data[9] * data[0xd]) == (char) (data[0x1c] * data[3] - 9) &&
               ((data[9] == 0x70 && ((char) (data[0x13] + data[0x15]) == (char) (data[6] - 0x80)))))))
             )) && (data[0x10] == (char) ((data[0xf] - data[0xb]) + 0x30))) &&
           (((((((char) (data[7] * data[0x1b]) == (char) (data[1] * data[0xd] + 0x2d) &&
                (data[0xd] == (char) (data[0x12] + data[0xd] - 0x65))) &&
               ((char) (data[0x14] - data[8]) == (char) (data[9] + 0x7c))) &&
              ((data[0x1f] == (char) ((data[8] - data[0x1f]) - 0x79) &&
               ((char) (data[0x14] * data[0x1f]) == (char) (data[0x14] + 0x04))))) &&
             ((char) (data[0x18] - data[0x11]) == (char) (data[0x15] + data[8] - 0x17))) &&
            ((((char) (data[7] + data[5]) == (char) (data[5] + data[0x1d] + 0x2c) &&
              ((char) (data[0xc] * data[10]) == (char) ((data[1] - data[0xb]) - 0x24))) &&
             ((((char) (data[0x1f] * *data) == (char) (data[0x1a] - 0x1b) &&
               ((((char) (data[1] + data[0x14]) == (char) (data[10] - 0x7d) &&
                 (data[0x12] == (char) (data[0x1b] + data[0xe] + 0x02))) &&
                ((char) (data[0x1e] * data[0xb]) == (char) (data[0x15] + 0x44))))) &&
              ((((char) (data[5] * data[0x13]) == (char) (data[1] - 0x2c) &&
                ((char) (data[0xd] - data[0x1a]) == (char) (data[0x15] - 0x7f))) &&
               (data[0x17] == (char) ((data[0x1d] - *data) + 0x58))))))))))) &&
          (((data[0x13] == (char) (data[8] * data[0xd] - 0x17) &&
            ((char) (data[6] + data[0x16]) == (char) (data[3] + 0x53))) &&
           ((data[0xc] == (char) (data[0x1a] + data[7] - 0x72) &&
            (((data[0x10] == (char) ((data[0x12] - data[5]) + 0x33) &&
              ((char) (data[0x1e] - data[8]) == (char) (data[0x1d] - 0x4d))) &&
             ((char) (data[0x14] - data[0xb]) == (char) (data[3] - 0x4c))))))))) &&
         (((char) (data[0x10] - data[7]) == (char) (data[0x11] + 0x66) &&
          ((char) (data[1] + data[0x15]) == (char) (data[0xb] + data[0x12] + 0x2b))))) {
        puts("License Correct");
        ret = 0;
      } else {
        puts("License Invalid");
        ret = -1;
      }
    } else {
      puts("Invalid License Format");
      ret = -1;
    }
  } else {
    puts("./spookylicence <license>");
    ret = -1;
  }

  return ret;
}

Here we see that we need to add a license as a command line argument. Moreover, the length of the license string must be 32.

Then, there is a huge if statement that performs many checks on the license characters.

`z3` solver

This is a perfect situation to use z3, we only need to define some variables in a model and add the constraints, so that z3 can find a solution:

#!/usr/bin/env python3

from z3 import BitVec, Solver

a = [BitVec(f'a{i}', 8) for i in range(32)]
s = Solver()

s.add(a[0x1d] == a[5] - a[3] + 0x46)
s.add(a[2] + a[0x16] == a[0xd] + 0x7b)
s.add(a[0xc] + a[4] == a[5] + 0x1c)
s.add(a[0x19] * a[0x17] == a[0] + a[0x11] + 0x17)
s.add(a[0x1b] * a[1] == a[5] + a[0x16] - 0x15)
s.add(a[9] * a[0xd] == a[0x1c] * a[3] - 9)
s.add(a[9] == 0x70)
s.add(a[0x13] + a[0x15] == a[6] - 0x80)
s.add(a[0x10] == a[0xf] - a[0xb] + 0x30)
s.add(a[7] * a[0x1b] == a[1] * a[0xd] + 0x2d)
s.add(a[0xd] == a[0x12] + a[0xd] - 0x65)
s.add(a[0x14] - a[8] == a[9] + 0x7c)
s.add(a[0x1f] == a[8] - a[0x1f] - 0x79)
s.add(a[0x14] * a[0x1f] == a[0x14] + 0x04)
s.add(a[0x18] - a[0x11] == a[0x15] + a[8] - 0x17)
s.add(a[7] + a[5] == a[5] + a[0x1d] + 0x2c)
s.add(a[0xc] * a[10] == a[1] - a[0xb] - 0x24)
s.add(a[0x1f] * a[0] == a[0x1a] - 0x1b)
s.add(a[1] + a[0x14] == a[10] - 0x7d)
s.add(a[0x12] == a[0x1b] + a[0xe] + 0x02)
s.add(a[0x1e] * a[0xb] == a[0x15] + 0x44)
s.add(a[5] * a[0x13] == a[1] - 0x2c)
s.add(a[0xd] - a[0x1a] == a[0x15] - 0x7f)
s.add(a[0x17] == a[0x1d] - a[0] + 0x58)
s.add(a[0x13] == a[8] * a[0xd] - 0x17)
s.add(a[6] + a[0x16] == a[3] + 0x53)
s.add(a[0xc] == a[0x1a] + a[7] - 0x72)
s.add(a[0x10] == a[0x12] - a[5] + 0x33)
s.add(a[0x1e] - a[8] == a[0x1d] - 0x4d)
s.add(a[0x14] - a[0xb] == a[3] - 0x4c)
s.add(a[0x10] - a[7] == a[0x11] + 0x66)
s.add(a[1] + a[0x15] == a[0xb] + a[0x12] + 0x2b)

s.check()
model = s.model()

flag = ''.join(chr(model[i].as_long()) for i in a)
print(flag)

Flag

If we run the above code, we will find the flag:

$ python3 solve.py
HTB{The_sp0000000key_liC3nC3K3Y}

The full script can be found in here: solve.py.

Reverse engineering

z3 solver

Flag

`z3` solver