【SVF-1】SVF过程间静态数值流分析简介
一、SVF介绍
1.SVF设计
svf框架是基于LLVM所写的,首先用clang将程序源码编译成bit code文件,然后使用LLVM Gold插件把bitcode文件整合到一个bc文件;指针分析——接着进行过程间的指针分析来生成指向信息;数值流构建——基于指向信息,构建内存SSA形式,这样就能识别顶层和地址变量的def-use关系链;应用——生成的数值流信息可用于检测数据泄露和空指针引用,也可以提高数值流分析和指针分析的精确度。
指针分析:指针分析的实现分为三个组件,分别是Graph,Rules和Solver。Graph从LLVM IR搜集抽象信息,确定对哪一部分进行指针分析;Rules定义了如何从语句中获得指向信息,例如graph中的约束;Solver确定约束的处理顺序。SVF提供了一个简洁可复用的接口,用户可以随意组合这三个组件来实现自己的指针分析。
数值流构建:基于获得的指向信息,我们实现了一个轻型的Mod-Ref Analysis,以寻找每个变量的过程间引用和被修改的副作用。给定Mod-Ref结果和指向信息,每个store/load/callsite的间接使用和定义都使用别名进行注释,每个别名都表示一组可以间接访问的抽象内存对象。注意,Open64和GCC都采用过程内的内存SSA,它是在过程内计算的,所有非局部变量都在一个单独的别名集中;相反,SVF提供了Mem Region Partitioning内存区域划分模块,允许用户定义自己的内存区域划分策略,以影响别名集的形成方式,这样在分析大型程序时可灵活地权衡可扩展性和精度。(总之,优点是能够划分模块进行分析)。
2.应用场景
(1)Source-Sink Analysis:如检测内存泄露漏洞,检查内存分配是否最终走到释放点,给定顶层和地址变量的数值流,SABER[36,37]/SPARROW[24]能检测到泄露漏洞,通过SVF框架还能检测double-free、文件open-close错误、污点数据使用错误。
(2)指针分析:能提高指针分析的可扩展性和准确性,例如SELFS[44],能基于数值流信息对部分程序区域实施选择流敏感指针分析;FSAM[34]是基于SVF的,能对多线程c程序进行线程交错分析,以进行稀疏流敏感指针分析。
(3)加速动态分析:动态分析,通过插桩监视程序执行行为,带来了运行时的开销。可以采用静态数值流信息来引导实施选择性插桩,这样就能消除一些不必要的插桩,降低运行开销。例如USHER[43]使用过程间数值流分析来识别多余的操作,移除该处的插桩,还能用于检测其他漏洞如空指针引用和缓冲区溢出[42];还可以与符号执行[10]和动态数据流测试[16]相结合,以更快生成更有意义的测试用例。
(4)程序调试与理解:SVF还能用于软件调试和程序理解[18,21,40],可以通过只追踪相关的数值流来寻找引发错误行为的语句,不必分析不相关的语句;可扩展和精确的过程间数值流分析也对软件可视化有帮助(code map[20])。
二、环境搭建
前4步,安装llvm和clang。
1.下载 LLVM-7.0.0, clang-7.0.0
2.解压
tar xf llvm-7.0.0.src.tar.xz
tar xf cfe-7.0.0.src.tar.xz
mv cfe-7.0.0.src llvm-7.0.0.src/tools/clang
3.创建目标build目录并make
mkdir llvm-7.0.0.obj
cd llvm-7.0.0.obj
cmake -DCMAKE_BUILD_TYPE=MinSizeRel ../llvm-7.0.0.src (or add "-DCMAKE_BUILD_TYPE:STRING=Release" for release version)
make -j8 #换 make V=1
4.添加LLVM和Clang的路径
export LLVM_SRC=/home/john/Desktop/kernel/llvm-7.0.0.src #路径要修改
export LLVM_OBJ=/home/john/Desktop/kernel/llvm-7.0.0.obj #路径要修改
export LLVM_DIR=/home/john/Desktop/kernel/llvm-7.0.0.obj #路径要修改
export PATH=$LLVM_DIR/bin:$PATH
#建议添加永久环境变量
$ sudo nano /etc/profile
#NODEPATH
export CLANG_PATH=/home/john/Desktop/kernel/llvm-7.0.0.obj/bin
export PATH=$PATH:$CLANG_PATH
安装SVF。
5.下载SVF源码
git clone https://github.com/SVF-tools/SVF.git SVF
6.用cmake构建SVF (也可以使用 build.sh 去构建release或debug版本的SVF)
cd SVF
mkdir Release-build
cd Release-build
cmake ../
make -j4
构建Debug版本:
cd SVF
mkdir Debug-build
cd Debug-build
cmake -D CMAKE_BUILD_TYPE:STRING=Debug ../
make -j4
7.添加SVF路径 ($SVF_HOME是本机的源码目录)
export PATH=$SVF_HOME/Release-build/bin:$PATH #路径要修改
#建议添加永久环境变量
$ sudo nano /etc/profile
export SVF_HOME=/home/john/Desktop/kernel/SVF #路径要修改
export PATH=$PATH:$SVF_HOME/Release-build/bin
source /etc/profile
8.编译单个c程序为LLVM bitcode文件,或者用llvm-link编译和链接多个文件。若要编译复杂的真实工程则需要使用 LLVM gold plugin。 安装步骤见 this 。
clang -c -emit-llvm -g example.c -o example.bc
clang -c -emit-llvm -g example1.c -o example1.bc
clang -c -emit-llvm -g example2.c -o example2.bc
llvm-link example1.bc example2.bc
9.设置环境变量
cd $SVF_HOME
. ./setup.sh
#若安装debug版本,则以下命令
cd $SVF_HOME
. ./setup.sh debug
三、使用方法
1.全程序分析
运行Andersen指针分析
wpa -ander example.bc
运行Andersen指针分析并生成全程序数值流图
wpa -ander -svfg example.bc
运行流敏感指针分析
wpa -fspta example.bc
2.分析输出
输出格式是 dot format,可以用 zgrviewer等工具展示。
dump CallGraph
wpa -ander -dump-callgraph example.bc
wpa -fspta -dump-callgraph example.bc
dump PAG (program assignment graph)程序赋值图
wpa -ander -dump-pag example.bc
Dump Constraint Graph
wpa -ander -dump-consG example.bc
Dump Value-Flow Graph
wpa -ander -svfg -dump-svfg example.bc
Dump Memory SSA
wpa -ander -svfg -dump-mssa example.bc
3.打印数据
wpa -ander -stat example.bc
wpa -fspta -stat example.bc
打印指向结果
wpa -ander -print-pts example.bc
wpa -fspta -print-pts example.bc
资料
主页:http://svf-tools.github.io/SVF/
github主页:https://github.com/SVF-tools/SVF
环境搭建:https://github.com/SVF-tools/SVF/wiki/Setup-Guide-(CMake)