The Diana Initiative 2021

Advanced binary analysis tools are gaining in popularity among CTF players, however there can be a steep learning curve to incorporating them into use. In this introduction to the power of concolic execution and satisfiability modulo theories (SMT) solvers, we will cover angr, an open-source binary analysis framework, and Z3, an SMT solver. This talk will give background on these tools and how they can each be applied to easy and advanced reverse engineering CTF problems. Audience members will walk away with an understanding of the technology behind these tools, how they can be applied to CTF problems as well as the foundation to continue their knowledge growth in this area.