基于机器学习约束求解的复杂软件代码符号执行框架研究
发布时间：2019-07-02 12:00
【摘要】：如何生成高质量的测试用例一直是软件测试领域的重要研究课题。不同于其他测试用例生成技术,基于符号执行的测试用例自动生成技术在程序执行的过程中使用符号化的变量代替具体值的变量,同时维护整个执行过程中的路径约束,当遇到分支语句的时候即调用底层的约束求解器求解该路径约束以生成触发该分支路径的测试用例。该技术经过多年发展已经被应用到了诸多测试工具,比如jCUTE,KLEE和SPF等。当前基于符号执行的测试用例生成技术在应用到真实程序时仍然面临着不少的挑战。其中一个最主要的挑战就是底层约束求解器无法对真实程序中的复杂路径约束提供有效支持。造成这个问题主要有两个方面的原因:一是真实程序中存在着大量复杂的数值计算,包括非线性数值计算,常见的数学函数的计算等,现有的约束求解器对这类约束很难提供有效支持;二是真实程序中存在着大量的函数调用,现有的约束求解器通常只提供纯数学表达式形式的约束支持,在函数具体实现细节无法得知的情况下,约束求解器很难对这类包含函数调用的路径约束进行求解。为了解决以上两个方面的问题,提高符号执行技术应用在真实程序的效率,本文的主要工作如下:·基于机器学习约束求解的符号执行框架。不同于传统的符号执行框架,本文提出了一种新的基于机器学习的符号执行框架——MLBSE。MLBSE与传统符号执行框架最显著的区别就是底层约束求解技术。针对复杂路径约束,MLBSE首先借助约束不满足程度将路径约束的满足性问题转化为优化问题,然后使用基于机器学习的优化算法RACOS对路径约束进行求解。借助于这种基于机器学习的约束求解方法的优势,MLBSE能够更好地支持包含大量复杂数值计算和函数调用的真实程序。·基于MLBSE的符号执行功能增强。在已有的基于机器学习约束求解的符号执行框架MLBSE的基础上,为了进一步增强MLBSE符号执行功能,本文做了包括黑盒执行模式,可解置信度报告和基于可解置信度报告的搜索策略三个方面的功能拓展。借助黑盒执行模式,MLBSE能更加高效地处理包含函数调用的真实程序。通过引入可解置信度报告,MLBSE能够在计算资源有限的情况下为用户提供额外参考,帮助用户判断是否需要投入更多计算资源在求解失败的路径约束上。除此以外,MLBSE还提供了一种基于可解置信度报告的搜索策略。基于该策略,MLBSE能自动为求解失败且可解置信度高的路径约束投入更多的计算资源,从而在不影响整体效率的前提下提高符号执行的效果。·实现和实验。在开源符号执行引擎SPF的基础上,本文完整地实现了基于机器学习约束求解的符号执行工具MLB。为了验证MLB在真实程序上执行的效果和效率,本文选择了 19个真实使用的程序作为测试程序,并同4个基于符号执行的测试用例自动生成工具做了严格的对比实验。实验表明,MLB在效率、稳定性和生成测试用例的质量上都有着更好的表现。除此之外,本文还针对MLB的三个拓展功能做了一系列的实验。实验表明,MLB提供的可解置信度报告是具有参考价值的,同时黑盒执行模式和基于可解置信度报告的搜索策略能进一步增强符号执行的功能。
[Abstract]:How to generate high-quality test cases has been an important research topic in the field of software testing. Unlike other test case generation techniques, the symbol-based test case automatic generation technology replaces the variable of the specific value by using the symbolized variable in the process of program execution, while maintaining the path constraint in the whole execution process, When a branch statement is encountered, the constrained solver of the bottom layer is called to solve the path constraint to generate a test case that triggers the branch path. The technology has been applied to many testing tools, such as jCUTE, KLEE, and SPF, for many years. Currently, the symbol-based test case generation technology still faces many challenges in the application to the real program. One of the most important challenges is that the underlying constraint solver is unable to provide effective support for complex path constraints in the real program. There are two main reasons for this problem: first, there are a lot of complex numerical calculation in the real program, including the non-linear numerical calculation, the calculation of the common mathematical functions, etc., and the existing constraint solver is difficult to provide effective support for such constraints; Second, there is a large number of function calls in the real program, the existing constraint solver usually only provides the constraint support in the form of pure mathematical expression, and in the case where the specific implementation details of the function cannot be known, the constraint solver is difficult to solve the path constraint containing the function call. In order to solve the above two problems, to improve the efficiency of the symbol execution technology in the real program, the main work of this paper is as follows: Different from the traditional symbol execution framework, this paper presents a new symbol execution framework based on machine learning. The most significant difference between MLBSE and traditional symbol execution framework is the underlying constraint solving technique. For complex path constraints, the MLBSE first converts the path constraint satisfaction problem to the optimization problem by means of the constraint dissatisfaction degree, and then uses the machine-based optimization algorithm RACOS to solve the path constraint. With this advantage of a machine-based constrained solution approach, the MLBSE can better support a real program that contains a large number of complex numeric calculations and function calls. 路 The symbol execution function is enhanced based on the MLBSE. On the basis of the existing symbol execution framework MLBSE based on machine learning constraint solution, in order to further enhance the MLBSE symbol execution function, this paper has done the function expansion of three aspects including the black box execution mode, the solvability confidence report and the search strategy based on the solution confidence report. MLBSE can handle the real program with function calls more efficiently with the black box execution mode. By introducing a detest confidence report, the MLBSE is able to provide the user with additional references in the case of limited computing resources to help the user to determine whether more computing resources are required to be placed on the path constraints of the solution failure. In addition, the MLBSE provides a search strategy based on a solvability report. Based on this strategy, MLBSE can put more computational resources into path constraints with failure and high confidence, so as to improve the effect of symbol execution without affecting the overall efficiency. 路 Implement and experiment. On the basis of open source symbol execution engine (SPF), this paper fully implements the symbol execution tool MLB based on machine learning constraint solution. In order to verify the effect and efficiency of MLB's execution on the real program, this paper chooses 19 real-use programs as the test program, and makes a strict contrast experiment with the four symbol-based test case automatic generation tools. The results show that MLB has better performance in terms of efficiency, stability and quality of generating test cases. In addition, this paper has done a series of experiments for the three development functions of MLB. The experiment shows that the solution confidence report provided by the MLB is of reference value, while the black box execution mode and the search strategy based on the solution confidence report can further enhance the function of the symbol execution.
【学位授予单位】：南京大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP311.53
本文编号：2508912
[Abstract]:How to generate high-quality test cases has been an important research topic in the field of software testing. Unlike other test case generation techniques, the symbol-based test case automatic generation technology replaces the variable of the specific value by using the symbolized variable in the process of program execution, while maintaining the path constraint in the whole execution process, When a branch statement is encountered, the constrained solver of the bottom layer is called to solve the path constraint to generate a test case that triggers the branch path. The technology has been applied to many testing tools, such as jCUTE, KLEE, and SPF, for many years. Currently, the symbol-based test case generation technology still faces many challenges in the application to the real program. One of the most important challenges is that the underlying constraint solver is unable to provide effective support for complex path constraints in the real program. There are two main reasons for this problem: first, there are a lot of complex numerical calculation in the real program, including the non-linear numerical calculation, the calculation of the common mathematical functions, etc., and the existing constraint solver is difficult to provide effective support for such constraints; Second, there is a large number of function calls in the real program, the existing constraint solver usually only provides the constraint support in the form of pure mathematical expression, and in the case where the specific implementation details of the function cannot be known, the constraint solver is difficult to solve the path constraint containing the function call. In order to solve the above two problems, to improve the efficiency of the symbol execution technology in the real program, the main work of this paper is as follows: Different from the traditional symbol execution framework, this paper presents a new symbol execution framework based on machine learning. The most significant difference between MLBSE and traditional symbol execution framework is the underlying constraint solving technique. For complex path constraints, the MLBSE first converts the path constraint satisfaction problem to the optimization problem by means of the constraint dissatisfaction degree, and then uses the machine-based optimization algorithm RACOS to solve the path constraint. With this advantage of a machine-based constrained solution approach, the MLBSE can better support a real program that contains a large number of complex numeric calculations and function calls. 路 The symbol execution function is enhanced based on the MLBSE. On the basis of the existing symbol execution framework MLBSE based on machine learning constraint solution, in order to further enhance the MLBSE symbol execution function, this paper has done the function expansion of three aspects including the black box execution mode, the solvability confidence report and the search strategy based on the solution confidence report. MLBSE can handle the real program with function calls more efficiently with the black box execution mode. By introducing a detest confidence report, the MLBSE is able to provide the user with additional references in the case of limited computing resources to help the user to determine whether more computing resources are required to be placed on the path constraints of the solution failure. In addition, the MLBSE provides a search strategy based on a solvability report. Based on this strategy, MLBSE can put more computational resources into path constraints with failure and high confidence, so as to improve the effect of symbol execution without affecting the overall efficiency. 路 Implement and experiment. On the basis of open source symbol execution engine (SPF), this paper fully implements the symbol execution tool MLB based on machine learning constraint solution. In order to verify the effect and efficiency of MLB's execution on the real program, this paper chooses 19 real-use programs as the test program, and makes a strict contrast experiment with the four symbol-based test case automatic generation tools. The results show that MLB has better performance in terms of efficiency, stability and quality of generating test cases. In addition, this paper has done a series of experiments for the three development functions of MLB. The experiment shows that the solution confidence report provided by the MLB is of reference value, while the black box execution mode and the search strategy based on the solution confidence report can further enhance the function of the symbol execution.
【学位授予单位】：南京大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP311.53
【参考文献】
中国期刊全文数据库 前2条
1 孙志永;;Windows Vista会成功吗[J];信息系统工程;2007年02期
2 周煜,周国庆,奚文骏;软件测试技术概述[J];中国测试技术;2005年03期
，本文编号：2508912
本文链接：https://www.wllwen.com/kejilunwen/ruanjiangongchenglunwen/2508912.html
