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

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:

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) ---