简单的活着

angr.solver

Posted on Jul 10, 2019 By Mista Cai

angr.solver

AST:符号执行产生的抽象语法树，可以解释为SMT解析器中的约束条件。

解决问题“已知输出，输入应该满足什么条件？”

位向量

位向量就是一个比特序列，可以解释为数学上的有界整数。

  • BVV：Bitvector value
  • BVS：Bitvector symbolic
In [14]: s = start_state

In [15]: one = s.solver.BVV(1,64) # 值，长度

In [16]: one
Out[16]: <BV64 0x1> # BV64代表长度64

每一个AST都有

  • .op定义了要执行运算的属性
  • .args参与运算的操作数

op是BVV/BVS时，args代表其参数：值/符号，宽度。其余情况args都是AST，AST终结点是BVV或BVS。

看例子比较好理解。

In [11]: tree = (x+1)/(y-2)

In [12]: tree
Out[12]: <BV64 (x_0_64 + 0x1) / (y_1_64 - 0x2)>

In [13]: tree.op
Out[13]: '__floordiv__'

In [14]: tree.args
Out[14]: (<BV64 x_0_64 + 0x1>, <BV64 y_1_64 - 0x2>)

In [15]: tree.args[0].op
Out[15]: '__add__'

In [16]: tree.args[0].args
Out[16]: (<BV64 x_0_64>, <BV64 0x1>)

In [17]: tree.args[0].args[1].op
Out[17]: 'BVV'

In [18]: tree.args[0].args[1].args
Out[18]: (1L, 64)

符号约束

任意两个类型相似的AST进行比较操作将产生一个新的AST，不是一个位向量，而是符号化的布尔类型。

In [22]: one = s.solver.BVV(1, 64)

In [23]: x == one
Out[23]: <Bool x_0_64 == 0x1>

用solver.is_true和solver.is_false,判断真假;直接使用if/while语句会产生异常，因为比较结果可是符号。

In [24]: con = one == 1

In [25]: s.solver.is_true(con)
Out[25]: True

In [26]: s.solver.is_false(con)
Out[26]: False

约束求解

state.solver.add:加入一个约束条件到state，将每一个符号化的布尔值作为一个关于符号变量合法性的断言。

state.solver.eval(symbol)对各个断言进行评测，求出一个合法值。

已知\(x > y, y > 0, 5 > x\),解得\(x=4,y=2\)

In [28]: s.solver.add(x > y)
Out[28]: [<Bool x_0_64 > y_1_64>]

In [30]: s.solver.add(y > 0)
Out[30]: [<Bool y_1_64 > 0x0>]

In [31]: s.solver.add(5 > x)
Out[31]: [<Bool x_0_64 < 0x5>]

In [32]: s.solver.eval(x)
Out[32]: 4L
  
In [34]: s.solver.eval(y)
Out[34]: 2L

如果两次求解之间没有加入其他约束，两次求解结果将会一致。

解决问题“已知输出，输入应该满足什么条件？”

In [37]: input = s.solver.BVS("input", 64)

In [38]: op = (((input + 4)*3)>>1) + input

In [39]: output = 200

In [40]: s.solver.add(op == output)
Out[40]: [<Bool ((((input_2_64 + 0x4) * 0x3) >> 0x1) + input_2_64) == 0xc8>]

In [41]: s.solver.eval(input)
Out[41]: 3689348814741910401L

In [45]: hex(s.solver.min(input))
Out[45]: '0x3333333333333381L'

state.satisfiable()检查一个state是否可解，

In [48]: s.solver.add(input < 2**32)
Out[48]: [<Bool input_2_64 < 0x100000000>]

In [49]: s.satisfiable
Out[49]: <bound method SimState.satisfiable of <SimState @ 0x40072d>>

In [50]: s.satisfiable()
Out[50]: False

cast_to接收一个参数把指定结果映射到某种数据类型，目前只能是str，将以字符串的形式显示结果。

In [52]: s.solver.eval(s.solver.BVV(0x41424344,32), cast_to=str)
Out[52]: 'ABCD'