llvm - 二进制符号执行工具

Question

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

Answer 1

也许miasm 可以满足您的要求。它是一个支持静态符号执行的逆向工程框架。据我所知，它比 KLEE 和 S2E 更简单。

Answer 2

规范列表在Awesome Symbolic Execution中。

Answer 3

以符号方式执行二进制代码要困难得多，所以我怀疑是否存在这样的工具。

但是请注意，使用 KLEE 时不一定需要修改代码，因为它可以对 POSIX 环境和 C 库进行建模（当然，在支持此编译时）。使用这些功能，您可以自动符号化argv参数和键盘交互。