Vertex RE

Software Analysis and Security Services

+44 1865 403253

Our classes focus on providing in-depth program analysis material in a manner that is real-world applicable. For bookings email  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

  • Intermediate languages

  • Static vs dynamic analysis - limitations, strengths, and contrasts

  • General guidance on adding automation to RE, code auditing, and exploitation workflows

A detailed syllabus can be found here. For further information, pricing and bookings please email Private trainings are available on request.