*See the attachments [here](https://gist.github.com/vient/4d4e1cf75e8aa59def8e281dabd09bf3)*

The binary is reading format strings one by one from provided file and prints them to `/dev/null`.

This `fprintf` receives a lot of parameters, which actually are 16 bytes of memory, 16 bytes of flag, and pointers to said bytes. That are 64 parameters in total. Because of using `%hhn` specifiers, format strings can write to provided memory addresses, so we can perform additions with them easily.

Since given "virtual program" was pretty big, almost 3400 lines, I wrote a parser to make "virtual instructions" (format strings) more human-readable. For example, `%2$*36$s%2$*41$s%4$hhn` becomes `mem[3] = mem[3] + mem[8]`.

After parsing in human-readable form patterns in code became more obvious, so the next thing I wrote were two "optimizing" passes that folded additions in multiplications and then multiplications into one big sum.

Next, after parsing we have pretty simple program already. It is clear that flag is checked using a linear system, so we can use z3 to solve it easily.

Original writeup (https://gist.github.com/vient/4d4e1cf75e8aa59def8e281dabd09bf3).