最近我一直在研究S2E中的文件解析器。这通常涉及调用s2ecmd symbfile 文件来使解析器的输入符号化，然后运行S2E来解析通过解析器的不同路径。但是，这是一个比较笨重的做法;它使整个输入文件产生一个非常大的符号化的块，这很快导致了路径爆炸。此外，我们可能只想探索行使特定功能的路径。

那么我们如何在基于文件的程序（如解析器）上实现更有针对性地实现符号执行呢？一种方法是编写一个自定义的S2E插件来处理onSymbolicVariableCreation事件,拦截s2ecmd symbfile文件。然后，您可以编写C++代码来迭代和具体调整符号化的数据内容。这种方法的缺点是显而易见的：编写C++代码是相当耗时且容易出错；它需要知道输入文件的格式;在处理不同的文件类型时还要重写，如何更好的实现呢？

暂时抛开S2E不谈，看看 Kaitai Struct。 Kaitai Struct是开发二进制结构解析器的工具。它提供了一种类似YAML的语言，可以简洁地定义二进制结构。 Kaitai Struct 编译器（ksc）然后根据这个定义生成一个解析器。该解析器可以用多种语言生成，包括C ++，Python和Java。

以下是Kaitai Struct中的ELF文件格式的部分定义（取自格式库)。它由许多描述ELF文件的“属性”（例如magic，abi_version等字段）组成：

强烈建议阅读Kaitai Struct文档以充分利用这篇文章，因为我跳过了大部分细节（主要是因为我自己并不擅长这方面）。 然而，有一个值得一提的功能是“处理规范”。

处理规范允许你以某种方式“处理”属性的自定义函数。 例如，可以对属性进行加密/编码。 处理规范可以在运行时对该属性进行解密/解码。

这与符号执行有关吗？ 假设我们有一个s2e_make_symbolic的文件处理规范，并且通过将此规范应用于特定的属性，我们只会使输入文件的这些部分符号化。 这会使我们更好的控制S2E的状态空间，并可能减少路径爆炸问题。 只需要将S2E和Kaitai Struct结合起来就可以实现！

我们将使用Lua编程语言来组合S2E和Kaitai Struct。使用Lua可以重用现有的组件--S2E包含一个嵌入式的Lua解释器（用于解析S2E配置文件，编写函数/指令注释），而ksc能够就生成Lua解析器。因此，我们可以使用ksc为我们的输入文件生成一个Lua解析器，并将该解析器嵌入到S2E配置文件中，使其可以被S2E访问。 （我们可以使用ksc来生成一个C++解析器，但这样的话，每次我们想要使用不同的文件格式时，都需要重新编译S2E）。通过在输入定义中选择性地应用s2e_make_symbolic处理规范，我们可以实现更有针对性的符号执行。

这篇文章剩余部分将介绍如何组合S2E和Kaitai Struct。我将使用ELF文件的定义（前面讨论过）和readelf来作为一个实例。

为了让其他人更容易地使用代码，我努力使它尽可能的独立。- 没有对S2E的核心引擎或ksc进行任何修改。然而，这意味着代码基本没有优化！代码由以下部件组成：

在客户操作系统中执行的命令行工具（s2e_kaitai_cmd）。这个工具读取输入文件并且调用S2E插件，选择性地使文件符号化;

一个S2E插件（KaitaiStruct），它调用Lua代码来运行由ksc生成的解析器;

一小段Lua代码连接 S2E配置文件和由ksc生成的解析器。

这些部件中的每一个在下面描述。完整的代码在这儿。

在这篇文章的开头,我提到我们通常会使用s2ecmd symbfile 来使输入文件的符号化。 symbfile命令使输入文件符号化：

我们将采取类似的方法，除了我们将步骤（3）修改为：

为此，我们将在S2E环境中添加以下目录/文件：

我会跳过步骤1,2和4，因为它们已经在s2ecmd中实现了。对于步骤3，我们会自己写一个自定义的S2E命令来调用一个插件（稍后描述），有选择地使输入的文件符号化。命令结构应放在source/s2e/guest/common/include/s2e/kaitai/commands.h中。它遵循从客户端调用S2E插件的标准方法：

然后我们可以将下面的函数添加到s2e_kaitai_cmd.c中。 这个函数包含指向文件内容（已经读入缓冲区）的指针和缓冲区的大小（由lseek确定），构造相关命令并将此命令发送到S2E。

现在我们需要一个S2E插件来处理这个命令。

让我们从一个skeleton插件开始（不要忘了在source/s2e/libs2eplugins/src/CMakeLists.txt中向s2e/Plugins/KaitaiStruct.cpp添加add_library命令）。

头文件：

cpp 文件：

我们的插件只有一个依赖关系：LuaBindings插件。这个插件配置了S2E的Lua解释器，并允许我们在S2E配置文件中调用Lua代码。

handleOpcodeInvocation方法遵循和其他插件类似的方法，实现了BaseInstructionsPluginInvokerInterface接口（例如FunctionModels和LinuxMonitor）：

最终实现MakeSymbolic。为了编写Lua代码，需要添加一些头文件：

最终实现的函数：

希望这比较容易理解（参见这里有关Lua语言的C API的更多信息）。首先，我们将输入文件读入Kaitai Struct解析器的Lua字符串。然后，我们调用Kaitai Struct解析器函数（我们将在下一部分中定义）。

我们必须设置解析器函数的参数才能调用它。用栈把值传递给Lua函数。函数名首先入栈。解析器函数在Lua的全局命名空间中定义（为了简单起见），因此我们可以使用lua_getglobal从S2E配置文件中检索该函数，并将其压入栈中。然后依次入栈：

现在要做的就是在S2E配置文件中实现这个解析器。

首先，我们需要将Kaitai Struct格式的定义编译成Lua解析器。既然我们是用readelf做实验，现在让我们创建一个readelf项目，并从Kaitai Struct Gallery获取ELF定义：

这将会产生elf.lua。 让我们用AFL的例子测试下。 如果您还没有安装它，您还需要Kaitai Struct的的Lua runtime：

你应该看到一个52字节大小的header（你可以运行readelf -h small_exec.elf来确认）。

我原先说过我们会用Kaitai Struct的处理规范来定位特定的文件属性来使其符号化。 我们在lua_runtime/s2e_make_symbolic.lua中定义这个处理规范：

目前已经定义了一个新的类S2eMakeSymbolic和一个构造函数(_init)，一个decode方法：
构造器包含以下参数：

当ELF解析器遇到应用s2e_make_symbolic处理规范的属性时，将自动调用decode。 然而，在从输入文件中读取数据之后才调用decode方法，所以使数据符号化（通过减去刚刚读取的存储器区域的大小）时，必须对此进行弥补。

让我们做一些符号化的东西。 我们现在将选择一些简单的部分 - ELF头部的e_machine字段。 在elf.ksy中，e_machine字段在endian_elf类型下定义：

处理规范只能应用于字节数组，所以我们必须用字节数组的size字段来替换type字段。 因为原始数据类型是无符号的双字节数，所以我们可以将该机器简单地视为一个大小为2字节的数组。我们还必须删除枚举映射，否则当它尝试将枚举类型应用到一个字节的数组时，ksc会引发编译错误。

最后，我们必须从解析器的构造函数传递另外两个参数--S2E执行状态和输入文件的起始地址--从解析器的构造器传到s2e_make_symbolic。 我们用“params spec”来实现。 machine属性嵌套在endian_elf和顶级elf类型下，因此下面的参数规范必须被定义。

我们还必须将header的类型从endian_elf修改为endian_elf（s2e_state，start_addr）。 这确保两个参数传递给endian_elf的构造函数。 （如果还有点困惑，看下这里的源代码）。

现在重新编译elf.ksy。 如果打开elf.lua，你应该看到，构造函数（Elf：_init）的前两个参数为s2e_state和start_addr。 这些参数被保存下来，并通过Elf.EndianElf构造函数传播到S2eMakeSymbolic构造函数。

剩下要做的就是在我们的S2E配置文件中写一个小的函数来实例化并运行我们的解析器。 该功能由KaitaiStruct插件中的handleMakeSymbolic方法调用。

完成了!

我们终于可以开始readelf部分的实验了。 在我们开始之前，请修改S2E配置文件，仅启用以下的插件：

我们还必须修改bootstrap.sh。 在${S2EGET} “readelf”下添加$ {S2EGET}“small_exec.elf”以便将测试用例复制到客户机。为了使用我们的测试用例，在prepare_inputs函数中，将truncate -s 256 $ {SYMB_FILE}替换为cp small_exec.elf $ {SYMB_FILE}。 还不用替换symbfile命令; 让我们先来看一下readelf如何在一个完全符号化的文件上执行。

运行S2E一分钟左右，然后结束进程。 你应该看到很多分叉的情况（我这里是136种情况）。 让我们生成代码覆盖信息：

这些分支情况发生在哪？ 由于readelf调用在符号化数据时调用了printf,所以libc中有很多。 readelf 自身的分支呢？ 下面的图片显示了readelf中的两个函数的片段：process_section_headers和init_dwarf_regnames。 绿色的部分表示由S2E执行的块。 分支节点受到的约束已由注释说明（KLEE中的KQuery格式）：

readelf's process_section_headers 代码覆盖

readelf's init_dwarf_regnames 代码覆盖

当检查到下列情况也会发生分叉：

还有许多其他的地方！眼下只对留下那些与ELF头部的e_machine字段有关的程序路径。编辑bootstrap.sh并用./s2e_kaitai_cmd ${SYMB_FILE}替换${S2ECMD} symbfile ${SYMB_FILE}。现在重新运行S2E一分钟。在运行期间，分支情况仅限于get_machine_name和init_dwarf_regnames函数，这两个函数都是取决于e_machine的值的switch语句。成功了！

让我们尝试在ELF文件中换一个不同的字段 -section header 的sh_type字段。不像e_machine字段，只会在ELF文件中出现一次。sh_type可以在整个文件中出现多次（取决于ELF文件中section的数量）。

我们必须将S2E执行状态和输入文件的起始地址传播到ELF声明中的相对应的属性中。这次我们必须将params spec添加到section_header类型中。 type属性定义为无符号的4字节枚举类型，因此我们必须将其更改为4字节的数组类型，以便我们可以使用s2e_make_symbolic：

我们还必须确保将这两个参数传递给SectionHeader的构造函数。 section头可以在section_headers实例下找到：

注意section_headers被声明为“实例规范”。 这意味着section_headers只能根据需要将要解析section头部的函数编译为一个函数。 因此，我们必须访问section_headers以强制解析它们。 为此，我们必须修改s2e-config.lua中的make_elf_symbolic函数：

运行ksc再次重新生成elf.lua。 在我们重新运行S2E之前，我们来看下elf.lua。 特别是在section_headers中的get方法中解析的section头部：

注意到ksc创建一个局部变量_io，它被传递给SectionHeader构造函数。 这个_io变量包含最终将被转换成SectionHeader对象的原始数据。 不幸的是，这会导致s2e_make_symbolic出现处理规范方面的问题。

回想一下，解析器的当前位置（_io.pos）被传递给s2e_make_symbolic处理规范。 但是糟糕的是当创建本地_io流时，这个地址将清零，因此符号化的时候使用这个地址会造成错误的内存地址。 不过，我们可以通过对稍微修改下Lua代码来解决这个问题：

是的，修改生成的Lua代码是令人厌恶的。但是，它确保了符号化时的内存地址是正确的。当我重新编译S2E时，分支被限制在process_section_headers函数中的sh_type比较部分。

在这篇文章中，探讨了如何更有针对性的执行文件解析器的符号执行问题。我们可以使用Kaitai Struct来定位输入文件的特定部分来进行符号化，而非给解析器一个完全符号的输入文件（这会很快导致路径爆炸问题）。这种方法似乎奏效，但还是有些问题。

首先，首先，它依赖于用户有一个有效的样例文件来执行符号执行。
。这个样例文件还必须包含我们希望运行的解析器部分的数据。比如，假设我们想将此技术应用于PNG解析器。如果我们拿这个PNG文件的定义，并希望看到当bkgd_truecolor属性符号化时发生了什么，我们的PNG文件也必须包含一个背景颜色块。否则我们的解析器将没有符号化的东西。

由于类似的原因，我们不能仅仅使用S2E引导脚本创建的“空”的符号文件。为当Kaitai Struct解析器执行时，它运行在文件中的具体数据上。 S2E创建的默认符号文件用NULL字符填充，因此解析器无法解析。如果我们可以凭空创造出文件，是不是会很酷？

其他问题取决于我们如何使用Kaitai Struct。这不是Kaitai Struct的错误;实际上，Kaitai Struct FAQ明确指出，生成的解析器本来就不是为了“基于事件”的解析模型而设计的。我们可以修改ksc来生成基本不需要手动修改的代码（例如，自动生成参数规范，使用非延迟的实例规范，始终跟踪解析器的绝对路径等等），但是为了简单起见不去考虑Kaitai Struct “原本的样子”。

不是基于文件的符号执行怎么办？例如，在我之前的帖子中，我展示了如何使用S2E来解决使用命令行字符串作为输入的CTF挑战。这篇文章中描述的方法对解决这个CTF的挑战是没有帮助的。同样我们可以扩展KaitaiStruct插件来处理命令行字符串。例如，我们可以在Kaitai Struct中定义CTF挑战的输入字符串如下：

加上一些额外的代码，我们可以在输入字符串上的运行此解析器，只将最后63个字节符号化。 这将允许我们从S2E插件中删除onSymbolicVariableCreation方法。

尽管出现了这些问题，但是把S2E和Kaitai
Struct组合起来似乎对我目前正在做的工作（尽管你的目的可能会有所不同）还是很有帮助的。 我们可以通过更多的工作（更多的代码）来解决这些问题。 所以，我想我会把那作为一个未来的帖子:)

2017年10月23日

原文链接
本文由看雪翻译小组fyb波翻译。

[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入！