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

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

isMHP.令 p 1 和 p 2 是来自一个给定 source-sink 路径 p 的两条路径,令 NL 1 和 NL 2 为从 p 1 和 p 2 中提取出来
的节点标签.路径 p 1 和 p 2 是 MHP 的,当:
;
(1) NL 1 []l  NL 2 []l 
]
(2) NL 1 [wn  NL 2 [wn  ;
]
(3)  L  1c NL 1 [],c 2  {L 2c : L  2c NL 2 [] wherec
L 2c [ID  ] L 1c [ID ] and L 2c []T  L 1c []},T  L  2c  2 ,L  NL 1 [ ]j  NL 2 [ ].j
2c
在本文所定义的线程模型下,这 3 个条件是 p 1 和 p 2 为 MHP 的充分条件,因为:(1) 它们没有被同一个锁所
保护;(2) 它们没有通过 wait 或 notify 进行同步;(3) 根据它们的调用轨迹存在一个没有被 join 的线程.最后,通
过 isFeasible 检测路径是否可行,它会提取出路径约束并调用一个常规的约束求解器来验证路径的可行性(第 10
行).对于一个数据竞争对,GUARD 验证两个路径约束.第 1 个约束来自被识别为 MHP 的线程标签,第 2 个是相
应 source 和 sink 的路径.如果它们的两种路径约束都是可满足的,则 GUARD 报告这一漏洞(第 11 行).
算法 3. CheckSourceSinkPair.
Input: source,sink,paths;
Output: isFeasible.
(1) if source {write read and sink  {write read then
}
,
}
,
(2) if source {read and sink  {read then
}
}
(3) continue;
(4) //Analyze every path in paths
(5) for p in paths do
(6) if isPathOrderReversed(p) or not isReachable(p) then
(7) continue;
(8) if not isMHP(source,sink,p) then
(9) continue;
(10) if not isFeasible(p) then
(11) return true;
(12) return false;

4 工具实现
GUARD 是基于 LLVM3.6.2 [25] 使用 Z3 [26] 作为 SMT 求解器来实现的.GUARD 中所有的模块都由 LLVM
pass 实现,LLVM pass 用于在编译器中执行程序分析、转换和优化 [27] .目前,GUARD 支持 C 语言中的 POSIX
thread [28] 以及 C++中的 std::thread [29] .
4.1 方法优化
为了提高效率,GUARD 采取了多种优化方式.第 1 种是 Thread escape 分析,它排除了那些不会与其他变量
同时被访问的变量.第 2 种优化是将全局变量内联为函数参数来简化分析过程.第 3 种优化是为数据竞争检测
优化 source-sink 的模式.
线程逃逸(thread escape)分析.众所周知,一个程序可能包含数目繁多的变量,更不用说与之相应的变量访
问.尽管 GUARD 只会分析过程间的变量(即实际参数和全局变量),但是变量的总数仍十分庞大.线程逃逸分析
能够避免分析那些无法与其他变量同时被访问的变量,即 GUARD 不会分析不带线程标签的变量.因为这样的
变量不可能与其他变量一起被并行访问.这个过程是保守且高效的,它能够尽快给出线程逃逸信息,同时也不会
产生漏报.例如,在第 1 次线程调用前使用的变量不会与任何线程中的变量并发执行.
内联全局变量.过程内的变量包含两种类型:函数实参以及全局变量.据我们所知,这两种变量是过程内分
析的两大挑战.对于能够获取函数体的所有函数,GUARD 将全局变量当作函数实参.换言之,GUARD 通过将全