【SVF-2】使用SVF进行简单分析

Posted 2023-03-15

参考技术A 我们使用一个例子来了解一下SVF的各个组件：(1) Memory Model 包含 PAG 和 Constraint Graph ；(2) Pointer Analysis 包含非流敏感分析和流敏感分析；(3) Value-Flow Construction 值流构建。

说明：展现了数值流的传递。

以上所示，PAG的一个node表示一个指针或抽象内存对象，圆圈表示指针( ValPN )，八边形表示抽象内存对象( ObjPN )。两个节点之间的边表示一个约束：绿边表示内存分配( AddrPE )，蓝边表示store( StorePE )，红边表示load( LoadPE )，黑点边表示参数传递( CallPE )。

( Constraint Graph )在Andersen的流敏感分析时用到，在基于包含的指针分析时，用到以下规则来求解程序约束。

分析时，新的copy边(实心黑色箭头)不断加入到约束图中，直到到达某个不动点，最终的约束图如下：

程序的( memory SSA )表示是通过添加MU和CHI函数到程序LLVM IR来构建的。

程序的过程间稀疏值流图( SVFG )是一个导向图，包含了顶层指针和对象的def-use链。

一个SVFG node可以是一个语句( PAGEdge )、一个参数或者一个内存区域（抽象对象集合）。

绿色矩形表示address PAG node内存对象( AddrPE )，红色矩形表示load PAG edge ( LoadPE )，蓝色矩形表示store PAG edge ( StorePE )。黄色矩形表示一个参数（如SVFG NodeID14，是一个实际参数，和PAG NodeID 21相关）或者表示函数entry或exit处、callsite处、load或store处的一个内存区域，例如，SVFG NodeID 27表示内存对象PAG NodeID 24在被调用函数swap中通过callsite ID 1间接读取。

SVFG可以使用（ SVFG Optimizer ）来消除不必要的node如ActualParm、AcutalIn、FormalRet、FormalOut，这样就更紧凑。

测试环境：Ubuntu 18.04。 源码示例

假设( wpa.cpp )是个使用SVF库的外部工程(注意：wap.cpp实际上是SVF的嵌入工具，我们只是用它作为例子，表示你也可以把SVF整合为你自己的工具链的一部分)，构建好SVF后需要添加以下环境变量。

首先需安装llvm-config，版本和编译SVF时的一样。

解释参数：

注意：保持参数顺序，否则会造成链接错误。

编译后得到可执行文件wpa.out，一个使用SVF作为库的外部工具。如果你想与SVF共享库Svf.so链接到一起，你可以使用以下命令：

CMake构建spa.cpp很容易。

模板是 CMakeList.txt , tools/CMakeLists.txt , wpa.cpp 。和 building SVF with CMake 一样，你需要export LLVM_DIR环境变量到包含LLVMConfig.cmake或LLVM-Config.cmake的目录；如果你用apt-get安装的话，这个目录通常是/usr/lib/llvm-7/lib，若用CMake从源码构建LLVM并使用默认安装目录，这个目录通常是/usr/local/lib/cmake/llvm。这个目录和使用SVF时导出的一样。

我们需要a graph、a solver和分析规则集合来实现指针分析，首先看看一个简单的流不敏感和域不敏感的基于包含的指针分析实现。你可能需要参考 Andersen.h 和 Andersen.cpp 来看看具体的实现。

1.从PAG构建约束图：

2.写一个约束求解器(对于更复杂的求解器，如wave propagation，请参考 AndersenWave.cpp 和 AndersenWaveDiff.cpp )：

3.处理不同约束的规则：

很容易基于过程间稀疏值流图来写source-sink分析，可以参考 LeakCheck.cpp 和 ProgSlice.cpp 的具体实现。

为了计算布尔值流guards，我们使用 CUDD-2.5.0 package (Binary Decision Diagrams -BDDs)来编码路径条件。

1.首先，使用Andersen的指针分析构建SVFG：

2.然后，选择候选的source和sink SVFGNodes集合：

3.最后，使用 AllPathReachableSolve 方法(来自 ProgSlice 类)来进行全路径可达性分析，通过迭代调用以下3个方法来计算值流guards，直到到达一个固定点。

https://github.com/svf-tools/SVF/wiki/Analyze-a-Simple-C-Program

https://github.com/SVF-tools/SVF/wiki/Using-SVF-as-a-lib-in-your-own-tool

https://github.com/SVF-tools/SVF/wiki/Write-a-flow--and-field---insensitive-pointer-analysis

https://github.com/SVF-tools/SVF/wiki/Write-a-source-sink-analyzer