Page 107 - 《软件学报》2021年第7期

石剑君 等:操作系统内核并发错误检测研究进展 2025

3.2 静态检测方法
目前常用的静态并发错误检测方法包括基于流分析的检测、基于符号执行的检测和针对操作系统内核的
特点而设计的检测方法等.主要通过构建并发错误触发的模式规范,并分析程序的控制流图或数据流图,以检查
和分析程序是否满足给定的并发错误模型 [34,5961] .
1) 基于数据流分析的检测
数据流分析最早由 Gary 和 Naval [62] 提出,通过构建程序的控制流图(control flow graph,简称 CFG),对 CFG
图中的每条语句或者每个基本块进行计算和分析,求解相关的数据流方程,并进行反复迭代计算,在出口点求得
最终结果.数据流分析最常见的应用包括可达定义分析和污点数据分析等.基于流分析的检测方法,通常采用编
译技术获取源代码的 CFG 或者抽象语法树(abstract syntax tree,简称 AST)等,再利用数据流分析、上下文分析
等技术,结合相应的并发错误检测算法进行检测.
RacerX [63] 采用流敏感的过程间分析检测 Linux 内核和 FreeBSD 中的死锁和数据竞争错误.该方法首先针
对程序中特有的锁操作(加锁、解锁以及是否允许或者禁止中断等)进行标注,然后提取程序的 CFG,并在 CFG
上运行死锁检测器和数据竞争检测器以检测出程序中存在的并发错误.RacerX 成功运行在 Linux kernel 2.5.62
版本(1.8MLOC)和一个代码行数将近 500K 的商业操作系统 System X 上,并最终检测出了 16 个并发错误.为了
能够进行大规模代码的分析,RacerX 没有采用指向分析等精确的分析技术,只进行了简单的数据流分析,并根据
经验对分析结果进行排序,因此找到的并发错误数目较少.Bai 等人 [64] 采用混合的流分析方法检测并发错误中
的 SAC 错误.SAC 错误通常出现在操作系统内核级别,在原子性上下文(如自旋锁加锁或者执行中断处理程序)
中出现了睡眠操作而导致.他们称 SAC 错误在之前的研究中没有得到足够的重视,主要是由于这类错误在实际
的执行过程中很少发生,因此比较难以发现.事实上,由于 SAC 会引起 CPU 的阻塞,甚至导致系统挂起.因此,在原
子性上下文中的睡眠操作是禁止的.然而,在操作系统内核中,SAC 错误仍然存在,尤其是在设备驱动程序和文
件系统模块.其原因主要有以下几点:(1) 一个操作是否可以睡眠往往需要特定的系统知识或经验;(2) 测试操
作系统内核模块是比较困难的;(3) SAC 错误在每次实际执行过程中并不总是出现问题,而且它们通常比较难
以复现.因此,Bai 等人提出 DSAC 方法,一个用于检测操作系统内核中的 SAC 错误的静态检测方法.该方法首先
采用过程间流敏感和流不敏感两者相结合的混合型流分析方法收集那些在原子性上下文中可能被调用的函
数;然后通过启发式的方法,结合程序的控制流图和内核代码注释,提取到在程序运行时可能睡眠的函数接口;
再利用混合数据流分析的方法检测可能存在的 SAC 错误,最后通过路径检查的方法过滤掉重复报告和误报的
SAC 错误.除此之外,他们还设计了一个基于模式匹配的自动化生成 SAC 错误修复补丁的工具.最终,该方法检
测到了 401 个 SAC 错误,其中 272 个被开发人员确认.只有 26 误报,误报率为 6.3%.生成了 61 个补丁,其中 43
个被用在了内核代码中.DSAC 方法可以有效地检测出 Linux 内核中的 SAC 错误,但仍有一些不足,如 DSAC 方
法没有解决函数指针的问题.因此,与函数指针相关的很多 SAC 错误无法被检测到.另外,路径检查的方法并不
能过滤掉所有的误报,还需要更有效的误报处理方法.
2) 基于符号执行的检测
符号执行最早由 King 等人 [65] 提出,用于提高程序分析中的代码覆盖率,从而挖掘更多的错误.基于符号执
行的静态分析方法,通过符号输入、路径探测和约束求解等方法尽可能地扩大代码的检测范围.RELAY [33] 设计
出用符号执行和数据流分析相结合的方法检测大规模复杂代码(如 Linux 内核包含 450 万行代码)中的数据竞
争问题.该方法采用一种相对锁集的分析方式,即一个锁集只描述相对于函数入口点开始的锁变化.相比于传统
的锁集算法,该方法支持模块化的分析,使得函数的分析相对独立.而且,该方法方便实现并行化分析,从而大大
提高了分析的效率.例如,分析 Linux 内核代码的时间从没有并行化的 72 小时降低到 5 个小时.该方法首先利用
符号执行的方法提取出函数中与调用上下文无关的函数行为的摘要信息,将函数内部本地变量的信息映射到
全局形式化符号上,然后执行一个自底向上的基于数据流分析的相对锁集分析,最后基于从每个程序入口点生
成的相对锁集信息,分析所有访存操作受保护的情况,生成数据竞争的检测报告.为了降低误报率,文献[33]还采
用了简单的语法过滤机制.例如,过滤掉那些不可能并发的函数报告.最终,该方法报告了 149 个数据竞争的警