Internetwache RE60 Writeup: Symbolic Execution Tramples CTF Challenge
I am always looking for problems that symbolic execution could be applied to in the capture the flag space. This past weekend, this challenge was met during the Internetwache CTF for its RE60 problem. Below I describe the application of symbolic execution to solve the challenge without much knowledge of the inner workings of the binary itself. Symbolic Execution gives the reverse engineer the ability to find a specific path from Point A to Point B in a binary. This path is represented by a series of boolean expressions. These expressions can then be passed to a solver such as Z3 from Microsoft to solve the equation, creating an input that will exercise the found path.