SVF |
您所在的位置：网站首页 › 分析框架 › SVF |
SVF
|
请查看我的讲解视频以及ppt： 讲解视频：程序依赖图分析-SVFppt：程序依赖图——以SVF为例.pdf这篇文章包括： SVF介绍SVF源码解读SVF优势与不足如何扩展改进文章包括一些个人观点，若觉得有误请留言纠正，感谢🙏 在这篇文章之前强烈推荐看我公众号之前推的一篇文章：CG0’2011 “Flow-sensitive pointer analysis for millions of lines of code” 1. SVF简介 静态值流分析（Static Value Flow Analysis）：静态地识别程序的控制依赖，数据依赖。例如“程序点A的信息是否能沿着某些程序路径流到程序点B”，“是否存在触发bug的不安全的内存访问”。（刚开始可以，简单地看成Def-Use或者数据依赖分析即可） 变量的值流。LLVM中存在两类变量： 未被取过地址的变量（top-level pointer），这类变量在LLVM IR中是register value，显式地编码为SSA形式。被取过地址的变量（address-token variable），LLVM IR中是allocated memory objects，比较难去精确地计算这些内存变量的Def-Use关系。 Memory SSA：top-level pointer和address-token variable的Def-Use关系都被编码成SSA形式的IR。 注解： (1) 实际上最早03年斯坦福提出的IPSSA就已经解决了这类针对top-level和address-token变量的Def-Use关系的建模，并形成工具。(2) 07年是FastCheck利用SAT求解器消除一些误报，不过FastCheck不能处理address-token变量(3) SVF (Saber) 相当于把(1)和(2)的工作结合了，不过SVF最初的SAT求解使用BDD编码的，最新的版本是用Z3编码SAT公式。 3. SVF框架
(1) LLVM IR前端。Clang编译程序为LLVM IR，可使用wllvm之类的工具将bitcode链接合并，以实现全程序的符号表构建。 (2) 指针分析框架。“only andersen/steensgaard for pre-computed SVFG” (4) 供上层客户端使用。 4. 运行案例 4.1 Swap例子 通过一个完整的小例子简单介绍一下SVF中间的IR。 (1) 编译LLVM IR clang -S -c -Xclang -o0 -g -fno-discard-value-names -emit-llvm swap.c -o swap.ll opt -S -mem2reg swap.ll -o swap.ll
(2) 查看生成的Memory SSA wpa -ander -svfg -stat=false -dump-mssa swap.ll >> swap_ssa.txt
SVFStmt 绿色方框是AddrStmt，红色是LoadStmt，蓝色是StoreStmt，黑色是CopyStmt，紫色是GepStmt，灰色是单目双目运算操作CmpStmt，BinaryOpStmt，UnaryOpStmt。绿色是Fork/Join。Parameter。黄色方框表示参数。 memory region。黄色方框。函数entry/exit或者调用点/load/store处的memory region。虚线黑边为参数传递，点线黑边为函数返回值。 (4) 查看Andersen流不敏感指针分析的约束图 （参考SVF_EUROLLVM2016 page 8/26） wpa -nander -dump-pag -dump-constraint-graph -brief-constraint-graph=false swap.ll 下面是流不敏感指针分析的约束规则： 目的：主要观察SVF对全局变量的处理，以及路径敏感分析的能力。我们已知，SVF/Saber的路径敏感分析能力是SAT逻辑求解，所以能力仍然不够，这里通过一个例子来演示。 Juliet CWE的内存泄漏的一个刁钻例子，这个例子主要是有全局变量作为分支条件。 #include #include static int static_t = 1; /* true */ static int static_f = 0; /* false */ void CWE401_Memory_Leak__char_malloc_05_bad() { char * data; data = NULL; if(static_t) { /* POTENTIAL FLAW: Allocate memory on the heap */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } else { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* FIX: Use memory allocated on the stack with ALLOCA */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } if(static_t) { /* POTENTIAL FLAW: No deallocation */ ; /* empty statement needed for some flow variants */ } else { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* FIX: Deallocate memory */ free(data); } } static void goodB2G1() { char * data; data = NULL; if(static_t) { /* POTENTIAL FLAW: Allocate memory on the heap */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } else { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* FIX: Use memory allocated on the stack with ALLOCA */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } if(static_f) { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* POTENTIAL FLAW: No deallocation */ ; /* empty statement needed for some flow variants */ } else { /* FIX: Deallocate memory */ free(data); } } static void goodB2G2() { char * data; data = NULL; if(static_t) { /* POTENTIAL FLAW: Allocate memory on the heap */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } else { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* FIX: Use memory allocated on the stack with ALLOCA */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } if(static_t) { /* FIX: Deallocate memory */ free(data); } else { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* POTENTIAL FLAW: No deallocation */ ; /* empty statement needed for some flow variants */ } } static void goodG2B1() { char * data; data = NULL; if(static_f) { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* POTENTIAL FLAW: Allocate memory on the heap */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } else { /* FIX: Use memory allocated on the stack with ALLOCA */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } if(static_t) { /* POTENTIAL FLAW: No deallocation */ ; /* empty statement needed for some flow variants */ } else { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* FIX: Deallocate memory */ free(data); } } static void goodG2B2() { char * data; data = NULL; if(static_t) { /* FIX: Use memory allocated on the stack with ALLOCA */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } else { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* POTENTIAL FLAW: Allocate memory on the heap */ data = (char *)malloc(100*sizeof(char)); /* Initialize and make use of data */ strcpy(data, "A String"); } if(static_t) { /* POTENTIAL FLAW: No deallocation */ ; /* empty statement needed for some flow variants */ } else { /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ /* FIX: Deallocate memory */ free(data); } } void CWE401_Memory_Leak__char_malloc_05_good() { goodB2G1(); goodB2G2(); goodG2B1(); goodG2B2(); } int main(int argc, char * argv[]) { CWE401_Memory_Leak__char_malloc_05_good(); CWE401_Memory_Leak__char_malloc_05_bad(); return 0; } (1) 编译 clang -S -c -Xclang -o0 -g -fno-discard-value-names -emit-llvm malloc.c -o malloc.ll opt -S -mem2reg malloc.ll -o malloc.ll (2) 检测内存泄漏 saber -leak -stat=false malloc.ll
如果追踪污点时，污点流进全局变量，那么不继续追踪。这个跟误报原因无关，本cwe的例子是条件约束是全局变量。 约束求解。 实际上就是SAT求解（可参考FastCheck，最初Saber使用BDD进行SAT公式化简与编码）。  可以看到，约束求解条件生成部分都是SAT公式（布尔变量），并不会考虑条件变量的数据依赖以形成整型等式公式（整数算数理论，BitVector）。  其中newCond为每条if条件跳转命名一些布尔变量（fresh bool variable）。 
4.3 嵌入式C程序代码片段
场景：局部循环导致越界，全局数组元素变量作为整个循环的路径条件判断。 这里主要查看SVF如何对这样的嵌入式代码片段建模的（实际上SVF并不能检测越界问题） typedef unsigned int uint_32; uint_32 SPIZL_buffer[10][4]; uint_32 control_data[10]; #define CD_SPIYC_FLAG 0 #define CD_SPIZL_T1 1 #define CD_SPI_phead 3 #define CD_SPI_ptail 9 #define C_SPI_BUFFER_LENGTH 10 void Proc_process_Buffer_SPI() { uint_32 tempi, SPIbufdata[5]; if ((0x00 == control_data[1]) && (0x00 == control_data[0])) { if (control_data[3] != control_data[9]) { if (0x55000000 == (SPIZL_buffer[control_data[9]][0] & 0xFF000000)) { for (tempi = 0 ; tempi > case_mssa.txt wpa -ander -svfg -dump-vfg case.ll dot -Tpng -o svfg_final.svg svfg_final.dot 生成的IR如下：
应用场景：分析指针是否越界，但是指针是通过数组传入成为函数的参数的，静态无法直接知道它的大小，通过指针分析就可以知道。 被测程序： #include typedef double float64; typedef struct _SQuater { float64 arr[4]; } SQuater; void foo4(float64 *pQ) { pQ[4] = 0; } void foo5(SQuater *pQ) { pQ->arr[4] = 0; } int bar4() { float64 arr[4]; foo4(arr); SQuater *p = (SQuater *)malloc(sizeof(SQuater)); foo5(p); } 编译生成LLVM IR，生成Memory SSA，SVFG clang -S -c -Xclang -o0 -g -fno-discard-value-names -emit-llvm case.c -o case.ll opt -S -mem2reg case.ll -o case.ll wpa -ander -svfg -dump-mssa -stat=false case.ll >> case_mssa.txt wpa -ander -svfg -dump-vfg case.ll bar4中arr的全局数据依赖图： SVF源码结构大致如下： SVF中存在几种图： (1) PAG。Program Assignment Graph程序赋值图。SVF中的核心IR。可惜它是流不敏感的，上下文不敏感的。它的存在只是为了方便构造Memory SSA时，进行指针分析预分析。 它是用来初始化Andersen式指针分析，描述初始状态下指针变量间的集合包含关系的。 (2) Constraint Graph。指针分析约束图。指针分析初始状态下，它就是PAG的一份copy，随着Andersen指针分析的迭代，会在该图上添加约束边。 (3) Call Graph。调用图，最基础的图，可直接复用。 (4) ICFG。Inter-procedural Control Flow Graph。函数间控制流图，对LLVM IR指令进行了封装。可方便地用它进行对LLVM IR分析的二次开发。 (5) SVFG。SVFG的构造严格按照3个步骤完成：① 流不敏感指针分析 ② 插入Mu/Chi ③ Full SSA构造 ④ 连接函数间Def-Use，形成SVFG 5.2 Program Assignment Graph (PAG) SVF源码中SVFIR数据结构，就是PAG。SVF输入LLVM IR后，最初建立的图结构就是SVFIR，也叫PAG。PAG的设计就是给后续执行Andersen式的flow-,context-insensitive指针分析作准备的。所以不能够直接在SVFIR上作flow-,context-sensitive指针分析，因为它的图结构就是流不敏感，上下文不敏感的。 LLVM IR输入SVF后，转换为PAG。其中 ①节点为指针变量，或者抽象对象(alloca,malloc等)。②边表示指针变量之间的关系。 SVF中是这么定义PAG上的节点和边的：①typedef SVFVar PAGNode ②typedef SVFStmt PAGEdge。可以看到，节点就是变量，边就是被封装好的LLVM IR指令。 边的类型指令连边Address边p = alloca_ialloca_i ⟶ A d d r \stackrel{Addr}{\longrightarrow} ⟶Addr pCopy边p = qq ⟶ C o p y \stackrel{Copy}{\longrightarrow} ⟶Copy pLoad边p = *qq ⟶ L o a d \stackrel{Load}{\longrightarrow} ⟶Load pStore边*p = qq ⟶ S t o r e \stackrel{Store}{\longrightarrow} ⟶Store pField边p = q gep fq ⟶ . f \stackrel{.f}{\longrightarrow} ⟶.f p 给定如下源代码及其LLVM IR： Constraint Graph为Andersen指针分析约束图。指针分析的初始状态时，Constraint Graph为PAG的一份拷贝，然后根据Andersen指针分析的传播规则，沿着Constraint Graph的边不断迭代地传播指向信息，在这个迭代的过程中可能在Constraint Graph上引入新的节点和边。 指针分析传播的规则如下： Inter-procedural Control Flow Graph, ICFG就是经典的函数间控制流图，这里主要结合源码查看SVF是如何封装LLVM IR指令的。 SVF中ICFG相关的数据结构如下： ICFG: 全程序的函数间控制流图。 ICFGEdge: ICFG的边，3个子类：IntraCFGEdge，CallCFGEdge，RetCFGEdge ICFGNode: ICFG的节点，7个子类：InterICFGNode（子类CallICFGNode，RetICFGNode，FunEntryICFGNode，FunExitICFGNode，GlobalICFGNode），IntraICFGNode。 每个ICFGNode都包含了SVFStmt，即LLVM IR指令的封装。每个SVFStmt实际上都可以在PAG上找到对应的边（PAGEdge），因为PAGEdge就是描述了一条指令，只不过边的用途是用来表示指针间的包含约束关系。 SVFStmt为LLVM IR指令封装的基类。子类为： AssignStmt AddrStmt: lhs = &rhsCallPE: lhs = call_fun (arg1, arg2, …)CopyStmt: lhs = rhsGepStmt: lhs = rhs -> field1 -> field2LoadStmt: lhs = *rhsStoreStmt: *lhs = rhsRetPE: return ®?TDForkStmt: fork()TDJoinStmt: join() MultiOpndStmt BinaryOpStmt: lhs = a op bCmpStmt: lhs = a cmp bPhiStmt: lhs = phi (op1, op2, …)SelectStmt: lhs = c ? rhs1 : rhs2 BranchStmt: if语句或者switch语句 switch/if (cond): case a1: goto label1 case a2; goto label2 … UnaryOpStmt: lhs = op rhs SVF指令中变量为SVFVar，它同时又是PAG中的节点，所以它有一个唯一节点ID，有前驱/后继边（PAGEdge）表示与它相关的语句（PAGEdge，SVFStmt）。 它的子类如下：DummyObjVarDummyValVarFIObjVar。o.*，字段不敏感时生成ObjVar: 抽象对象 MemObj。alloca, malloc等。GepObjVar。o->field，表示MemObj的一个字段 ValVar: 指针变量 GepValVar。var->field，表示指针变量的一个字段 RetPN: 返回值变量 5.3 Sparse Value-Flow Graph Sparse Value-Flow Graph, SVFG的构造分为如下几个阶段： SVF自带的流敏感指针分析实现。①在PAG上构造Constraint Graph执行预分析，flow-,context-insensitive Andersen式全程序指针分析AndersenWaveDiff。②利用已有全程序指针分析结果对程序划分内存 ③构造Full SSA，连接全程序函数间Def-Use形成SVFG ④在稀疏图上执行稀疏指针分析，该指针分析是流敏感的。 可以看到在PAG IR上不能直接作流敏感指针分析，也不能作单函数模块化指针分析。SVF的框架要求它先构造全程序Memory SSA，SVFG，然后在SVFG上执行稀疏的流敏感指针分析。 所以，我们的任务是作模块化的，单函数流敏感的指针分析，不能在PAG/SVFIR上作，因为它是全程序的，flow-,context-insensitive的。于是得在SVF封装的Interprocedural Control Flow Graph (ICFG)上自己重新实现一套。 方案：①利用SVF提供的Steensgaard执行指针分析并构造调用图 ②在SVF提供的ICFG上对每个函数作单函数，流敏感的模块化指针分析。③利用单个函数指针分析的结果对每个函数单独构造Memory SSA。③连接单函数，函数间Def-Use形成数据依赖图。 优点：(全程序)指针分析框架比较成熟，能够支持并切换各种指针分析。 |
(3) 构造Def-Use关系 （Memory SSA）。
(3) 生成SVFG，dot调试查看
其中，SVF节点
下面是生成的约束图： 
报告5个，误报4个。分析原因：5个case每个case中都存在全局变量作为分支条件，但是SVF利用SAT求解器没有对全局变量进行跨函数整数等式逻辑的处理，具体查看IR: 下面是goodG2B1函数的LLVM IR： 
下面是Memory SSA：
查看SVFG：
从图中可以看到，全局变量是全部考虑进来的(actual -> formal)，并不是误报的原因。下面分析误报原因，分析方法为调试跟踪SVF的Saber运行源代码。 
Saber在作污点分析的时候：
生成的MemorySSA如下： 
生成SVFG如下： 
下面是control_data[]的局部数据依赖关系图： 
下面是SPIZL_buffer[][]的局部数据依赖图： 
下面是SPIbufdata[]的局部数据依赖图： 
查询指针分析结果 （指针指向的数组类型，可用于检查数组越界） 
bar4中p的全局数据依赖图： 
输入SVF，解析并生成如下PAG/SVFIR： 
下图为约束图上指针分析传播的示意图： 
（1）Andersen-style Flow-, Context-Insensitive Pointer Analysis。输入LLVM IR，构造PAG，并克隆一份PAG形成Constraint Graph，在Constraint Graph上执行全程序Andersen式流-上下文不敏感指针分析。 SVF中默认使用AndersenWaveDiff全程序指针分析作预分析。 （2）依据已有的全程序指针分析结果，对内存进行划分。 （3）根据划分的内存，对每个Load，Store，Call语句插入Mu/Chi语句。然后根据经典的SSA构造算法构造SSA。 （4）根据SSA连接所有的Def-Use。
正如上图所示，流不敏感指针分析，上下文敏感指针分析在Constraint Graph上进行。因为ConstraintGraph是流不敏感的，它不考虑指令的先后顺序。 而流敏感，路径敏感指针分析是在SVFG上进行的。它要求先预分析构造Memory SSA，SVFG，然后再在SVFG上进行稀疏指针分析。
MemorySSA目前两阶段：流不敏感全程序指针分析 + MemorySSA构造。第一阶段进行全程序指针分析时，针对大程序可能会存在性能问题，不过嵌入式程序规模应该没问题（待测试）。同时，SVF中所有全局变量副作用显式化，针对嵌入式全局变量多的情况，可能会存在构造的SVFG巨大，而导致的性能问题。 指针分析对数组偏移不敏感，arr[1]与arr[2]等同于arr[*]，只是针对数组元素赋值不执行强更新（Strong Update）。 业界主流商业工具类似CodeSonar，Coverity都是使用模块化指针分析。而非SVF类似的全程序指针分析（层次化的，先进行全程序指针分析然后再进行缺陷检测） 目前的框架Saber支持的检查器，是利用Z3进行SAT求解，所以相对来说误报率会高一些。改进的点就是传递闭包地计算条件分支变量的数据依赖，并转换为SMT算数理论公式。 SVF框架主要针对SourceSink类污点分析，数值类的缺陷检测基础设施仍然不够完善。不过最新的代码似乎已经着手开发了（抽象解释）：svf/include/AbstractExecution (https://github.com/SVF-tools/SVF/issues/1039)【本文地址】
今日新闻 |
推荐新闻 |