To err is human; to be caught at compile-time, divine

— Jacob Torrey (@JacobTorrey) March 2, 2016

 Next week at TROOPERS I am acting as a TA for Tamas on our VM Introspection training as well as giving a talk aimed at developers and their managers to augment their software development life-cycle (SDLC) with LangSec principles. Last year, one of the co-founders of the LangSec field of computer science, Sergey Bratus, gave a keynote on "My Favorite Things", espousing the security implications of the underlying computational complexities involved with computation and input parsing. As a development lead for a small team, I wanted to adopt many of these principles and make them managable for existing software teams without having to hit the books to understand complexity theory terms such as: "Chomsky hierarchy" or "Recursively enumerable".

Language-theoretical security, or LangSec, is a field of study examining the reasons why software fails and how the majority of vulnerabilities exist due to the presence of "weird machines" stemming from ad hoc parsing. A major point in LangSec is how the parser (i.e., the program's code) creates a virtual machine environment upon which the input data is used to direct execution flow. If these processes are not strictly managed, attackers can find "non-standard" control-flow paths through the virtual environment, exploiting the program.

My upcoming talk aims to "translate" the theory into practice as well as provide concrete tools and strategies to incorporate and audit LangSec-inspired theories in the SDLC. As the amount of code developed in software development shops continues to rapidly grow, no longer (if ever was the case) can each developer be trusted to not introduce mistakes, or bugs, into product.By aiming to develop code that can be easily verified or tested for bugs, and by adopting techniques to "push" those bugs to surface earlier, the SDLC can be improved. The Soviet adage "trust, but verify" (doveryai no proveryai) applies now more than ever in software development and security, so "verification-oriented programming" helps ease the computational challenges we face when checking code for errors.

The talk has two main thrusts after some precursory background: how to translate LangSec principles into concrete coding standards and conventions, and tools to help developers and their managers prevent and check code for errors. Through the lens of LangSec, NASA JPL's top ten programming guidelines and MISRA's conventions will be examined to understand the underlying theory. A number of tools both to aid in the development of more secure code (e.g., parser generators) as well as auditing tools to improve testing coverage and decrease defect rate are introduced. Finally, my small collection of tools, Sledgehammer, will be provided as open-source for use in software development shops.