前言

静态分析工具可以很全面地检测软件，但是误报率也很高。人工地去验证这些静态分析报告是费时费力的过程。BovInspector可以去自动化地验证静态分析找出的缓冲区溢出漏洞。本文将介绍BovInspector的基本原理，安装使用方法。

 

1.简介

BovInspector来源于2020年期刊 Journal of Computer Science and Technology的一篇文章《Automatic Buffer Overflow Warning Validation》，最早是16年软工A类会议ASE上的一篇short paper。

该工具主要是基于KLEE，实现了一个自动验证静态分析报告的工具。换个角度看，也有点像利用静态分析来减少符号执行的路径爆炸问题的工作。

 

2.原理

工具的基本框架如下图所示（下图来源于论文）。主要工作有以下3点：

a. Warning Reachability Analysis（基于LLVM的PASS实现）

b.Guided Symbolic Execution（基于KLEE实现）

c. Targeted Automatic Repair Suggestions（Python脚本）

下面将主要对Warning Reachability Analysis和Guided Symbolic Execution做重点介绍，并简单介绍自动修补。

2.1 Warning Reachability Analysis

这部分工作主要是确认静态分析找出的缓冲区溢出是否存在一条路径到达程序入口。首先，这部分内容的输入主要有两个，一个是源码，一个是buffer overflow warning。

buffer overflow warning用一个三元组表示(d,[l1,l2,…,ln],o)​，其中d表示buf定义的行号，l1,l2,…,ln表示对buf操作的行号，o表示溢出点。

由于静态分析工具检测的漏洞有可能在路径上是不可达的，因此，作者打算先过滤掉从程序入口到达不了的漏洞警告。具体来说，作者写了一个llvm pass先构建控制流图，再基于调用关系构建过程间的控制流图。然后在过程间的控制流图上，从漏洞点出发，往上追溯buf操作的语句，如果能够追溯到程序入口，说明这个漏洞有可能被触发。

这部分源码主要包含以下组件，核心是buildCFG.cpp

|-- CFGWriter.h //打印CFG
|-- ReverseSearchPath.cpp//逆向搜索路径
|-- ReverseSearchPath.h
|-- buildCFG.cpp //warning reachability analysis的核心
|-- convinent.cpp//包含一些方便的函数，比如获取行号，获取源文件名等等
|-- convinent.h
|-- mylib
|   -- printSTL.h
|-- programCFG.cpp//构建过程间控制流图
|-- programCFG.h
|-- targetPosition.cpp//将缓冲区溢出警告里的行号映射为基本块
|-- targetPosition.h

下面这段是buildCFG.cpp的主要代码，首先构建过程间控制流图（line 4）。

然后基于buffer overflow warning的信息，去获取buf定义、操作、溢出的行号在哪些基本块里（line 5-7）。也就是targetPosition.cpp里的逻辑。

接着从溢出点的基本块和离溢出最近的一个buf操作的基本块开始，搜索这两个基本块的路径（ReverseSearchPath.cpp），直到遍历完所有的target point。

bool buildCFG::doInitialization(Module &M){ 

    errs()<<"build programCFG-------------------------------------------------------------------\n";
    new ProgramCFG(M);
    std::vector<pair<BasicBlock*,BasicBlock*> > *target_point=NULL;
    if(!targetListFileName.empty())
        target_point=getTargetPoint(targetListFileName,M);
    errs()<<target_point->size()<<"\n";
    if(target_point->size()!=0){
        errs()<<"the path number is  "<<target_point->size()<<"\n";
        for(unsigned int i=0;i<target_point->size();i++){
            Function *main = M.getFunction("main");
            SearchReversePaths(target_point->at(i).first,target_point->at(i).second,&main->getEntryBlock(),M,i);
        }
    }
    else errs()<<"No valid path in checklist!!"<<"\n";
     return false;
}

2.2 Guided Symbolic Execution

指导符号执行的目的是验证缓冲区溢出漏洞是否可以被触发。整个流程大致如下图所示。首先，从执行状态池里选择一个状态。接着，执行指令，如果执行到漏洞点，调用验证模块，检测一下当前的状态是否满足漏洞的约束条件，如果满足，则说明是漏洞，反之则是误报。如果执行到分支指令，就复制当前状态，同时筛选状态。最后就是更新状态。

筛选状态的算法如下图所示，图来源于论文。es，es2分别表示分支为true的状态和分支为false状态。因此，l1，l2分别表示es，es2状态的将要执行的下一条指令的行号。如果之前提取的warning路径集合里包含l1或l2，则筛选掉另外一个。但如果路径集合里没有l1，l2，或者都有l1，l2，就不做筛选操作。

不筛选的原因有两个。第一，路径集合里没有l1，l2，有可能是符号执行去探索一些没有出现在警告路径里的库函数调用。第二，路径集合里有l1和l2，可能是溢出点在循环里，这样两个分支就都存在warning路径。

漏洞验证模块是去求解当前状态是否满足人工设定的漏洞约束条件。设定的约束条件如下表所示（表来源于论文）。这部分代码可以查看project/src/klee_symbolic_execution/lib/Core/Executor.cpp里的BFO_Check函数。代码量比较大，大概2000行左右，就不贴出来了。主要思路就是根据各种容易出问题的库函数API，设定缓冲区溢出的约束条件。

2.3 Targeted Automatic Repair Suggestions

BovInspector修补漏洞的策略采用专家知识构建的模板，主要有以下11种修补模式（表源于论文）。具体实现可以去看代码（位于project/src/repair_buffer_overflow/repair.py ）

 

3.安装

想跳过下面的安装步骤，可以直接用我构建好的docker 镜像

docker pull iskindar/bov:v1
docker run -ti --ulimit='stack=-1:-1' --name="bovinspector" iskindar/bov:v1
source /etc/profile #加载环境变量

3.1 源码安装

这里提供了docker的安装方式，因为原工具的开发时间比较早，一些环境比较老旧，用docker方便一点。

构建docker镜像

docker run -ti --ulimit='stack=-1:-1' --name="bovinspector" ubuntu:14.04

进入docker容器安装依赖

$ apt-get update
$ apt-get install g++ python curl cmake git bison flex bc libcap-dev
$ apt-get install zlib1g-dev

安装llvm-gcc

$ wget http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
$ tar -jxvf llvm-gcc4.2-2.9-x86_64-linux.tar.bz2

将llvm-gcc添加到环境变量

$ vim /etc/profile
export PATH=$PATH:/root/llvm-gcc4.2-2.9-x86_64-linux/bin #把这行加入/etc/profile文件末尾
$ source /etc/profile

源码安装llvm-2.9，安好之后，可以把按上面的步骤把llvm-2.9/Release+Asserts/bin加入环境变量

$ wget http://llvm.org/releases/2.9/llvm-2.9.tgz
$ tar -zxvf llvm-2.9.tgz  
$ cd llvm-2.9  
$ ./configure --enable-optimized --enable-assertions  
$ make

安装minisat（STP需要这个）

$ git clone https://github.com/stp/minisat.git
$ cd minisat
$ mkdir build
$ cd build
$ cmake ../
$ make
$ sudo make install

安装STP(约束求解器)

$ tar xzfv 2.1.0.tar.gz  
$ cd stp-2.1.0
$ mkdir build
$ cd build
$ cmake ..  
$ make
$ sudo make DESTDIR=/root/stp_install install

安装uclibc（KLEE用来模拟库函数的组件）

$ git clone git://github.com/klee/klee-uclibc.git
$ cd klee-uclibc
$ ./configure --make-llvm-lib
$ make -j2
$ cd ..

安装bovinspector，为方便使用，也可以把project/src/klee_symbolic_execution/Release+Asserts/bin加入环境变量

git clone https://github.com/BovInspectorTool1/project.git
cd project/src/klee_symbolic_execution/
./configure --with-llvm=/root/llvm-2.9 --with-stp=/root/stp_install --with-uclibc=/root/klee-uclibc --enable-posix-runtime
make -j $(grep -c processor /proc/cpuinfo) ENABLE_OPTIMIZED=1

安装llvm pass

将project/src/build_control_flow_graph移到llvm-2.9/lib/Transform/下，并将文件夹重命名为buildCFG

修改lib/Transform/Makefile为(就是第二行加个buildCFG：

LEVEL = ../..
PARALLEL_DIRS = Utils Instrumentation Scalar InstCombine IPO Hello BuildCFG

include $(LEVEL)/Makefile.config

# No support for plugins on windows targets
ifeq ($(HOST_OS), $(filter $(HOST_OS), Cygwin MingW Minix))
  PARALLEL_DIRS := $(filter-out Hello, $(PARALLEL_DIRS))
  PARALLEL_DIRS := $(filter-out buildcfg, $(PARALLEL_DIRS))
endif

include $(LEVEL)/Makefile.common

回到llvm-2.9/目录下

./configure --enable-optimized --enable-assertions  
make

可以看到/root/llvm-2.9/Release+Asserts/lib目录下有buildCFG.so，就说明安装成功了。

 

4. 使用

论文中给的一个简单的测试程序src.c：

#include <string.h>
#include <stdlib.h>
#include <stdio.h>
#define MAX_LEN  24
#define MIN_LEN  4
void usage() {
    char des_buffer[MIN_LEN];  
    char* src_buffer="this is an example";
    strcpy(des_buffer,src_buffer);
}
int initialize(char* argv_string) {
    char mapped_argv[MIN_LEN];
    if (strlen(argv_string) >= MAX_LEN)
        return 0;
    strcpy(mapped_argv,argv_string);
    if (argv_string[0] != '-') {
        strcat(mapped_argv, "-");
    }
    return MAX_LEN;
}

int main(int argc, char **argv) {    
    char* mode = (char*)malloc(MIN_LEN);
    int len = 0;
    if (strlen(argv[1]) < MIN_LEN)
        len = initialize(argv[1]);
    if (len > 0) {
        mode = (char*)realloc(mode, len);
    }  
    else {
        mode[0] = argv[1][0];
    }
    mode[MIN_LEN-1] = '\0';
    free(mode);
    return 0;
}

假设用某些静态分析工具跑出的结果checklist_bufferoverflow：

0
src.c    7    DEF
src.c    9    BOF
END_PATH
1
src.c    22    DEF
src.c    26    N/A
src.c    12    N/A
src.c    15    N/A
src.c    17    BOF
END_PATH
2
src.c    28    DEF
src.c    33    BOF
END_PATH
3
src.c    22    DEF
src.c    26    N/A
src.c    12    N/A
src.c    15    BOF
END_PATH

新建一个文件夹，比如paper_example

mkdir paper_example
vim src.c # 将上面的内容复制进来
vim checklist_bufferoverflow #将上面的内容复制进来

用llvm-gcc生成字节码

llvm-gcc --emit-llvm -c -g src.c

构建CFG，生成GuideSrc.txt，programCFG.dot

opt -load /root/llvm-2.9/Release+Asserts/lib/buildCFG.so -buildCFG -targetList=./checklist_bufferoverflow src.o

运行klee，验证warning

klee --libc=uclibc --posix-runtime --guided-execution src.o --sym-args 1 3 25

最后应该会生成report_BFO.txt和report_NOTBFO.txt文件，内容如下：

report_BFO.txt：真实的缓冲区溢出所在行数

src.c_17 strcat

report_NOTBFO.txt：误报的缓冲区溢出漏洞行数

src.c_15 strcpy

 

5. 总结

最后简单总结下，这个工具的思路虽然很简单，但实际实现过程的代码量还是相当大的。另外，可能因为这个工作比较早完成的，一些软件的版本比较老，让我安装起来着实费了不少劲。非常感谢这篇论文作者将工作开源了，让本菜鸡能够学习到如何去修改KLEE实现相应的功能，并加深了对于KLEE工作的理解。

 

6. 参考

0x1. Gao F, Wang L, Li X. BovInspector: Automatic inspection and repair of buffer overflow vulnerabilities. In Proc. the 31st IEEE/ACM Int. Conference on Automated Software Engineering, Sept. 2016, pp.786-791.
0x2. bovinspector：https://github.com/BovInspectorTool1/project
0x3. bovinspector项目介绍：https://bovinspectortool1.github.io/project/