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

高凤娟 等:高精度的大规模程序数据竞争检测方法 2041

后,对于可能并发的数据访问子路径,采用一种更精确且更重量级的方法求解路径的可行性,以此来实现路径
敏感.
MHP 分析对于 GUARD 的总体性能是至关重要的,这需要以很高的精度识别非并发的访问对.然而,前沿的
MHP 分析技术 [8,1923] 面临着精度问题.例如,大多数工作 [1923] 聚焦于简单的线程模型(即缺少丰富的并行化模
型),且都未考虑路径约束.为了克服这种局限性,GUARD 引入了一种称作线程流图(TFG)的线程信息表示形式,
用于高效且精确地编码并发信息.TFG 中的每个节点按线程标签总结了其过程内的 MHP 信息.为了最小化计算
开销,线程标签将每个线程操作(例如 thread_create)编码为一个三元组.根据实验结果,这一步会筛除大约 99.5%
的数据访问对.为了保证精度以及可扩展性,MHP 分析和数据访问分析都采用了一种自定义的约束求解器来筛
除“简单但矛盾”的路径,以此进一步减少不会导致数据竞争的路径.最后,GUARD 对于剩余的候选项调用一个
完整的 SMT 求解器(例如 Z3).基于该分段分析方法,GUARD 能够精确地为程序行为建模,同时也保证了效率.
为了对 GUARD 的有效性以及效率进行评估,我们选取 12 个现实世界中的开源项目.评估工作显示
GUARD 能够在 1 870s 内完成对 130 万行代码的工业规模项目的检测,平均误报率为 16.0%.并且,GUARD 比现
有的前沿技术平均快 6.08 倍,与此同时取得了更低的误报率及更高的召回率.
本文的贡献总结如下:
 提出了 GUARD,一种检测数据竞争的分段分析方法.GUARD 与其他前沿技术相比具有更高的扩展性及
精度.
 评估了 GUARD 在多线程测试基准以及现实世界 C/C++应用程序上的性能,结果表明,它能够在短时间
内以可观的精度检测数据竞争.
 GUARD 已经发现 12 个真实程序中存在的漏洞,并且其中的 8 个已得到确认.
本文第 2 节通过一个示例程序阐述 GUARD,并介绍 GUARD 的分析基础.第 3 节详细描述 GUARD.第 4 节、
第 5 节为实现和实验,评估 GUARD 的效率和有效性.第 6 节介绍相关工作.最后第 7 节给出结论.

2 GUARD 概览和分析基础

本节从一个示例程序开始,结合 GUARD 框架介绍 GUARD 各个模块的作用.之后再介绍整个分析过程基
于的线程模型.最后是提出所需的基础结构,即线程流图(TFG).
2.1 启发性案例
图 1 是一个示例程序.图中函数 foo 创建了一个线程执行函数 writer(第 4 行).接着,它将变量 arg 自增(第 7
行),然后等待线程结束(第 8 行).最后,它再一次将 arg 自增.在第 14 行和第 7 行存在数据竞争,因为函数 writer
和 arg++指令能够并行执行.但是第 14 行和第 9 行不存在数据竞争,因为 writer 线程在第 8 行被执行了等待终
止操作.此外,静态分析工具在报告数据竞争漏洞时也应附带路径信息作为佐证,在此例中可能发生数据竞争的
路径是第 4 行~第 14 行、第 6 行~第 7 行.

Fig.1 A motivating example
图 1 示例程序