A Formal Approach to Vulnerability Discovery in Binary Programs

Date of Award

6-13-2013

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Department of Electrical and Computer Engineering

First Advisor

Rusty O. Baldwin, PhD.

Abstract

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

AFIT-ENG-DS-13-J-03

DTIC Accession Number

ADA586099 (See comments below)

Comments

The full text of this dissertation is not available directly on AFIT Scholar.

Readers in the DOD may locate the dissertation in DTIC R&E Gateway. The DTIC Accession number, ADA586099, can be used as the search term.

Registration for DTIC is required. Your eligibility for registration is at the discretion of DTIC.

This document is currently not available here.

Share

COinS