Dynamic symbolic execution is a widely used technique for automated software testing, designed for execution paths exploration and program errors detection. A hybrid approach has recently become widespread, when the main goal of symbolic execution is helping fuzzer increase program coverage. The more branches symbolic executor can invert, the more useful it is for fuzzer. A program control flow often depends on memory values, which are obtained by computing address indexes from user input. However, most DSE tools don't support such dependencies, so they miss some desired program branches. We implement symbolic addresses reasoning on memory reads in our dynamic symbolic execution tool Sydr. Possible memory access regions are determined by either analyzing memory address symbolic expressions, or binary searching with SMT-solver. We propose an enhanced linearization technique to model memory accesses. Different memory modeling methods are compared on the set of programs. Our evaluation shows that symbolic addresses handling allows to discover new symbolic branches and increase the program coverage.
翻译:动态符号执行是一种广泛使用的自动软件测试技术,设计用于执行路径探测和程序错误探测。 混合方法最近变得很普遍, 当象征性执行的主要目标是帮助模糊器扩大程序覆盖范围。 符号执行者越多分支可以反转, 就越对模糊器有用。 程序控制流程往往取决于记忆值, 而这些值是通过用户输入的地址索引计算获得的。 然而, 大多数 DSE 工具不支持这种依赖性, 因而它们错过了某些想要的程序分支。 我们用动态符号执行工具Sydr 来解释记忆的符号地址推理。 可能存在的存储访问区域通过分析记忆信号表达方式或SMT- 索尔的二进式搜索来确定。 我们建议用强化的线性技术来模拟存储访问。 不同的记忆模型方法在程序集中比较。 我们的评估显示, 符号地址处理可以发现新的符号分支, 并增加程序覆盖范围。