TamuCTF 2019 - Cr4ckZ33C0d3 (reverse)

This challenge was a key validator we needed to keygen. I used z3 like in the picoCTF challenge keygen me 2 in order to satisfy all the constraints.

 

nc rev.tamuctf.com 8189   

Difficulty: hard 
prodkey

check_0X

First we have the function verify_key(char *) who is verifying a lot of constraints. If one of theses is not satisfied then the flag will not be printed. The only way to get the flag is to satisfied each constraints split in 15 functions.

_BOOL8 __fastcall verify_key(const char *a1)
{
  size_t v1; // rsi
  _BOOL8 result; // rax
  bool v3; // al

  if ( strlen(a1) > 0x1C )
  {
    v3 = (unsigned __int8)check_01(a1)
      && (unsigned __int8)check_02(a1)
      && (unsigned __int8)check_03(a1)
      && (unsigned __int8)check_04(a1)
      && (unsigned __int8)check_05(a1)
      && (unsigned __int8)check_06(a1)
      && (unsigned __int8)check_07(a1)
      && (unsigned __int8)check_08(a1)
      && (unsigned __int8)check_09(a1)
      && (unsigned __int8)check_0A(a1)
      && (unsigned __int8)check_0B(a1)
      && (unsigned __int8)check_0C(a1)
      && (unsigned __int8)check_0D(a1)
      && (unsigned __int8)check_0E(a1)
      && (unsigned __int8)check_0F(a1);
    result = v3;
  }
  else
  {
    v1 = strlen(a1);
    printf("Key was too short %d.\n", v1);
    result = 0LL;
  }
  return result;
}

The flag has to be longer than 28 chars. But in fact, once all the constraints extracted I saw the last checked char is the 29th so it will be our key length.

 

For the last challenge I did with z3 I only used the IntVector object, but because some constraints like 

v1 = (unsigned int)((a1[15] + a1[4] + a1[27] - 18) >> 31) >> 28;
return (((_BYTE)v1 + a1[15] + a1[4] + a1[27] - 18) & 0xF) - v1 == 8;

require bits operations we need to use the BitVec object. You can define a 32 bits objects or 64 both will work.

 

I defined 29 objects inside a list in order to retrieve the same behavior like and IntVector of size 29.

#!/usr/bin/python2
from z3 import *
from pwn import remote, log

s =  Solver()
flag = [ BitVec('b%i' % i, 32) for i in range(0, 30) ]

 

Our key must only contains ASCII char so wee need only char greater than 47 and smaller than 123. The "-" ASCII number is 45 so we need to add a condition in order to allow it 

for i in range(0, 30):
    s.add(Or(flag[i] >= 48, flag[i] == 45))
    s.add(flag[i] < 123)

Then we add all our constraints to the solver

s.add(flag[0] == 77)
s.add(flag[5] == 45)
s.add(flag[11] == 45)
s.add(flag[17] == 45)
s.add(flag[23] == 45)
s.add(flag[20] == 66)
s.add(flag[21] == 66)

s.add((flag[1] - 48) <= 9)
s.add((flag[4] - 48) <= 9)
s.add((flag[6] - 48) <= 9)
s.add((flag[9] - 48) <= 9)
s.add((flag[15] - 48) <= 9)
s.add((flag[18] - 48) <= 9)
s.add((flag[22] - 48) <= 9)
s.add((flag[27] - 48) <= 9)
s.add((flag[28] - 48) <= 9)

s.add(flag[4] - 48 == 2 * (flag[1] - 48) + 1)
s.add(flag[4] - 48 > 7)
s.add(flag[9] == flag[4] - (flag[1] - 48) + 2)

s.add((flag[27] + flag[28]) % 13 == 8)
s.add((flag[27] + flag[22]) % 22 == 18)
s.add((flag[18] + flag[22]) % 11 == 5)
s.add((flag[22] + flag[28] + flag[18]) % 26 == 4)
s.add((flag[1] + flag[4] * flag[6]) % 41 == 5)

s.add((((((flag[15] - flag[28]) >> 31) >> 30) + flag[15] - flag[28]) & 3)-(((flag[15] - flag[28]) >> 31) >> 30) ==1 )
s.add((((((flag[22] + flag[4]) >> 31) >> 30) + flag[22] + flag[4]) & 3)- (((flag[22] + flag[4]) >> 31) >> 30) == 3 )
s.add((((((flag[15] + flag[4] + flag[27] - 18) >> 31) >> 28) + flag[15]  + flag[4] + flag[27] - 18) & 0xf) - (((flag[15] + flag[4] + flag[27] - 18) >> 31) >> 28) == 8)

s.add(((0 + flag[28] - flag[29]) & 1 ) - 0 == 1)
s.add((flag[6] + flag[15] * flag[19] ) % 10 == 1)

 

For the constraints v1 = *(char *)(a1 + 28) < *(char *)(a1 + 9); I stated that it will be false so v1 will be 0. It may have been true but It worked like this, if it did not work I would have set it to 1 and tried it again.

 

Then we cross our finger, tighten our butt and compute our models

if s.check() != unsat:
    mod = s.model()
    flag_plain = ""
    log.success("Equation solved")
    for i in range(30):
        x = mod[flag[i]].as_long()
        flag_plain += chr(x)


    server = remote("rev.tamuctf.com", 8189)
    log.success("Keygen {}".format(flag_plain))
    server.sendline(flag_plain)
    print server.readall()
switch :: pain $ python xploit_prodkey.py 
[+] Equation solved
[+] Opening connection to rev.tamuctf.com on port 8189: Done
[+] Keygen M4449-84474-44494-6UBB2-444883
[+] Receiving all data: Done (63B)
[*] Closed connection to rev.tamuctf.com port 8189

Please Enter a product key to continue: 
gigem{z3_b3st_thr33}