2010‘FSE-Practical and Effective Symbolic Analysis for Buffer Overflow Detection 利用符号分析方法检测缓冲区溢出

本文只是试着读一读，若有理解错误的地方，望指正，谢谢！（～求生欲拉满。

今天继续读缓冲区溢出检测技术，这篇文章发表在2010年的FSE会议上。一作是中科院计算所李炼老师，彼时作者仍在Oracle澳大利亚实验室，相关的研究被应用到Oracle内部的静态分析器Parfait，后在国内商业化中科天齐悟空静态分析工具（点击详情）。

作者在本文提出一个新的利用符号分析来检测缓冲区溢出的方法，该方法是路径敏感的，能够处理循环等复杂特性。该方法能够在11分钟内分析860万行代码，误报率低于10%。

1. 简介

公众号之前已经讨论过几个数值相关的缺陷检测技术。

FSE’03 ARCHER - 路径敏感的内存越界检查中提到，利用符号执行，沿着调用图自底向上对每个函数构建trigger summary。这种方法简单地将循环特殊处理（例如展开一次，对for循环直接给出循环不变式。
ICSE’08 - 路径敏感bug-finding工具Calysto 中与FSE’03 ARCHER类似的方法，利用符号执行，沿着调用图自底向上对每个函数构造最大共享图（MSG），该图上编码了控制依赖，数据依赖，以及函数的副作用摘要。该方法也是简单的将循环展开一次。
ICSE’22 数值除零bug检测中作者利用VFG上编码的数据依赖，控制依赖信息，迭代地计算每个节点的符号值（Guarded Symbolic Value Set），然后利用SMT求解器求解divisor的符号值是否可能为0。该方法是intra-procedural的，循环展开一次。

另外，还有抽象解释方法，精心设计各种数值抽象域对程序进行抽象解释，生成循环不变式，最经典的工具有Astree分析器[1]。B站上有抽象解释相关的视频：数值程序分析

作者提出的方法是：demand-driven地针对缓冲区访问索引变量，求解其数据依赖的符号值，并利用控制依赖的符号值精化该值。该过程是迭代地进行求解，所以能够很好地处理循环。

下面是一个例子：

左侧是源代码，右侧是对应的LLVM IR，它是partial SSA的。

在LLVM IR上构建CFG后，提取出控制依赖，数据依赖得到简化后的图叫做Reduced Dependency Graph，下面是一个例子：

然后在此(稀疏地)图上迭代地进行符号分析。下面对作者的符号分析方法进行研究。

注意，作者的方法只处理top-level变量，所以虽然误报率比较低，但是会存在一些漏报，作者在实验作了说明。

2. 符号分析方法

2.1 符号值的表示

作者使用符号化的区间来表示变量(partial SSA’s top-level variable)的值。

变量V在指令P处的符号值为一个符号化区间，表示为 E=[SV,Pmin,SV,Pmax]E = [S_{V,P_{min}}, S_{V,P_{max}}]E=[SV,Pmin,SV,Pmax]
定义E上的偏序E1 < E2 当且仅当 E1 - E2不会大于0 (偏序<可以简单理解为小于等于) ;
对任意E, $ E < \top , \bot < E$
[⊤,⊥][\top, \bot][⊤,⊥] 表示空范围

meet, join操作也很直观（分别对应最大下界，最小上界）

两个符号范围的并集，交集也很直观（理解为两个区间的并集，交集即可）

并集：左侧取更小的，右侧取更大的 (例如[-1, 2] U = [0, 1] = [-1, 2])
- 主要用在符号值的保守运算，以及phi节点的数据依赖汇聚传播
交集：左侧取更大的，右侧取更小的 (例如[-1, 2] ∩\cap∩ [1, 3] = [1, 2])
- 主要用在控制依赖精化符号值

给定表达式Buff[v], 令B为缓冲区的大小符号值，V为索引变量符号值，则如下条件成立，则报告缓冲区溢出缺陷：KaTeX parse error: Undefined control sequence: \or at position 34: …_{V,P_{max}} ) \̲o̲r̲ ̲(S_{V,P_{min}} … 。这里的<是偏序关系上的小于 (数值上的小于等于)

2.2 符号值的代数运算

给定两个符号值，它们的代数运算如下表所示。

它的计算规则是保守的，也就是上近似。所以对于特定的符号值，如果：判断它的索引区间在缓冲区大小内，则保证不会缓冲区溢出。否则，潜在缓冲区溢出缺陷。

2.3. 数据依赖传播符号值

上文提到，在Reduced Dependency Graph上存在数据依赖，控制依赖。先传播数据依赖的符号值。下面是传播规则：

针对运算规则，进行符号值的代数运算
针对phi节点，取并集
Load是作者的特殊处理，算是挽救一下弥补不能处理堆元素的缺点。如果针对指令 V = A[I]，A是一个常数数组，即在编译时就能够确定其内存值的数组，例如 int[] A = {1, 2, 3, 4};
针对外界环境，配置等未知值，设置为类型的整个区间。
针对不能处理的语言特性，设置为该变量符号本身。

2.4 控制依赖精化数据依赖得到的值

在数据依赖传播完符号值之后，开始利用控制依赖精化该值。值得注意的是，作者提出的方法只处理这种严格控制依赖。如下所示的代码：

a = xxx;         // def aif (a >= b) {    // op1 op op2 // 并且V求出的符号值可以写成 op1的形式: // V = C1 * op1 + C2// ...V = C1 * a + C2  // use a
}

应用控制依赖精化符号值的规则如下：

3. 提升方法

上面的符号分析方法是最基本的方法，有两个方法可以提升。

3.1 循环归纳变量分析 (Loop Induction Variable Analysis)

把循环迭代次数的变量认为是induction variable, 因为它常常被用作循环内的缓冲区下标访问。

for (int i = 0 ; i < ite_num ; i++ ) {  // 考虑ite_num// ...buff[i] = ...
}

之前的文章 FSE’03 ARCHER - 路径敏感的内存越界检查中，我们提到：作者针对这样的代码，直接将i的值设置一个范围 [0, ite_num)。

3.2 路径敏感分析 (Path-Sensitive)

之前的文章 ICSE’08 - 路径敏感bug-finding工具Calysto 中，我们提到：SSA虽然能够直接得到Def-Use，但是他们之间值的传播是无条件的。通过Gated Single Assignment[2]，可以在值的传播边上标记一个路径条件，在传播时可以路径敏感地编码逻辑上的Path Condition，以实现路径敏感。

4. Demand-Driven算法

Demand-Driven值得是只针对缓冲区访问变量相关的依赖进行符号值传播。该算法的迭代实现，作者利用递归实现。

算法1: demand-driven调用的入口，同时也是迭代递归的一个子过程：首先传播Def-Range，然后利用控制依赖信息Refine该Range。

算法2:

Def-Range首先计算incoming operands的符号值，然后按照数据依赖的代数运算法则进行符号值的运算/传播。

UpdateDefRange类似常见的worklist算法：def改变之后沿着def-use传播给它的use，如果use改变之后，再沿着use->def对后续的def进行更新，如此不断迭代。

(def1 -> use -> def2 -> ...)

算法3:

下面就是对计算的Def-Range，利用控制依赖信息进行精化。

5. 实验结果

算法集成到静态分析工具Parfait中，它构建在LLVM之上。
Intel E8600 3.33GHz, 8GBRAM

测试集：

精度比较高，平均误报率10.4%

10分钟能分析800w行的代码，够scalable。

与其它工具对比：

6. 不足

作者的方法只能处理显式数组类型，不能处理指针。
不能处理内存依赖，也就是只能处理top-level变量，没考虑address-token变量/间接内存读写。这需要精确的指针分析。。

下面是作者统计的，当前分析不能定位的，潜在的缓冲区溢出百分比。

7. 总结

跟之前看的 ICSE’22 数值除零bug检测在技术上相似之处，可以再对比对比。
很喜欢看这篇文章，各种技术都点到了（～
尝试扩展，添加函数间分析，内存依赖

8. 参考文献

[1] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min´e, D. Monniaux, and X. Rival. The ASTREE analyser. In ´Proceedings of the 2005 European Symposium on Programming, pages 21–30. Springer, April 2005.

[2] [21] K. J. Ottenstein, R. A. Ballance, and A. B. MacCabe. The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages. In Proceedings of the 1990 conference on Programming Language Design and Implementation, pages 257–271. ACM Press, 1990.