Group of Software Security In Progress

GoSSIP @ LoCCS.Shanghai Jiao Tong University

安全论文每日读-- 2015.03.16

今天我们送上一篇关于程序分析工具BAP的论文,BAP: A Binary Analysis Platform 这篇论文 发表于CAV 2011 (the Proceedings of 2011 Conference on Computer Aided Verification),主要介绍了鼎鼎大名的CMU Cylab实验室(PPP的大本营)所开发的一款二进制程序分析引擎。BAP现已发布到0.9.5版本,而论文发布于2011,所涉及的是0.3.0版本。

BAP是为了用于程序验证(program verification)和二进制程序分析而开发的一款基础平台工具,支持x86和ARM架构。BAP将整个工具简单地分为两部分:前端和后端两部分,通过中间语言表式的代码进行联系:

前端程序 包括Trace Interface、Instruction Lifting、Binary Format Interface,用于将所得到的一段二进制代码(可以是静态获得的代码段,也可以是动态得到的trace)反汇编成汇编指令,再转换为中间语言语句。

后端程序 对前端所生成的中间语言语句进行分析操作,文中列出了包括Program Analysis、Program Verification、Graphs、Optimizations、Code Generation等一系列可以提供的分析功能,同时用户也可以进行自定义的分析测试。

考虑到汇编指令执行过程中带来的副作用(对标志寄存器的影响),作者在BAP中引入了自己设计中间语言——BIL(中间语言语法可参考 http://bap.ece.cmu.edu./doc/bap.pdf ,但是在0.9.5的版本中所使用的BIL语法与手册中提到的语法有出入)。BIL会将汇编指令所涉及的对标志寄存器的操作分离出来,形成单独的语句,文中认为这些得到的中间语言语句是side-effect free的。其目的就是能明确地分析这些隐藏的对控制流产生影响的操作。相较于以往的二进制反汇编分析工具,这是BAP最突出的优点。同时BIL也可以转换为其他有效的表示方式,例如static single assignment(SSA) form,便于后端程序的分析操作.

BAP在CyLab之后的一些研究中被大量使用,例如:1)Q, the ROP compiler;2)Mayhem, a binary symbolic executor;3)Tie, a type recovery system等等,具体可参见 http://bap.ece.cmu.edu/

BAP 0.8的安装

BAP 0.9.5相较于0.8版本做了很大的修改,原有的handbook不再适用,有兴趣的话可以去git上下载,安装较为方便,以下主要介绍一下ubuntu上安装0.8版本的BAP

系统要求:

Ubuntu 11.04/11.10/12.04。不建议使用14.04等高于12.04的版本,由于BAP依赖于Ocaml,建议安装的OCaml版本号3.12 <= v < 4.01.00,否则在编译过程中极易出现一些程序语法上的错误。Ubuntu 12.04可提供的Ocaml安装包最高版本为3.12.1,可以直接下载获得。

前期准备:

安装所依赖的一些工具的软件包

# __BEGIN_REQUIRED__
sudo apt-get -y install ocaml-nox ocaml-native-compilers ocaml-findlib \
camlidl binutils-dev automake libcamomile-ocaml-dev otags libpcre3-dev \
camlp4-extra bison flex zlib1g-dev libgmp3-dev g++ libtool make
# __END_REQUIRED__

如果系统是64位系统,还需安装一下软件包

$ sudo apt-get install gcc-multilib g++-multilib lib32z1-dev

由于BAP可以将BIL程序转换成LLVM的中间语言,还需要LLVM code generation。 、

$ sudo apt-get install libllvm-3.1-ocaml-dev

原作认为3.1至3.3版本都可以使用,但都没有测试过。(在我自己的编译过程中使用了3.1版本)

编译BAP:

$ ./autogen.sh
$ ./configure
$ make
$ make test      #test意义不大

在执行配置文件configure时可能会出现以下提醒:

configure: WARNING: Pin not found. BAP pintraces will be unavailable.
configure: WARNING: ETAGS not found. BAP will not build tags.
configure: WARNING: lablgnomecanvas not found: the graph editor and view_graph will not be compiled

其中Pin的安装可以独立出来,稍后进行,后两个只要安装etags工具以及liblablgtk2-gnome-ocaml-devliblablgtk2-ocaml-dev软件包,对BAP并无很大影响。

Pin的安装:

由于BAP能够对程序动态运行后的trace进行分析,使用了pin这个动态插桩工具。pin的安装较为简单,直接在`$BAPDIR/pintraces`目录下的运行getpin.sh,即可自动下载`pin-2.13-61206-gcc.4.4.7-linux.tar.gz`并解压安装。并在`$BAPDIR/pintraces`目录下编译所需的pintools,会生成`$BAPDIR/pintraces/obj-ia32/gentrace.so`

BAP toolkit:

编译完成后会生成数个工具,包括:
toil: Lifting Binary Code to BIL
iltrans: Programs Transformations on BIL Code 
topredicate: Predicate-based Program Verification 
ileval: Concrete evaluation 
codegen: LLVM-based code generation

以上工具在handbook里都给出了简单的使用例子,而每个工具的详细使用方法都可以通过-help选项进行查看