Precise and Scalable Detection of Double-Fetch Bugs in OS Kernels

开源项目地址：https://github.com/sslab-gatech/deadline

本文发表于IEEE S&P 2018，作者是Meng Xu, Chenxiong Qian, Kangjie Lu, Michael Backes, Taesoo Kim。第一作者Meng Xu来自佐治亚理工学院。本文的第四作者Michael Backes为CISPA亥姆霍兹信息安全中心主席兼创会理事。

主要内容

操作系统的系统调用执行期间，操作系统内核可能会多次读取同一块用户空间的内存（multi-read）。如果在两次读取之间，用户空间内存由于条件竞争等原因使数据发生了变化，则可能导致double-fetch bug。前人工作中曾尝试通过静态或动态方法来检测这种bug，然而由于对double-fetch没有准确的定义，这些工作会导致大量的误报和漏报，还需要引入大量的人工分析。

本文首先对double-fetch进行了正式和准确的定义，并设计实现静态分析工具——DEADLINE来自动化检测系统内核中的double-fetch bug。DEADLINE使用静态分析系统性地找到内核中的multi-read行为，并使用符号化检测确认multi-read行为是否是double-fetch bug。DEADLINE发现了在Linux内核中的23个新bug和FreeBSD内核中的1个新bug。之后，作者基于自身经验及与内核开发者的交流，总结了4个patch和预防double-fetch的策略。

形式化定义

作者在定义double-fetch之前，先对其相关概念进行了定义：

Fetch：对于一次fetch操作，使用一个(A,S) 二元组来表示本次操作的属性，其中A表示读取数据的地址，S表述数据的大小

Overlapped-fetch：对于两次不同的Fetch (A₀, S₀) 和 (A₁, S₁)，若满足A₀ <= A₁ < A₀ + S₀ or A₁ <= A₀ < A₁ + S₁的关系，则称两次fetch为overlapped-fetch。其中重叠部分表示为(A₀₁, S₀₁)，并用三元组 (A₀₁, S₀₁, i = [0,1])来分别表示两次fetch中读取的重叠数据部分。

控制依赖：对于一个变量V∈（A₀₁,S₀₁, 0），若V在第二次fetch之前受一组约束条件[Vc]的约束，则认为V与（A₀₁,S₀₁）间存在控制依赖。若要证明在此情况下不存在double-fetch bug，必须证明第二次fetch中的V’∈（A₀₁,S₀₁, 1）满足约束条件[Vc].

数据依赖：对于一个变量V∈（A₀₁,S₀₁, 0），若V在第二次fetch之前被消耗（例如赋值给其他变量，进行了计算相关操作，作为参数传入函数调用），则认为V与（A₀₁,S₀₁）间存在数据依赖。若要证明在此情况下不存在double-fetch bug，必须证明第二次fetch中的V’∈（A₀₁,S₀₁, 1）满足V==V’.

作者认为，double-fetch bug遵循以下四个条件：

1. 至少有两次对用户空间的读取操作，即double-fetch的前提是multi-read。用户空间的读取操作可以通过copy_from_user等传递函数进行识别。

2. 两次读取的内容必须存在重叠部分。即两次fetch存在overlapped-fetch区域。

3. 两次读取的重叠部分必须有一定的关联，可以是数据依赖或控制依赖。

4. 不能被证明两次读取的重叠部分在两次读取中是相同的。即用户空间可以通过条件竞争在两次读取之间修改重叠部分的值。

Figure 1 double-fetch示例

如上图所示，perf_copy_attr_simplified函数内部进行了两次fetch，第一次fetch从uattr中拷贝了4个字节的数据到size中，即F1（A=uattr, S=4）；第二次fetch从uattr中拷贝了size长度的数据到attr中， 即F2（A=uattr，S=size）。这显然是一次multi-read。两次fetch操作都以uattr为起始地址，数据重叠区域为（A=uattr，S=4），因此两次fetch满足overlapped-fetch条件。图中11-14行代码可以看到，第一次fetch所得的变量size受一组条件约束，且变量size与第二次fetch的得到的attr->size重叠，即重叠区域存在控制依赖，需要证明其的约束条件一致。然而attr->size没有受到任何条件的约束，无法证明两次fetch的重叠部分相同，因此认为这是一个double-fetch bug。

工具设计

DEADLINE首先使用静态分析收集内核代码中的multi-read操作，并对每一组有关联的multi-read进行符号化执行检查（符号化执行在LLVM IR层面上进行），确定是否满足double-fetch的上述形式化定义。如果是，则将其加入输出集合。

收集multi-read

首先，扫描内核代码，通过识别代码中的copy_from_user等读取用户空间数据的传递函数找到所有的fetch操作（如Figure 1所示）；其次，对于每个fetch操作所在的函数内部，进行函数内的自底向上分析，以找到一个fetch pair（如Figure 2所示）。如果找到了一个fetch pair，则说明找到了一个multi-reads操作，并将其用一个三元组<F0, F1, Fn>表示。在这个三元组中，F0和F1分别表示两次fetch指令的位置，Fn表示这两条指令所在的函数名称。如果在分析的过程中遇到了带有fetch操作的函数，则会将这个函数代码内联进来进行分析。

Figure 2 查找Fetch操作 Figure 3 收集fetch pair

从multi-read到double-fetch bug

前人的一些论文中的工具大都止步于找到内核中的multi-reads情况，之后采用人工分析来确定double-fetch的bug，需要耗费大量的人力。本文设计的工具在发现multi-reads之后，将继续使用符号执行构建约束进行求解，来进行静态分析，看multi-read是否满足形式化定义中的四个条件，从而求解是否存在double-fetch bug。

Figure 4 符号化执行检查案例

文中给出了一个完整的案例分析，如Figure3所示。首先将函数参数和全局变量转变为符号化表述形式，作为根SR（symbolic representation），之后将其他指令转化为符号化表述。符号化的过程中，遇到与fetch数据相关的条件分支判断，则将其转化为assert断言作为条件约束之一。两次fetch之后，使用前述对double-fetch的形式化定义来插入约束并求解：即先判断两次所fetch的数据是否有重叠，再判断在函数内是否可以证明两次fetch的数据重叠部分是相同的。在这个案例中，由于两次fetch分别被标识为U0和U1，且没有约束证明两者是相同的，故约束求解失败，DEADLINE得出检测结果，即此处存在double-fetch bug。

评估及讨论：

DEADLINE在Linux和freeBSD中分别发现了23个和1个新的double-fetch bud。这些bug中的一些已经与开发者进行沟通并修补，有两个被开发者标注为“won’t fix”。

作者通过与开发者交流bug修复的过程，总结了一些关于预防double-fetch的缓解策略：

• 重写：对于第二次fetch的数据中重叠部分，使用第一次fetch时读取的数据进行覆盖；

• 检测到数据变化就中止：如果检测到两次fetch数据不一致，则中止后续操作；

• 增量读取：第二次fetch时，跳过第一次fetch过的数据，以避免读取重复数据；

• 重构为一次性fetch：如果是控制依赖，则可以一次fetch所有的数据。

局限性

DEADLINE在以下几个方面存在局限性：

1. 代码覆盖率：作者使用LLVM对内核进行编译，对于没有编译成功的文件和没有展开的宏代码，将不会被测试覆盖；

2. 路径构建：
   1）在函数内构建fetch-pair路径时，限制了最大的路径数（4096），如果两次fetch超过了这个路径长度限制，则无法进行分析；
   2）循环展开时仅展开一重循环，对于需要展开多次循环或跨循环的double-fetch bug无法分析；
   3）如果循环中有分支，仅会处理循环中的一条分支路径，这种情况会有路径遗漏。

3. 符号化执行检查：
   1）忽略了内联函数，假设其对符号执行没有影响；
   2）从指针到内存对象的映射可能存在误差；
   3）将约束检查限制在封闭函数内，对于在函数外进行检查的情况就会出现误报。

文丨DR.XX, xcz, Wisher

---