buffer-overflow - 如何使用符号执行来查找错误，例如 SAGE、KLEE、S2E

Question

就像标题一样，任何人都知道这些工具用于查找错误的方式的区别？KLEE 和 SAGE 可能会发现越界访问和缓冲区溢出，KLEE 可以使用断言，但还有其他方法吗？

Answer 1

你的问题很笼统。我建议阅读科学论文和文档以获取深入的信息。

但是，SAGE 主要使用 Concolic 执行，而 KLEE 使用（香草）符号执行。S2E 仍然与这些不同（即使是一个遥远的 KLEE 分支），因为它使用符号执行和具体执行之间的动态切换，使用允许 QEMU-BC 和 LLVM-BC 之间动态转换的 jit。

这与这些特定工​​具使用的执行范例的根本差异有关，但显然它只能触及表面。

对于最终用户来说，一个相关的区别是 KLEE 必须使用能够发出 llvm 代码（例如 llvm-gcc 或 clang）的特定编译器进行编译，并且开发人员必须弄乱构建系统。这通常意味着 KLEE 仅限于纯 C。S2E 不关心您使用哪种语言，您可以运行已编译的二进制文件，但缺点是无法检测到某些缓冲区溢出并且执行速度有点慢（取决于100 倍）。这取决于您要分析的内容。