TL;DR: I’ll be running a new version of the Advanced Tool Development with SMT Solvers training course in London, starting November 6th 2017. The most significant change is the addition of an extra day covering some diverse real world analysis platforms. See vertex.re/training for details. Read on for more info on the new content.
For almost 5 years I’ve been running training courses on SMT-based program analysis technology. The contents have evolved continuously over the this time, keeping up with new advances in the space, but I’ve stuck with the 3 day format as it has allowed for the best balance between catering for complete newbies and those with prior experience.
For much of this time, the number of real world symbolic execution tools that are 1) publicly available, 2) still being actively maintained and 3) amenable to extension, improvement and re-purposing, has been quite limited. Due to this, most of the training has focused on fundamentals of SMT-based analysis, under the assumption that there’s a significant chance the students would have to develop their own systems from scratch. In the early days I did include introductions to S2E and KLEE, but both are rather large C++-based projects which students seemed to struggle with in the compressed time frame of a training course.
Recently, partially due to the DARPA Cyber Grand Challenge, and partially due to an uptick in industry interest in the technology, the number of public frameworks and architectures made available has increased significantly. Due to this, I’ve decided to add a 4th day which will focus entirely on introducing, comparing and contrasting some publicly available systems. While the exact contents may change between now and November, the preliminary list looks as follows: angr, CBMC, KLEE and manticore. These four tools occupy different points in the design space of symbolic execution platforms and show interesting takes on the fundamental concepts. There are lots of different ways to achieve the same end with symbolic execution tools and I think these four implementations should well prepare students to develop their own tech, as well as enabling them to build on public code if they so wish.