Tags: rev z3 

Rating:

I did not participate in STEM STF, but this task seemed interesting to me.

But since almost all writeups with angr get boring and monotonous - I decided to make it with Z3(lol, almost all my Z3 writeups boring and monotonous also :D).

We have some file `keygenme`. So let's start analysis!

```
pc@pc:~/$ file keygenme
keygenme: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 2.6.32, BuildID[sha1]=2df07d316e0400087379638a40614b8dd0d635c0, not stripped
```

In main we have
```C
void main(void) {
char flag[24];

printf("Give me a key: ");
scanf("%21s", flag);
check_1(flag);
check_2(flag);
check_3(flag);
check_4(flag);
check_5(flag);
check_6(flag);
check_7(flag);
check_8(flag);
check_9(flag);
check_10(flag);
check_11(flag);
check_12(flag);
check_13(flag);
check_14(flag);
check_15(flag);
check_16(flag);
check_17(flag);
check_18(flag);
check_19(flag);
printf("Grats! You made it!");
}
```

Funcs check_NUM is almost same, like
```
void check_1(char *x) {
if ( x[16] - x[8] - x[9] * x[1] - x[19] != -4464 )
fail();
}
```

Now create Z3 script to solve this equations:

```python
from z3_staff import * # https://github.com/KosBeg/z3_staff

x = create_vars(21, size=8) # create and return 21 BitVecs with size 8
s = solver() # create and return solver
set_ranges() # set ASCII ranges(printable chars) for all vars created by create_vars

set_known_bytes('MCA{*}', type='ff') # set known flag format, or we can use without ", type='ff'" like "set_known_bytes('MCA{' + '*'*16 + '}')"

# add all known equations
add_eq( x[19] + x[8] - x[13] + x[9] == 104 ) # check_0
add_eq( x[16] - x[8] - x[9] * x[1] - x[19] == -4464 ) # check_1
add_eq( x[14] * x[15] == 2912 ) # check_2
add_eq( x[2] * x[13] + x[6] == 4541 ) # check_3
add_eq( x[7] + x[4] * x[7] * x[2] == 211300 ) # check_4
add_eq( x[15] * (x[12] + 1) + x[14] == 3748 ) # check_5
add_eq( x[19] * x[18] - x[20] * x[4] - x[13] == -5332 ) # check_6
add_eq( x[3] * x[0] * x[5] == 454608 ) # check_7
add_eq( x[3] * x[9] - x[8] == 8064 ) # check_8
add_eq( x[1] - x[5] * x[9] - x[5] + x[1] == -3082 ) # check_9
add_eq( x[11] * x[4] + x[9] == 3511 ) # check_10
add_eq( x[14] * x[19] + x[3] == 3091 ) # check_11
add_eq( x[16] * x[0] * x[4] * x[18] == 17567550 ) # check_12
add_eq( x[17] + x[16] * x[19] + x[13] * x[7] == 6950 ) # check_13
add_eq( x[14] + x[4] * x[7] - x[8] == 3252 ) # check_14
add_eq( x[17] + x[0] * x[10] * x[11] == 212267 ) # check_15
add_eq( x[17] + x[16] - x[15] + x[12] == 138 ) # check_16
add_eq( x[8] + x[5] * x[14] == 2742 ) # check_17
add_eq( x[5] * x[2] == 3120 ) # check_18
add_eq( x[20] - x[8] + x[1] * x[12] - x[12] == 4691 ) # check_19
add_eq( x[5] + x[6] + x[9] == 170 ) # check_20

i = 0
start_time = time.time()
if s.check() == sat: # https://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models
founded = prepare_founded_values() # return founded values as array
print ''.join( chr(j) for j in founded ) # print flag as string
iterate_all() # prepare to next iteration, anticollision
i += 1
print('--- %.2f second(s) && %d answer(s) ---' % ((time.time() - start_time), i) )
```
```
PS C:\!CTF> python keygenme_solver.py
MCA{A0826B45FE84A765}
--- 0.04 second(s) && 1 answer(s) ---
```