Angr 学习

参考链接

angr 库 功能

Project

我们若要使用 angr 来分析一个二进制文件，第一步则是创建一个 angr.Project 类——我们一切后续操作都将基于这个类实例进行展开，以下是一个例子：

1
2
3
4
>>> import angr
>>> bin_path = './test' # file to be analyzed
>>> proj = angr.Project(bin_path)
WARNING | 2022-11-23 19:25:30,006 | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.

首先，我们可以通过一个 project 获取对应二进制文件的基本信息：

1
2
3
4
5
6
>>> proj.arch     # architecture of the binary file
<Arch AMD64 (LE)>
>>> hex(proj.entry)    # entry point of the binary file
'0x401060'
>>> proj.filename # name of the binary file
'./test'

  • arch 是一个 archiinfo.Arch 类实例，其包含了运行该文件的 CPU 信息等各种数据：

    • arch.bits & arch.bytes ：CPU 的字长（单位为位/字节）。

    • arch.name：架构名，例如 X86 。

    • arch.memory_endness：端序，大端为 Endness.BE ，小端为 Endness.LE。

      源码里还有一个 “中端序” Endness.ME

factory - 实用类工厂

project.factory 为我们提供了一些实用的类的构造器。

block - 基本块

angr 以基本块为单位分析代码，我们可以通过 project.factory.block(address) 获取给定地址所在的基本块——一个 Block 类实例：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
>>> block = proj.factory.block(proj.entry) # extract the basic block
>>> block.pp() # pretty-print of disassemble code of the block
        _start:
401060  endbr64
401064  xor     ebp, ebp
401066  mov     r9, rdx
401069  pop     rsi
40106a  mov     rdx, rsp
40106d  and     rsp, 0xfffffffffffffff0
401071  push    rax
401072  push    rsp
401073  lea     r8, [__libc_csu_fini]
40107a  lea     rcx, [__libc_csu_init]
401081  lea     rdi, [main]
401088  call    qword ptr [0x403fe0]
>>> block.instructions # instructions in the block
12
>>> block.instruction_addrs # addr of each instruction
(4198496, 4198500, 4198502, 4198505, 4198506, 4198509, 4198513, 4198514, 4198515, 4198522, 4198529, 4198536)
state - 模拟执行状态

angr 使用 SimState 类表示一个 模拟的程序状态 （simulated program state），我们的各种操作实际上是由一个 state 步进到另一个 state 的过程。

我们使用 project.factory.entry_state() 获取一个程序的初始执行状态，

使用 project.factory.blank_state(addr) 获取一个程序从指定地址开始执行的空白状态：

1
2
>>> state = proj.factory.entry_state()
>>> state = proj.factory.blank_state(0xdeadbeef)

  • state.regs：寄存器状态组，其中每个寄存器都为一个 位向量 （BitVector），我们可以通过寄存器名称来访问对应的寄存器（例如 state.regs.esp -= 12 ）。

  • state.mem：该状态的内存访问接口，我们可以直接通过 state.mem[addr].type 完成内存访问（例如 state.mem[0x1000].long = 4 ，对于读而言还需指定 .resolved 或 .concrete 表示位向量或是实际值，例如 state.mem[0x1000].long.concrete）。

  • state.memory：另一种形式的内存访问接口：

    • state.memory.load(addr, size_in_bytes) ：获取该地址上指定大小的位向量。

    • state.memory.store(addr, bitvector) ：将一个位向量存储到指定地址。

      angr 9.2.173 中 view.py 的实现：

      1
      2
      3
      4
      5
      6
      7
      @property
      def resolved(self):
       return self._type.extract(self.state, self._addr)          # 不传 concrete

      @property
      def concrete(self):
       return self._type.extract(self.state, self._addr, True)    # 传 concrete=True

      而 sim_type.py 里的 extract 是：

      1
      2
      3
      4
      5
      6
      7
      8
      def extract(self, state, addr, concrete=False):
       out = state.memory.load(addr, self.size // state.arch.byte_width, endness=...)
       if not concrete:
           return out                        # ← .resolved：直接返回原始位向量
       n = state.solver.eval(out)            # ← .concrete：求解器求一个具体值
       if self.signed and n >= 1 << (self.size - 1):
           n -= 1 << self.size               # 有符号类型做符号扩展处理
       return n

      所以两者读的是同一块内存，区别只在最后一步：resolved 原样返回加载出来的位向量；concrete 多调了一次 state.solver.eval() 把它”求值”成整数。

  • state.posix：POSIX 相关的环境接口，例如 state.posix.dumps(fileno) 获取对应文件描述符上的流。

除了这些对模拟执行状态的信息获取接口外，还有一些解决方法的对应接口 state.solver，我们将在后续章节中进行讲解。

simulation_manager - 模拟执行器

angr 将一个状态的执行方法独立成一个 SimulationManager 类，以下两种写法等效：

1
2
3
4
>>> proj.factory.simgr(state)
<SimulationManager with 1 active>
>>> proj.factory.simulation_manager(state)
<SimulationManager with 1 active>

比较重要的两个条件：

  • simgr.step()：以基本块为单位的单步执行。
  • simgr.explore()：进行路径探索找到满足相应条件的状态。

simgr.explore() 的默认参数是 find，即期望条件，当模拟执行器在路径探索的过程中发现当前状态满足该条件时，该状态会被放到 simgr.found 列表中，若无法找到则该列表为空。

期望条件通常可以是执行到某个地址：

1
2
3
4
5
6
7
8
9
>>> simgr.explore(find=0x80492F0) # explore to a specific address
WARNING  | 2023-07-17 04:04:28,825 | angr.storage.memory_mixins.default_filler_mixin | The program is accessing memory with an unspecified value. This could indicate unwanted behavior.
WARNING  | 2023-07-17 04:04:28,825 | angr.storage.memory_mixins.default_filler_mixin | angr will cope with this by generating an unconstrained symbolic variable and continuing. You can resolve this by:
WARNING  | 2023-07-17 04:04:28,826 | angr.storage.memory_mixins.default_filler_mixin | 1) setting a value to the initial state
WARNING  | 2023-07-17 04:04:28,826 | angr.storage.memory_mixins.default_filler_mixin | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions hold null
WARNING  | 2023-07-17 04:04:28,826 | angr.storage.memory_mixins.default_filler_mixin | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to suppress these messages.
WARNING  | 2023-07-17 04:04:28,826 | angr.storage.memory_mixins.default_filler_mixin | Filling memory at 0x7ffeff60 with 4 unconstrained bytes referenced from 0x819af30 (strcmp+0x0 in libc.so.6 (0x9af30))
WARNING  | 2023-07-17 04:04:28,826 | angr.storage.memory_mixins.default_filler_mixin | Filling memory at 0x7ffeff70 with 12 unconstrained bytes referenced from 0x819af30 (strcmp+0x0 in libc.so.6 (0x9af30))
<SimulationManager with 1 active, 16 deadended, 1 found>

期望条件也可以是自定义的以 状态 为参数的布尔函数。例如，若是我们想要寻找一条输出指定字符串的路径，可以选择通过判断该字符串是否在输出中的方式，我们可以通过 state.posix.dumps(文件描述符) 来获取对应文件描述符上的字符流：

1
2
3
4
5
>>> def foo(state):
...     return b"Good" in state.posix.dumps(1)
... 
>>> simgr.explore(find=foo)
<SimulationManager with 17 deadended, 1 found>

除了 find 参数外，我们也可以指定 avoid 参数——模拟器运行中应当要避开的条件，当一个状态符合这样的条件时，其会被放在 .avoided 列表中并不再往后执行。类似地，**avoid 参数可以是某个地址，也可以是自定义的布尔函数。**

此外，我们还可以通过指定 num_find 参数来指定需要寻找的符合条件的状态的数量，若未指定则会在 .found 列表中存储所有的符合条件的状态。

Claripy

Claripy 是 angr 的求解引擎（solver engine），其内部会无缝混合使用几种后端（concrete bitvectors、SAT solvers 等），对于我们而言一般不需要直接与其进行交互，但通常我们会使用其提供的一些接口

bitvector - 位向量

位向量（bitvector）是 angr 求解引擎中的一个重要部分，其表示了 一组位 （a sequence of bits）。

我们可以通过 claripy.BVV(int_value, size_in_bits) 或 claripy.BVV(string_value) 创建带有具体值（concrete value）的指定长度的位向量值（bitvector value）：

1
2
3
4
5
6
>>> bvv = claripy.BVV(b'arttnba3')
>>> bvv
<BV64 0x617274746e626133>
>>> bvv2 = claripy.BVV(0xdeadbeef, 32)
>>> bvv2
<BV32 0xdeadbeef>

相同长度的位向量可以进行运算，对于不同长度的位向量则可以通过 .zero_extend(extended_bits) 完成位扩展（0填充）后进行运算，需要注意的是位向量的值运算同样存在溢出：

1
2
3
4
5
>>> bvv2 = bvv2.zero_extend(32)
>>> bvv + bvv2
<BV64 0x617274754d102022>
>>> bvv * bvv
<BV64 0x9842ff8e63f3b029>

位向量除了代表具体值（concrete value）的 bitvector value 以外，还有代表符号变量（symbolic variable）的 bitvector symbol，我们可以通过 claripy.BVS(name, size_in_bits) 创建带名字的指定长度的位向量符号（bitvector symbol）：

1
2
3
4
5
6
>>> bvs = claripy.BVS("x", 64)
>>> bvs
<BV64 x_0_64>
>>> bvs2 = claripy.BVS("y", 64)
>>> bvs2
<BV64 y_1_64>

位向量符号与位向量值之间同意可以进行运算，组合成更加复杂的表达式：

1
2
3
>>> bvs3 = (bvs * bvs2 + bvv) / bvs
>>> bvs3
<BV64 (x_0_64 * y_1_64 + 0x617274746e626133) / x_0_64>

我们可以通过 .op 与 .args 获得位向量的运算类型与参数：

1
2
3
4
5
6
7
8
9
10
>>> bvv.op
'BVV'
>>> bvs.op
'BVS'
>>> bvs3.op
'__floordiv__'
>>> bvs3.args
(<BV64 x_0_64 * y_1_64 + 0x617274746e626133>, <BV64 x_0_64>)
>>> bvv.args
(7021802812440994099, 64)

state - 模拟执行状态

状态求解

前面讲到 state.solver 提供了一些基于状态的求解接口，例如 solver 同样有创建位向量的 .BVV() 与 .BVS() 接口。

在需要对位向量符号进行具体值的求解时，我们可以先将位向量符号存放到状态的内存/寄存器中，之后用 simgr 探索到对应的状态后，再使用 state.solver.eval() 成员函数来获取对应位向量在当前状态下的值，以下是一个简单的例子：

1
2
3
4
5
6
7
8
bvs_to_solve = claripy.BVS('bvs_to_solve', 64)
init_state = proj.factory.entry_state()
init_state.memory.store(0xdeadbeef, bvs_to_solve)
simgr = proj.factory.simgr(init_state)
simgr.explore(find = 0xbeefdead)

solver_state = simgr.found[0]
print(solver_state.solver.eval(bvs_to_solve))
内存操作

前面讲到，对于一个状态的内存，我们可以使用 state.memory 的对应接口进行操作：

  • state.memory.load(addr, size_in_bytes) ：获取该地址上指定大小的位向量
  • state.memory.store(addr, bitvector) ：将一个位向量存储到指定地址

需要注意的是如果要储存具体值，则需要通过 endness 参数指定大小端序。

Emulated Filesystem

在 angr 当中与文件系统间的操作是通过 SimFile 对象完成的，SimFile 为对 存储 的抽象模型，一个 SimFile 对象可以表示一系列的字节、符号等。

我们可以通过 angr.SimFile() 来创建一个模拟文件，创建带有具体值与符号变量的 SimFile 例子如下：

1
2
3
4
>>> import angr, claripy
>>> sim_file = angr.SimFile('a_file', content = "flag{F4k3_f1@9!}\n")
>>> bvs = claripy.BVS('bvs', 64)
>>> sim_file2 = angr.SimFile('another_file', bvs, size=8) # size in bytes there

模拟文件需要与特定的状态进行关联，通过 state.fs.insert(sim_file) 或 sim_file.set_state(state) 我们可以将 SimFile 插入到一个状态的文件系统中：

1
>>> state.fs.insert('test_file', sim_file)

我们还可以从文件中读取内容：

1
2
>>> pos = 0
>>> data, actural_read, pos = sim_file.read(pos, 0x100)

对于 流 （Streams，例如标准IO、TCP连接等）类型的文件，我们可以用 angr.SimPackets() 来创建：

1
2
3
>>> sim_packet = angr.SimPackets('my_packet')
>>> sim_packet
<angr.storage.file.SimPackets object at 0x7f75626a2e80>

Constraints

前面我们讲到位向量之间可以进行运算，类似地，位向量之间也可以进行比较运算 ，其结果为 Bool 类型的对象：

1
2
3
4
5
6
7
8
9
10
>>> bvv = claripy.BVV(0xdeadbeef, 32)
>>> bvv2 = claripy.BVV(0xdeadbeef, 32)
>>> bvv == bvv2
<Bool True>
>>> bvs = claripy.BVS('bvs', 32)
>>> bvs == bvv + bvv2
<Bool bvs_0_32 == 0xbd5b7dde>
>>> bvs2 = claripy.BVS('bvs2', 32)
>>> bvs2 > bvs * bvv + bvv2
<Bool bvs2_1_32 > bvs_0_32 * 0xdeadbeef + 0xdeadbeef>

对于带有符号值的比较而言， Bool 类型的对象直接表示了对应的式子，因此可以作为约束条件被添加到一个状态当中，我们可以通过 state.solver.add() 为对应状态添加约束：

1
2
3
>>> state.solver.add(bvs == bvv + bvv2)
>>> state.solver.add(bvs2 > bvs * bvv + bvv2)
>>> state.solver.eval(bvs2) # get the concrete value under constraints

除了 Bool 类以外，Claripy 还提供了一些以位向量作为结果的运算操作，以下是一个例子（完整的还是去读文档吧）：

1
2
>>> claripy.If(bvs == bvs2, bvs, bvs2)
<BV32 if bvs_0_32 == bvs2_1_32 then bvs_0_32 else bvs2_1_32>

Function hook

有的时候我们会有需要 hook 掉某个函数的需求，此时我们可以使用 project.hook(addr = call_insn_addr, hook = my_function, length = n) 来 hook 掉对应的 call 指令：

  • call_insn_addr：被 hook 的 call 指令的地址
  • my_function ：我们的自定义 python 函数
  • length： call 指令的长度

我们的自定义函数应当为接收 state 作为参数的函数，angr 还提供了 decorator 语法糖，因此以下两种写法都可以：

1
2
3
4
5
6
7
8
9
10
11
# method 1
@project.hook(0x1234, length=5)
def my_hook_func(state):
    # do something, this is an example
    state.regs.eax = 0xdeadbeef

# method 2
def my_hook_func2(state):
    # do something, this is an example
    state.regs.eax = 0xdeadbeef
proj.hook(addr = 0x5678, hook = my_hook_func2, length = 5)

Simulated Procedure

在 angr 中 angr.SimProcedure 类用来表示在一个状态上的一个运行过程——即函数实际上是一个 SimPrecedure。

我们可以通过创建一个继承自 angr.SimProcedure 的类并重写 run() 方法的方式来表示一个自定义函数，其中 run() 方法的参数为该函数所接收的参数：

1
2
3
4
class MyProcedure(angr.SimProcedure):
    def run(self, arg1, arg2):
        # do something, this's an example
        return self.state.memory.load(arg1, arg2)

自定义函数过程主要用于对文件中的原有函数进行替换，例如 angr 缺省会用内置的一些 SimProcedure 来替换掉一些库函数。

若我们已经有该二进制文件的符号表，我们可以直接使用 project.hook_symbol(symbol_str, sim_procedure_instance) 来自动 hook 掉文件中所有的对应符号，其中 run() 方法的参数为被替换函数所接收的参数，示例如下：

1
2
3
4
5
6
7
8
9
10
import angr
import claripy

class MyProcedure(angr.SimProcedure):
    def run(self, arg1, arg2):
        # do something, this's an example
        return self.state.memory.load(arg1, arg2)

proj = angr.Project('./test')
proj.hook_symbol('func_to_hook', MyProcedure())

当然，在 SimProcedure 的 run() 过程中我们也可以使用一些有用的成员函数：

  • ret(expr): 函数返回。
  • jump(addr): 跳转到指定地址。
  • exit(code): 终止程序。
  • call(addr, args, continue_at): 调用文件中的函数。
  • inline_call(procedure, *args): 内联地调用另一个 SimProcedure。

stash

在 angr 当中，不同的状态被组织到 simulation manager 的不同的 stash 当中，我们可以按照自己的需求进行步进、过滤、合并、移动等。

stash 类型

在 angr 当中一共有以下几种 stash：

  • simgr.active：活跃的状态列表。在未指定替代的情况下会被模拟器默认执行
  • simgr.deadended：死亡的状态列表。当一个状态无法再被继续执行时（例如没有有效指令、无效的指令指针、不满足其所有的后继（successors））便会被归入该列表
  • simgr.pruned：被剪枝的状态列表。在指定了 LAZY_SOLVES 时，状态仅在必要时检查可满足性，当一个状态在指定了 LAZY_SOLVES 时被发现是不可满足的（unsat），状态层（state hierarchy）将会被遍历以确认在其历史中最初变为不满足的时间，该点及其所有后代都会被 剪枝 （pruned）并放入该列表
  • simgr.unconstrained：不受约束的状态列表。当创建 SimulationManager 时指定了 save_unconstrained=True，则被认为不受约束的（unconstrained，即指令指针被用户数据或其他来源的符号化数据控制）状态会被归入该列表
  • simgr.unsat：不可满足的状态列表。当创建 SimulationManager 时指定了 save_unsat=True，则被认为无法被满足的（unsatisfiable，即存在约束冲突的状态，例如在同一时刻要求输入既是"AAAA" 又是 "BBBB"）状态会被归入该列表

还有一种不是 stash 的状态列表——errored，若在执行中产生了错误，则状态与其产生的错误会被包裹在一个 ErrorRecord 实例中（可通过 record.state 与 record.error 访问），该 record 会被插入到 errored 中，我们可以通过 record.debug() 启动一个调试窗口

stash 操作

我们可以使用 stash.move() 来在 stash 之间转移放置状态，用法如下：

1
>>> simgr.move(from_stash = 'unconstrained', to_stash = 'active')

在转移当中我们还可以通过指定 filter_func 参数来进行过滤：

1
2
3
4
>>> def filter_func(state):
...     return b'arttnba3' in state.posix.dumps(1)
...
>>> simgr.move(from_stash = 'unconstrained', to_stash = 'active', filter_func = filter_func)

stash 本质上就是个 list，因此在初始化时我们可以通过字典的方式指定每个 stash 的初始内容：

1
2
3
4
5
>>> simgr = proj.factory.simgr(init_state,
...     stashes = {
...             'active':[init_state],
...             'found':[],
...     })

符号执行

符号执行（symbolic execution）是一种程序分析技术，用于同时探索程序的多个执行路径。与使用特定输入运行程序的普通执行不同，符号执行将输入视为符号变量而非具体值。这意味着执行可以用符号表达式来表示一大类输入。符号执行可以在模拟执行的任意时刻，确定某个分支采取或不采取所需满足的全部条件。每个变量都被表示为一个符号值，每个分支都被表示为一条约束。因此，通过求解这些约束，符号执行让我们能够看到哪些条件允许程序从 A 点到达 B 点。随后，通过求解这些符号表达式生成的约束来分析执行路径，从而发现常规测试中可能遗漏的 bug 和漏洞。

示例：

考虑下面这个简单的程序：

1
2
3
4
5
6
7
const char* check_value(int x) {
    if (x > 10) {
        return "Greater";
    } else {
        return "Lesser or Equal";
    }
}

在普通执行中，如果 x 被设置为 5，程序将沿着 x <= 10 的路径执行并返回“Lesser or Equal”。而在符号执行中，x 被视为一个符号变量 X。执行引擎会探索两条路径：

  • 路径 1：X > 10，结果为“Greater”
  • 路径 2：X <= 10，结果为“Lesser or Equal”

两条路径的约束都会被生成并求解，以了解程序所有可能的行为。

在软件验证中，它有助于确保代码在所有可能的输入和状态下都符合预期行为。在安全分析中，符号执行可以揭示诸如输入验证错误之类的漏洞，这些漏洞可能被攻击者利用。此外，在自动化测试中，它有助于生成全面的测试用例，覆盖边界情况和罕见执行路径，从而增强软件系统的健壮性和安全性。总而言之，符号执行提供了一种强大的手段，用于严谨地分析和改进软件及固件的可靠性。

基本执行

现在让我们看一个使用 angr 进行符号执行的示例。考虑下面的示例代码：

1
2
3
4
5
6
7
8
9
void helloWorld() {
    printf("Hello, World!\n");
}


void firstCall(uint32_t num) {
    if (num > 50 && num <100)
        HelloWorld();
}

firstCall 函数接受一个 32 位数字作为输入，如果该数字介于 50 和 100 之间，就会调用 helloWorld 函数。

你可以使用下面的示例代码进行符号执行，用 angr 找到一个正确有效的输入，使其到达最终的 helloWorld 函数调用。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
import angr, claripy
# Load the binary
project = angr.Project('./3func', auto_load_libs=False)

# Define the address of the firstCall function
firstCall_addr = project.loader.main_object.get_symbol("firstCall")

# Define the address of the helloWorld function
helloWorld_addr = project.loader.main_object.get_symbol("helloWorld")
# Create a symbolic variable for the firstCall arg
input_arg = claripy.BVS('input_arg', 32)

# Create a blank state at the address of the firstCall function
init_state = project.factory.blank_state(addr=firstCall_addr.rebased_addr)

# Assuming the calling convention passes the argument in a register
# (e.g., x86 uses edi for the argument)
init_state.regs.edi = input_arg

# Create a simulation manager
simgr = project.factory.simulation_manager(init_state)

# Explore the binary, looking for the address of helloWorld
simgr.explore(find=helloWorld_addr.rebased_addr)

# Check if we found a state that reached the target
if simgr.found:
    input_value = simgr.found[0].solver.eval(input_arg)
    print(f"Value of input_arg that reaches HelloWorld: {input_value}")
    # Get the constraints for reaching the helloWorld function
    constraints = simgr.found[0].solver.constraints
    # Create a solver with the constraints
    solver = claripy.Solver()
    solver.add(constraints)
    min_val = solver.min(input_arg)
    max_val = solver.max(input_arg)
    print(f"Function arg: min = {min_val}, max = {max_val}")
else:
    print("Did not find a state that reaches HelloWorld.")

它将产生如下输出，其中包含一个可以到达 helloWorld 函数的有效示例函数参数，你可以将其用作测试用例。

1
2
Value of input_arg that reaches HelloWorld: 71
Function arg: min = 51, max = 99

加载二进制

之前，你只是浅尝辄止地接触了 angr 的加载功能——你加载了 /bin/true，然后又在不加载共享库的情况下加载了一次。你还见到了 proj.loader 以及它能做的一些事情。现在，我们将深入探讨这些接口的细节以及它们能告诉你的信息。

我们之前简要提到过 angr 的二进制加载组件 CLE。CLE 是 “CLE Loads Everything”（”CLE 加载一切”）的缩写，它负责接收一个二进制文件（以及它所依赖的任何库），并以一种易于使用的方式将其呈现给 angr 的其余部分。

加载器

让我们加载 examples/fauxware/fauxware，更深入地看看如何与加载器交互。

1
2
3
>>> import angr, monkeyhex
>>> proj = angr.Project('examples/fauxware/fauxware')
>>> proj.loader

已加载的对象

CLE 加载器（cle.Loader）表示所有已加载的二进制对象的整体，这些对象被加载并映射到同一个内存空间中。每个二进制对象都由一个能够处理其文件类型的加载器后端（cle.Backend 的子类）加载。例如，cle.ELF 用于加载 ELF 二进制。

内存中还会有一些不对应任何已加载二进制的对象。例如，一个用于提供线程局部存储支持的对象，以及一个用于提供未解析符号的 externs 对象。

你可以用 loader.all_objects 获取 CLE 已加载对象的完整列表，以及几个更有针对性的分类：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
# All loaded objects
>>> proj.loader.all_objects
[,
 ,
 ,
 ,
 ,
 ]

# This is the "main" object, the one that you directly specified when loading the project
>>> proj.loader.main_object


# This is a dictionary mapping from shared object name to object
>>> proj.loader.shared_objects
{ 'fauxware': ,
  'libc.so.6': ,
  'ld-linux-x86-64.so.2':  }

# Here's all the objects that were loaded from ELF files
# If this were a windows program we'd use all_pe_objects!
>>> proj.loader.all_elf_objects
[,
 ,
 ]

# Here's the "externs object", which we use to provide addresses for unresolved imports and angr internals
>>> proj.loader.extern_object


# This object is used to provide addresses for emulated syscalls
>>> proj.loader.kernel_object


# Finally, you can to get a reference to an object given an address in it
>>> proj.loader.find_object_containing(0x400000)

你可以直接与这些对象交互，从中提取元数据：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
>>> obj = proj.loader.main_object

# The entry point of the object
>>> obj.entry
0x400580

>>> obj.min_addr, obj.max_addr
(0x400000, 0x60105f)

# Retrieve this ELF's segments and sections
>>> obj.segments
,
           ]>
>>> obj.sections
,
           <.interp | offset 0x238, vaddr 0x400238, size 0x1c>,
           <.note.ABI-tag | offset 0x254, vaddr 0x400254, size 0x20>,
            ...etc

# You can get an individual segment or section by an address it contains:
>>> obj.find_segment_containing(obj.entry)

>>> obj.find_section_containing(obj.entry)
<.text | offset 0x580, vaddr 0x400580, size 0x338>

# Get the address of the PLT stub for a symbol
>>> addr = obj.plt['strcmp']
>>> addr
0x400550
>>> obj.reverse_plt[addr]
'strcmp'

# Show the prelinked base of the object and the location it was actually mapped into memory by CLE
>>> obj.linked_base
0x400000
>>> obj.mapped_base
0x400000

符号与重定位

使用 CLE 时，你还可以处理符号。符号是可执行文件格式世界中的一个基本概念，本质上就是将名称映射到地址。

从 CLE 获取符号最简单的方法是使用 loader.find_symbol，它接受一个名称或一个地址，并返回一个 Symbol 对象。

1
2
>>> strcmp = proj.loader.find_symbol('strcmp')
>>> strcmp

符号最有用的属性是它的名称、所有者（owner）和地址，但符号的”地址”可能有些含糊。Symbol 对象有三种报告其地址的方式：

  • .rebased_addr 是它在全局地址空间中的地址。这也是打印输出中显示的内容。
  • .linked_addr 是它相对于二进制预链接基址的地址。例如，这就是 readelf(1) 中报告的地址。
  • .relative_addr 是它相对于对象基址的地址。这在文献中（尤其是 Windows 相关文献中）被称为 RVA（相对虚拟地址，relative virtual address）。
1
2
3
4
5
6
7
8
9
10
11
12
>>> strcmp.name
'strcmp'

>>> strcmp.owner


>>> strcmp.rebased_addr
0x1089cd0
>>> strcmp.linked_addr
0x89cd0
>>> strcmp.relative_addr
0x89cd0

除了提供调试信息之外，符号还支持动态链接的概念。libc 将 strcmp 符号作为导出提供，而主二进制依赖它。如果我们让 CLE 直接从主对象中取出 strcmp 符号，它会告诉我们这是一个导入符号。导入符号没有与之关联的有意义的地址，但它们确实提供了对用于解析它们的符号的引用，即 .resolvedby。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
>>> strcmp.is_export
True
>>> strcmp.is_import
False

# On Loader, the method is find_symbol because it performs a search operation to find the symbol.
# On an individual object, the method is get_symbol because there can only be one symbol with a given name.
>>> main_strcmp = proj.loader.main_object.get_symbol('strcmp')
>>> main_strcmp

>>> main_strcmp.is_export
False
>>> main_strcmp.is_import
True
>>> main_strcmp.resolvedby

导入与导出之间的链接在内存中的具体注册方式由另一个称为重定位的概念处理。重定位的意思是：”当你把 [import] 与一个导出符号匹配上时，请把导出的地址写入 *[location]*，格式为 *[format]*。”我们可以通过 obj.relocs 查看一个对象的完整重定位列表（以 Relocation 实例的形式），或者通过 obj.imports 查看从符号名到 Relocation 的映射。没有对应的导出符号列表。

重定位对应的导入符号可以通过 .symbol 访问。重定位将要写入的地址可以通过任何你能用于 Symbol 的地址标识符来访问，你也可以通过 .owner 获取请求该重定位的对象的引用。

1
2
3
4
5
6
7
8
9
# Relocations don't have a good pretty-printing, so those addresses are Python-internal, unrelated to our program
>>> proj.loader.shared_objects['libc.so.6'].imports
{'__libc_enable_secure': ,
 '__tls_get_addr': ,
 '_dl_argv': ,
 '_dl_find_dso_for_object': ,
 '_dl_starting_up': ,
 '_rtld_global': ,
 '_rtld_global_ro': }

如果一个导入无法解析到任何导出，例如因为找不到某个共享库，CLE 会自动更新 externs 对象（loader.extern_obj），声明它将该符号作为导出提供。

加载选项

如果你用 angr.Project 加载某个东西，并想向 Project 隐式创建的 cle.Loader 实例传递一个选项，你可以直接把关键字参数传给 Project 构造器，它会原样传递给 CLE。如果你想了解所有可以传入的选项，应该查看 CLE API 文档，但这里我们会介绍一些重要且常用的选项。

基本选项

我们已经讨论过 auto_load_libs——它启用或禁用 CLE 自动解析共享库依赖的尝试，默认关闭。此外，还有一个与之相反的 except_missing_libs，如果设置为 true，每当二进制存在无法解析的共享库依赖时，就会抛出异常。

你可以向 force_load_libs 传入一个字符串列表，其中列出的任何内容都会从一开始就被当作未解析的共享库依赖；或者你可以向 skip_libs 传入一个字符串列表，防止任何具有该名称的库被解析为依赖。此外，你还可以向 ld_path 传入一个字符串列表（或单个字符串），它将作为共享库的附加搜索路径，优先于所有默认路径：加载程序所在的目录、当前工作目录和系统库目录。

逐二进制选项

如果你想指定一些只适用于特定二进制对象的选项，CLE 也允许你这样做。参数 main_opts 和 lib_opts 通过接受选项字典来实现这一点。main_opts 是从选项名到选项值的映射，而 lib_opts 是从库名到选项字典的映射，每个选项字典又将选项名映射到选项值。

可以使用的选项因后端而异，但一些常见的选项有：

  • backend —— 使用哪个后端，可以是类或名称
  • base_addr —— 要使用的基地址
  • entry_point —— 要使用的入口点
  • arch —— 要使用的架构名称

示例：

1
>>> angr.Project('examples/fauxware/fauxware', main_opts={'backend': 'blob', 'arch': 'i386'}, lib_opts={'libc.so.6': {'backend': 'elf'}})

后端

CLE 目前拥有用于静态加载 ELF、PE、CGC、Mach-O 和 ELF 核心转储文件的后端，以及将文件加载到平坦地址空间的后端。在大多数情况下，CLE 会自动检测要使用的正确后端，因此除非你在做一些相当特殊的事情，否则不需要指定使用哪个后端。

如上所述，你可以通过在对象的选项字典中加入一个键来强制 CLE 为该对象使用特定后端。有些后端无法自动检测要使用的架构，必须指定 arch。该键不需要与任何架构列表匹配；只要给出任何受支持架构的几乎任何常见标识符，angr 就能识别你指的是哪个架构。

要引用后端，请使用下表中的名称：

后端名称 描述 需要 arch？
elf 基于 PyELFTools 的 ELF 文件静态加载器 否
pe 基于 PEFile 的 PE 文件静态加载器 否
mach-o Mach-O 文件的静态加载器。不支持动态链接或重基址（rebasing）。 否
cgc Cyber Grand Challenge 二进制的静态加载器 否
backedcgc 允许指定内存和寄存器 backer 的 CGC 二进制静态加载器 否
elfcore ELF 核心转储的静态加载器 否
blob 将文件作为平坦镜像加载到内存中 是

符号函数摘要

默认情况下，Project 会尝试使用称为 SimProcedure 的符号摘要来替换对库函数的外部调用——它们本质上只是模仿库函数对状态影响的 Python 函数。我们已经将一大批函数实现为 SimProcedure。这些内置过程可以在 angr.SIM_PROCEDURES 字典中找到，该字典是两级的：先按包名（libc、posix、win32、stubs）作为键，再按库函数名作为键。执行 SimProcedure 而不是从你的系统中加载的实际库函数，会使分析容易得多，代价是可能产生一些不准确。

当某个函数没有可用的此类摘要时：

  • 如果 auto_load_libs 为 True，则改为执行真实的库函数。这是否是你想要的，取决于具体的函数。例如，libc 的某些函数分析起来极其复杂，很可能会导致试图执行它们的路径的状态数量爆炸。
  • 如果 auto_load_libs 为 False（这是默认值），则外部函数保持未解析状态，Project 会将它们解析为一个通用的 “stub”（桩）SimProcedure，名为 ReturnUnconstrained。它的行为正如其名：每次被调用时返回一个唯一的无约束符号值。
  • 如果 use_sim_procedures（这是 angr.Project 的参数，不是 cle.Loader 的）为 False（默认为 True），那么只有 extern 对象提供的符号才会被替换为 SimProcedure，并且它们会被替换为一个除返回符号值外什么都不做的桩 ReturnUnconstrained。
  • 你可以使用 angr.Project 的参数 exclude_sim_procedures_list 和 exclude_sim_procedures_func，指定要从被替换为 SimProcedure 的符号中排除的特定符号。
  • 有关确切算法，请查看 angr.Project._register_object 的代码。

挂钩

angr 用 Python 摘要替换库代码的机制称为挂钩（hooking），你也可以这样做！在执行模拟时，angr 会在每一步检查当前地址是否已被挂钩，如果是，就运行该挂钩而不是该地址处的二进制代码。实现这一点的 API 是 proj.hook(addr, hook)，其中 hook 是一个 SimProcedure 实例。你可以用 .is_hooked、.unhook 和 .hooked_by 来管理项目中的挂钩，这些方法应该不需要解释。

还有一个用于挂钩地址的替代 API，它允许你通过将 proj.hook(addr) 用作函数装饰器，来指定自己的临时函数作为挂钩。如果这样做，你还可以选择指定 length 关键字参数，使执行在挂钩完成后向前跳过一定数量的字节。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
>>> stub_func = angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'] # this is a CLASS
>>> proj.hook(0x10000, stub_func())  # hook with an instance of the class

>>> proj.is_hooked(0x10000)            # these functions should be pretty self-explanitory
True
>>> proj.hooked_by(0x10000)

>>> proj.unhook(0x10000)

>>> @proj.hook(0x20000, length=5)
... def my_hook(state):
...     state.regs.rax = 1

>>> proj.is_hooked(0x20000)
True

此外，你可以使用 proj.hook_symbol(name, hook)，以符号名作为第一个参数，来挂钩该符号所在的地址。这方面一个非常重要的用途是扩展 angr 内置库 SimProcedure 的行为。由于这些库函数只是类，你可以对它们进行子类化，覆盖部分行为，然后在挂钩中使用你的子类。

机器状态 —— 内存、寄存器等等

到目前为止，我们只是以最基础的方式使用了 angr 的模拟程序状态（SimState 对象）来演示 angr 运行的基本概念。在这里，你将了解状态对象的结构，以及如何以各种有用的方式与之交互。

回顾：读写内存与寄存器

如果你一直在按顺序阅读本书（至少第一部分应该如此），你已经了解了访问内存和寄存器的基础知识。state.regs 通过以各寄存器命名的属性提供对寄存器的读写访问；而 state.mem 则提供对内存的带类型读写访问，使用下标访问表示法指定地址，再通过属性访问指定你希望将内存解释为的类型。

此外，你现在应该已经掌握了 AST 的使用方法，因此可以理解：任何位向量类型的 AST 都可以存储到寄存器或内存中。

下面是一些从状态中复制数据并对其执行运算的快速示例：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
>>> 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

基本执行

前面我们展示了如何使用 Simulation Manager 进行一些基本执行。我们将在下一章展示 simulation manager 的全部功能，但就目前而言，我们可以使用一个更简单的接口来演示符号执行的工作原理：state.step()。该方法会执行一步符号执行，并返回一个名为 angr.engines.successors.SimSuccessors 的对象。与普通的模拟不同，符号执行可以产生多个后继状态，这些状态可以按多种方式分类。现在，我们关心的是该对象的 .successors 属性，它是一个列表，包含某一步的所有”正常”后继状态。

为什么是一个列表，而不是仅仅一个后继状态？因为 angr 的符号执行过程，就是把编译进程序里的各条指令的操作取出来执行，从而改变一个 SimState。当执行到类似 if (x > 4) 这样的代码时，如果 x 是一个符号位向量，会发生什么？在 angr 深处的某个地方，x > 4 这个比较会被执行，其结果是一个 4>。

这没问题，但接下来的问题是：我们走”真”分支还是”假”分支？答案是：两个都走！我们会生成两个完全独立的后继状态——一个模拟条件为真的情况，另一个模拟条件为假的情况。在第一个状态中，我们添加 x > 4 作为约束；在第二个状态中，我们添加 !(x > 4) 作为约束。这样一来，无论我们用哪个后继状态进行约束求解，该状态上的条件都能确保我们得到的任何解都是有效输入，这些输入会使执行沿着该状态所走过的同一条路径前进。

为了演示这一点，让我们以一个假的固件镜像 <../examples/fauxware/fauxware> 为例。如果你查看这个二进制的源代码 <../examples/fauxware/fauxware.c>，就会发现该固件的认证机制留有后门：任何用户名只要使用密码 “SOSNEAKY” 就能以管理员身份通过认证。此外，程序对用户输入进行的第一个比较就是与后门密码的比较，因此如果我们逐步执行直到出现多个后继状态，其中一个状态就会包含将用户输入约束为后门密码的条件。下面的代码片段实现了这一点：

1
2
3
4
5
6
7
8
9
10
11
12
>>> 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

>>> state2

不要直接查看这些状态上的约束——我们刚刚经过的分支涉及 strcmp 的结果，这是一个难以进行符号模拟的函数，其产生的约束非常复杂。

我们模拟的这个程序从标准输入读取数据，而 angr 默认将标准输入视为一个无穷的符号数据流。为了进行约束求解，得到一个能够满足约束的、输入可能取的值，我们需要获取 stdin 实际内容的引用。稍后我们就会在本页介绍文件和输入子系统的工作方式，但现在只需使用 state.posix.stdin.load(0, state.posix.stdin.size) 来获取一个表示迄今为止从 stdin 读入的所有内容的位向量。

1
2
3
4
5
6
7
>>> input_data = state1.posix.stdin.load(0, state1.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 找出它的后门，你正在参与一项伟大的传统——建立起对如何使用符号执行从二进制中提取含义的基本理解！

状态预设

到目前为止，每当我们使用状态时，都是用 project.factory.entry_state() 创建的。这只是 project factory 上可用的几个状态构造器之一：

  • .blank_state() 构造一个”白纸一张”的空白状态，其大部分数据保持未初始化。访问未初始化的数据时，会返回一个无约束的符号值。
  • .entry_state() 构造一个准备从主二进制的入口点开始执行的状态。
  • .full_init_state() 构造一个准备依次执行主二进制入口点之前需要运行的所有初始化器的状态，例如共享库构造函数或预初始化器。执行完这些之后，它会跳转到入口点。
  • .call_state() 构造一个准备执行给定函数的状态。

你可以通过这些构造器的若干参数来定制状态：

  • 所有这些构造器都可以接受 addr 参数来指定确切的起始地址。
  • 如果你执行的环境可以接受命令行参数或环境变量，你可以通过 args 向 entry_state 和 full_init_state 传入参数列表，通过 env 传入环境变量字典。这些结构中的值可以是字符串或位向量，它们会被序列化到状态中，作为模拟执行的参数和环境。默认的 args 是空列表，因此如果你分析的程序期望至少有一个 argv[0]，你应该始终提供它！
  • 如果你希望 argc 是符号化的，可以向 entry_state 和 full_init_state 构造器传入一个符号位向量作为 argc。不过要小心：如果这样做，你还应该给生成的状态添加一个约束，即 argc 的值不能大于你传入 args 的参数个数。
  • 要使用调用状态，你应该用 .call_state(addr, arg1, arg2, ...) 来调用它，其中 addr 是你想调用的函数的地址，argN 是该函数的第 N 个参数，可以是 Python 整数、字符串、数组或位向量。如果你希望分配内存并真正传入指向某个对象的指针，应该用 PointerWrapper 把它包装起来，例如 angr.PointerWrapper("point to me!")。这个 API 的结果有时有点不可预测，但我们正在改进。
  • 要为 call_state 指定函数使用的调用约定，你可以传入一个 SimCC 实例作为 cc 参数。我们会尽量选择一个合理的默认值，但在特殊情况下你需要帮 angr 一把。

这些构造器中还可以使用更多选项！更多细节请参见 project.factory 对象（一个 angr.factory.AngrObjectFactory）的文档。

内存的低层接口

state.mem 接口便于从内存中加载带类型的数据，但当你想要对一段内存区域进行原始的加载和存储时，它就非常笨拙了。实际上，state.mem 只是一堆用于正确访问底层内存存储的逻辑，而该存储只是一个填满位向量数据的平坦地址空间：state.memory。你可以直接使用 state.memory，配合 .load(addr, size) 和 .store(addr, val) 方法：

1
2
3
>>> s = proj.factory.blank_state()
>>> s.memory.store(0x4000, claripy.BVV(0x0123456789abcdef0123456789abcdef, 128))
>>> s.memory.load(0x4004, 6) # load-size is in bytes

如你所见，数据的加载和存储是”大端”方式的，因为 state.memory 的主要用途就是加载和存储不带附加语义的数据块。不过，如果你想对加载或存储的数据进行字节交换，可以传入关键字参数 endness——如果你指定小端，就会发生字节交换。endness 应该是 archinfo 包中 Endness 枚举的成员之一（archinfo 包保存着 angr 所用的、关于 CPU 架构的声明性数据）。此外，被分析程序的端序可以通过 arch.memory_endness 获取——例如 state.arch.memory_endness。

1
2
>>> import archinfo
>>> s.memory.load(0x4000, 4, endness=archinfo.Endness.LE)

还有一个用于寄存器访问的低层接口 state.registers，它使用与 state.memory 完全相同的 API，但要解释它的行为，需要深入了解 angr 用来无缝支持多种架构的抽象。简而言之，它就是一个寄存器文件，寄存器与偏移量之间的映射在 archinfo 中定义。

状态插件

除了刚才讨论的选项集合之外，SimState 中存储的所有内容实际上都存储在附加到状态上的插件中。到目前为止我们讨论过的状态上的几乎所有属性都是插件——memory、registers、mem、regs、solver 等等。这种设计既保证了代码的模块化，也使得为模拟状态的其他方面轻松实现新的数据存储类型或提供插件的替代实现成为可能。

例如，普通的 memory 插件模拟一个平坦的内存空间，但分析可以选择启用”抽象内存”插件，该插件使用备选的地址数据类型来模拟与地址无关的自由浮动内存映射，从而提供 state.memory。反过来，插件也能降低代码复杂度：state.memory 和 state.registers 实际上是同一个插件的两个不同实例，因为寄存器也是用地址空间来模拟的。

globals 插件

state.globals 是一个极其简单的插件：它实现了标准 Python dict 的接口，允许你在状态上存储任意数据。

history 插件

state.history 是一个非常重要的插件，它存储状态在执行过程中所走路径的历史数据。它实际上是由多个历史节点组成的链表，每个节点代表一轮执行——你可以用 state.history.parent.parent 等来遍历这个链表。

为了更方便地使用这种结构，history 还提供了一些高效的迭代器，用于遍历某些值的历史。一般来说，这些值以 history.recent_NAME 的形式存储，而对应的迭代器就是 history.NAME。例如，for addr in state.history.bbl_addrs: print hex(addr) 会打印出该二进制的基本块地址轨迹；而 state.history.recent_bbl_addrs 是最近一步执行的基本块列表，state.history.parent.recent_bbl_addrs 是上一步执行的基本块列表，依此类推。如果你需要快速获得这些值的扁平列表，可以访问 .hardcopy，例如 state.history.bbl_addrs.hardcopy。不过请记住，迭代器上实现了基于索引的访问。

下面是 history 中存储的一些值的简要列表：

  • history.descriptions 是在该状态上执行的每一轮执行的字符串描述列表。
  • history.bbl_addrs 是该状态执行过的基本块地址列表。每轮执行可能对应多个地址，而且并非所有地址都对应二进制代码——有些可能是挂钩了 SimProcedure 的地址。
  • history.jumpkinds 是该状态历史中每个控制流转移的处理方式的列表，以 VEX 枚举字符串表示。
  • history.jump_guards 是该状态遇到的每个分支的守卫条件列表。
  • history.events 是执行过程中发生的”有趣事件”的语义列表，例如出现符号跳转条件、程序弹出消息框，或执行以某个退出码终止。
  • history.actions 通常为空，但如果你向状态添加 angr.options.refs 选项，它就会被填充为程序执行过的所有内存、寄存器和临时值访问的日志。

callstack 插件

angr 会为模拟的程序跟踪调用栈。每执行一条 call 指令，就会在跟踪的调用栈顶部压入一个栈帧；每当栈指针下降到低于最顶层栈帧被调用的位置时，就会弹出一个栈帧。这使得 angr 能够稳健地存储当前模拟函数的局部数据。

与 history 类似，callstack 也是一个节点链表，但没有提供遍历节点内容的迭代器——相反，你可以直接迭代 state.callstack 来获取每个活动栈帧的调用栈帧，顺序从最近到最旧。如果你只想要最顶层的栈帧，它就是 state.callstack。

  • callstack.func_addr 是当前正在执行的函数的地址
  • callstack.call_site_addr 是调用当前函数的基本块的地址
  • callstack.stack_ptr 是当前函数开始时的栈指针值
  • callstack.ret_addr 是当前函数返回时将返回到的位置

更多关于 I/O：文件、文件系统与网络套接字

关于 angr 中 I/O 建模的更完整、更详细的文档，请参阅使用文件系统、套接字和管道。

复制与合并

状态支持非常快速的复制，这样你就可以探索不同的可能性：

1
2
3
4
5
6
7
>>> 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

状态也可以合并在一起。

1
2
3
4
5
6
7
# 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

模拟管理器

angr 中最重要的控制接口是模拟管理器（SimulationManager），它允许你同时对一组状态执行符号执行，并应用搜索策略来探索程序的状态空间。本章将介绍如何使用它。

模拟管理器让你能够以灵活的方式同时处理多个状态。状态被组织在“stash（暂存区）”中，你可以随意对它们进行前向步进、过滤、合并和移动。例如，你可以让两个不同 stash 中的状态以不同的速率步进，然后再将它们合并到一起。大多数操作的默认 stash 是 active stash，当你初始化一个新的模拟管理器时，状态会被放入其中。

步进

模拟管理器最基本的能力是让指定 stash 中的所有状态前进一个基本块，方法是调用 .step()。

1
2
3
4
5
6
7
8
9
10
>>> import angr
>>> proj = angr.Project('examples/fauxware/fauxware', auto_load_libs=False)
>>> state = proj.factory.entry_state()
>>> simgr = proj.factory.simgr(state)
>>> simgr.active
[]

>>> simgr.step()
>>> simgr.active
[]

当然，stash 模型的真正威力在于：当一个状态遇到符号分支条件时，两个后继状态都会出现在 stash 中，你可以同步地对它们进行步进。当你不想精细地控制分析过程、只想一路步进到无路可走时，直接使用 .run() 方法即可。

1
2
3
4
5
6
7
8
9
10
11
12
# Step until the first symbolic branch
>>> while len(simgr.active) == 1:
...    simgr.step()

>>> simgr

>>> simgr.active
[, ]

# Step until everything terminates
>>> simgr.run()
>>> simgr

现在我们有 3 个 deadended（死路）状态！当一个状态在执行过程中无法产生任何后继时——例如它执行到了 exit 系统调用——它会被从 active stash 中移除，并放入 deadended stash。

Stash 管理

让我们看看如何使用其他 stash。

要在 stash 之间移动状态，请使用 .move() 方法，它接受 from_stash、to_stash 和 filter_func 参数（filter_func 可选，默认移动所有状态）。例如，让我们把所有输出中包含某个特定字符串的状态移动出来：

1
2
>>> simgr.move(from_stash='deadended', to_stash='authenticated', filter_func=lambda s: b'Welcome' in s.posix.dumps(1))
>>> simgr

仅仅通过要求把状态移动到名为“authenticated”的 stash，我们就创建了它。这个 stash 中的所有状态的 stdout 中都包含“Welcome”字符串，目前这算是一个不错的判定标准。

每个 stash 本质上就是一个列表，你可以通过索引或遍历列表来访问其中的每个状态，但也有一些其他的访问方式。如果在 stash 名称前加上 one_ 前缀，你将获得该 stash 中的第一个状态；如果在 stash 名称前加上 mp_ 前缀，你将获得该 stash 的 mulpyplexed 多路并行版本。

1
2
3
4
5
6
7
8
9
10
11
12
13
>>> for s in simgr.deadended + simgr.authenticated:
...     print(hex(s.addr))
0x1000030
0x1000078
0x1000078

>>> simgr.one_deadended

>>> simgr.mp_authenticated
MP([, ])
>>> simgr.mp_authenticated.posix.dumps(0)
MP(['\x00\x00\x00\x00\x00\x00\x00\x00\x00SOSNEAKY\x00',
    '\x00\x00\x00\x00\x00\x00\x00\x00\x00S\x80\x80\x80\x80@\x80@\x00'])

当然，step、run 以及任何其他针对单个状态 stash 进行操作的方法，都可以接受一个 stash 参数，用于指定要操作哪个 stash。

模拟管理器还提供了许多用于管理 stash 的有趣工具。这里我们不再逐一介绍，但你应该查看 API 文档。

Stash 类型

你可以按自己的需要随意使用 stash，但有几种 stash 专门用于归类一些特殊类型的状态，它们是：

Stash 描述
active 该 stash 包含默认会被步进的状态，除非指定了其他 stash。
deadended 当状态因某种原因无法继续执行时——包括没有更多有效指令、所有后继状态都不可满足（unsat），或指令指针无效——该状态会被放入 deadended stash。
pruned 使用 LAZY_SOLVES 时，状态不会在非必要时检查可满足性。当在启用 LAZY_SOLVES 的情况下发现某个状态不可满足（unsat）时，会遍历状态层级结构，找出它在历史中最初变为不可满足的时间点。该点之后的所有后代状态（它们也必然不可满足，因为状态不可能从不可满足重新变回可满足）都会被剪除并放入此 stash。
unconstrained 如果向 SimulationManager 构造函数提供了 save_unconstrained 选项，那么被判定为无约束的状态（即指令指针受用户数据或其他符号数据源控制的状态）会被放入此 stash。
unsat 如果向 SimulationManager 构造函数提供了 save_unsat 选项，那么被判定为不可满足的状态（即约束相互矛盾的状态，例如要求输入同时既为“AAAA”又为“BBBB”）会被放入此 stash。

还有一个不属于 stash 的状态列表：errored。如果在执行过程中抛出错误，该状态会被封装进一个 ErrorRecord 对象——该对象包含状态本身以及它所抛出的错误——随后这个记录会被插入 errored。你可以通过 record.state 获取导致错误的那次执行步进开始时的状态，通过 record.error 查看抛出的错误，通过 record.debug() 在错误发生处启动一个调试 shell。这是一个非常有价值的调试工具！

简单探索

符号执行中一个极其常见的操作是：找到一个到达某个地址的状态，同时丢弃所有经过另一个地址的状态。模拟管理器为这种模式提供了一个快捷方式——.explore() 方法。

使用 find 参数调用 .explore() 时，执行会一直进行，直到找到一个匹配 find 条件的状态。find 条件可以是需要停下的指令地址、地址列表，或者一个接受状态并返回其是否满足某些条件的函数。当 active stash 中的任意状态匹配 find 条件时，它们会被放入 found stash，执行随即终止。之后你可以继续探索找到的状态，也可以决定丢弃它并继续处理其余状态。你还可以用与 find 相同的格式指定 avoid 条件：当状态匹配 avoid 条件时，它会被放入 avoided stash，执行继续。最后，num_find 参数控制返回之前应找到的状态数量，默认值为 1。当然，如果在找到这么多解之前 active stash 中的状态就用尽了，执行同样会停止。

让我们来看一个简单的 crackme 示例：

首先，加载二进制文件。

1
>>> proj = angr.Project('examples/CSCI-4968-MBE/challenges/crackme0x00a/crackme0x00a')

接下来，创建一个 SimulationManager。

1
>>> simgr = proj.factory.simgr()

现在，我们进行符号执行，直到找到一个符合条件（即“获胜”条件）的状态。

1
>>> simgr.explore(find=lambda s: b"Congrats" in s.posix.dumps(1))

现在，我们可以从那个状态中取出 flag！

1
2
3
4
5
6
7
>>> s = simgr.found[0]
>>> print(s.posix.dumps(1))
Enter password: Congrats!

>>> flag = s.posix.dumps(0)
>>> print(flag)
g00dJ0B!

很简单，不是吗？

更多示例可以通过浏览 示例 找到。

核心要点回顾：

  1. stash = 带名字的 SimState 列表，全部存在 simgr.stashes 这个字典里；
  2. 内置 7 个盒子：active（默认步进对象）、deadended（死路）、unsat（矛盾）、pruned（剪枝）、unconstrained（IP 失控）、stashed（临时搁置）、errored（严格说是独立的 ErrorRecord 列表，不是 stash）；
  3. step() 自动分类：无后继 → deadended，符号分支 → 多个后继都回 active；
  4. move()/stash()/drop()/split()/merge() 手动搬运，目标盒子不存在就自动创建——stash 名是自由的标签；
  5. explore(find=...) 是 CTF 解 flag 的核心套路：命中条件的状态自动进 found，取 simgr.found[0] 提取输入；
  6. one_ / mp_ 前缀让你便捷地取单个状态或批量操作整个盒子。

符号表达式与约束求解

angr 的强大之处不在于它是个模拟器，而在于它能够使用我们所说的符号变量来执行程序。与其说某个变量具有一个具体的数值，不如说它保存着一个符号——本质上只是一个名字。然后，用该变量进行算术运算会得到一棵操作树（编译器理论中称为抽象语法树，即 AST）。AST 可以被转换为SMT 求解器（如 z3）的约束，从而回答诸如“给定这串操作的输出，输入必须是什么？”这样的问题。本章将介绍如何使用 angr 来回答这类问题。

使用位向量

先创建一个临时项目和状态，这样我们就可以开始摆弄数字了。

1
2
3
>>> import angr, monkeyhex
>>> proj = angr.Project('/bin/true')
>>> state = proj.factory.entry_state()

位向量（bitvector）本质上就是一串比特，在算术运算中按照有界整数的语义来解释。让我们创建几个。

1
2
3
4
5
6
7
8
9
10
11
# 64-bit bitvectors with concrete values 1 and 100
>>> one = claripy.BVV(1, 64)
>>> one
 
>>> one_hundred =claripy.BVV(100, 64)
>>> one_hundred
 

# create a 27-bit bitvector with concrete value 9
>>> weird_nine = claripy.BVV(9, 27)
>>> weird_nine

如你所见，任意一串比特都可以被称为位向量，你还可以对它们进行数学运算：

1
2
3
4
5
6
7
8
>>> one + one_hundred


# You can provide normal Python integers and they will be coerced to the
appropriate type: >>> one_hundred + 0x100 

# The semantics of normal wrapping arithmetic apply
>>> one_hundred - one*200

但你不能写 one + weird_nine。对不同长度的位向量进行运算是类型错误。不过，你可以扩展 weird_nine，让它具有合适的比特数：

1
2
3
>>> weird_nine.zero_extend(64 - 27)

>>> one + weird_nine.zero_extend(64 - 27)

zero_extend 会在位向量的左侧填充指定数量的零比特。你还可以使用 sign_extend，用最高位的副本进行填充，从而在二进制补码有符号整数的语义下保持位向量的值不变。

现在，让我们引入一些符号。

1
2
3
4
5
6
# Create a bitvector symbol named "x" of length 64 bits
>>> x = claripy.BVS("x", 64)
>>> x

>>> y = claripy.BVS("y", 64)
>>> y

x 和 y 现在都是符号变量，有点像你在七年级代数课上学过的变量。请注意，你提供的名字会通过追加一个递增计数器的方式被改写（mangle）。你可以对它们进行任意多的算术运算，但得到的不是数字，而是 AST。

1
2
3
4
5
6
7
>>> x + one


>>> (x + one) / 2


>>> x - y

严格来说，x、y 甚至 one 也都是 AST——任何位向量都是一棵操作树，即使这棵树只有一层。为了理解这一点，让我们学习如何处理 AST。

每个 AST 都有 .op 和 .args。op 是一个字符串，指明所执行的操作；args 是该操作作为输入接收的值。除非 op 是 BVV 或 BVS（或者其他少数几种），否则 args 全部都是其他 AST，这棵树最终以 BVV 或 BVS 终止。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
>>> tree = (x + 1) / (y + 2)
>>> tree

>>> tree.op
'__floordiv__'
>>> tree.args
(, )
>>> tree.args[0].op
'__add__'
>>> tree.args[0].args
(, )
>>> tree.args[0].args[1].op
'BVV'
>>> tree.args[0].args[1].args
(1, 64)

从现在开始，我们用“位向量”一词来指代任何顶层操作产生位向量的 AST。AST 还可以表示其他数据类型，包括浮点数，以及我们马上就会看到的布尔值。

符号约束

对任意两个类型相似的 AST 进行比较运算会得到另一个 AST——它不再是位向量，而是一个符号布尔值。

1
2
3
4
5
6
7
8
9
10
11
>>> x == 1

>>> x == one

>>> x > 2
 0x2>
>>> x + y == one_hundred + 5

>>> one_hundred > 5

>>> one_hundred > -5

从这个小例子中可以看出，比较默认是无符号的。最后一个例子中的 -5 被强制转换为一个很大的无符号数，它显然不小于一百。如果你想进行有符号比较，可以写 one_hundred.SGT(-5)（即“有符号大于”）。完整的操作列表可以在本章末尾找到。

这段代码还说明了使用 angr 时的一个重要注意事项——绝不要直接在 if 或 while 语句的条件中使用变量之间的比较，因为结果可能没有确定性的真值。即使结果有确定性的真值，if one > one_hundred 也会抛出异常。相反，你应该使用 solver.is_true 和 solver.is_false，它们可以在不进行约束求解的情况下测试确定性的真/假。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
>>> yes = one == 1
>>> no = one == 2
>>> maybe = x == y
>>> state.solver.is_true(yes)
True
>>> state.solver.is_false(yes)
False
>>> state.solver.is_true(no)
False
>>> state.solver.is_false(no)
True
>>> state.solver.is_true(maybe)
False
>>> state.solver.is_false(maybe)
False

约束求解

你可以把任何符号布尔值作为关于符号变量合法取值的断言，通过将它作为约束添加到状态中。然后，你可以通过请求对符号表达式求值来查询符号变量的合法取值。

这里一个例子可能比解释更清楚：

1
2
3
4
5
>>> state.solver.add(x > y)
>>> state.solver.add(y > 2)
>>> state.solver.add(10 > x)
>>> state.solver.eval(x)
4

通过向状态添加这些约束，我们强制约束求解器把它们视为对其返回的任何取值都必须满足的断言。如果你运行这段代码，得到的 x 值可能不同，但该值一定大于 3（因为 y 必须大于 2，而 x 必须大于 y）且小于 10。此外，如果你接着调用 state.solver.eval(y)，得到的 y 值会与你得到的 x 值保持一致。如果两次查询之间没有添加任何约束，结果将彼此一致。

至此，很容易看出如何完成本章开头提出的任务——找出产生给定输出的输入。

1
2
3
4
5
6
7
8
# get a fresh state without constraints
>>> state = proj.factory.entry_state()
>>> input = claripy.BVS('input', 64)
>>> operation = (((input + 4) * 3) >> 1) + input
>>> output = 200
>>> state.solver.add(operation == output)
>>> state.solver.eval(input)
0x3333333333333381

注意，再说一次，这个解之所以成立，完全是因为位向量的语义。如果我们在整数域上运算，这个方程将无解！

如果我们添加相互冲突或矛盾的约束，使得不存在任何变量赋值能满足这些约束，那么状态就会变成不可满足的（unsatisfiable，简称 unsat），对它的查询将抛出异常。你可以用 state.satisfiable() 检查状态的可满足性。

1
2
3
>>> state.solver.add(input < 2**32)
>>> state.satisfiable()
False

你还可以对更复杂的表达式求值，而不只是单个变量。

1
2
3
4
5
6
7
8
9
10
# fresh state
>>> state = proj.factory.entry_state()
>>> state.solver.add(x - y >= 4)
>>> state.solver.add(y > 0)
>>> state.solver.eval(x)
5
>>> state.solver.eval(y)
1
>>> state.solver.eval(x + y)
6

由此我们可以看出，eval 是一个通用方法，可以在保证状态一致性的前提下，把任意位向量转换为 Python 基本类型。这也是我们用 eval 把具体位向量转换为 Python 整数的原因！

还要注意，x 和 y 虽然是在旧状态下创建的，却可以在新状态中使用。变量不绑定于任何特定状态，可以自由存在。

浮点数

z3 支持 IEEE754 浮点数的理论，因此 angr 也可以使用它们。主要区别在于，浮点数没有宽度（width），而是有一个种类（sort）。你可以使用 FPV 和 FPS 创建浮点数值和浮点符号。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
# fresh state
>>> state = proj.factory.entry_state()
>>> a = claripy.FPV(3.2, claripy.fp.FSORT_DOUBLE)
>>> a


>>> b = claripy.FPS('b', claripy.fp.FSORT_DOUBLE)
>>> b


>>> a + b


>>> a + 4.4


>>> b + 2 < 0

这里有几处需要说明——首先，浮点数的美化打印（pretty-printing）没那么智能。除此之外，大多数运算实际上还有第三个参数——舍入模式（rounding mode）——在使用二元运算符时会隐式添加。IEEE754 规范支持多种舍入模式（就近舍入、向零舍入、向正无穷舍入等），因此 z3 也必须支持它们。如果你想为某个运算指定舍入模式，请显式使用 fp 运算（例如 claripy.fpAdd），并把舍入模式（claripy.fp.RM_* 之一）作为第一个参数。

约束和求解的工作方式与此相同，只不过 eval 会返回浮点数：

1
2
3
4
>>> state.solver.add(b + 2 < 0)
>>> state.solver.add(b + 2 > -1)
>>> state.solver.eval(b)
-2.4999999999999996

这很不错，但有时我们需要直接以位向量的形式操作浮点数的表示。你可以使用 raw_to_bv 和 raw_to_fp 方法在位向量与浮点数之间相互转换：

1
2
3
4
5
6
7
8
>>> a.raw_to_bv()

>>> b.raw_to_bv()


>>> claripy.BVV(0, 64).raw_to_fp()

>>> claripy.BVS('x', 64).raw_to_fp()

这些转换保持比特模式不变，就像把浮点指针强制转换为整型指针（或反过来）一样。不过，如果你想尽可能保持数值不变——就像把浮点数强制转换为整数（或反过来）——可以使用另一组方法 val_to_fp 和 val_to_bv。由于浮点数的本质特性，这些方法必须以目标值的大小（size）或种类（sort）作为参数。

1
2
3
4
5
>>> a

>>> a.val_to_bv(12)

>>> a.val_to_bv(12).val_to_fp(claripy.fp.FSORT_FLOAT)

这些方法还可以接受一个 signed 参数，用于指定源或目标位向量的有符号性。

更多求解方法

eval 会给出表达式的一个可能解，但如果你想要多个解呢？如果你想要确保解是唯一的呢？求解器为常见的求解模式提供了几个方法：

  • solver.eval(expression) 会给出给定表达式的一个可能解。
  • solver.eval_one(expression) 会给出给定表达式的解，如果可能存在多个解，则抛出错误。
  • solver.eval_upto(expression, n) 会给出给定表达式最多 n 个解，如果可能的解少于 n 个，则返回较少数量。
  • solver.eval_atleast(expression, n) 会给出给定表达式的 n 个解，如果可能的解少于 n 个，则抛出错误。
  • solver.eval_exact(expression, n) 会给出给定表达式的恰好 n 个解，如果可能的解多于或少于 n 个，则抛出错误。
  • solver.min(expression) 会给出给定表达式的最小可能解。
  • solver.max(expression) 会给出给定表达式的最大可能解。

此外，所有这些方法都可以接受以下关键字参数：

  • extra_constraints 可以传入一个约束元组。这些约束会在本次求值中被考虑，但不会添加到状态中。
  • cast_to 可以传入一个数据类型，用于将结果强制转换。目前仅支持 int 和 bytes，这会使方法返回底层数据对应的表示形式。例如，state.solver.eval(claripy.BVV(0x41424344, 32), cast_to=bytes) 将返回 b'ABCD'。

完整运行日志

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
==============================================================================
【使用位向量】
==============================================================================
>>> import angr, monkeyhex  # 等价：import angr + 内联 monkeyhex 显示层
>>> proj = angr.Project('/bin/true')
>>> state = proj.factory.entry_state()
>>> # 64-bit bitvectors with concrete values 1 and 100
>>> one = claripy.BVV(1, 64)
>>> one
<BV64 0x1>
>>> one_hundred = claripy.BVV(100, 64)
>>> one_hundred
<BV64 0x64>
>>> # create a 27-bit bitvector with concrete value 9
>>> weird_nine = claripy.BVV(9, 27)
>>> weird_nine
<BV27 0x9>
>>> one + one_hundred
<BV64 0x65>
>>> one_hundred + 0x100
<BV64 0x164>
>>> one_hundred - one*200
<BV64 0xffffffffffffff9c>
    # 64 位无符号环绕：100 - 200 = -100 (mod 2^64)

>>> # 对不同长度的位向量做运算是类型错误（文档：但你不能写 one + weird_nine）
    !!! ClaripyOperationError: args' length must all be equal
>>> weird_nine.zero_extend(64 - 27)
<BV64 0x9>
>>> one + weird_nine.zero_extend(64 - 27)
<BV64 0xa>
>>> x = claripy.BVS('x', 64)
>>> x
<BV64 x_45_64>
>>> y = claripy.BVS('y', 64)
>>> y
<BV64 y_46_64>
    # 名字被追加递增计数器改写（mangle）：这里 x_45_64 的 45 是全局符号计数器，与文档里的 x_0_64 不同，因为加载 /bin/true 及其共享库时 angr 内部创建了大量符号。
>>> x + one
<BV64 x_45_64 + 0x1>
>>> (x + one) / 2
<BV64 (x_45_64 + 0x1) / 0x2>
>>> x - y
<BV64 x_45_64 - y_46_64>
>>> tree = (x + 1) / (y + 2)
>>> tree
<BV64 (x_45_64 + 0x1) / (y_46_64 + 0x2)>
>>> tree.op
'__floordiv__'
>>> tree.args
(<BV64 x_45_64 + 0x1>, <BV64 y_46_64 + 0x2>)
>>> tree.args[0].op
'__add__'
>>> tree.args[0].args
(<BV64 x_45_64>, <BV64 0x1>)
>>> tree.args[0].args[1].op
'BVV'
>>> tree.args[0].args[1].args
(0x1, 0x40)
    # monkeyhex 风格显示十六进制；十进制为 (1, 64)
    # 注意：tree.op 恰为文档所写的 '__floordiv__'（`/` 在本版本会发一条'Use BV.__floordiv__ instead of BV.__truediv__' 弃用警告，但 op 仍是 '__floordiv__'）：
>>> tree2 = (x + 1) // (y + 2)
>>> tree2.op
'__floordiv__'

==============================================================================
【符号约束】
==============================================================================
>>> x == 1
<Bool x_45_64 == 0x1>
>>> x == one
<Bool x_45_64 == 0x1>
>>> x > 2
<Bool x_45_64 > 0x2>
>>> x + y == one_hundred + 5
<Bool x_45_64 + y_46_64 == 0x69>
>>> one_hundred > 5
<Bool True>
>>> one_hundred > -5
<Bool False>
    # -5 被强制转换为很大的无符号数，100 当然不小于它（比较默认无符号）
>>> one_hundred.SGT(-5)
<Bool True>
    # SGT = 有符号大于（signed greater than）

>>> # 绝不要直接在 if/while 条件里用变量之间的比较（即使结果确定也会抛异常）
    !!! ClaripyOperationError: testing Expressions for truthiness does not do what you want, as these expressions can be symbolic
>>> yes = one == 1
>>> no = one == 2
>>> maybe = x == y
>>> state.solver.is_true(yes)
True
>>> state.solver.is_false(yes)
False
>>> state.solver.is_true(no)
False
>>> state.solver.is_false(no)
True
>>> state.solver.is_true(maybe)
False
>>> state.solver.is_false(maybe)
False

==============================================================================
【约束求解】
==============================================================================
>>> state.solver.add(x > y)
>>> state.solver.add(y > 2)
>>> state.solver.add(10 > x)
>>> state.solver.eval(x)
0x5
    # 文档中为 4；任何取值都满足 x > y > 2 且 x < 10
>>> state.solver.eval(y)
0x4
    # 与上一步取自同一约束集，结果互相一致（y < x）

>>> # 找出产生给定输出的输入（本章开头的任务）
>>> state = proj.factory.entry_state()  # 全新状态，无约束
>>> input = claripy.BVS('input', 64)
>>> operation = (((input + 4) * 3) >> 1) + input
>>> output = 200
>>> state.solver.add(operation == output)
>>> state.solver.eval(input)
0x3333333333333381
    # 文档中为 0x3333333333333381；实际值随求解器选择而异，但必然很大（见下一行）
    # 这个解成立完全是因为位向量环绕语义；若在整数域上运算，该方程无解。
>>> state.solver.add(input < 2**32)
>>> state.satisfiable()
False
    # 无解则状态不可满足 → False

>>> # 对更复杂的表达式求值
>>> state = proj.factory.entry_state()  # 全新状态
>>> state.solver.add(x - y >= 4)
>>> state.solver.add(y > 0)
>>> state.solver.eval(x)
0x3
>>> state.solver.eval(y)
0xffffffffffffffff
>>> state.solver.eval(x + y)
0x2
    # eval 是通用方法：在保证状态一致性的前提下把任意位向量转成 Python 整数。x、y 虽是旧状态创建的，却不绑定任何状态，可在新状态中自由使用。

==============================================================================
【浮点数】
==============================================================================
>>> state = proj.factory.entry_state()  # 全新状态
>>> a = claripy.FPV(3.2, claripy.fp.FSORT_DOUBLE)
>>> a
<FP64 FPV(3.2, DOUBLE)>
>>> b = claripy.FPS('b', claripy.fp.FSORT_DOUBLE)
>>> b
<FP64 FPS(FP_b_48_64, DOUBLE)>
>>> a + b
<FP64 fpAdd(RM.RM_NearestTiesEven, FPV(3.2, DOUBLE), FPS(FP_b_48_64, DOUBLE))>
>>> a + 4.4
<FP64 FPV(7.6000000000000005, DOUBLE)>
>>> b + 2 < 0
<Bool fpLT(fpAdd(RM.RM_NearestTiesEven, FPS(FP_b_48_64, DOUBLE), FPV(2.0, DOUBLE)), FPV(0.0, DOUBLE))>
    # 浮点数没有宽度(width)，而是有种类(sort)：DOUBLE 等。二元运算隐式带上舍入模式参数（这里显示 RM_NearestTiesEven）。
>>> state.solver.add(b + 2 < 0)
>>> state.solver.add(b + 2 > -1)
>>> state.solver.eval(b)
-2.000001348172201
    # 约束给出 b ∈ (-3, -2)，文档中为 -2.4999999999999996
>>> a.raw_to_bv()
<BV64 0x400999999999999a>
    # 保持比特模式不变（把 double 当 64 位整数看）
>>> b.raw_to_bv()
<BV64 fpToIEEEBV(FPS(FP_b_48_64, DOUBLE))>
>>> claripy.BVV(0, 64).raw_to_fp()
<FP64 FPV(0.0, DOUBLE)>
>>> claripy.BVS('x', 64).raw_to_fp()
<FP64 fpToFP(x_49_64, DOUBLE)>
>>> a.val_to_bv(12)
<BV12 0x3>
    # 按数值转换（3.2 → 3），需指定目标位宽
>>> a.val_to_bv(12).val_to_fp(claripy.fp.FSORT_FLOAT)
<FP32 FPV(3.0, FLOAT)>
    # 再转回浮点（这里是单精度 FLOAT）

==============================================================================
【更多求解方法】（文档列出、无具体示例，此处补演示）
==============================================================================
>>> state = proj.factory.entry_state()  # 全新状态
>>> state.solver.add(x > 2)
>>> state.solver.add(x < 10)
>>> state.solver.eval(x)
0x8
    # eval：一个可能解
>>> state.solver.eval_upto(x, 3)
[0x8, 0x3, 0x9]
    # eval_upto：最多 n 个解
>>> state.solver.eval_atleast(x, 3)
[0x8, 0x3, 0x9]
    # eval_atleast：至少 n 个解
>>> state.solver.eval_exact(x, 7)
[0x6, 0x5, 0x8, 0x4, 0x7, 0x3, 0x9]
    # eval_exact：恰好 n 个解（x∈[3,9] 恰 7 个）
>>> state.solver.eval_one(x)   # 多个解时抛异常
    !!! SimValueError: Concretized 2 values (must be exactly 1) in eval_exact
>>> state.solver.min(x)
0x3
>>> state.solver.max(x)
0x9
>>> state.solver.eval(x, extra_constraints=(x < 5,))
0x3
    # extra_constraints：本次求值临时生效，不加入状态
>>> state.solver.eval(claripy.BVV(0x41424344, 32), cast_to=bytes)
b'ABCD'
    # cast_to=bytes：返回底层字节