|Student Name:||Mr. William Kimball|
|Thesis:||A Formal Approach to Vulnerability Discovery in Binary Programs|
|Attendance Restrictions:||TS/SCI Cleared Personnel Only|
|Date & Time:||04/29/2013 at 1430|
|Abstract:|| This research investigates the complexity of, and develops a formal approach for, vulnerability discovery (VD) (a.k.a. bug hunting) in binary programs. First, it is proved that safe and precise memory-bounded disassembly is NP-hard, so VD for binary programs then is NP-hard. Second, VD's intractability is addressed by focusing on a class of 32-bit Windows-based programs executing on Intel Architecture (IA-32). We investigate the structure of memory corruption errors to develop approximation algorithms and heuristics for VD. Third, we develop a formal framework to automate VD for Windows IA-32 binary programs. Our approach converts instruction paths in binary programs to logical formulas (“path models”) in quantifier free fixed-width bit vector theory which precisely represent the codes behavior - a type of symbolic execution. This conversion reduces VD to deciding satisfiability of each path model conjuncted with vulnerability properties of interest. Fourth, we develop optimizations to reduce the size of each path model, and a novel memory model to reason about pointers. Fifth, we implement our approach in a tool named Jiseki and provide experimental data for real world applications to show the overhead of each reduction and our memory model.