angr 的力量不是来自于它是一个模拟器，而是来自于能够使用我们所谓的符号变量来执行。 与其说变量具有具体的数值，不如说它包含一个符号，实际上只是一个名称。 然后，使用该变量执行算术运算将产生一个运算树（根据编译器理论称为抽象语法树或 AST）。 AST 可以转换为 SMT 求解器（如 z3）的约束，以便提出诸如“给定此操作序列的输出，输入必须是什么？”之类的问题。 在这里，您将学习如何使用 angr 来回答这个问题

使用位向量(Bitvectors)

让我们得到一个虚拟项目和状态，这样我们就可以开始玩数字了。

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

位向量只是一个位序列，用有界整数的语义来解释以进行算术。 让我们做几个。

  1. # 64-bit bitvectors with concrete values 1 and 100
  2. >>> one = state.solver.BVV(1, 64)
  3. >>> one
  4.  <BV64 0x1>
  5. >>> one_hundred = state.solver.BVV(100, 64)
  6. >>> one_hundred
  7.  <BV64 0x64>
  9. # create a 27-bit bitvector with concrete value 9
  10. >>> weird_nine = state.solver.BVV(9, 27)
  11. >>> weird_nine
  12. <BV27 0x9>

如您所见，您可以拥有任何位序列并将它们称为位向量。 你也可以用它们做数学运算：

  1. >>> one + one_hundred
  2. <BV64 0x65>
  4. # You can provide normal python integers and they will be coerced to the appropriate type:
  5. >>> one_hundred + 0x100
  6. <BV64 0x164>
  8. # The semantics of normal wrapping arithmetic apply
  9. >>> one_hundred - one*200
  10. <BV64 0xffffffffffffff9c>

但是，您不能计算one + weird_nine。 对不同长度的位向量执行操作是一种类型错误。 但是，您可以扩展weird_nine 使其具有适当的位数：

  1. >>> weird_nine.zero_extend(64 - 27)
  2. <BV64 0x9>
  3. >>> one + weird_nine.zero_extend(64 - 27)
  4. <BV64 0xa>

zero_extend 将使用给定数量的零位填充左侧的位向量。 您还可以使用 sign_extend 填充最高位的副本，从而在二进制补码有符号整数语义下保留位向量的值。

  1. # Create a bitvector symbol named "x" of length 64 bits
  2. >>> x = state.solver.BVS("x", 64)
  3. >>> x
  4. <BV64 x_9_64>
  5. >>> y = state.solver.BVS("y", 64)
  6. >>> y
  7. <BV64 y_10_64>

x和y 现在是符号变量，它们有点像您在 7 年级代数中学习使用的变量。 请注意，您提供的名称已通过附加一个递增计数器进行了修改，您可以对它们进行任意数量的算术运算，但是您不会得到一个数字，而是会得到一个 AST。

  1. >>> x + one
  2. <BV64 x_9_64 + 0x1>
  4. >>> (x + one) / 2
  5. <BV64 (x_9_64 + 0x1) / 0x2>
  7. >>> x - y
  8. <BV64 x_9_64 - y_10_64>

从技术上讲，x 和 y 甚至one也是 AST——任何位向量都是一棵抽象语法树，即使该树只有一层深。 为了理解这一点，让我们学习如何处理 AST。
每个 AST 都有一个 .op 和一个 .args。 op 是一个命名正在执行的操作的字符串，而 args 是操作作为输入的值。 除非操作是 BVV 或 BVS（或其他一些……），否则参数都是其他 AST，树最终以 BVV 或 BVS 终止。

  1. >>> tree = (x + 1) / (y + 2)
  2. >>> tree
  3. <BV64 (x_9_64 + 0x1) / (y_10_64 + 0x2)>
  4. >>> tree.op
  5. '__floordiv__'
  6. >>> tree.args
  7. (<BV64 x_9_64 + 0x1>, <BV64 y_10_64 + 0x2>)
  8. >>> tree.args[0].op
  9. '__add__'
  10. >>> tree.args[0].args
  11. (<BV64 x_9_64>, <BV64 0x1>)
  12. >>> tree.args[0].args[1].op
  13. 'BVV'
  14. >>> tree.args[0].args[1].args
  15. (1, 64)

从现在开始，我们将使用“bitvector”这个词来指代任何最顶层操作产生一个位向量的 AST。 可以通过 AST 表示其他数据类型，包括浮点数和我们即将看到的布尔值。

符号约束(Symbolic Constraints)

在任何两个类似类型的 AST 之间执行比较操作将产生另一个 AST——不是位向量，而是一个符号布尔值。

  1. >>> x == 1
  2. <Bool x_9_64 == 0x1>
  3. >>> x == one
  4. <Bool x_9_64 == 0x1>
  5. >>> x > 2
  6. <Bool x_9_64 > 0x2>
  7. >>> x + y == one_hundred + 5
  8. <Bool (x_9_64 + y_10_64) == 0x69>
  9. >>> one_hundred > 5
  10. <Bool True>
  11. >>> one_hundred > -5
  12. <Bool False>

您可以从中看到的一个花絮是默认情况下比较是无符号的。 最后一个例子中的-5被强制为<BV64 0xffffffffffffffb>，绝对不小于一百。 如果您希望比较有符号，则可以说 one_hundred.SGT(-5)（即“有符号大于”）。 本章末尾提供了完整的操作列表。
这个片段还说明了关于使用 angr 的一个重要点——你永远不应该直接在 if- 或 while- 语句的条件中使用变量之间的比较，因为答案可能没有具体的真值。 即使有具体的真值，if one > one_hundred 也会引发异常。 相反，您应该使用solver.is_true 和solver.is_false，它们在不执行约束求解的情况下测试具体的真实性/虚假性。

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

约束求解(Constraint Solving)

通过将任何符号布尔值添加为状态的约束，您可以将任何符号布尔值视为关于符号变量有效值的断言。 然后，您可以通过要求对符号表达式求值来查询符号变量的有效值。
以下是一个例子：

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

通过将这些约束添加到状态，我们迫使约束求解器将它们视为必须满足其返回的任何值的断言。 如果您运行此代码，您可能会得到不同的 x 值，但该值肯定会大于 3（因为 y 必须大于 2 且 x 必须大于 y）且小于 10。此外，如果您然后 说state.solver.eval(y)，你会得到一个 y 值，它与你得到的 x 值一致。 如果在两个查询之间不添加任何约束，结果将相互一致。
从这里，很容易看出如何完成我们在本章开头提出的任务 - 找到产生给定输出的输入。

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

请再次注意，此解决方案仅适用于位向量语义。 如果我们在整数域上操作，将没有解决方案！
如果我们添加冲突或矛盾的约束，这样就没有可以分配给满足约束的变量的值，状态变得不可满足或不满足，并且对它的查询将引发异常。 您可以使用 state.satisfiable() 检查状态的可满足性。

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

您还可以计算更复杂的表达式，而不仅仅是单个变量。

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

从中我们可以看出 eval 是一种通用方法，可以将任何位向量转换为 python 原语，同时尊重状态的完整性。 这也是我们使用 eval 将具体位向量转换为 Python 整数的原因！
另请注意，尽管 x 和 y 变量是使用旧状态创建的，但仍可在此新状态中使用。 变量与任何一种状态无关，可以自由存在。

浮点数(Floating point numbers)

z3 支持 IEEE754 浮点数理论，因此 angr 也可以使用它们。 主要区别在于浮点数具有排序而不是宽度。 您可以使用 FPV 和 FPS 创建浮点符号和值。

  1. # fresh state
  2. >>> state = proj.factory.entry_state()
  3. >>> a = state.solver.FPV(3.2, state.solver.fp.FSORT_DOUBLE)
  4. >>> a
  5. <FP64 FPV(3.2, DOUBLE)>
  7. >>> b = state.solver.FPS('b', state.solver.fp.FSORT_DOUBLE)
  8. >>> b
  9. <FP64 FPS('FP_b_0_64', DOUBLE)>
  11. >>> a + b
  12. <FP64 fpAdd('RNE', FPV(3.2, DOUBLE), FPS('FP_b_0_64', DOUBLE))>
  14. >>> a + 4.4
  15. <FP64 FPV(7.6000000000000005, DOUBLE)>
  17. >>> b + 2 < 0
  18. <Bool fpLT(fpAdd('RNE', FPS('FP_b_0_64', DOUBLE), FPV(2.0, DOUBLE)), FPV(0.0, DOUBLE))>

所以这里有一点需要解开——对于初学者来说，漂亮的打印对于浮点数来说并不那么聪明。 但除此之外，大多数操作实际上都有第三个参数，当您使用二元运算符时隐式添加 - 舍入模式。 IEEE754 规范支持多种舍入模式（舍入到最近、舍入到零、舍入到正等），因此 z3 必须支持它们。 如果要为操作指定舍入模式，请显式使用 fp 操作（例如，solver.fpAdd），并将舍入模式（solver.fp.RM_* 之一）作为第一个参数。
约束和求解以相同的方式工作，但 eval 返回一个浮点数：

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

这很好，但有时我们需要能够直接将浮点数表示为位向量。 您可以使用 raw_to_bv 和 raw_to_fp 方法将位向量解释为浮点数，反之亦然：

  1. >>> a.raw_to_bv()
  2. <BV64 0x400999999999999a>
  3. >>> b.raw_to_bv()
  4. <BV64 fpToIEEEBV(FPS('FP_b_0_64', DOUBLE))>
  6. >>> state.solver.BVV(0, 64).raw_to_fp()
  7. <FP64 FPV(0.0, DOUBLE)>
  8. >>> state.solver.BVS('x', 64).raw_to_fp()
  9. <FP64 fpToFP(x_1_64, DOUBLE)>

这些转换保留了位模式，就像将浮点指针转换为 int 指针一样，反之亦然。 但是，如果您想尽可能地保留值，就像将浮点型转换为 int（反之亦然）一样，您可以使用一组不同的方法，val_to_fp 和 val_to_bv。 由于浮点数的浮点性质，这些方法必须将目标值的大小或排序作为参数。

  1. >>> a
  2. <FP64 FPV(3.2, DOUBLE)>
  3. >>> a.val_to_bv(12)
  4. <BV12 0x3>
  5. >>> a.val_to_bv(12).val_to_fp(state.solver.fp.FSORT_FLOAT)
  6. <FP32 FPV(3.0, FLOAT)>

这些方法还可以采用带符号参数，指定源或目标位向量的签名。

更多的求解方法(More Solving Methods)

eval 会给你一个可能的表达式解决方案，但如果你想要几个怎么办？ 如果您想确保解决方案是唯一的怎么办？ 求解器为您提供了几种常见求解模式的方法：

  • solver.eval(expression) 将为您提供给定表达式的一种可能解决方案。
  • solver.eval_one(expression)将为您提供给定表达式的解决方案，如果可能有多个解决方案，则抛出错误。
  • solver.eval_upto(expression, n) 将为您提供最多 n 个给定表达式的解决方案，如果可能少于 n，则返回少于 n。
  • solver.eval_atleast(expression, n) 将为您提供给定表达式的 n 个解决方案，如果可能少于 n，则抛出错误。
  • solver.eval_exact(expression, n) 将为您提供给定表达式的 n 个解决方案，如果少于或多于可能，则抛出错误。
  • solver.min(expression) 将为您提供给定表达式的最小可能解决方案。
  • solver.max(expression) 将为您提供给定表达式的最大可能解决方案。

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

  • extra_constraints 可以作为约束元组传递。

这些约束将在此评估中考虑在内，但不会添加到状态中。

  • cast_to 可以传递一个数据类型来转换结果。

目前，这只能是int 和 bytes，这将导致方法返回底层数据的相应表示。
例如， state.solver.eval(state.solver.BVV(0x41424344, 32), cast_to=bytes) 将返回b'ABCD'。

总结

那是很多！！ 阅读本文后，您应该能够创建和操作位向量、布尔值和浮点值以形成操作树，然后查询附加到状态的约束求解器以获取一组约束下的可能解决方案。 希望此时您已经了解使用 AST 来表示计算的能力，以及约束求解器的能力。