简单的活着

MDPC

Posted on By Mista Cai

Towards Optimal Concolic Testing

ABSTRACT

符号测试集成了用于生成测试用例的具体执行(例如,随机测试)和符号执行。它有时比随机测试或符号执行更具成本效益。一个符号测试策略是一个决定何时应用随机测试或符号执行的函数,如果是后一种情况,则是一个符号执行的程序路径。已经提出了许多基于启发式的策略。什么是最佳的符号测试策略仍然是一个开放的问题。在这项工作中,我们为解决这个问题做出了两点贡献。首先,我们展示了可以基于程序路径的概率和约束求解的成本来定义最优策略。然后将识别最优策略的问题简化为具有成本的马尔可夫决策过程的模型检查问题。其次,鉴于识别最优策略的复杂性,我们设计了一种近似最优策略的贪婪算法。我们进行了两组实验。一种是基于随机生成的模型,另一种是基于一组C程序。结果表明,现有的启发式方法有很大的提升空间,我们的贪婪算法往往优于现有的启发式算法。

1 INTRODUCTION

Concolic testing,也称为动态符号执行,是具体执行(a.k.a.测试)与符号执行的集成[22,41]。具体执行和符号执行在本质上相互补充。一方面,具体执行在计算上便宜。也就是说,我们根据所有测试输入的先前概率分布继续对测试输入进行采样,并且具体地执行具有测试输入的程序,直到满足某些测试覆盖标准。问题是如果某个程序路径的概率非常低,则必须对大量测试输入进行采样以覆盖程序路径。另一方面,符号执行通过识别必须满足的约束来解决该问题,以便覆盖程序路径并解决约束以获得测试输入。换句话说,用符号执行覆盖程序路径的概率是1。问题在于符号执行通常在计算上很昂贵。直观地说,有效的分析测试策略应该象征性地执行那些低概率程序路径,并具体执行那些路径条件难以解决的程序路径。

关于什么是最优的符号测试策略仍然是一个悬而未决的问题。在文献中,已经有多种尝试来解决这个问题[6,7,23,33,38,42]。例如,已经开发了几种启发式方法来回答这个问题:我们在符号测试中象征性地执行哪些程序路径(在所有程序路径中)?仅举几例,Burnim等。提出了CFG策略[6],它计算从执行路径中的分支到任何未覆盖语句的距离,并选择具有最小距离的分支。在[23]中,Godefroid等人。提出了代际策略,它测量执行路径中每个分支的增量覆盖增益,并通过扩展具有最高覆盖增益的分支来指导搜索。在[33]中,李等人。引入了一种技术,将符号执行引导到较少行进的路径。虽然现有的启发式方法已被证明在经验上是有效的,但尚不清楚是否可以实现更好的性能或者它们与最佳性能的距离。

此外,现有工作在很大程度上忽略了问题的另一部分,即我们如何在具体执行和符号执行之间切换以实现最佳性能?据我们所知,这个问题最近才在[3,4,45]中讨论过。作者基于程序的概率视图比较了随机测试和系统测试方法(包括但不限于符号执行)的有效性,并提出了一种混合策略,当随机测试发现更多时,从随机测试切换到系统测试每单位时间的错误。然而,他们的方法对系统测试方法有一个非常抽象的观点,并没有考虑,例如,应用符号执行的不同策略。此外,他们的算法是非常高级的,并且仅在模拟模型上验证。

在这项工作中,我们的目标是开发一个框架,使我们能够定义和计算最佳的分析测试策略。也就是说,我们的目标是系统地回答何时应用具体的执行,何时应用符号执行以及应用符号执行的程序路径。特别是,我们做出以下技术贡献。

  • 首先,我们表明可以基于程序行为的概率抽象来定义最优的范数测试策略。
  • 其次,我们证明了识别最优策略的问题可以简化为具有成本的马尔可夫决策过程的模型检验问题。因此,我们可以重用现有的工具和算法来解决问题。
  • 第三,我们使用一组模拟实验来验证现有的启发式算法,并表明它们有很大的改进空间。
  • 第四,鉴于计算最优策略的高度复杂性,我们提出了一种近似最优策略的贪婪算法。我们根据模拟实验和C程序实验对贪婪算法进行了实证评估,并证明它比KLEE中现有的启发式算法获得更好的性能[7]。

论文的剩余部分安排如下。第2节定义了研究问题,并显示了它与一个例子的相关性。第3节将问题简化为模型检查问题,并将现有的启发式算法与最优策略进行比较。第4节开发了一种贪婪算法,它允许我们近似最优策略。第5节介绍了我们的实现并评估了贪婪算法。第6节回顾了相关工作,第7节得出结论。

7 CONCLUSION

在这项工作中,我们提出了一个框架来推导出最优的符号测试策略,在此基础上我们分析现有的启发式算法,并提出一种新算法来近似最优策略。 对随机生成的模型和一组真实C程序的评估表明,我们的算法经常优于大多数现有的基于启发式的算法。 对于未来的工作,我们希望研究估算概率和解决程序路径成本的替代方法。 此外,我们希望将我们的框架扩展到其他测试用例生成方法。