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

2024 Journal of Software 软件学报 Vol.32, No.7, July 2021

有潜在的并发错误的检测技术.静态检测方法可以覆盖到尽可能多的并发错误,但是由于不能获取代码的动态
运行时信息,可能造成较高的误报率.动态检测是指在程序运行的过程中进行并发错误检测的方法.一般情况
下,动态检测方法只能检测出程序运行过程中暴露出来的并发错误,而无法检测未执行的代码路径中可能存在
的并发错误.因此,动态检测方法的漏报率较高.为了提高并发错误检测的效率,很多研究人员提出了静态与动
态相结合的并发错误检测方法.首先用静态检测方法定位到尽可能多的并发错误,再用动态检测方法进一步提
升检测结果的准确性.
3.1 形式化验证方法
形式化验证作为形式化方法的一个重要应用,最近几年在软件程序的安全性验证方面取得了很大进展.基
于形式化验证的操作系统内核并发错误的研究主要包含两个方面:基于定理证明的操作系统验证和基于模型
检验的并发错误检测 [46] .
1) 基于定理证明的操作系统验证
基于定理证明的形式化验证方法通常利用从系统生成的一组规则并进行推理证明,以验证系统是否满足
指定的规则.例如,Owicki 和 Gries 提出的并发程序验证方法 [47] ,对单个线程的执行进行单独验证,以保证每个线
程的执行过程不受其他线程的影响,并要求所有共享数据的访问都必须在互斥锁的保护下进行,以确保并发访
问的正确性.
研究人员还提出一些用于操作系统内核验证的方法.如 Yang 等人 [48] 利用基于 Hoare 逻辑的自动定理证明
器,并将 C#编写的内核代码编译成中间语言 Boogie [49] 进行验证.华盛顿大学的 Nelson 等人 [50] 设计的
Hyperkernel 是针对 Unix 内核的验证方法,该方法的实现基于 LLVM 中间代码,并利用 Z3 求解器进行验证,最终
证明 Hyperkernel 可以实现一键完成验证,并能避免 bug.Yggdrasil [51] 是一个自动验证文件系统的工具.该工具的
设计基于一个称为“崩溃改进(crash refinement)”的新的文件系统正确性的定义,通过在文件系统实现过程中的
一些硬盘状态(包括崩溃状态)来进行规则定义,从而使得开发人员实现一个可用于自动验证的文件系统.除此
之外,还有一些操作系统内核验证的工作,包括 Xu 等人 [52] 对抢占式内核C/OS-II 验证、Klein 等人对微内核 seL4
的验证 [53] 以及 Gu 等人对并发操作系统内核的验证 CertiKOS [42] 等.
2) 基于模型检验的检测
模型检验是一种对有限状态的并发软件系统进行自动化验证的技术.该方法最早由 Clarke 和 Emerson 以及
Queille 和 Sifakis 于 20 世纪 80 年代分别开发出来 [54] .模型检验技术通过代码的简化描述方法,对所有可能的输
入进行测试,以实现对程序的状态空间进行有效测试 [55] .基于模型检验的分析方法通常具有较高的准确率,但分
析的开销也比较大.
MOKERT [56] 是一个基于模型检验的内核测试框架.该框架可以在真实的内核代码中重复执行反例以帮助
开发人员进行内核调试、错误检测以及补丁验证.相比于传统的手动构建测试模型的方法,MOKERT 框架设计
了半自动化的模型构建方法,采用 Modex [57] 从 C 代码中提取形式化模型,并将原始 C 代码与相应的 Promela 模
型 [58] 进行映射,从而便于根据生成的反例对目标代码进行插桩.MOKERT 允许用户重复对一个反例进行回放,
从而方便用户识别出并发错误发生的原因.该框架还支持模型的不断优化,如果在内核代码测试过程中发现一
个反例是一个假反例,则可对模型进行不断的优化以保证模型的有效性.此外,该框架还可以帮助用户验证生成
的补丁是否可以真正地消除内核中的错误.MOKERT 对 Linux 内核 2.6 中出现的两个并发错误进行了回放测试,
以验证该框架的有效性,并检测出了 Linux 内核中的一个数据竞争错误.但模型检验方法的有效性取决于构建
的测试模型,由于内核的线程交叉复杂,配置项繁多,很难构建一个精确的模型触发内核中的并发错误,例如
MOKERT 无法处理中断相关的并发错误,因此,该检测方法的漏报率较高.
基于形式化验证方法的并发错误检测目前也成为一个研究热点.如何对内核的特性进行抽取,构建更有利
于操作系统内核并发验证的规则和模型是利用形式化验证实现操作系统内核并发错误检测所面临的重要
挑战.