PicoCTF 2018 - Keygen-me 2 (Reverse)

 

The software has been updated. Can you find us a new product key for the program in /problems/keygen-me-2_3_5e45e804e9c1a9de2f8124266b173c35
A binary and the hint "z3"

 

Main

Like the first Keygen-Me, we see through the main function that we need to provide a 16 bytes key matching [A-Z0-9].

Only if the function validate_key return True will the flag be displayed.

 

_BOOL4 __cdecl check_valid_char(char a1)
{
  return a1 > 47 && a1 <= 57 || a1 > 64 && a1 <= 90;
}

 

validate_key(char *s)

This function take our input and apply 12 constraints on it, we quickly see that each key_constraint must return true. So we have to determinate how each of theses function could return true !

 

 

key_constraint_XX

The pictures just below are showing how each constraints functions works, they are really similars but are checking different char of the key.

 

Making the equation

We will need z3 for solve this equation. Z3 is a Theorem Prover we can use through it python lib, we can found the project here and some documentations about.

 

I always wanted to learn about but never did it, until I really need it for this challenge, thank's to twitter community I could get some help quickly to understand the basics. Thanks again guys !

 

Oh I forgot, in each key_constraints function two functions are used : mod and ord. They are trivial function but I quickly implemented in Python in order to be sure to get the exact same behavior

 

def _ord(c):
    if c > 47 and c <= 57:
        return c - 48
    else:
        return c - 55

def _mod(a, b):
    if a % b >= 0:
        return a % b
    else:
        return a % b + b

 

The we need to declare a IntVector of 16 value, this Z3 object is kind of a list of integer constants of size 16 in our case.

 

Then we add the first kind of constraint : each byte must be >= 0 and <= 35 (because of the key value possibilities and mod / ord function).

 

And finaly we implement in Python each of these constraints like this :

 

from z3 import *

flag = IntVector("f", 16)
s = Solver()


for i in range(0, 16):
	s.add(flag[i] >= 0)
	s.add(flag[i] <= 35)


s.add(((flag[0] + flag[1]) % 36) == 14)
s.add(((flag[2] + flag[3]) % 36) == 24)
s.add(((flag[2] - flag[0]) % 36) == 6)
s.add(((flag[3] + flag[1] + flag[5]) % 36) == 4)
s.add(((flag[4] + flag[2] + flag[6]) % 36) == 13)
s.add(((flag[4] + flag[3] + flag[5]) % 36) == 22)
s.add(((flag[8] + flag[6] + flag[10]) % 36) == 31)
s.add(((flag[4] + flag[1] + flag[7]) % 36) == 7)
s.add(((flag[12] + flag[9] + flag[15]) % 36) == 20)
s.add(((flag[14] + flag[13] + flag[15]) % 36) == 12)
s.add(((flag[9] + flag[8] + flag[10]) % 36) == 27)
s.add(((flag[12] + flag[7] + flag[13]) % 36) == 23)


# if there is a solution
if s.check() != unsat:

    mod = s.model() # we display the model

    for i in range(16): # and we print nicely the two possible values due to the ord function
        x = mod[flag[i]].as_long()
        print (chr(x + 55), chr(x + 48))

 

switch :: ~/CTF/pico2018/keygen-me-2 » python solv2.py
[f__4 = 32,
 f__6 = 11,
 f__15 = 7,
 f__1 = 14,
 f__7 = 33,
 f__13 = 20,
 f__0 = 0,
 f__9 = 7,
 f__8 = 23,
 f__3 = 18,
 f__2 = 6,
 f__14 = 21,
 f__11 = 0,
 f__10 = 33,
 f__5 = 8,
 f__12 = 6]

('7', '0')
('E', '>')
('=', '6')
('I', 'B')
('W', 'P')
('?', '8')
('B', ';')
('X', 'Q')
('N', 'G')
('>', '7')
('X', 'Q')
('7', '0')
('=', '6')
('K', 'D')
('L', 'E')
('>', '7')

 

We can quickly remove all values not in [A-Z0-9] then I choosed to check each value manually step by step. You can notice that none of the constraints use the 11th char so it could be any value, so I used X at this position !

 

a = _ord(ord("0")) 
b = _ord(ord("E"))
c = _ord(ord("6"))
d = _ord(ord("I")) 
e = _ord(ord("W")) 
f = _ord(ord("8"))
g = _ord(ord("B")) 
h = _ord(ord("X")) 
i = _ord(ord("N"))
j = _ord(ord("7"))
k = _ord(ord("X")) 

m = _ord(ord("6"))
n = _ord(ord("K"))
o = _ord(ord("L"))
p = _ord(ord("7"))
   
print _mod(a + b, 36) == 14
print _mod(c + d, 36) == 24
print _mod(c - a, 36) == 6
print _mod(d + b + f, 36) == 4
print _mod(e + c + g, 36) == 13
print _mod(e + d + f, 36) == 22
print _mod(i + g + k, 36) == 31
print _mod(e + b + h, 36) == 7
print _mod(m + j + p, 36) == 20
print _mod(o + n + p, 36) == 12
print _mod(j + i + k, 36) == 27
print _mod(m + h + n, 36) == 23

 

switch :: ~/CTF/pico2018/keygen-me-2 » python solv2.py
True
True
True
True
True
True
True
True
True
True
True
True

 

And the key and flag are : 0E6IW8BXN7X6KL7 and picoCTF{c0n5tr41nt_50lv1nG_15_W4y_f45t3r_252103361}