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

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

Table 1 Comparison of concurrency bug detection for OS kernels
表 1 操作系统内核并发错误检测方法对比分析
类别 名称 技术手段 错误类型 内核版本及模块 检测算法 检测结果 检测速度
RacerX [63] 数据流分析 并发错误 Linux kernel Lokset 锁集 18 个死锁,13 个数据竞争, 2~14 分/1.8MLOC
v2.5.62 其中 12 个误报
Linux kernel Linux kernel 3.17.2 中检
v3.17.2 测到 215 个并发 SAC 错
混合数据流 并发 SAC Linux kernel 108 分/7.3MLOC-
[64]
DSAC  误,15 个误报;Linux
分析 错误 v4.11.1 129 分/9.4MLOC
驱动程序、文件 kernel 4.11.1 中发现 340
系统、网络模块 个 SAC 错误,20 个误报
单机:72 小时
符号执行、 Linux kernel 相对 Lockset /4.5MLOC
RELAY [33] 数据竞争 53 个数据竞争
数据流分析 v2.6.15 锁集 并行化后:5 小时
/4.5MLOC
静态 [35] Linux kernel v4.0, 符号对
检测 WHOOP 符号执行 并发错误 驱动程序 Lockset 锁集 发现 45 个并发错误 144.5s/7.2KLOC
aComment [66] 代码注释 并发错误 Linux kernel  12 个并发错误,其中 3 个 整个 Linux kernel
误报 需要 265 分钟
Linux kernel
v2.6.30.4
COBET [68] 模式匹配 并发错误 文件系统、驱动  10 个新的并发错误 48.85s/100KLOC
程序、网络模块
Linux kernel 3.14 中发现
Linux kernel v3.14 559 个错误,33 个误报;
基于内核 并发 UAF 基于摘要的 23 分/11.2KLOC
[25]
DCUAF Linux kernel v4.19 Linux kernel 4.19 中发现
代码特性 错误 驱动程序 Locset 锁集 679 个 UAF 错误,39 个 28 分/16.6KLOC
误报
DataCollider [77] 动态调试 数据竞争 Windows 7 kernel  发现 25 个数据竞争,其中 小于 1.3x 的开销
12 个已被修复
Linux kernel
[78]
DRDDR 动态调试 数据竞争  发现 2 个良性数据竞争 小于 1.1x 的开销
文件系统
在 Wrapfs 中发现 49 个数
据竞争,其中 2 个已被确
数据竞争 Linux kernel 认,45 个是良性数据竞争,
Redflag [72] 动态二进制 原子性 文件系统、 Lockset 锁集 2 个是误报;在 Btrfs 中发 2.65x 的插桩和日
插桩 志记录开销
违例 驱动程序 现 8 个良性数据竞争;在
Noveau 中发现 11 个误报
的数据竞争
Linux kernel 在 Linux kernel 3.3.1 中发
v3.3.1
动态 DILP [74] 动态二进制 数据竞争 Linux v4.16.9 Lockset 锁集 现 13 个数据竞争;在 平均 7.2x 的开销
检测 插桩 Linux kernel 4.16.9 中发
驱动程序 现 25 个数据竞争
LockDoc [89] 动态二进制 并发错误 Linux kernel   291 分/5.7MLOC
插桩
发现 190 个并发错误,
Linux kernel 其中 76 个误报,53 个良性
SKI [81] 系统化调度 并发错误 v2.6.28–v3.13.5  
文件系统 数据竞争,24 个恶性数据
竞争
Landslide [79] 系统化调度 数据竞争 Pebbles kernel  用于课程教学,未发现 
真正内核数据竞争
Linux kernel 发现了 23 个数据竞争, 7 天的模糊测试,96
模糊测试、 v5.4-rc5 Lockset 锁集
KRACE [86] 数据竞争 其中 9 个恶性数据竞争, 小时的数据竞争
动态插桩 文件系统 和 HB 关系
btrfs,ext4,VFS 11 个良性数据竞争 检测
Linux kernel 发现了 30 个恶性数据
动静 Razzer [45] 指向分析、 数据竞争 v4.16-rc3  竞争,其中 16 个被开发 整个 Linux kernel
结合 模糊测试 需要 7 天
-v4.18rc3 人员确认
形式 CertiKOS [42] 定理证明 并发错误 CertiKOS   
化 [56] Linux kernel v2.6
验证 MOKERT 模型检验 并发错误 文件系统  发现了 1 个数据竞争 