A Lazy SMT Bit-vector Solver for Binary Symbolic

Presented as part of the 2013 HCSS conference.

ABSTRACT:

A significant focus in software security is to leverage verification tech- niques to check security-relevant properties. These techniques work by au- tomatically generating verification conditions (VCs), formulas that capture the logical semantics of a program fragment and its desired properties. If the assertions hold, the program is safe, if not, the program is vulnerable. SMT solvers are typically used to check the VCs. Of particular interest are approaches that work on binary programs. For simplicity, we call the overall approach of generating a VC from a binary program and checking its satisfiability binary symbolic execution.

An example application is Automatic Exploit Generation (AEG),1 which works by exploring paths in a program, looking for potential security vulner- abilities. AEG builds one VC to check the feasibility of the current path and a second VC exploitability VC that includes additional security constraints, e.g. whether an attacker can overwrite critical data structures such as the instruction pointer.

VCs generated by binary symbolic execution typically require the SMT solver to reason in a combination of the theory of fixed-width bit-vectors (used to model the binary instructions and data) and the theory of ex- tensional arrays (used to model registers and memory). State-of-the-art bit-vector solvers operate by eagerly reducing the problem to SAT via a technique known as bit-blasting. While efficient in practice on many appli- cations, eager bit-blasting loses word-level information and structure.

This talk will describe an online lazy solver for the theory of bit-vectors. Making the solver lazy instead of eager enables several optimizations, in- cluding: (i) integrating word-level reasoning as in-processing, not just pre- processing; and (ii) using an ATPG-based decision heuristic to lazily select only the relevant parts of the problem. Early results on AEG benchmarks suggest that these techniques can drastically reduce the problem size and give a competitive edge over eager bit-blasting solvers.

1see, e.g., http://forallsecure.com/ 

BIO:

Clark Barrett received his PhD from Stanford University in 2003, advised by David Dill. He now leads the Analyis of Computer Systems group at New York University. His PhD thesis laid the groundwork for the architecture of modern Satisfiability Modulo Theories (SMT) solvers. He has written numerous articles on SMT, and in addition has developed five major SMT systems: SVC, CVC, CVC Lite, CVC3, and CVC4. These open-source systems have been used by academic and industry researchers all over the world. His latest system, CVC4, was publicly released in December 2012 (see http://cvc4.cs.nyu.edu).

Professor Barrett is a founder of the SMT competition, a leader of the SMT-LIB initiative, and was a founding member of the SMT steering com- mittee. He received the IBM Software Quality Innovation Award for CVC3 in 2008, and he was the recipient of the Haifa Verification Conference award in 2010 for his pioneering work in SMT.