SAT, SMT, and CTF, oh my!

Presented at ToorCon San Diego 18 (2016), Oct. 15, 2016, 3 p.m. (50 minutes)

This talk will give an introduction to SAT solvers, SMT solvers, and their applicability to security CTF challenges. Real challenges from recent CTFs will be used to show how these tools can sometimes be used to find flags automagically. Finally, cutting-edge applications of SAT/SMT solvers such as shellcode and ROP chain generation and concolic execution will be touched upon.


  • Tom Samstag / tecknicaltom as Tom Samstag
    Tom Samstag (tecknicaltom) is a Principal Security Engineer at Security Innovation in Seattle and member of the Neg9 CTF team. A Perl hacker and C programmer at heart, his interests tend to gravitate towards reverse engineering, exploitation, static analysis, and other bit-fu aspects of software and security.

Similar Presentations: