This challenge was solved by and the write up was written by one of my teammates, nguyen
We got x64 ELF binary ‘license’
Decompile result of main function starts with opening a file
_a\nb\tc_, since it is inconvenient to create file with such name, we replace the filename with following command
now we create a file name “keyfile” and get following error.
from next logic, we can see that size of keyfile should satisfy some equation.
we solve this using z3 solver and found out that size should be 34 byte. next, the file should contain 5 newlines
the file contents needs to be separated with newline and each line has to contain 6bytes which will be compared after XORing with hardcoded XORed key:
As a result, the following equation should be satisfied.
solving this equation with z3 yields
generating keyfile with these keys concatenated with newline we get following result