问题标签 [symbolic-execution]

现在我对符号执行（SE）和可达性分析（RA）感到困惑。据我所知，SE 使用符号来执行一些代码以到达具有分支条件的每个分支。而且 RA 可以用来查找每个分支的可达性，对吧？当使用 RA 时，我们可以提取每个分支的分支条件。如果是这样，它们之间有什么区别？他们能快点吗？都是静态分析吗？

谢谢，夏娃

我正在考虑使用符号执行来测试用特定语言（如 java）编写的程序的健壮性。我读过一些介绍符号执行基本概念的论文。但我不清楚如何开始。

例如，如何从具体输入生成约束条件？那么任何人都可以就符号执行的实现基础给我一些建议吗？此外，concolic execution(concrete + symbolic) 怎么样？

我想在 llvm IR 中做点分析。我希望它是路径敏感的，这意味着当我打印出结果时，我需要附加“May”指向的条件。

我计划使用符号执行来实现这个目标。

llvm中是否有任何工具，或独立工具来解决符号方程。

谢谢！

是否有任何用于位向量（QF_BV 逻辑）的工具，它将象征性地执行操作并根据位向量的符号值返回输出，以便我可以根据需要对它们应用我自己的计算？或者是否有任何 SMT 求解器可以在位爆破后提取变量的符号值？例如：

让，

1. X[3:0], Y[3:0], Z[4:0], W[4:0] 被声明为位向量而不初始化任何值
2. 打印 X[3:0]
3. X[3:0] <- X[3:0] >> 1（逻辑移位）
4. 打印 X[3:0]
5. Z[4:0] <- X[3:0] + Y[3:0]
6. 打印 Z[4:0]
7. 打印 Y[3:0]
8. W[4:0] <- Y[3:0] + 0000
9. 打印 W[4:0]
10. …………

所需的输出（像这样的符号）：

是否可以在 Linux 内核或部分内核上运行符号执行？Concolic测试怎么样？谢谢！

当我了解concolic 测试的概念时，我遇到了“具体和符号执行”这些术语。（那里提到的文章“CUTE: A concolic unit testing engine for C”在其摘要部分使用了该术语。）

“所使用的方法建立在先前结合符号和具体执行的工作的基础上，更具体地说，使用这种组合来生成测试输入以探索所有可行的执行路径。”

谁能确认“具体执行”是什么意思？尽管我进行了搜索，但我找不到任何直接引用/明确的陈述。

据我了解，“具体执行”是指“执行具有实际输入值的程序，这与符号执行不同，符号执行将符号值假定为变量、输入等”。如果我错了，请纠正我（如果可能的话，举个小例子）。

我最近阅读了EJ Schwartz 博士的一篇题为“所有你想知道的关于动态污点分析和正向符号执行（但可能不敢问）”的论文。在论文中，他主要讨论了它们在二进制级别安全上下文中的应用。

我很好奇动态污点分析和正向符号执行之间的确切区别。

据我所知，只要存储在 x 中的信息传输到对象 y ，污点分析就会跟踪从对象 x( source ) 到对象 y( sink ) 的信息流。所以主要关心的是什么对象可以被源传递地影响。而符号执行将一些输入视为符号值，并尝试用符号值来表达其他变量；因此它回答了符号输入影响后续程序的条件。

我可以看到，在二进制层面，污点分析经常被提到返回地址覆盖导致的漏洞；而符号执行可以处理更多类型的易受攻击的问题，例如整数溢出、运行时断言错误、资源泄漏（例如，内存泄漏、文件打开/关闭）、缓冲区溢出。

然而，现代污点分析似乎不仅仅涉及数据流分析，它们大多会跟踪控制流条件；在几个漏洞检测场景中，受污染的输入也表示为符号值，并像符号执行一样传播。另一方面，由于底层约束求解器和执行/解释运行时的限制，符号执行引擎不能完全使用由不同路径条件分隔的符号值；因此，它们无法达到预期的高分支或路径覆盖率。

那么在一般情况下，是否可以说污点分析是一种粗略的符号执行，或者说符号执行是一种精确的污点分析呢？

是否有任何用于在二进制文件上进行符号执行的工具。我的意思是使用哪个，我们不需要修改源代码 - 比如 klee_make_symbolic 或者我们可以在 IR（llvm ir 等）中进行此类更改，提前谢谢

我正在使用 Angr，一个符号执行框架。它只接受 C 中的“读取”函数来获取输入。它解决了 C 中的一个程序并将其符号值转换为具体值，我在其输出中得到了这个：

它实际上是由 read(0, input, 8) 读取的 char[8] 变量的值，但我不知道最后输入的值是什么。

请帮我。非常感谢。

静态分析（例如编译器）可以检测到哪些错误，而符号执行无法检测到哪些错误？符号执行可以检测到静态分析无法检测到的哪些错误？例如，符号执行可以检测语法错误吗？