程序静态分析中的符号执行引擎及状态合并研究总结

版权申诉
0 下载量 103 浏览量 更新于2024-04-19 收藏 2.59MB PDF 举报
C语言作为一种底层机器操控灵活性较高的编程语言,在操作系统、嵌入式软件、底层驱动等领域有着广泛的应用。然而,由于其对计算机的完全掌控和效率考量,C语言程序在安全性方面存在一定的弱点,如非法指针解引用、内存泄漏、缓冲区溢出等内存安全问题。为了提高软件的可靠性,软件开发过程中使用了多种方法,包括程序动态测试、程序静态分析和程序验证。其中,程序验证是一种通过形式化方法对程序的各种性质给出严格数学证明来保证程序正确性的手段,但由于需要大量的人工证明而未能在工业界得到广泛应用。 程序动态测试的测试结果依赖于给定的测试集,对于复杂的软件系统很难实现高覆盖率,同时动态测试的成本和风险也相对较高。而程序静态分析则在程序运行之前对代码进行分析,能够较早、低成本地发现代码中可能存在的缺陷。符号执行技术因其精度控制和代码覆盖率的优点而被广泛应用于程序静态分析中。在对程序进行分析时,符号执行引擎会模拟真实的程序执行过程,分析程序的数据流和控制流信息,并检查程序的执行过程。 本文《搜索引擎-形状分析符号执行引擎中的状态合并.pdf》就探讨了在形状分析符号执行引擎中的状态合并问题。形状分析符号执行引擎是一种基于符号执行技术的静态程序分析方法,旨在通过符号执行过程中抽象程序的状态信息来发现潜在的缺陷。其中,状态合并是形状分析符号执行引擎中一项重要的优化技术,旨在减少状态空间的大小,提高程序分析的效率。 在本文中,研究者提出了一种结合路径条件的状态合并算法,可以根据路径条件具有相同的程序执行路径来合并具有相似状态的程序路径,从而减少状态空间的大小,提高程序分析的效率。研究者在测试了多个程序样例后,得出了结论:该状态合并算法能够有效地减少程序状态空间的规模,提高程序分析的效率。 总的来说,本文的研究对形状分析符号执行引擎中的状态合并问题进行了深入的探讨,提出了一种路径条件结合的状态合并算法,该算法在多个程序样例上取得了显著的效果。这对于提高形状分析符号执行引擎的分析效率和准确性具有一定的实际意义,也为软件安全性和可靠性的提升提供了有益的参考。