[论文笔记] Machine-Learning-Guided Selectively Unsound Static Analysis

Introduction

现有的静态分析工具都是 unsound 的，并且体现为 uniformly unsound。这里的“uniformly”指静态分析工具会用一种统一地忽略所有不能处理的特性，而不考虑代码上下文。这种策略会减少误报率 \(\frac{false \ alarm}{all \ alarm}\)，但是会提高漏报率 \(\frac{true \ bug}{all \ bug}\)。另一种方法是把分析改进为 uniformly sound，但是这会降低漏报率，提高误报率。

一个结论是：产生误报的程序片段（循环和库调用）是相似的、可预测的，并且具有一些共同特性。与此同时，真实的漏洞通常是由不同的原因引起的，这些原因在某种程度上是非典型和不可预测的。提出一种方法：通过传统机器学习的手段捕捉无害但降低精度的程序片段的共同特征，在 uniformly sound analysis 中识别可能引入 false alarm 的程序片段，然后选择性的应用 unsound analysis。

实验结果证明 selectively unsound analysis 在大幅减少漏报数量的同时维持了原有的精度。

Overview

考虑区间分析 interval analysis 的一个例子，这段代码包含两次缓冲区访问，第一次是安全的，而第二次是不安全的：

Uniformly unsound analysis 会放弃对循环的分析，转而将每个循环 unroll 成下面的形式，这会使得分析认为 \(i\) 的区间始终是 \([0, 0]\)，从而没有发现第二次的不安全缓冲区访问：

Uniformly sound analysis 会注意到循环，但由于无法处理 \(i \neq 11\) 的特征，认为 \(i\) 的区间始终是 \([0, +∞]\)，从而在第一次缓冲区访问的位置产生了 false alarm。如果在第一次的缓冲区访问使用 unsound analysis，在第二次的缓冲区访问使用 sound analysis 就可以解决误报率和漏报率的问题：

没了解过区间分析，他也没给定义，感觉这个例子找的不够好，看上去是可以通过一些手段实现更 soundy 的区间分析的

学习阶段分为三个步骤：

• 收集具备无害特征的代码段

• 用一组预先定义的特征集合为每个无害代码段构建一个特征向量

• 使用无监督的机器学习方法训练一个能够区分无害代码的分类器

Technique

Parameterized static analysis

A variant of well-known setting for parameterized static analysis。程序 \(P \in Pgm\)，程序 \(P\) 的片段 \(J_P\)（可能是循环的集合，库调用的集合等等）和程序点 \(C_P\)，分析器被定义为：\(Pgm \times \delta(J) \rightarrow \delta(C)\)，由 soundness parameter \(\pi \in \delta(J)\) 参数化。\(\pi \in \delta(J)\) 是一组需要被 soundly 分析的程序片段。例如，所有的循环 \(J = \{J_1, J_2, ...\}\)，\(J_1 \in \pi\) 意味着 \(J_1\) 需要被 soundly 分析。

Learning a classifier

手动构建的一组 features：\(f_i: J \rightarrow \{0, 1\}\)，\(f = \{f_1, f_2, ..., f_n\}\)

分类器 \(C\) 应当接受某个程序片段及其特征向量作为输入，输出这个程序片段是否 harmless：\(C: \{0, 1\}^n \rightarrow \{0, 1\}\)

模型 \(M\) 根据给出的程序 \(P\) 得到参数 \(\pi\)：\(M: Pgm \rightarrow \delta(J)\)

使用 One-Class Support Vector Machine（OC-SVM）学习这个模型。首先逐个对代码库中的每个程序片段应用不可靠分析，运行分析并从给定代码库中收集所有无害组件的特征向量。如果在不可靠分析中真实警报的数量保持不变且虚假警报的数量减少，则认为一个程序片段是无害的。

Instance analysis

给出了一个通用的分析框架，这个框架对于循环和标准库调用是 selectively sound 的，选择了两个分析及其对应的两种程序片段作为实例。

A Generic, Selectively Unsound Static Analysis

抽象文法如下：

抽象语义如下，函数 \(s\) 是一个从抽象位置到抽象值的映射，可以看作程序状态的一种表示，\(s[L \rightarrow V]\) 可以看作 \(s\) 中 \(L\) 对应的应设置被更新为 \(V\)；为了简化形式语义，定义两个函数 \(L\) 和 \(S\) 来区分左值右值的语义：

注意到 while 和 lib() 是受参数 \(\pi\) 调控的

下面的两个形式语义没啥大意思，可能是写给审稿人看的

对于区间分析，有：

对于污点分析，有：

Experiments

要解决如下的问题：

• Selectively unsound analysis 的表现怎么样？

• OC-SVM 的表现怎么样？

• 如何手动设计一组合适的 features？

• Selectively unsound analysis 的效率怎么样？

Setting

Baseline：在一个完整C语言的静态分析器上实现了上述方法，对于每个分析，建立了一个 sound 的版本（BASELINE）、一个 uniformly unsound 的版本（UNIFORM）和一个 selectively unsound 的版本（SELECTIVE）。

Benchmark：36个已知存在缺陷的程序，来自开源软件或之前关于静态分析的工作，包含138个真实的缓冲区溢出漏洞和106个真实的 formatted string 漏洞

Effectiveness of approach

Time cost

BASELINE分析所有列出的程序花费了42.1秒，而UNIFORM仅花费了27.7秒，减少了14.4秒（34.2%）。SELECTIVE花费了33.8秒，减少了8.3秒（19.7%）。