关键词:
数据竞争
Petri网
网展开
动态程序分析
摘要:
数据竞争是多线程程序的常见漏洞之一,传统的数据竞争分析方法在查全率和准确率方面难以两全,而且所生成检测报告难以定位漏洞的根源.鉴于Petri网在并发系统建模和分析方面具有行为描述精确、分析工具丰富的优点,提出一种基于Petri网展开的新型数据竞争检测方法.首先,对程序的某一运行轨迹进行分析和挖掘,构建程序的一个Petri网模型,它由单一轨迹挖掘得到,却可隐含程序的多个不同运行轨迹,由此可在保证效率的同时降低传统动态分析方法的漏报率;其次,提出基于Petri网展开的潜在数据竞争检测方法,相比静态分析方法在有效性上有较大提升,而且能明确给出数据竞争的产生路径;最后,对上一阶段检测到的潜在数据竞争,给出基于CalFuzzer平台的潜在死锁重演调度方法,可剔除误报,保证数据竞争检测结果的真实性.开发相应的原型系统,结合公开的程序实例验证了所提方法的有效性.