Modern static security checking of C / C++ programs

In this talk, Julien discusses the amenability of source-level static analysis to find some of the past major security vulnerabilities of the last decade using the HAVOC tool (the Heap Aware Verifier for C/C++).

In particular, the presentation covers the concept of "static variation analysis" of:

• The Webkit CSS type confusion vulnerability leading toww information disclosure found by Chris Rohlf in 2010.

• The Sendmail crackaddr vulnerability discovered by Mark Dowd in 2003 (a non-trivial challenge for static analysis as presented by Halvar Flake at the Infiltrate 2011 conference)

• Other common security properties of OS kernels such as untrusted pointer validation and zero allocation vulnerabilities (a generalization of the integer wrapped memory allocations vulnerabilities)

The presentation covers analysis of object oriented constructs in commonly deployed C++ programs as well as inter-procedural bit-level analysis and loop analysis. The approach is based on translating the program into an intermediate form for consumption by theorem prover Boogie and SMT solver Z3. HAVOC users make use of annotations and instrumentations to guide static analysis, thus compromising automation for more configurability. Practical scalability and refinement of the approach are also discussed based on three years of experiments on checking security properties in Microsoft codebase.