Our classes focus on providing in-depth program analysis material in a manner that is real-world applicable. For bookings email email@example.com. Private classes are available on request, provided a minimum number of students is reached.
Advanced Tool Development with SMT Solvers (4 Days)
Trainer: Sean Heelan
This class is designed to introduce students to the cutting edge of research in program analysis based on SMT solvers and symbolic reasoning. With a focus on practical applications, we will cover the theory and implementation behind a number of techniques developed in recent years that have relevance in vulnerability discovery, exploit development, and reverse engineering. Over the four days, we will go from the foundations of problem solving with SMT solvers through to the construction of analysis systems capable of reasoning about complex problems in real software. Students will also be introduced to a variety of existing analysis systems, including KLEE, angr, manticore and CBMC, and learn their strengths and weaknesses.
This class features extensive exercises and we require students to be comfortable developing software in Python and have familiarity with the x86 ISA. A grasp of foundational computer science, such as propositional logic, will also be of use but is not a requirement. Some of the topics to be covered include:
Modelling problems with SMT solvers, and their usage in understanding complex code
Vulnerability detection and program exploration with symbolic execution
Concolic execution & whitebox fuzzing, i.e. SMT solver driven fuzzing
Usage of open-source symbolic execution frameworks
Static vs dynamic analysis - limitations, strengths, and contrasts
General guidance on adding automation to RE, code auditing, and exploitation workflows