论文部分内容阅读
现代社会,软件已经成为最重要的基础设施之一,在很多行业中发挥着不可或缺的作用。同时,软件的安全性也越来越受人们的重视。软件测试作为保障软件可靠性的重要手段之一,一直以来都是国内外科研人员的研究热点。动态符号执行技术是软件测试领域的前沿技术,从诞生以来一直受人们的广泛关注。国内外研究人员基于动态符号执行技术开发了很多实用的软件测试工具,KLEE就是其中的佼佼者。然而,KLEE只能对单线程程序进行符号执行。鉴于此,瑞典洛桑联邦理工学院的Stefan Bucur与其合作伙伴在KLEE的基础上开发了并行符号执行工具Cloud9,实现了对多线程程序的符号执行。但是Cloud9在对多线程程序进行符号执行时没有考虑线程交错调度问题,不能完全探索多线程程序的所有路径。因此,本文在Cloud9的基础上,设计并实现了可以覆盖所有路径分支的一般多线程符号执行框架,并在此基础上,提出了基于断言制导的多线程符号执行方法。本文的主要贡献包括以下三点:在研究了符号执行基本理论和Cloud9对多线程程序符号执行的方法的基础上,给出了可以覆盖所有路径分支的一般多线程程序符号执行框架,从三个方面来讲述:首先,对多线程符号执行的相关概念进行描述,为后续算法的提出做准备;其次,引入广义交错图(Genernalized Interleaving Graph,GIG)的概念,实现对多线程符号执行过程的模型化;最后,用算法的形式给出了一般多线程符号执行的基本过程。为了缓解多线程符号执行面临的路径爆炸问题,本文在一般多线程符号执行框架的基础上,提出了基于断言制导的多线程符号执行方法。然后,给出了该方法中重要模块的设计方案,最终在Cloud9上实现了该方法。使用软件验证竞赛(The 2018 Software Verfication Competition)提供的多线程程序测试用例对本文提出的方法进行了测试,测试结果表明了该方法对于删减多线程符号执行的冗余执行具有可行性,即可以在一定程度上缓解多线程符号执行的路径爆炸问题。