angr-doc 3: Solver Engine

求解引擎 Solver Engine

angr的能力不仅体现在它是一个模拟器上,也体现在它能够使用被称为符号变量的方式执行。我们可以说一个变量拥有一个符号,这个符号只要一个名字就能生效,而不是说一个变量拥有一个确实的数值。然后对符号变量执行算术操作就产生了由操作构成的树(在编译原理中它的术语是语法抽象树或者AST)。AST可以被翻译成能被一个SMT求解器,比如z3,接受的约束条件,从而能够提出像“如果给定了这个操作序列的输出,那它的输入应该是什么?”这样的问题。在这里,你会学到如何使用angr回答这样的问题。


使用位向量

让我们随便找一个项目和状态来开始玩这些数字。

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

一个位向量只是一个位的序列,为了算数操作在语义上被翻译成一个有边界的整数。让我们创建几个。

# 64-bit bitvectors with concrete values 1 and 100
>>> one = state.solver.BVV(1, 64)
>>> one
 <BV64 0x1>
>>> one_hundred = state.solver.BVV(100, 64)
>>> one_hundred
 <BV64 0x64>

# create a 27-bit bitvector with concrete value 9
>>> weird_nine = state.solver.BVV(9, 27)
>>> weird_nine
<BV27 0x9>

正如你看到的那样,你可以创建任意的位序列并把它叫做位向量。你还可以使用它们进行算数。

>>> one + one_hundred
<BV64 0x65>

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

# The semantics of normal wrapping arithmetic apply
>>> one_hundred - one*200
<BV64 0xffffffffffffff9c>

但是,你不能进行one + weird_nine。对不同长度的位向量执行操作会引发类型错误。但是你可以扩展weird_nine的长度以使其拥有正确长度的位:

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

zero_extend会在位向量的左边填充给定数字的零。你也可以使用sign_extend最高位的比特拷贝来填充,以保留补码表示的带符号整数的语义值。

现在,让我们带入一些符号。

# Create a bitvector symbol named "x" of length 64 bits
>>> x = state.solver.BVS("x", 64)
>>> x
<BV64 x_9_64>
>>> y = state.solver.BVS("y", 64)
>>> y
<BV64 y_10_64>

xy现在成为了符号变量,它们有点像你在七年级代数中学习的变量。你会注意到你提供的名字的后面附带了一个递增的计数器,并且你可以使用它们做你想做的任何计算,但是你不会得到一个数值,而是一个AST。

>>> x + one
<BV64 x_9_64 + 0x1>

>>> (x + one) / 2
<BV64 (x_9_64 + 0x1) / 0x2>

>>> x - y
<BV64 x_9_64 - y_10_64>

从原理上说xy甚至是one也是AST——任何位向量都是一个操作的树,尽管这棵树只有一层的深度。为了理解这一点,我们来学习如何处理AST。

每一个AST都有一个.op和一个.args运算op是一个用来命名执行操作的字符串,参数arg是操作中作为输入获取的值。除非运算BVV或者BVS(或者一些其他的),参数都是其他的AST,这棵树最终都以BVV或者是BVS终结。

>>> tree = (x + 1) / (y + 2)
>>> tree
<BV64 (x_9_64 + 0x1) / (y_10_64 + 0x2)>
>>> tree.op
'__floordiv__'
>>> tree.args
(<BV64 x_9_64 + 0x1>, <BV64 y_10_64 + 0x2>)
>>> tree.args[0].op
'__add__'
>>> tree.args[0].args
(<BV64 x_9_64>, <BV64 0x1>)
>>> tree.args[0].args[1].op
'BVV'
>>> tree.args[0].args[1].args
(1, 64)

从这里开始,我们会把最顶层操作产生一个位向量的AST都叫做位向量。AST也可以用来表示其他一些数据类型,包括浮点数和布尔值,我们很快就会看到。


符号约束

在两个类型相似类型的AST之间进行比较的操作会产生另一个AST——不是一个位向量,而是一个符号布尔值。

>>> x == 1
<Bool x_9_64 == 0x1>
>>> x == one
<Bool x_9_64 == 0x1>
>>> x > 2
<Bool x_9_64 > 0x2>
>>> x + y == one_hundred + 5
<Bool (x_9_64 + y_10_64) == 0x69>
>>> one_hundred > 5
<Bool True>
>>> one_hundred > -5
<Bool False>

从这里你能看出一些有趣的东西,作比较时默认是无符号的。在最后一个例子中-5被强制转换成了,肯定大于一百。如果你想要带符号比较,你可以使用one_hundred.SGT(-5)(这表示“带符号的更大)。在这章的最后有操作的完整列表。

这个小例子也展示了使用angr中的一个要点——你不应该在if或者while语句条件中直接使用变量之间的比较,因为结果可能没有一个确实的真值。即使确实的真值存在,if one > one_hundred会引发异常。你应该转而使用solver.is_truesolver.is_false,它们可以不执行约束求解而测试得到确实的真或假。

>>> 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)
4

通过向状态添加这些约束,我们强迫约束求解器将它们看作必须满足的有关任何返回值的断言。如果你运行这段代码,你也许会得到一个不同的x的值,但是那个值必然比3要大(因为y必须比2大而x必须比y大)并且小于10。此外,如果你调用`state.solver.eval(y),你会得到和你得到的x的值一致的y的值。如果你没有在两次查询之间添加任何约束,每次结果将保持一致。

从这里开始,我们很容易就能看出我们如何去做我们在这章开头提出的任务——找到产生给定输出的输入。

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

需要再次注意的是,这个解只因为位向量的语义而成立。如果我们在整数环境中进行运算,将会找不到解!

如果我们添加冲突的或者相反的约束,比如没有可以满足约束的赋予变量的值,状态会变成无法满足的,或者不令人满意的,并且对它的查询会引发异常。你可以使用state.satisfiable()检查一个状态的条件是否可以被满足。

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

你也可以计算更多复杂表达式的值,而不只是单个的变量。

# 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也可以使用。主要的区别不在于宽度而在于浮点数拥有分类。你可以通过FPVFPS使用浮点符号和数值。

# fresh state
>>> state = proj.factory.entry_state()
>>> a = state.solver.FPV(3.2, state.solver.fp.FSORT_DOUBLE)
>>> a
<FP64 FPV(3.2, DOUBLE)>

>>> b = state.solver.FPS('b', state.solver.fp.FSORT_DOUBLE)
>>> b
<FP64 FPS('FP_b_0_64', DOUBLE)>

>>> a + b
<FP64 fpAdd('RNE', FPV(3.2, DOUBLE), FPS('FP_b_0_64', DOUBLE))>

>>> a + 4.4
<FP64 FPV(7.6000000000000005, DOUBLE)>

>>> b + 2 < 0
<Bool fpLT(fpAdd('RNE', FPS('FP_b_0_64', DOUBLE), FPV(2.0, DOUBLE)), FPV(0.0, DOUBLE))>

所以这里有一些需要解释的——对于初学者来说pretty-printing对于浮点数不是那么聪明的。但是忽略掉它,实际上大部分算数操作拥有第三个静默添加的参数,这个参数在你使用二进制运算——取整模式时会静默添加。IEEE754格式支持多种多种取整模式(最近舍入,向零舍入,向正无穷方向舍入等等),所以z3求解器必须支持它们。如果你想要指定一个算术操作的取整模式,需要明确地将一个舍入模式(solver.fp.RM_*中的一个)作为浮点(fp)操作(比如solver.fpAdd)的第一个参数提供。

约束和求解按照同样的方式工作,但是使用eval会返回一个浮点数:

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

这很好,但是有时候我们需要能够直接操作以位向量格式表示的浮点数。你可以使用raw_to_bvraw_to_fp方法在位向量和浮点数之间相互翻译:

>>> a.raw_to_bv()
<BV64 0x400999999999999a>
>>> b.raw_to_bv()
<BV64 fpToIEEEBV(FPS('FP_b_0_64', DOUBLE))>

>>> state.solver.BVV(0, 64).raw_to_fp()
<FP64 FPV(0.0, DOUBLE)>
>>> state.solver.BVS('x', 64).raw_to_fp()
<FP64 fpToFP(x_1_64, DOUBLE)>

这些转换如同你将在浮点数指针和整数指针之间强制转换一样,位模式会被保留。然而,如果你想要像将一个浮点数强制转换成一个整数(或者反之)那样,尽可能地保留更精确的值时,你可以使用一组不同方法,val_to_fpval_to_bv。由于浮点数本身的性质,这些方法必须将目标值的大小或者类型作为参数输入。

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

这些方法也可以接受一个signed参数,来指定来源或者目标的位向量是否带符号。


更多求解方法

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个解,如果可能的解多于或少于n,则抛出错误。
  • solver.min(expression)会提供给定表达式可能的最小的解。
  • solver.max(expression)会提供给表达式可能的最大的解。

除此之外,所有这些方法可以接受如下的关键词作为参数:

  • extra_constraints可以作为一个约束的元组来传递。这些约束会在计算值的时候被考虑,但是不被添加进状态中。
  • cast_to可以传递一个数据类型来转换结果。目前可以传递的数据类型只有intbyte,这会使方法返回底层数据的对应表示。比如,state.solver.eval(state.solver.BVV(0x41424344, 32), cast_to=bytes)会返回b'ABCD'

总结 Summary

内容挺多!读完这章以后,你应该就可以创建和操作位向量,布尔值和浮点数值来构造操作树,然后通过查询附加在一个状态上的约束求解器来获得一系列约束条件下的可能的解。不出意外的话此刻你已经理解了使用AST来表示运算和约束求解器的强大之处了。

在附录中,你可以找到能在AST中使用的所有额外操作的索引,以防你想要一个可以快速查询的表。

上一篇
下一篇