如何为特定语言实现符号执行引擎？

Question

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

例如，如何从具体输入生成约束条件？那么任何人都可以给我一些有关符号执行实现的基础知识的建议吗？此外，concolic执行（具体+象征）怎么样？

Answer 1

如何从具体输入生成约束条件？

使用符号或联合执行

那么任何人都可以给我一些有关符号执行实现的基础知识的建议吗？

我的建议和赵子明一样：使用现有的符号执行工具。不要尝试自己实现，这会非常困难且耗时。

以下是最受欢迎的项目（更完整的列表请参见此处）：

Java：JPF + 符号探路者、JCute。

C 和 C++：KLEE、Kite