问题标签 [symbolic-execution]

我想使用angr来分析 IoT 固件文件。我已经阅读了angr的文档，但是我找不到分析固件文件的解决方案。那么angr如何生成Firmware的CFG文件呢？或者我如何用angr作为符号执行来分析固件文件？

我是angr的新手，试图解决一个简单的可执行文件，它读取 3 个字符并与字符串“abc”进行比较。

angr脚本：

当我没有明确地为bland_state. 但是当提供“stdin”时它显示“未找到”。

• 问题 1：示例中的语法，但我的代码有什么问题？我尝试了 3 个和 4 个字节（1 个用于 '\n'），它们都不起作用。

• 问题 2：另一个示例的语法，为什么它在示例中有效，但在我的代码中无效？

我正在添加对在 concolic 引擎中检测 invokedynamic 的支持，我们目前检测的方式是使用自定义类加载器，该类加载器在类路径中查找与该类相关的资源，但由于 lambda 是动态创建的合成类，它不是实际上在那里。

您知道如何检测调用动态生成的类吗？我已经看到使用代理可能是一种选择，但我想确保我不能重用我已经拥有的东西。

在哪些情况下不能使用符号执行进行断言检查？为了说明，举以下例子：

在这里，我们可以使用符号执行并找出¬A ^ (B < 5) ^ C违反我们的断言。现在，假设我们将第一个条件更改如下：

通过这种变化，我们不知道 x 和 b 的新值。那么，我们仍然可以使用符号执行来进行断言检查吗？

一般来说，有什么情况我们不能使用符号执行？即，我们必须分析程序所有可能运行的情况。

我正在尝试使用基于 SMT Solver Z3 的符号执行逻辑生成测试用例。

我有以下代码。

现在，在 SMT 解决过程中发生错误，生成的错误日志如下所示。

我已经用这段代码做了一些测试。

如果我不在 assert 函数中使用 x, y, z ，则没有错误。

如果第一个'if 语句'为真（即a != 0），那么程序将永远不会进入'if (!a && c) 语句。如果我删除这些“if 语句”之一，则没有错误。但我不明白为什么会发生这个错误。谁能向我解释为什么 Z3 无法解决这个问题？谢谢你。

我不明白符号执行与白盒模糊测试有何不同？据我了解，Whitebox Fuzzers 以某种初始输入格式象征性地执行代码。此外，如果有人可以参考 KLEE 和 AFL 工具区分这两种形式，那将会很有帮助。

我正在尝试使用 angr 通过为给定结果导出正确的输入来验证函数的行为。该函数修改了一个缓冲区，在这种情况下，它只是将输入复制到其中，因此我在堆上设置了符号变量，并对其应用了等式约束。然后我为函数的输入创建一个符号变量。我打算发生的事情是 angr 本质上运行该函数，直到找到输入，这样当它被复制到缓冲区时，它满足放置在其上的约束。但是，当它运行时，我只得到一个死分支，其中输出具有正确的值，但输入没有。我在下面附上了求解器和测试程序源。这是我的实施失败吗？还是这种解决问题的方法无效

求解器

测试程序

当我运行求解器时，我得到如下输出，尽管第一个值（输入值）看似随机变化。有没有办法应用这个约束，以便程序的副作用优先？我不明白这两个值有何不同。这是我准备记忆的方式错误吗？

介绍

给定一个用 C++ 编写的简单函数，如下所示：

问题

如何注释程序以执行以下操作z3？

1. 检测死代码。(x = x + 4)
2. 生成测试用例（代码覆盖率）。
3. 分析不变量。
4. Pre&Post代码检查。

我做了什么？

我知道我需要识别代码中每个块的每个路径：

然后，如果我使用 Z3，我可以检查这些路径中是否有任何一个unsat推断与它们相关的代码块将是Dead code.

我需要什么帮助？

• 对于死码检测：

我真的不知道如何在z3. 我应该为每条路径使用不同的求解器吗？像这样：

我认为这是检测死代码的低效方法。如果有一百种不同的路径怎么办？所以必须有更好的方法来做到这一点。

• 对于分析不变量：

同样，我应该为每个代码块使用不同的求解器吗？例如：

• 而且我不知道如何Generate test cases做Pre和Post代码检查

最后，我的问题实际上是，如何使用 z3 针对不同的场景分析程序，例如Dead Code Detection、Invariant analysis、Test-case generation等。更具体地说，我正在寻找这方面的最佳实践。中的示例代码z3-solver将有很大帮助。更优选地，我想看看如何改进z3我上面提供的示例代码。

谢谢你的帮助