动态符号执行（Dynamic symbolic execution，DSE）是一种目前较流行的，强大的分析方法，它通常用在下面几种情况中，如：

Miasm并不是第一个实现了这一功能的工具，但是，因为它已经满足所有实现DSE的必要条件,所以将其他功能添加到main branch只是时间问题。

本文用几个例子和一个简单的API来教你怎么在脚本中使用DSE。

概述：

这篇分析基于1fb3326版Miasm

动态符号执行（DSE，也叫做concolic execution)使用一个具体的值进行符号执行。这种符号执行可以避免由循环引起的路径爆炸，和在表达式太复杂或系统调用会生成值时给符号一个具体的值。

在这种方法中，我们每次只考虑一条路径，输入约束会随着程序路径的不断延伸而不断增长，当路径走到尽头时，将其中某一个约束条件取反，以到达新的代码路径。

接下来我们通过一个例子来介绍DSE。

思考下列代码：

我们先用一个具体的值来进行第一次代码执行，此处令arg=0。

接下来，在进行一次符号执行之后，我们得到下述表达式：

因为表达式无解，符号执行运行不到函数结尾。当然，在这里我们可以采用其他方法，比如说多路径符号执行，但这不是本例的重点。

到这一步，在不考虑条件的前提下，通过使用具体的值进行符号执行，我们已经有了一个条件输出（也就是一条可能的路径）

接下来对条件进行取反，也就是假设(ARG & 0xFF == 0x12)不成立，或者说是(ARG & 0xFF != 0x12),我们把新的条件加入到条件执行状态中。接下来我们统一把这样的条件叫做约束。

执行最终会结束，然后返回ARG + 1。这样，我们就可以得出这一块代码在(ARG & 0xFF != 0x12)时返回ARG + 1。尽管代码可能会被混淆，但我们使用这种方式根据不需要看代码。

你以为这些就是全部了吗，我们还可以用DSE做更多的事！我们可以用SMT求解器把路径中的约束取反。假设求解器求出的答案是ARG = 0x123412,它满足条件(ARG & 0xFF == 0x12)。

在对输入进行上述操作之后，我们又得到了一条新的路径和一个新的结果：如果(ARG & 0xFF == 0x12)代码段返回ARG + 14。上面这些就是在程序中产生新的输入以到达新的代码区域的全部过程了。这一方法常常被一些顶级团队用在网络安全挑战赛中，他们通过构造新的输入以使代码到达模糊测试到达不了的地方，以此加强模糊测试的效果。模糊测试在测试输入时确实非常快，但当碰见"复杂的条件"时，例如比较输入和magic值（译者注：事先约定好的几个固定的字节时，它们就不那么有效了）.所幸，这正是DSE的长处。

接下来我们用这一技术对一个被混淆过的算法进行恢复。我们用的例子来自于 J. Salwan的Tigress.

整个Tigress由几个程序组成，它们接收命令行参数，通过算法运算后输出一个值。

首先，我们写个脚本用Miasm来运行这个程序。PR #515可以让我们模拟运行Linux二进制文件的环境。

现在启动这个程序会报错，因为strtoul这个桩还没有插入程序中。

接下来我们手动实现一个strtoul。

写好strtoul后，再次运行程序，这次程序直接崩溃了。原因是这个函数使用了栈空间，所以我们要模拟栈操作（段+内存管理）

我们还需要支持128位的操作，所以我们会使用llvmjitter(python也可以，但会比较慢)

写好这些后，程序就能正常运行了。

接下来，我们需要用输入建立一个输出值的等式

也就是说，我们需要把strtoul的返回值"符号化"，并取得printf第二个参数的等式。

要做到这一步，我们需要在strtoul的末尾，把DSE引擎附加到jitter。在附加之后，Miasm会自动通知符号引擎具体值的状态，收集约束，检查符号执行是否与具体状态相同等等。

首先，实例化DSEEngine对象，用它向外部API中插入我们的代码（像沙盒一样）

接下来，在strtoul的末尾把DSE对象附加到jitter，把所有寄存器的值设置为具体值（我们不需要追踪它们的值）最后把返回值赋值给符号

这个脚本的执行时间会有点长。运行到后面还会报错，这时我们看一下xxx_printf_symb这个函数，它是printf的桩函数。

别被吓到了，我们只需要查看它的第二个参数。

最后我们得到下面这个复杂的等式。

把VALUE=123456789代进去算一下，用assert关键字把它的值断言为和具体值一样。

可以发现，这一次的输入令我们的等式成立了。

在J. Salwan用来对结果进行验证的多个测试用例上运行，我们可以获得同样的准确率。（下一个例子涉及到信号处理，为简单起见，这里就不介绍了）

不出所料，我们的公式对于VM-0的Challenge-2是不成立的。

通过用同一模块中的DSEPathConstraint类替换DSEEngine类，可以让Miasm跟踪路径上的约束。

这些约束会存放在z3.Solver对象上，我们可以通过dse.cur_solver来对他们进行访问（然后是dse.cur_solver.assertions）。

不过这个对象能做的不仅仅是这些，根据produce_solution选项的不同，它可以实现不同的功能，几个选项如下：

它会为试着为每块没走过的代码段，CFG分支和CFG路径分别生成一个新的反例.

默认情况下，这个方法会在new_solutions这个属性中存放多个（solution identifier和其对应的输入）。

这些方案可以通过重写produce_solution（判断是否应该生成新的求解器）和handle_solution（将结果求解器模型转化成新的解法）进行扩展

所以，在这个例子中，用默认选项（code coverage）运行脚本后，程序就返回一些（新目标，解决方案）：

事实上，我们可以根据错误的输入值对公式的输出值进行验证，除了633318710181888（两条不同的路径可以产生相同的结果）

进一步来说，通过重写handle_solution并找到对应的路径约束，然后根据对应的公式用新的值重新模拟这个过程，我们就可以还原最初的约束（if(cond)会影响到产生的公式）条件。example/symbol_exec/dse_strategies.py这个例子可以用作这种方法的入门学习。

在模糊测试中，我们可以用这些值作为新的输入来到达新的代码段。

还记得这个shellcode吗？

提醒一下，这个shellcode通篇只有字母和数字，它实际上有一个自修改的桩（self-modifying stub）可在适当位置对真正的shellcode进行脱壳。

shellcode中的桩程序会在跳转到真正的payload之前运行两个解密循环，而真正的shellcode会下载并执行指定程序。

剧透：我们会使用DSE来获得一个类似的shellcode，但是是从一个受控制的URL上下载下来的。

首先，我们运行一个脚本来加载这个shellcode（起码到达初始进入点）。

首先要获得存储初始状态函数的结果的方程。要做到这一步，我们会使用DSE引擎，在内存中符号化初始的shellcode，符号化的内存范围可以通过symbolize_memory函数指定。

这样就可以获取0x42th处的等式了。

也就是：(MEM_0x400053^(MEM_0x400052*0x10))

MEM_<addr>是DSE引擎用于表示符号化addr处的内存而创建的符号，这个符号可以通过dse.memory_to_expr(addr)函数获得。

从我们先前的分析来看，最终的内存由桩程序，下载并执行的payload，以unicode编码的URLs和一些无用的字节组成。

要想达成我们的目的，需要保留最终的payload和更新URL，也就是说，我们会把最终状态设置为和内存中在0x368字节处（stub+payload），以及接下来我们更新过URL。

要完成上述目标，我们先用DSEPathConstraint这个对象来保存路径约束。

接下来，用我们的URL构建我们期望的内存布局。

注意，这个脚本也可以用来修改payload...
现在，把最终状态设为内存布局那样。

在这个阶段，用求解器计算一下结果：

但等等，如果看一看结果的字节，我们就会发现它不仅仅是由字母和数字构成！

是的，我们从来没有限制输入是字母和数字。这个问题很好解决。

最终我们得到了新鲜出炉的shellcode。

用前面一篇文章中的脚本，对shellcode是否正确进行一下验证:

完美！

这不是魔法：这只是一个自解压的桩程序，不依赖数据流和控制流。例如，使用了压缩的桩程序不会只有这么点代码。

目标程序是example/samples/dse_crackme.c，对应的脚本是example/symbol_exec/dse_crackme.py

这个crackme的主要流程是，从文件中加载一个key，然后运行几个测试用例。这些测试用例包括：

最终的目的是输出"OK"。

我们会使用公用的提高覆盖率的策略：

脚本dse_crackme.py是实现这个例子的代码，不过这超出了本文的范围。

正如前面看到的，我们使用了DSE引擎来追踪路径约束，使用的是下面这些熟悉的代码：

在这一步中，进行模拟会导致程序跳转到一个未知的地址，事实上，在具体执行的时候，对__libc_start_main的调用是作为桩程序来使用的（见miasm2/os_dep/linux_stdlib.py）。但要想使DSE工作，还需要把它符号化。

在这里，我们实现了这个程序的一个原始版本。我们使用"_symb"后缀作为命令约定。

我们可以通过add_handler函数把这一函数注册到__libc_start_main的地址中去。（相当于加了一个断点）。

但为了减轻工作量，我们可以使用：

用这行代码，Miasm会使用当前脚本中定义的这个函数，自动为imports进行注册。这和沙盒执行时的机制是一样的。

要继续执行程序，接下来我们需要FILE相关的函数。我们定义了一个SymbolicFile类，它可以使用一个具体的size和nmemb参数对文件进行读取，并返回符号化的byte。

我们也实现了相关的函数：

它们的实现很简单，这里就不介绍了。主要功能就是，读取文件并返回字节，当然，文件大小也是用符号表示。

最后，调用puts来显示"BAD"或"OK"。一旦程序运行到这里，执行就停止了。

要做到这点，并保存最终的结果（BAD或OK），在puts桩程序中，我们需要raise一个exception。

现在，我们可以从程序的开始，到最终的puts，都保持DSE运行.下一步就是产生新的输入了。

当DSEPathConstraint对象可以解出到达新分支的约束时，它的handle_solution函数就会被调用。这个函数接收相关的z3模型以及新的目标作为参数。一个解可以重写这一方法来生成新的解。

我们也可以使用与new_solutions属性中的新的解相关的模型.（见上面）

然后重用目前的策略来生成的新的输入。例如，我们使用代码覆盖的策略来生成新的输入以到达之前没到达过的代码段。

在程序执行到最后时，我们就必须建立与计算出的解（new_solutions的属性值）相对应的文件内容，并保存它们，为之后做准备.

在这一步，我们可以运行文件中的二进制程序，并为每个分支生成新的输入。

我们现在需要做的就是自动探测所有的解。首先，我们需要恢复两次实验之间的状态。

相关的DSE功能是它的快照功能。因为要保存已生成的解-避免为已探测的代码段生成新的解-keep_known_solutions选项设置为true:

所以，我们先建立一个空文件：

现在，只要还有候选输入，我们不断进行下述步骤：

相关代码很简单：

启动这个最终的脚本，得到下列输出：

我们可以观察到上面这些检查点，分别是：

我们可以用已得到的结果来检查结果是否正确：

最终我们得到了正确的结果。

在这里，代码覆盖率的策略已经足够了；但并不总是这样。如果这一最简单的策略不够好，那就使用更强力，当然也更麻烦，的策略，比如说分支和路径覆盖策略。要使用新的策略，只需要修改DSEPathConstraint的produce_solution参数。

边注：对于那些对内部实现感兴趣的人，你可能注意到了，CRC16是基于表实现的。最后，一些待求解的约束如下所示：
@16[table_offset + symbolic_element] == CST
我们可以用z3查找符号，解出这个约束，要做到这点，z3需要知道表的值。

为了达到这一目的，我们可以使用Miasmexpr_range工具来取得可到达的地址区间。如果区间不是太大的话，我们可以在内存内容中添加一个约束给z3（@16[table_offset + 2] == 0x1021等）.

因为地址是用符号保存的，所以这也是可以做到的。因为性能的原因，其它的一些框架没有选择这种方法.要在Miasm中模仿这一过程，寻址过程可以由它们的DSE.handle方法中的具体值来完成。

这篇文章对DSE能完成的工作做了一个大体的介绍。

Miasm的实现方式非常灵活；它可以满足大部人的需要。此外，只需要几行代码，就可以将DSE添加到现有脚本中。事实证明它是一种强大的逆向工具。

相关的脚本：

原文链接：http://www.miasm.re/blog/2017/10/05/playing_with_dynamic_symbolic_execution.html#inversing-a-shellcode-packer

编译：看雪翻译小组 梦野间
校对：看雪翻译小组 lumou

[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课