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```Cvoid 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:
```pythonfrom z3_staff import * # https://github.com/KosBeg/z3_staff
x = create_vars(21, size=8) # create and return 21 BitVecs with size 8s = solver() # create and return solverset_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 equationsadd_eq( x[19] + x[8] - x[13] + x[9] == 104 )            # check_0add_eq( x[16] - x[8] - x[9] * x[1] - x[19] == -4464 )   # check_1add_eq( x[14] * x[15] == 2912 )                         # check_2add_eq( x[2] * x[13] + x[6] == 4541 )                   # check_3add_eq( x[7] + x[4] * x[7] * x[2] == 211300 )           # check_4add_eq( x[15] * (x[12] + 1) + x[14] == 3748 )           # check_5add_eq( x[19] * x[18] - x[20] * x[4] - x[13] == -5332 ) # check_6add_eq( x[3] * x[0] * x[5] == 454608 )                  # check_7add_eq( x[3] * x[9] - x[8] == 8064 )                    # check_8add_eq( x[1] - x[5] * x[9] - x[5] + x[1] == -3082 )     # check_9add_eq( x[11] * x[4] + x[9] == 3511 )                   # check_10add_eq( x[14] * x[19] + x[3] == 3091 )                  # check_11add_eq( x[16] * x[0] * x[4] * x[18] == 17567550 )       # check_12add_eq( x[17] + x[16] * x[19] + x[13] * x[7] == 6950 )  # check_13add_eq( x[14] + x[4] * x[7] - x[8] == 3252 )            # check_14add_eq( x[17] + x[0] * x[10] * x[11] == 212267 )        # check_15add_eq( x[17] + x[16] - x[15] + x[12] == 138 )          # check_16add_eq( x[8] + x[5] * x[14] == 2742 )                   # check_17add_eq( x[5] * x[2] == 3120 )                           # check_18add_eq( x[20] - x[8] + x[1] * x[12] - x[12] == 4691 )   # check_19add_eq( x[5] + x[6] + x[9] == 170 )                     # check_20
i = 0start_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 += 1print('--- %.2f second(s) && %d answer(s) ---' % ((time.time() - start_time), i) )``````PS C:\!CTF> python keygenme_solver.pyMCA{A0826B45FE84A765}--- 0.04 second(s) && 1 answer(s) ---```