Tags: z3 

Rating:

TL;DR. Parse the checking functions to extract the constraints and solve for the flag. Or use ANGR. I don't know how to use ANGR so it's the old-fashioned way for me: walking through the binary with a clunky FSA and solving with Z3.

Original writeup (https://nave1337.herokuapp.com/index.html#bbf2021_flagcheckerrevenge).