当前位置：首页 > news >正文

Fusion: 无需路径条件的路径敏感分析

news 2025/7/13 11:56:08

Fusion

1.Introduction
- 1.1.问题
- 1.2.基础方案
- 1.3.优化
- 1.4.完整算法
- 1.5.实现
2.实验
参考文献

文章理解可能有不对，欢迎大家批评指正

1.Introduction

Fusion $^{[3]}$ 是基于Pinpoint $^{[1]}$ 和Falcon $^{[2]}$ 实现的。个人理解Fusion对pinpoint的改进是在query SEG (pinpoint中定义的symbolic expression graph)时求解路径条件，SEG构造的步骤应该跟pinpoint/Falcon一样。主要的改进是计算路径条件时不缓存，每次需要重新遍历SEG计算路径条件，这样反而更快，内存占用更低。

1.1.问题

在路径敏感分析中，为了实现上下文敏感性（context-sensitivity），需要将被调用函数（callee）的条件复制（克隆）到调用点。这种克隆会导致条件数量指数级增长，严重影响静态分析和SMT求解的性能。

这里Fusion假定分析的程序形式如下，这里忽略了 store/load 等内存操作，这是因为作者在指针分析方面和之前工作一致，重点讨论路径条件分析。 $v1=ite(v2,v3,v4)v_1 = \text{ite}(v_2, v_3, v_4)$ 类似于C中的三目表达式 $v_1 = v_2 ? \; v_3 : v_4$ 以及LLVM IR中的 select 指令 $v1=selectv2,v3,v4v_1 = \text{select} \; v_2, v_3, v_4$ 。这里 $if(v1=v2)\text{if}(v_1 = v_2)$ 感觉表述有点多余，编译成LLVM IR后应该类似 $v_1 = v_2$ , $if(v1)\text{if}(v_1)$ ，同时 $returnv1=v2\text{return} \; v_1= v_2$ 应该相当于 $v_1 = v_2$ , $returnv1\text{return} \; v_1$ （后面按照这个表达）。二元运算 $⊕\oplus$ 包括基本逻辑运算以及+、-运算。

请添加图片描述

1.2.基础方案

问题：构造完程序依赖图后，给定一个path $Π=(v1→v2,...,vn−1→vn)\Pi = (v_1 \rightarrow v_2, ..., v_{n - 1} \rightarrow v_n)$ ，如何更好的进行路径条件分析。解决方案：作者定义了下面规则进行分析。

1.首先在程序依赖图上进行切片，表示为 $G[Π]={V[Π],Ec[Π],Ed[Π]}G[\Pi] = \{V[\Pi], E_c[\Pi], E_d[\Pi]\}$ ，分别表示切片的结点、控制依赖边、数据依赖边集合。切片对规则如下，其中:
- Rule (1) 表示假如存在语句 $v1=ite(v2,v3,v4)v_1 = \text{ite}(v_2, v_3, v_4)$ ) 并且 $v3→v1v_3 \rightarrow v_1$ 在 $Π\Pi$ 中，那么将 $v4→v1v_4 \rightarrow v_1$ 添加到 $X_d$ 中， $X_d$ 表示应该被排除出当前Slice的边集合。
- Rule (2) 表示控制依赖的切片规则，也就是从 $Π\Pi$ 中的结点 $v$ 开始，前向遍历控制依赖图，将所有遇到的结点和控制依赖边分别添加进 $V[Π]V[\Pi]$ 和 $Ec[Π]E_c[\Pi]$ 中。这里需要注意的是 $π∈Π,v∈π\pi \in \Pi, v \in \pi$ ，也就是结点 $v$ 一定是被切片的路径，新添加进 $V[Π]V[\Pi]$ 的结点不会被控制依赖切片。
- Rule (3) 为数据依赖的切片规则，对于结点 $v$ ，沿着数据依赖边后向遍历，将所有遇到的结点和数据依赖边分别添加进 $V[Π]V[\Pi]$ 和 $Ed[Π]E_d[\Pi]$ 。这里需要注意的是 $\in V[\Pi]$ ，也就是 $v$ 不是原始路径 $Π\Pi$ 上的结点。

请添加图片描述

2.针对切片中的每条边生成对应的路径条件。
- 控制依赖边 $if(v1)→s\text{if}(v_1) \rightarrow s$ 的路径条件为 $v1≡truev_1 \equiv \text{true}$ 。文中没有直接提 else 分支，感觉是 $¬v1≡true\neg v_1 \equiv \text{true}$ 。
- 数据依赖边的路径条件生成规则如下。其实有点没明白 $v1≡ite(v2,v3,v4)v_1 \equiv \text{ite}(v_2, v_3, v_4)$ 实际运行起来要怎么算，感觉应该是 $v1≡v3∨v1≡v4v_1 \equiv v_3 \vee v_1 \equiv v_4$ 。

语句	前置条件	路径条件
$v_1 = v_2$	无	$v1≡v2v_1 \equiv v_2$
$v1=v2⊕v3v_1 = v_2 \oplus v_3$	无	$v1≡v2⊕v3v_1 \equiv v_2 \oplus v_3$
$v1=ite(v2,v3,v4)v_1 = \text{ite}(v_2, v_3, v_4)$	$v3→v1∈Ed[Π]∧v4→v1∉Ed[Π]v_3 \rightarrow v_1 \in E_d[\Pi] \wedge v_4 \rightarrow v_1 \notin E_d[\Pi]$	$v2≡true∧v1≡v3v_2 \equiv \text{true} \wedge v_1 \equiv v_3$
$v1=ite(v2,v3,v4)v_1 = \text{ite}(v_2, v_3, v_4)$	$v4→v1∈Ed[Π]∧v3→v1∉Ed[Π]v_4 \rightarrow v_1 \in E_d[\Pi] \wedge v_3 \rightarrow v_1 \notin E_d[\Pi]$	$v2≡false∧v1≡v4v_2 \equiv \text{false} \wedge v_1 \equiv v_4$
$v1=ite(v2,v3,v4)v_1 = \text{ite}(v_2, v_3, v_4)$	其它情况	$v1≡ite(v2,v3,v4)v_1 \equiv \text{ite}(v_2, v_3, v_4)$
其它语句	无	$true\text{true}$

3.用 $∧\wedge$ 运算合并每条边的路径条件。

示例：给定下面程序

foo(_a, _p) = {a = _a; p = _p;b = a > 20;c = b;if (c) {q = p;d = a * 2;e = d > 90;f = e;if (f) r = q;}…
}

给定路径 $Π=(p=_p→q=p→r=q)\Pi = (p = \_p \rightarrow q = p \rightarrow r = q)$ 。其程序依赖图（语句级）的切片如下，标注 c 的边为控制依赖边，其它为数据依赖边。

$Ec[Π]={q=p→c,r=q→f,f→c}E_c[\Pi] = \{q= p \rightarrow c, r = q \rightarrow f, f \rightarrow c\}$ 。 $Ed[Π]E_d[\Pi]$ 则把下面部分的数据依赖边全包括了。计算路径条件时：

几个控制依赖边的约束为 $\equiv \text{true} \wedge c \equiv \text{true}$ 。
数据依赖边计算出的约束为 $\equiv b \; \wedge b \equiv a > 20 \; \wedge f \equiv e \; \wedge e \equiv d > 90 \; \wedge d \equiv a * 2$ 。
最终路径是把这两个条件用 $∧\wedge$ 进行合并。

1.3.优化

线性SMT求解：计算路径约束的公式如下图所示。首先通过一系列等可满足性公式转换对输入公式进行简化和标准化（如线性时间/空间的预处理步骤）。预处理阶段能显著提升性能，21%的案例在此阶段即可判定可满足性。预处理后，公式会根据所选理论（如位向量理论）发送至特定求解器。例如，位向量理论会将条件转换为纯布尔公式，并通过SAT求解器判定可满足性。

请添加图片描述

减少不必要的clone: 在路径敏感分析中，传统方法需要克隆被调用函数（callee）的条件以实现上下文敏感分析，但这会导致条件数量爆炸。新方法（Algorithm 6）通过过程间优化（如常量传播、无约束值传播等）提前消除不必要的函数调用，从而减少克隆需求。

Unconstrained-value propagation （无约束值传播）：下面示例中，通过该优化，可以直接求解路径条件，无需克隆 bar 函数。
Inter-procedural constant propagation（过程间常量传播）

int bar(int x) {int y = x * 2;int z = y;return z;
}int* foo (int a, int b ) {int* p = nullptr;…int c = bar(a);int d = bar(b);…if (bool e = c < d) return p;…
}

请添加图片描述

模块化加速预处理

1.在函数的入口（entry）和出口（exit）之间建立快速路径：上面这张图中 y = x * 2 到 return z 之间添加了一个快速路径，避免重复处理。
2.分解高开销预处理步骤（如高斯消元）：全局预处理（如高斯消元）的复杂度取决于所有函数及其克隆体的条件总大小，即 $O(sizeof(⋀f∈FΦΠ,f))O(\text{sizeof}(\bigwedge\limits_{f \in F} \Phi_{\Pi, f}))$ 。 $F$ 是所有函数和所有clone版本的集合。将高开销预处理按函数分解（intra-procedural），避免对同一条件的多个克隆体重复计算。优化后复杂度为 $O(∑f∈F′sizeof(ΦΠ,f))+O(sizeof(⋁f∈F−F′ΦΠ,f))O(\sum\limits_{f \in F^{' }} \text{sizeof}(\Phi_{\Pi, f})) +O(\text{sizeof}(\bigvee\limits_{f \in F - F^{' }} \Phi_{\Pi, f}))$ ， $F^{'}$ 为无需clone的函数集合。

1.4.完整算法

完整的跨函数分析算法如下图所示，给定路径 $Π\Pi$ ，1-5行按照之前步骤计算函数内路径条件 $ΦΠ,f\Phi_{\Pi, f}$ 。

请添加图片描述

1.5.实现

Fusion的主要目标是找bug而不是验证程序的正确性。因此做了一些unsound假设：

1.struct/class 的每一个field被视为不同的object。
2.array/union 的每一个成员都被视为和其它成员存在别名。
3.不处理全局变量。
4.对于循环直接展开2次处理。对于递归调用也是展开2次处理。

作者基于Fusion实现了Checker：path traversal (CWE-23) 以及transmission of private resources (CWE-402).

2.实验

benchmark信息如下，包括代码行数、函数数量、PDG结点数、边数。

请添加图片描述

作者对比Fusion和Pinpoint的检测效果。由于检测的原理一致，主要是对开销进行优化，因此主要对比性能开销。

请添加图片描述
bug检测方面的开销

请添加图片描述
可以看到Fusion优于Pinpoint。

参考文献

[1].Shi Q, Xiao X, Wu R, et al. Pinpoint: Fast and precise sparse value flow analysis for million lines of code[C]//Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2018: 693-706.

[2].Yao P, Zhou J, Xiao X, et al. Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis[J]. Proceedings of the ACM on Programming Languages, 2024, 8(PLDI): 567-592.

[3].Qingkai Shi, Peisen Yao, Rongxin Wu, and Charles Zhang. 2021. Path-sensitive sparse analysis without path conditions. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Association for Computing Machinery, New York, NY, USA, 930–943

查看全文

http://www.dtcms.com/a/276488.html