[论文笔记] Lifting On-Demand Analysis to Higher-Order Languages

Introduction

很多静态分析工具在进行按需静态分析之前都假设存在一个调用图。但是这种假设不够好，对于 JavaScript 这种具有多种动态特性的语言，调用图分析和数据流分析之间的相互依赖关系要更强。如果忽略这种相互依赖关系，调用图分析不得不牺牲一部分精确或效率，甚至使得按需分析带来的性能优势不再成立。这篇文章提出了一种基于数据流分析的按需调用图分析方法，通过交替执行向前和向后数据流分析来逐步扩充调用图。

Overview

一个 JavaScript 程序及其污点分析案例：

这个 JavaScript 程序展示了一个数据泄露：敏感数据从 readUserData() 流动到敏感操作 log()。下面会展示如何使用向前和向后数据流分析从敏感操作 log() 开始逐步构建调用图。

向前数据流分析/前向查询 (langle l, f, rightarrow rangle)：一个函数 (f) 可能流向哪些表达式

向后数据流分析/后向查询 (langle l, c, leftarrow rangle)：哪些函数可能流向表达式 (c)

前 4 个步骤的分析过程：

1. log 对应一个敏感操作，那么需要检查 arg 是否是一个敏感数据，有查询 (langle 2, text{arg}, leftarrow rangle)

2. arg 来源于函数 writeToLog() 的参数，因此要查询 writeToLog() 可能在哪些位置被调用，提出查询 (langle 1, text{writeToLog}, rightarrow rangle)

3. 根据数据流分析 handler = writeToLog，然后有 process(readUserData, handler)，为了知道 (process) 是什么提出查询 (langle 13, text{process}, leftarrow rangle)，容易查询到 (process) 定义在第 8 行，因此有答案 ({text{process}@8})

4. 根据步骤 3 的查询和答案，回溯到上一个查询 (langle 1, text{writeToLog}, rightarrow rangle) 有答案 ({text{handler}@10})，但是 handler(data) 的 data 仍然未知，目前的数据流分析已知 data = getData() 因此提出了一个新的查询 (langle 9, text{getData}, leftarrow rangle)

5. 以此类推

下表展示了整个分析过程：

在分析过程中构建的调用图如下：

Precision

上面的按需分析过程可以和上下文敏感技术相结合，考虑这样的一个 JavaScript 程序，对于后向查询 (langle 15, text{retrieveFunc(obj1)}, leftarrow rangle) 及其一个子查询 (langle 15, text{retrieveFunc}, leftarrow rangle)，使用上下文敏感可以得到 obj1['func'] 从而得到更精确的调用图：

On-demand call graph soundness

程序直接被建模为一组 call-traces：

当函数调用时，一个 call 会在调用处发生，然后一个 entry 会发生在被调用的函数处，当被调用的函数 return 时会触发 exit，在调用处再触发 return，一个调用及其对应的 events 如下：

一个 trace (tau = e_1e_2...e_n) 是 events 的有限序列，(|tau| in mathbb{N}) 被定义为序列长度；程序被定义为一组可能的 trace 集合 (mathcal{S} in mathcal{P}(Trace))，(mathcal{S}) 上有一些限制用来排除不可能在真实程序中产生的 trace，比如一个函数不可能先 exit 再 entry：

下游的 client analysis 可能使用两种调用图查询：

1. callee query：对于调用点 (c in CallSite) 哪些函数 (f in Function) 会被调用

2. caller query：函数 (f) 会在哪些调用点 (c) 被调用

直观上 callee query 可以看作后向数据流分析，caller query 可以看作前向数据流分析；每一个 query 都隐式定义了程序 sub-trace 的一个集合：

完整的向后 sub-trace 定义：(text{complete-bwd-traces}(c) = { tau mid exists tau_0. tau_0 cdot tau in S land tau = text{ref}(f, r) cdot _ cdot text{call}(c, f, r) })

而向后 sub-trace 定义为：(text{bwd-traces}(c) = { tau_2 mid exists tau_1. tau_1 cdot tau_2 in text{complete-bwd-traces}(c) })；直观上，如果从A到Z的整个路径都与我们的查询相关，那么从路径中任意一点（比如M）到终点Z的部分（M -> Z）也被认为同样是相关的。

引用点 (r) 仅用于限定与给定调用点 (c) 相关的向后 trace。类似地，我们为向前查询 (f) 定义向前 sub-trace 集：

(text{fwd-traces}(f) = { tau mid exists tau_0. tau_0 cdot tau in S land tau = text{ref}(f, _) cdot _ })

调用图 (G subseteq Callsite times Func) 其顶点是调用点和函数，边连接调用点 (c in text{CallSite}) 到函数 (f in text{Func})，用 (CG = Callsite times Func) 表示所有调用图的集合，程序的完整调用图 (whole-cg) 定义为：

(text{whole-cg} = { (c, f) mid exists tau in S, 0 < i leq |tau| . tau_i = text{call}(c, f, _) }.)

定义 (C subseteq text{CallSite}) 和 (F subseteq text{Func}) 分别是客户端分析在分析程序时发出的 callee query 和 caller query 的集合，按需方法的目标是计算一个子图 (G) ，使其包含所有回答查询 (C) 和 (F) 所需的边，按需调用图的 soundness 定义为：

方法以两种数据流分析为参数。向前数据流分析 (F: text{CG} times text{Func} rightarrow P(text{Trace}))，用于检测调用者查询 (f in F) 可能被调用的调用点。向后数据流分析 (B: text{CG} times text{CallSite} rightarrow P(text{Trace}))，用于检测被调用者查询 (c in C) 可能调用的函数。假设两种数据流分析都是按需分析。仅需在给定的部分调用图包含边 ((c, f)) 时，发现调用点 (c) 和函数 (f) 之间的过程间数据流，返回给定调用图查询相关的子轨迹集的上近似。

一个轨迹 (tau) 与调用图 (G) 是向前兼容的，记为 (text{compat} to(G, tau))，如果对于 (tau) 中的任何事件 (text{enter}(c, f)) 或 (text{return}(c, f))，都有 ((c, f) in G)。类似地，一个轨迹与调用图 (G) 是向后兼容的，记为 (text{compat} leftarrow (G, tau))，如果对于 (tau) 中的任何事件 (text{call}(c, f, r)) 或 (text{exit}(c, f))，都有 ((c, f) in G)

形式上，(F) 是向前 sound 的，当且仅当：

[{ tau in text{fwd-traces}(f) mid text{compat} to(G, tau) } subseteq F(G, f) ]

并且如果 (tau cdot text{enter}(c, f) in text{fwd-traces}(f)) 且 (text{compat} to(G, tau))，则有 (tau cdot text{enter}(c, f) in F(G, f))。请注意，这一定义意味着 (F(G, f)) 超近似所有对 (f) 的引用 (text{ref}(f, r))，因为单例轨迹 (text{ref}(f, r)) 与任何调用图都是兼容的。类似地，(B) 是向后 sound 的，当且仅当对任意 (tau in text{bwd-traces}(c)) 使得 (tau = tau' cdot text{call}(c, f, r)) 且 (text{compat} leftarrow (G, tau'))，则 (tau in B(G, c))，并且如果 (text{call}(c, f, r) in text{bwd-traces}(c))，则 (text{call}(c, f, r) in B(G, c))。

如果两种数据流分析满足假设，那么整个按需分析都是 sound 的。

按需调用图构建算法维护一个状态并在这个状态上通过规则迭代，直到达到不动点为止。状态由三元组 ((G, C, F)) 组成，其中 (G) 是当前已知的调用图， (C) 包含与调用点 (c in C) 相关的向后查询的集合， (F) 包含与函数 (f in F) 的调用者相关的向前查询的集合。

其余的规则描述了在向前或向后方向上到达某个调用时，调用目标需要通过怎样的额外查询进行解析：

一旦算法达到一个不动点，调用图便是与已回答查询相关的按需 sound 的。

证明思路如下：

1. 首先定义一个收集语义 (rightarrowtail)，这个语义按 (leadsto) 添加调用边和查询的顺序添加 subtraces 和新的查询。收集语义维护两个部分映射 (F) 和 (B)，(F: f rightarrow text{fwd-traces}(f))，(B: c leftarrow text{bwd-traces}(c))。每一步转移 ((F, B) rightarrowtail (F', B')) 会向映射中已知的路径 (tau) 的开头或者末尾添加一个新的 event。(rightarrowtail) 收集程序运行中所有真实的路径片段。它不可计算。

2. 通过数学归纳法证明 (leadsto) 过近似 (rightarrowtail)。

3. 通过反证法证明 (rightarrowtail) 是 sound 的。

4. 结合 2 和 3 完成 soundness 证明。

Implementation

算法的实现基于 TAJS 和 SPDS。主函数位于 sas.artifact.experiments.Main void main()，调用 void runExperiment() 启动分析。getTaintQueries() 为程序中每个可能的 sink 位置（函数调用）创建两种查询：为调用的每个参数创建查询，如果函数是某个对象的方法那么为这个对象创建查询。查询的类型是 Node<NodeState, Value>，可以理解为 location 及被查询的对象。然后通过调用 getOrStartBackwardQuery() 对于每个 query 都启动一个后向查询。*MerlinSolver 是前向分析和后向分析的主运行逻辑，*FlowFunctions 是对应的 FWD 和 BWD 规则的建模。