到目前为止,我们仅以最简单的方式使用了 angr 的模拟程序状态(SimState 对象),以演示有关 angr 操作的基本概念。 在这里,您将了解状态对象的结构以及如何以各种有用的方式与其交互。
复习:读写内存和寄存器
如果您一直在按顺序阅读本书(至少在第一部分应该如此),那么您已经了解了如何访问内存和寄存器的基础知识。 state.regs 通过带有每个寄存器名称的属性提供对寄存器的读写访问,state.mem 提供对内存的类型化读写访问,使用索引访问表示法指定地址,后跟属性访问以指定类型你想解释的内存。
此外,您现在应该知道如何使用 AST,因此您现在可以理解任何位向量类型的 AST 都可以存储在寄存器或内存中。
以下是从状态复制和执行数据操作的一些快速示例:
>>> import angr, claripy>>> proj = angr.Project('/bin/true')>>> state = proj.factory.entry_state()# copy rsp to rbp>>> state.regs.rbp = state.regs.rsp# store rdx to memory at 0x1000>>> state.mem[0x1000].uint64_t = state.regs.rdx# dereference rbp>>> state.regs.rbp = state.mem[state.regs.rbp].uint64_t.resolved# add rax, qword ptr [rsp + 8]>>> state.regs.rax += state.mem[state.regs.rsp + 8].uint64_t.resolved
基本操作(Basic Execution)
早些时候,我们展示了如何使用模拟管理器进行一些基本的执行。 我们将在下一章展示模拟管理器的全部功能,但现在我们可以使用一个更简单的界面来演示符号执行的工作原理:state.step()。 该方法将执行一个符号执行步骤并返回一个名为SimSuccessors的对象。与正常仿真不同,符号执行可以产生多个可按多种方式分类的后继状态。 现在,我们关心的是这个对象的 .successors 属性,它是一个包含给定步骤的所有“正常”后继的列表。
为什么是一个列表,而不是一个单一的后继状态? 好吧,angr 的符号执行过程只是将编译到程序中的各个指令的操作和执行它们以改变 SimState。 当一行代码如 if (x > 4) 到达时,如果 x 是一个符号位向量会发生什么? 在 angr 深处的某个地方,将执行比较 x > 4,结果将是 <Bool x_32_1 > 4>。
那很好,但下一个问题是,我们是选择“真”分支还是“假”分支? 答案是,我们两个都拿! 我们生成两个完全独立的后继状态——一个模拟条件为真的情况,一个模拟条件为假的情况。 在第一个状态中,我们添加 x > 4 作为约束,在第二个状态中,我们添加 !(x > 4) 作为约束。 这样,每当我们使用这些后继状态中的任何一个执行约束求解时,状态上的条件确保我们获得的任何解决方案都是有效的输入,这将导致执行遵循给定状态所遵循的相同路径。
为了描述这个原理,我们用fake firmware image作为一个例子。如果你查看这个二进制的源码,你会看到固件的身份验证机制是后门的;任何用户名都可以通过密码“SOSNEAKY”认证为管理员。 此外,发生的第一个与用户输入的比较是与后门的比较,所以如果我们一步一步直到获得多个后继状态,其中一个状态将包含限制用户输入为后门密码的条件。 以下代码段实现了这一点:
>>> proj = angr.Project('examples/fauxware/fauxware')>>> state = proj.factory.entry_state(stdin=angr.SimFile) # ignore that argument for now - we're disabling a more complicated default setup for the sake of education>>> while True:... succ = state.step()... if len(succ.successors) == 2:... break... state = succ.successors[0]>>> state1, state2 = succ.successors>>> state1<SimState @ 0x400629>>>> state2<SimState @ 0x400699
不要直接看这些状态的约束——我们刚刚经过的分支涉及到strcmp的结果,这是一个很棘手的函数,象征性地模拟,产生的约束非常复杂。
我们模拟的程序从标准输入中获取数据,默认情况下,angr 将其视为无限的符号数据流。 要执行约束求解并获得输入可能采用的值以满足约束,我们需要获得对 stdin 实际内容的引用。 我们稍后将在这个页面上讨论我们的文件和输入子系统如何工作,但现在,只需使用 state.posix.stdin.load(0, state.posix.stdin.size) 来检索表示所有内容的位向量 到目前为止从标准输入读取。
>>> input_data = state1.posix.stdin.load(0, state.posix.stdin.size)>>> state1.solver.eval(input_data, cast_to=bytes)b'\x00\x00\x00\x00\x00\x00\x00\x00\x00SOSNEAKY\x00\x00\x00'>>> state2.solver.eval(input_data, cast_to=bytes)b'\x00\x00\x00\x00\x00\x00\x00\x00\x00S\x00\x80N\x00\x00 \x00\x00\x00\x00'
如您所见,为了沿着 state1 路径前进,您必须将后门字符串“SOSNEAKY”作为密码。 为了沿着 state2 路径走下去,除了“SOSNEAKY”之外,你还必须给出一些东西。 z3 提供了符合此标准的数十亿个字符串中的一个。
Fauxware 是第一个成功运行 angr 符号执行程序的程序,早在 2013 年。通过使用 angr 找到它的后门,您就参与了一个伟大的传统,即对如何使用符号执行从二进制文件中提取含义有一个基本的了解!
状态预设(State Presets)
到目前为止,每当我们处理一个状态时,我们都会使用 project.factory.entry_state() 创建它。 这只是项目工厂中可用的几个状态构造函数之一:
.blank_state()构造一个“空白石板”空白状态,其大部分数据未初始化。.entry_state()构造一个准备在主二进制入口点执行的状态。.full_init_state()构造一个状态,该状态准备通过任何需要在主二进制入口点之前运行的初始化程序执行,例如,共享库构造函数或预初始化程序。
完成这些后,它将跳转到入口点。
.call_state()构造一个准备执行给定函数的状态。
您可以通过这些构造函数的几个参数自定义状态:
- 所有这些构造函数都可以使用
addr参数来指定要开始的确切地址。 - 如果您在可以接受命令行参数或环境的环境中执行,则可以通过
args将参数列表和环境变量字典通过env传递到entry_state和full_init_state。 这些结构中的值可以是字符串或位向量,并将被序列化为状态作为模拟执行的参数和环境。 默认的args是一个空列表,因此如果您正在分析的程序期望找到至少一个argv[0],您应该始终提供它! - 如果您希望
argc是符号的,您可以将符号位向量作为argc传递给entry_state和full_init_state构造函数。 不过要小心:如果你这样做,你还应该向结果状态添加一个约束,即你的 argc 值不能大于你传递给 args 的 args 数量。 - 要使用调用状态,您应该使用
.call_state(addr, arg1, arg2, ...)调用它,其中addr是您要调用的函数的地址,argN 是该函数的第 N 个参数,或者作为 python 整数、字符串或数组,或位向量。 如果你想分配内存并实际传递一个指向对象的指针,你应该将它包装在一个 PointerWrapper 中,即angr.PointerWrapper("point to me!")。 这个 API 的结果可能有点不可预测,但我们正在努力。 - 剩下详情见原文档
内存的低级接口(Low level interface for memory)
state.mem 接口对于从内存加载类型化数据很方便,但是当您想要在内存范围内进行原始加载和存储时,它非常麻烦。 事实证明,state.mem 实际上只是一堆正确访问底层内存存储的逻辑,它只是一个填充了位向量数据的平面地址空间:state.memory。 您可以通过 .load(addr, size) 和 .store(addr, val) 方法直接使用 state.memory:
>>> s = proj.factory.blank_state()>>> s.memory.store(0x4000, s.solver.BVV(0x0123456789abcdef0123456789abcdef, 128))>>> s.memory.load(0x4004, 6) # load-size is in bytes<BV48 0x89abcdef0123>
正如您所看到的,数据以“大端”方式加载和存储,因为 state.memory 的主要目的是加载存储数据,没有附加语义。 但是,如果您想对加载或存储的数据执行字节交换,则可以传递关键字参数 endness - 如果指定 little-endian,则将发生字节交换。 endness 应该是 archinfo 包中 Endness 枚举的成员之一,用于保存有关 angr 的 CPU 架构的声明性数据。 此外,正在分析的程序的结束可以作为 arch.memory_endness 找到 - 例如 state.arch.memory_endness。
>>> import archinfo>>> s.memory.load(0x4000, 4, endness=archinfo.Endness.LE)<BV32 0x67452301>
还有一个用于寄存器访问的低级接口 state.registers,它使用与 state.memory 完全相同的 API,但是解释这个需要深入。简而言之,它只是一个寄存器文件,寄存器和偏移量之间的映射定义在archinfo
状态选项(State Options)
可以对 angr 的内部进行很多小的调整,这些调整将在某些情况下优化行为,而在其他情况下则是不利的。 这些调整是通过状态选项控制的。
在每个 SimState 对象上,都有一组 (state.options) 的所有启用选项。 每个选项(实际上只是一个字符串)都以某种细微的方式控制 angr 执行引擎的行为。 可以在附录找到完整的选项域列表以及不同状态类型的默认值。您可以通过 angr.options 访问用于添加到状态的单个选项。 各个选项以 CAPITAL_LETTERS 命名,但也有一些您可能希望捆绑在一起使用的通用对象分组,以小写字母命名。
通过任何构造函数创建 SimState 时,您可以传递关键字参数 add_options 和 remove_options,它们应该是修改默认设置的初始选项集的选项集。
# Example: enable lazy solves, an option that causes state satisfiability to be checked as infrequently as possible.# This change to the settings will be propagated to all successor states created from this state after this line.>>> s.options.add(angr.options.LAZY_SOLVES)# Create a new state with lazy solves enabled>>> s = proj.factory.entry_state(add_options={angr.options.LAZY_SOLVES})# Create a new state without simplification options enabled>>> s = proj.factory.entry_state(remove_options=angr.options.simplification)
状态插件(State Plugins)
全局插件(The globals plugin)
历史插件(The history plugin)
callstack插件(The callstack plugin)
More about I/O:FIles,file systems, and network sockets
复制和合并(Copying and Merging)
状态支持非常快的复制,因此您可以探索不同的可能性:
>>> proj = angr.Project('/bin/true')>>> s = proj.factory.blank_state()>>> s1 = s.copy()>>> s2 = s.copy()>>> s1.mem[0x1000].uint32_t = 0x41414141>>> s2.mem[0x1000].uint32_t = 0x42424242
状态也可以被合并在一起
# merge will return a tuple. the first element is the merged state# the second element is a symbolic variable describing a state flag# the third element is a boolean describing whether any merging was done>>> (s_merged, m, anything_merged) = s1.merge(s2)# this is now an expression that can resolve to "AAAA" *or* "BBBB">>> aaaa_or_bbbb = s_merged.mem[0x1000].uint32_t
