SMT Solvers Summerschool at MIT

Earlier this summer Beans attended the weeklong SMT Solver Summer school held at MIT campus in Boston, Mass. Over the last few years having seen some of the presentations by Pablo Sole on DEPLIB, blogposts by Sean Heelan, and having messed around a little bit with the REIL in BinNavi we were really curious to get a bigger picture on SMT Solvers. What was the current state of research on this stuff? and how were other industries applying it? Sean Heelan has a great series of blogposts that summarize all the days of presentations so we aren’t going to parrot any of that. Check out his great blog posts. Additionally, all the presentations, presentation summaries, presenter bios, and even some videos are available on a publicly accessible MIT wiki. The other Steve has also written a bit about his experience at Infiltrate Conference and the SMT Solver/DEPLIB talks that were given there. Pablo Sole’s EkoParty talk on DEPLIB is also available here.

In general (I personally) found the SMT Summerschool to be very academic and high-level. Much of it was over my head. But this was good and bad. It was a good experience because I (perhaps masochistically) like to be exposed to new things especially things that I know nothing about.  The “bad” part of all of this was that of what I could comprehend (with the exception of a few presentations)  I found the ideas to be spectacular but completely divorced from any kind of practical implementation.

For example: In the presentation: Liquid Types: SMT Solver-based Types the researcher (Ranjit Jhala) demonstrated how a simple high-level type system can be used to describe many “insecure patterns” in an abstract way so that a user needs not fumble with building these constraints by hand. During the first half of his presentation I began to get really excited and when it came closer to time for demonstration of the tools and such, it was partially implemented for use only with OCAML (with C support maybe later)! This to me was such a big let-down, and from the comments and questions of others in the audience, I was not the only one. These kinds of post-presentations discussions were a common theme that demonstrated how divorced academia is from industry. In many of the Q&A sessions small discussions would break out between presenters and audience members on the practicality of implementation. The age old tension between the purity of academia and the “get it done so it’s usable” mentality of industry.

Of all of the presentations most relevant to vulnerability research, these were my favorites because the concepts were the most accessible for me:

• BitBlaze & WebBlaze: Tools for computer security using SMT Solvers
• Constraint Solving Challenges in Dynamic Symbolic Execution
• Liquid Types: SMT Solver-based Types
• SMT Solver-based Compiler Optimization Verification
• SAGE: Automated Whitebox Fuzzing using SMT solvers
• Symbolic Execution and Automated Exploit Generation

Of all the talks, the Constraint Solving Challenges in Dynamic Symbolic Execution was probably the best introduction to the use of SMT Solvers for basic vulnerability research. The researchers leveraged symbolic execution and the STP constraint solver to find bugs laying dormant in GNU CoreUtils. Some of these bugs were simple enough to trigger with command-line arguments (see slide 36 “Ten Command Lines of Death”).

In the end, it was a great experience to have participated in the SMT Summer School. I learned a lot and got interested in new and different applications for SMT Solvers…but I will probably have to work with them a bit more before I can get more value from another conference like this.

Also a very short slideshow of some photos taken during the SMT Summer School are here.