SVF Saber

1.基本原理
2.API类型定义
3.Memory Leak Checker
- 3.1.示例
- 3.2.初始化
- 3.3.程序切片
- 3.4.路径约束求解
- 3.5.报告错误
4.总结
5.参考文献

Saber是一个静态漏洞检测器，最初集成到open64中，现已集成到SVF中，主要检测内存泄漏，DoubleFree，操作（检查open/close是否一致）。

1.基本原理

关于内存泄漏检测可以参考Saber paper 2.6章，主要的思路是

进行指针分析和value flow分析建立sparse value flow graph
基于sparse value flow graph（svfg）进行some path分析，即在value flow graph上进行source-sink分析（从 malloc 到 free 的svfg路径）。如果一个source点不能在svfg上到达sink点，那么表示该 malloc 从没有被 free，一定存在内存泄漏，报出 NeverFree 错误。
接下来进行all path分析，主要目的是确保在每个control-flow路径上source点都能达到sink点，如果存在一个control-flow路径source点没有到达sink点，那么报出 PartialLeak 错误。

关于all path分析，作者定义了如下概念:

S: $S_{src}$ 表示source点在value flow graph上可达的所有sink点
vfpaths(src, tgt): 从source点 src 到sink点 tgt 的所有value- flow路径（可能不止有1条路径）
vfguard(P): value flow路径 P 的路径条件， $\bigwedge_{(p, q) \in P} cfguard(p, q)$ ，(p, q) 是一个value-flow（def-use）路径。
FREED(src): $\bigvee\limits_{tgt \in S_{src}}(\bigvee_{P \in vfpaths(src, tgt)} vfguard(P))$ ， $\equiv true$ 表示 src 分配的内存一定会被free，反之则表示可能在某些路径存在泄漏，需要报出 PartialLeak 错误。前面的公式表示对应一对 (src, tgt)，如果这对中间有一个value flow path对应的路径条件一定能得到满足，那么 src 不管沿着哪条control-flow路径都能到达 tgt。对于一个 src 点，在value-flow graph中所有可达的sink点中，只要有1个一定可达，那么该 src 点一定会被 free。
cfpaths(p, q): 表示def点 p 到use点 q 之间所有的控制流路径。
cfguard(p, q) 表示def点 p 到use点 q 之间的路径条件，为 true 表示在控制流图上 p 一定能到达 q。 $\bigvee_{Q \in cfpaths(p, q)} pguard(Q)$ 。Q 为一条控制流路径。
pguard(Q) 表示控制流路径 Q 的路径条件， $\bigwedge_{e \in E(Q)} eguard(e)$ ，E(Q) 为 Q 上的边集合， eguard(e) 为边 e 对应的约束条件。

2.API类型定义

Saber的入口文件是Saber.cpp，可以看到：

FileChecker 类实现对File操作的检查。
DoubleFreeChecker 类实现对DoubleFree的检查。
LeakChecker 类实现对Use-After-Free和其它泄漏漏洞的检查。

其中 DoubleFreeChecker 和 FileChecker 继承自LeakChecker，因此先看看 LeakChecker。

首先Saber中定义了4种API类型，参考SaberCheckerAPI.h，具体的API名称在SaberCheckerAPI.cpp中可查看，包括

SaberCheckerAPI::CK_ALLOC：包括 malloc, alloc 等，isMemAlloc 函数判断给定API是否属于 Alloc。
SaberCheckerAPI::CK_FREE：包括 free 等函数，isMemDealloc 判断给定API是否属于 CK_FREE。
SaberCheckerAPI::CK_FOPEN：包括 fopen 等函数，isFOpen 判断给定API是否属于 CK_FOPEN。
SaberCheckerAPI::CK_FCLOSE：包括 fclose, pclose 等函数，isFClose 判断给定API是否属于 CK_FCLOSE。

同时定义了一个 StringMap 类变量 TDAPIMap 来将函数名映射为 type。

3.Memory Leak Checker

执行Checker调用的函数顺序如下：

main -> LeakChecker:runOnModule -> SrcSnkDDA::analyze

分析的主要过程是在 SrcSnkDDA::analyze 中实现，而LeakChecker 主要重新定义了 src 和 sink 相关信息。

3.1.示例

取自saber论文中的样例，改写之后如下

#include <stdio.h>
#include <stdlib.h>


char** readBuf() {
   char** mBuf = (char**)malloc(2*sizeof(char*)); //o
   *mBuf = (char*)malloc(10*sizeof(char)); //o1
   scanf("%6s", *mBuf);  //... (write into **mBuf);
   return mBuf;
}

void freeBuf(char** fBuf) {
    char* z = *fBuf;
    free(z);
    free(fBuf);
}

int main() {
    for (int i = 0; i < 100; ++i) {
        char** buf = readBuf();
        char* tmp = *buf;
        if (*tmp != '\n')
            printf("%s\n", tmp);
        else
            continue;
        freeBuf(buf);
    }
    return 0;
}

LLVM IR如下

; ModuleID = 'test.c'
source_filename = "test.c"
target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
target triple = "arm64-apple-macosx12.0.0"

@.str = private unnamed_addr constant [4 x i8] c"%6s\00", align 1
@.str.1 = private unnamed_addr constant [4 x i8] c"%s\0A\00", align 1

; Function Attrs: noinline nounwind optnone ssp uwtable
define dso_local i8** @readBuf() #0 {
entry:
  %mBuf = alloca i8**, align 8
  %call = call i8* @malloc(i64 16) #3
  %0 = bitcast i8* %call to i8**
  store i8** %0, i8*** %mBuf, align 8
  %call1 = call i8* @malloc(i64 10) #3
  %1 = load i8**, i8*** %mBuf, align 8
  store i8* %call1, i8** %1, align 8
  %2 = load i8**, i8*** %mBuf, align 8
  %3 = load i8*, i8** %2, align 8
  %call2 = call i32 (i8*, ...) @scanf(i8* getelementptr inbounds ([4 x i8], [4 x i8]* @.str, i64 0, i64 0), i8* %3)
  %4 = load i8**, i8*** %mBuf, align 8
  ret i8** %4
}

; Function Attrs: allocsize(0)
declare i8* @malloc(i64) #1

declare i32 @scanf(i8*, ...) #2

; Function Attrs: noinline nounwind optnone ssp uwtable
define dso_local void @freeBuf(i8** %fBuf) #0 {
entry:
  %fBuf.addr = alloca i8**, align 8
  %z = alloca i8*, align 8
  store i8** %fBuf, i8*** %fBuf.addr, align 8
  %0 = load i8**, i8*** %fBuf.addr, align 8
  %1 = load i8*, i8** %0, align 8
  store i8* %1, i8** %z, align 8
  %2 = load i8*, i8** %z, align 8
  call void @free(i8* %2)
  %3 = load i8**, i8*** %fBuf.addr, align 8
  %4 = bitcast i8** %3 to i8*
  call void @free(i8* %4)
  ret void
}

declare void @free(i8*) #2

; Function Attrs: noinline nounwind optnone ssp uwtable
define dso_local i32 @main() #0 {
entry:
  %retval = alloca i32, align 4
  %i = alloca i32, align 4
  %buf = alloca i8**, align 8
  %tmp = alloca i8*, align 8
  store i32 0, i32* %retval, align 4
  store i32 0, i32* %i, align 4
  br label %for.cond

for.cond:                                         ; preds = %for.inc, %entry
  %0 = load i32, i32* %i, align 4
  %cmp = icmp slt i32 %0, 100
  br i1 %cmp, label %for.body, label %for.end

for.body:                                         ; preds = %for.cond
  %call = call i8** @readBuf()
  store i8** %call, i8*** %buf, align 8
  %1 = load i8**, i8*** %buf, align 8
  %2 = load i8*, i8** %1, align 8
  store i8* %2, i8** %tmp, align 8
  %3 = load i8*, i8** %tmp, align 8
  %4 = load i8, i8* %3, align 1
  %conv = sext i8 %4 to i32
  %cmp1 = icmp ne i32 %conv, 10 # 这个指令对应 *tmp != '\n'，是all path分析中唯一出现的路径约束
  br i1 %cmp1, label %if.then, label %if.else

if.then:                                          ; preds = %for.body
  %5 = load i8*, i8** %tmp, align 8
  %call3 = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([4 x i8], [4 x i8]* @.str.1, i64 0, i64 0), i8* %5)
  br label %if.end

if.else:                                          ; preds = %for.body
  br label %for.inc

if.end:                                           ; preds = %if.then
  %6 = load i8**, i8*** %buf, align 8
  call void @freeBuf(i8** %6)
  br label %for.inc

for.inc:                                          ; preds = %if.end, %if.else
  %7 = load i32, i32* %i, align 4
  %inc = add nsw i32 %7, 1
  store i32 %inc, i32* %i, align 4
  br label %for.cond, !llvm.loop !7

for.end:                                          ; preds = %for.cond
  ret i32 0
}

declare i32 @printf(i8*, ...) #2

attributes #0 = { noinline nounwind optnone ssp uwtable "disable-tail-calls"="false" "frame-pointer"="non-leaf" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-a12" "target-features"="+aes,+crc,+crypto,+fp-armv8,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.3a,+zcm,+zcz" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { allocsize(0) "disable-tail-calls"="false" "frame-pointer"="non-leaf" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-a12" "target-features"="+aes,+crc,+crypto,+fp-armv8,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.3a,+zcm,+zcz" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #2 = { "disable-tail-calls"="false" "frame-pointer"="non-leaf" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-a12" "target-features"="+aes,+crc,+crypto,+fp-armv8,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.3a,+zcm,+zcz" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #3 = { allocsize(0) }

!llvm.module.flags = !{!0, !1, !2, !3, !4, !5}
!llvm.ident = !{!6}

!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{i32 1, !"branch-target-enforcement", i32 0}
!2 = !{i32 1, !"sign-return-address", i32 0}
!3 = !{i32 1, !"sign-return-address-all", i32 0}
!4 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
!5 = !{i32 7, !"PIC Level", i32 2}
!6 = !{!"clang version 12.0.0"}
!7 = distinct !{!7, !8}
!8 = !{!"llvm.loop.mustprogress"}

value flow graph如下（没有截取全部，只是一些关键部分），图中红框为识别的source点，蓝框为sink点（sink点不是 call 指令而是对应的加载参数指令，可能是因为 call 指令并没有出现在value flow graph中）。

第一部分
请添加图片描述第二部分

请添加图片描述

3.2.初始化

SrcSnkDDA::analyze 首先调用 SrcSnkDDA::initialize

void SrcSnkDDA::initialize(SVFModule* module)
{
	PAGBuilder builder;
	PAG* pag = builder.build(module);

    AndersenWaveDiff* ander = AndersenWaveDiff::createAndersenWaveDiff(pag);
    svfg =  memSSA.buildPTROnlySVFG(ander);
    setGraph(memSSA.getSVFG());
    ptaCallGraph = ander->getPTACallGraph();
    //AndersenWaveDiff::releaseAndersenWaveDiff();
    /// allocate control-flow graph branch conditions
    getPathAllocator()->allocate(getPAG()->getModule());

    initSrcs();
    initSnks();
}

主要流程是：

之后就是初始化source和sink点，LeakChecker, FileChecker 和 DoubleFreeChecker 都是基于相关API调用识别source和sink点。初始化source和sink集合的方法也相同，主要的区别在于关注的API类型不同，具体的差别在 isSinkLikeFUn 和 isSourceLikeFun 中

先看LeakChecker 的 isSourceLikeFun 和 isSinkLikeFun。LeakChecker 将 CK_ALLOC 视为 src 点而将 CK_FREE 类视为 sink 点。

初始化src 点的代码可以参考 LeakChecker::initSrcs 函数。主要是将 malloc 类的函数调用添加到 src 点中，如果存在多层嵌套情况，比如

char *customizedMalloc() {
	char *buf = (char*)malloc(10);
	// ... read content to buf
	return buf;
}

int main() {
    char *buf = customizedMalloc();
    return 0;
}

那么被添加到 src 集合的是 customizedMalloc 调用而不是 malloc。

初始化 sink 点的代码可以参考 LeakChecker::initSnks，这里主要关注 free 类函数调用，并将对应参数加载指令（不是 call 指令）添加到 sink 集合。

%4 = bitcast i8** %3 to i8*
call void @free(i8* %4)

上述IR中，加载参数的指令是 %4 = bitcast i8** %3 to i8*，因此该指令会被添加为 sink 点而不是 free 函数调用。这么设计的一个原因可能是对应 free 调用并不会出现在value flow graph中，取而代之的是参数加载指令（这点是本人推测，目前对value flow graph不是很熟，欢迎大佬指正）。

3.3.程序切片

这部分即some-path分析，代码参考SrcSnkDDA::analyze，主体代码如下：

for (SVFGNodeSetIter iter = sourcesBegin(), eiter = sourcesEnd(); iter != eiter; ++iter){
    setCurSlice(*iter); // 初始化该source点对应的切片
      
    ContextCond cxt;
    DPIm item((*iter)->getId(),cxt);
    forwardTraverse(item); // 从source点开始前向遍历

    /// do not consider there is bug when reaching a global SVFGNode
    /// if we touch a global, then we assume the client uses this memory until the program exits.
    if (getCurSlice()->isReachGlobal()) // 如果涉及到全局变量，那么不认为会出现bug
        DBOUT(DSaber, outs() << "Forward analysis reaches globals for slice:" << (*iter)->getId() << ")\n");
       
    else {
        // 前向遍历会将从source点可达的所有value flow graph结点添加到forwardSlice集合中，下面的for循环会遍历所有source点可达的sink点
        for (SVFGNodeSetIter sit = getCurSlice()->sinksBegin(), esit = getCurSlice()->sinksEnd(); sit != esit; ++sit) {
            ContextCond cxt;
            DPIm item((*sit)->getId(),cxt);
            // 从sink点开始反向遍历
            backwardTraverse(item);
        }

        if(_curSlice->AllPathReachableSolve())
            _curSlice->setAllReachable();

   }

   reportBug(getCurSlice());
}

每个切片都会包含 forwardslice, backwardslice, sinks, partialReachable, fullReachable, reachGlob 等局部变量。其中

partialReachable 表示source点沿着某些控制流路径可能到达sink点。
fullReachable 表示source点沿着每条控制流路径都能到达sink点（也就是source点一定会经过sink点）。
reachGlob 表示这个切片是否会到达局部变量。

forwardTraverse 和 backwardTraverse 都是采用worklist算法前向/反向遍历从指定结点可达的所有结点，需要关注的有SrcSnkDDA::FWProcessCurNode 和 SrcSnkDDA::BWProcessCurNode。这2个函数分别是前向/反向对每个结点的处理过程。

前向遍历时需要将每个访问的结点添加到 forwardslice，如果遍历的结点属于sink点，那么再将它添加到 sinks 集合中。
反向遍历时如果该结点在 forwardslice 集合中，那么将它添加到 backwardslice 集合中。

用上面示例对应的部分value flow graph来说明

请添加图片描述
图中蓝框87号结点为source点，最右下角绿框中90号为sink点，那么

蓝框 + 红框部分为 forwardslice 的内容。
蓝框 + 3个绿框为 backwardslice 中的内容。

可以看到slice的主要目的是找到从source点到sink点的路径， backwardslice 中不应有除了路径以外的结点。

3.4.路径约束求解

这一部分即all-path分析，主要由上面代码中 _curSlice->AllPathReachableSolve() 完成，ProgSlice::AllPathReachableSolve 主要是对该 slice 上 backwardslice 上的所有结点进行约束求解，看看是否所有的控制流路径都能得到满足。

主要代码如下（删除了一些代码，部分打了注释）

// 这个函数主要进行路径约束合并
bool CustomizedProgSlice::AllPathReachableSolve()
{
    const SVFGNode* source = getSource();
    VFWorkList worklist;
    worklist.push(source);
    /// 将初始路径约束设置为true
    setVFCond(source,getTrueCond());

    while(!worklist.empty())
    {
        const SVFGNode* node = worklist.pop();
        setCurSVFGNode(node);
        Condition* cond = getVFCond(node);
        for(SVFGNode::const_iterator it = node->OutEdgeBegin(), eit = node->OutEdgeEnd(); it!=eit; ++it)
        {
            const SVFGEdge* edge = (*it);
            const SVFGNode* succ = edge->getDstNode();
            // 只对backwardslice上的结点进行求解
            if(inBackwardSlice(succ))
            {
                Condition* vfCond = nullptr;
                // 将value flow node映射为basic block node，每个value flow node结点都保存了一个指针类型局部变量指向对应ICFG结点，而ICFG又保存了一个指针指向basic block
                const BasicBlock* nodeBB = getSVFGNodeBB(node);
                const BasicBlock* succBB = getSVFGNodeBB(succ);

                errs() << "current SVFG node: " << node->toString() << "\n";
                errs() << "succeed SVFG node: " << succ->toString() << "\n";
                errs() << "current basic block\n";
                nodeBB->dump();
                errs() << "succeed basic block\n";
                succBB->dump();


                /// clean up the control flow conditions for next round guard computation
                clearCFCond();
							
							 // 根据不同的情况计算当前value flow edge对应的路径约束条件 
                if(edge->isCallVFGEdge())
                {
                    vfCond = ComputeInterCallVFGGuard(nodeBB,succBB, getCallSite(edge)->getParent());
                }
                else if(edge->isRetVFGEdge())
                {
                    vfCond = ComputeInterRetVFGGuard(nodeBB,succBB, getRetSite(edge)->getParent());
                }
                else
                    vfCond = ComputeIntraVFGGuard(nodeBB,succBB); // cfguard(node, succ) = pguard(Q1) or ... pguard(Qn)

                // vfguard(P) = vfguard(P-) and cfguard(node, succ)，
                Condition* succPathCond = condAnd(cond, vfCond);
                // cfguard(p, q) = pguard(Q1) or ... pguard(Qm)
                if(setVFCond(succ,  condOr(getVFCond(succ), succPathCond) ))
                    worklist.push(succ);
            }

            DBOUT(DSaber, outs() << " node (" << node->getId()  <<
                                 ") --> " << "succ (" << succ->getId() << ") condition: " << getVFCond(succ) << "\n");
        }
    }

    return isSatisfiableForAll();
}

/*!
 * Solve by computing disjunction of conditions from all sinks (e.g., memory leak)
 * 路径约束求解
 */
bool CustomizedProgSlice::isSatisfiableForAll()
{

    Condition* guard = getFalseCond();
    // each it represents vfguard(src, it);
    for(SVFGNodeSetIter it = sinksBegin(), eit = sinksEnd(); it!=eit; ++it)
        guard = condOr(guard,getVFCond(*it));

    setFinalCond(guard);
    errs() << "final condition: " << guard->getExpr().to_string() << "\n";
    return pathAllocator->isAllPathReachable(guard);
}

在计算路径约束部分，不管是value-flow还是control-flow graph，路径上的每个结点都会映射一个约束条件，给定下面示例（结点是指令，边包含约束条件）

vfcond(inst1) = true
vfcond(inst2) = c1
vfcond(inst3) = c2
vfcond(inst4) = (c1 and c4) or (c2 and c3)

在Saber约束求解部分我并没有发现调用z3的代码，貌似saber会将每个路径约束计作 c1, c2 ..., cn 格式并做简单SAT求解，并不会进行复杂的约束求解。

上面出现的示例中唯一出现的约束条件是 %cmp1 = icmp ne i32 %conv, 10，在求解中会被转换成谓词 c1。这个约束条件在求解value flow edge store i8** %call, i8*** %buf, align 8 ----> %7 = load i8**, i8*** %buf, align 8会出现。这2条指令对应的basic block分别是

for.body:                                         ; preds = %for.cond
  %call = call i8** @readBuf()
  store i8** %call, i8*** %buf, align 8
  %1 = load i8**, i8*** %buf, align 8
  %2 = load i8*, i8** %1, align 8
  store i8* %2, i8** %tmp, align 8
  %3 = load i8*, i8** %tmp, align 8
  %4 = load i8, i8* %3, align 1
  %conv = sext i8 %4 to i32
  %cmp1 = icmp ne i32 %conv, 10
  br i1 %cmp1, label %if.then, label %if.else

和

if.end:                                           ; preds = %if.then
  %7 = load i8**, i8*** %buf, align 8
  call void @freeBuf(i8** %7)
  br label %for.inc

3.5.报告错误

参考LeakChecker::reportBug，如果 isAllPathReachable() == false && isSomePathReachable() == false，也就是一条从 malloc 到 free 的路径都不存在，那么报出 NeverFree 错误（个人感觉按照paper所说 isSomePathReachable 就可以报出了，不需要再做all-path分析了）。如果 isAllPathReachable() == false && isSomePathReachable() == true 那么表示存在某些控制流路径会导致泄漏，报出 PartialLeak 错误。

FileChecker 的原理类似，不过是将 malloc, free 替换成 fopen, fclose。

上面示例会报出2个partial leak错误，对应的slice分别是2个示例value flow graph中从红框到蓝框的那条路径。

4.总结

这篇blog主要说明saber是如何基于sparse value flow graph进行source-sink分析查找memory leak漏洞，double free和file close的原理类似。尚未提到的内容有：

sparse value flow graph的建立过程，包括怎么映射到ICFG node。
all-path分析时候是如何进行路径条件求解的，这里只是看了一下代码发现不是调用z3进行约束求解，再dump了一下路径约束发现dump出来的是 c1 这种简化表达式，于是猜测可能只是将碰到的条件表达式简化成 ci 形式进行简单SAT求解，论文中提到的BDD或许是一种SAT求解的优化形式。

不过saber貌似可能对不同优化程度编译出来的IR会产生不同的结果，这个还得看看后续会如何改进。

5.参考文献

[1] Sui Y , Ye D , Xue J . Static memory leak detection using full-sparse value-flow analysis[C]// International Symposium on Software Testing and Analysis. ACM, 2012.