Petri网的反向展开及其在程序数据竞争检测的应用

展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定,以此为目标,有望缩减网系统展开的规模.为此,针对安全Petri网的可覆盖性判定问题提出了一种目标导向的反向展开算法,结合启发式技术缩减展开的规模,以此提高目标标识可覆盖性判定的效率.进而,将反向展开算法应用于并发程序的形式化验证,将并发程序的数据竞争检测问题转换为Petri网特定标识的可覆盖性判定问题.实验对比了正向展开与反向展开在Petri网可覆盖性判定问题上的效率,结果表明:当Petri网展开的正向分支较多时,反向展开相比正向展开具有更高的可覆盖性判定效率.最后,对影响反向展开效率的关键因素做了分析与总结.

目标导向的多线程程序UAF漏洞预测方法

Use-after-free(UAF)漏洞是多线程程序的常见并发缺陷.预测性UAF漏洞检测方法因兼顾误报率和漏报率而备受关注.然而,已有的预测性UAF检测方法未结合待检测目标作针对性优化,当程序规模大或行为复杂时会导致检测效率低下.为了解决上述问题,提出一种目标导向的多线程程序UAF漏洞检测方法.首先,由程序运行轨迹挖掘程序的Petri网模型;之后,针对每一个潜在可构成UAF漏洞的内存Free/Use操作对,以触发该漏洞为目标导向,在程序的Petri网模型中添加保持操作间因果约束和数据一致性的行为控制结构;在此基础上,设计了一种基于Petri网反向展开的UAF漏洞检测方法.该方法每次只针对1个潜在的UAF漏洞,有针对性地验证其真实性,从而保证检测的效率.与此同时,为了减少待检测的潜在UAF漏洞数量,提出了一种新型向量时钟进行Free操作与Use操作间的因果关系自动识别,据此对潜在的UAF漏洞进行筛选.结合多个程序实例对所提方法进行了实验评估.实验结果表明,所提方法在检测的效率和准确性方面较主流方法有所提高.