A Formal Approach to Vulnerability Discovery in Binary Programs

Date of Award


Document Type


Degree Name

Doctor of Philosophy (PhD)


Department of Electrical and Computer Engineering

First Advisor

Rusty O. Baldwin, PhD.


This research investigates the complexity of, and develops a formal approach for, vulnerability discovery (VD) in binary programs. First, it is proved that safe and precise memory-bounded disassembly is NP-hard, which infers that VD for binary programs, in general, is NP-hard. Second, VD's intractability is addressed by focusing on a special 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 code's behavior { a type of symbolic execution. This conversion reduces VD to deciding satisfiability of each path model conjuncted with vulnerability properties of interest. In addition, we develop optimization algorithms to soundly reduce the size of each path model, and a novel memory model to precisely reason about input dependent pointers. Optimization algorithms include a data dependency reduction, a novel constant function reduction, and a cone-of-influence reduction. Fourth, we implement our approach (path model construction, reductions and memory model) in a tool named Jiseki and provide experimental data for real world applications to show the overhead of each reduction and our memory model. We demonstrate Jiseki discovering buffer overflows and index out-of-bounds errors in binary programs. Last, we propose future approaches to vulnerability discovery which build on the research herein.

AFIT Designator


DTIC Accession Number

ADA586099 (See comments below)


The full text of this dissertation is not available directly on AFIT Scholar. AFIT readers can click the Link to Full Text button at right to download the full text from ProQuest Dissertations & Theses, a subscription database.

Other readers may locate the dissertation in DTIC R&E Gateway, searching the DTIC Accession number, ADA586099. Registration is required. Your eligibility for registration at the discretion of DTIC.