我们终于可以开始readelf部分的实验了。 在我们开始之前，请修改S2E配置文件，仅启用以下的插件：
-
BaseInstructions
-
HostFiles
-
VMI
-
TranslationBlockCoverage
-
ModuleExecutionDetector
-
ForkLimiter
-
ProcessExecutionDetector
-
LinuxMonitor
我们还必须修改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种情况）。 让我们生成代码覆盖信息：
# The actual disassembler isn't important
s2e coverage basic_block --disassembler=binaryninja readelf_kaitai
这些分支情况发生在哪？
由于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：
# Elf(32|64)_Shdr
section_header:
params:
- id: s2e_state
- id: start_addr
seq:
# sh_name
- id: name_offset
type: u4
# sh_type
- id: type
size: 4
process: s2e_make_symbolic(s2e_state, start_addr, _io.pos, "sh_type")
# ...
我们还必须确保将这两个参数传递给SectionHeader的构造函数。 section头可以在section_headers实例下找到：
# The original section_headers
section_headers:
pos: section_header_offset
repeat: expr
repeat-expr: qty_section_header
size: section_header_entry_size
type: section_header
# Redefined for symbolic execution
section_headers:
pos: section_header_offset
repeat: expr
repeat-expr: qty_section_header
size: section_header_entry_size
type: section_header(s2e_state, start_addr)
注意section_headers被声明为“实例规范”。
这意味着section_headers只能根据需要将要解析section头部的函数编译为一个函数。
因此，我们必须访问section_headers以强制解析它们。
为此，我们必须修改s2e-config.lua中的make_elf_symbolic函数：
function make_symbolic_elf(state, start_addr, buffer)
-- ...
-- This will kick-start the parser. However, now we do care about the final
-- result, because we must access the section headers to force them to be
-- parsed
local elf_file = Elf(state, start_addr, KaitaiStream(ss))
-- This will kick-start the section header parser
_ = elf_file.header.section_headers
end
运行ksc再次重新生成elf.lua。 在我们重新运行S2E之前，我们来看下elf.lua。 特别是在section_headers中的get方法中解析的section头部：
function Elf.EndianElf.property.section_headers:get()
-- ...
for i = 1, self.qty_section_header do
self._raw__m_section_headers[i] = \
self._io:read_bytes(self.section_header_entry_size)
local _io = KaitaiStream(stringstream(self._raw__m_section_headers[i]))
self._m_section_headers[i] = Elf.EndianElf.SectionHeader(self.s2e_state,
self.start_addr,
_io, self,
self._root,
self._is_le)
end
-- ...
end
注意到ksc创建一个局部变量_io，它被传递给SectionHeader构造函数。 这个_io变量包含最终将被转换成SectionHeader对象的原始数据。 不幸的是，这会导致s2e_make_symbolic出现处理规范方面的问题。
