Introduction

Buffer overflow is one of the most common type of software vulnerabilities. Various static analysis and dynamic testing techniques have been proposed to detect buffer overflow vulnerabilities. With automatic tool support, static buffer overflow detection technique has been widely used in academia and industry. However, it tends to report too many false positives fundamentally due to the lack of software execution information. Currently, static warnings can only be validated by manual inspection, which significantly limits the practicality of the static analysis. In this paper, we present BovInspector, a tool framework for automatic static buffer overflow warnings inspection and valid bugs repair. Given the program source code and static buffer overflow vulnerability warnings, BovInspector first performs warning reachability analysis. Then, BovInspector executes the source code symbolically under the guidance of reachable warnings. Each reachable warning is validated and classified by checking whether all the path conditions and the buffer overflow constraints can be satisfied simultaneously. For each validated true warning, BovInspector fix it by adding boundary checking or replacing unsafe APIs by safe ones. BovInspector is complementary to prior static buffer overflow discovery schemes. Experimental results on real open source programs show that BovInspector can automatically inspect 74.9% of total warnings in average, and identify from 25% to 100% of the false warnings with an average of 59.9%. And a short video for demonstrating the capabilities of BovInspector is now available at Demo Video on YouTube. And the test case used in the video and its corresponding inspection and repair steps and results are availble at Demo.

Overview

Method Flow Chart

BovInpsector has four main steps: warning reachability analysis, guided symbolic execution, buffer overflow validation, and targeted automatic repair. The key idea of BovInspector is to use symbolic execution to automatically identify those buffer overflow warnings reported by static analysis that are true warnings or false warnings. To avoid the infamous path explosion issue of symbolic execution, BovInspector uses static analysis to guide the symbolic execution so that it only focuses on the execution paths that cover the buffer overflow warnings generated by static program analysis. After validating the buffer overflow vulnerabilities, BovInspector will automatically repair these buffer overflow vulnerabilities according to programmer suggested repair methods. BovInspector has two inputs, the static buffer overflow vulnerability warnings and the source code, and two outputs, validated buffer overflow position reports and repaired source code. Validated buffer overflow position reports include true warnings, false warnings and undecided warnings. True warnings are those that there exists at least one test case that triggers buffer overflow. For each true warning, BovInspector also outputs such a test case. In addition, BovInspector can automatically repair the vulnerabilities for validated true warnings by checking array boundaries or replacing unsafe API by safe ones. False warnings are those that there exists no test case that triggers buffer overflow or totally unreachable. For such warnings, no human inspection is needed. Undecidable warnings are those that BovInspector can neither find a test case to trigger buffer overflow nor prove that no such test case exists within a given time limit. The optimization goal of BovInspector is to minimize the number of undecided warnings. Ideally, we want to minimize the number of undecidable warnings to zero for all programs; however, this is theoretically impossible because of the problem of using one program to find non-trivial properties of another program is fundamentally undecided.

Tool

We implemented BovInspector on KLEE, a state-of-the-art symbolic execution engine built on top of the LLVM compiler infrastructure. We extended functions of klee from two directions: guided symbolic execution and buffer overflow validation.The static buffer overflow detector used in our experiments is HP Fortify version 3.2. We used fvdlParser to convert the results of Fortify into static buffer overflow warning. We uesd buildCFG.so which is complied by LLVM pass to build CFG ,analyse reachablity in the graph and get warning path set. We modified source code of klee to inspect buffer overflow warnings.With the position of buffer overflow in the source code, we used repair.py to repair the vulnerability.You can download the source code from here.

BovInspector Tool Architecture

Experiment

All experiments were conducted on a quad-core machine with an Intel Core (TM) Corei5-2400 3.10GHz processor and 4G memory, running Linux 3.11.0. To evaluate our method, we designed two sets of experiments. The first set of experiments is designed to evaluate the correctness and accuracy of our method. The second set of experiments is designed to check the scalability and effectiveness of our method for real-world open source programs. Through these experiments, we hope to answer the following key research questions: (1) How much effort can a developer save by validating buffer overflow warnings using our technique(2) How does our technique perform on large-scale, real-world applications (3) How efficient is our technique.(4) The correctness of our Targeted Automatic Repair

Test cases

You may download the test cases tested in our paper via the download page.

Tutorial

Installation

Usage

Paper Example

You can see turotial here.

Contributors

Fengjuan Gao; Yu Wang; Linzhang Wang; Zijiang Yang; Xuandong Li; Tieyun Bao; You Li; Yongchao Li;

If you have any questions or problems with BovInspector, please feel free to contact me: fjgao@smail.nju.edu.cn