自动化工具

reverse , , 评论

angr

angr是一个二进制的代码分析工具, 能够自动化的完成二进制文件的分析并找出漏洞。可以进行动态的符号执行分析。

1
2
3
4
5
6
import angr
p = angr.Project('signal.exe') #装载一个项目，即进程
st = p.factory.entry_state() #创建一个SimState对象，即程序状态
sm = p.factory.simulation_manager(st) #为上面对象创建模拟器
sm.explore(find=0x40179E, avoid=0x4016E6) #利用explore求解
print(sm.found[0].posix.dumps(0)) #打印找到的结果

​

z3

z3 是一个微软出品的开源约束求解器，能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题，功能强大且易于使用。z3 约束求解器是针对 Satisfiability modulo theories Problem 的一种通用求解器。所谓 SMT 问题，在 z3 环境下是指关于算术、位运算、数组等背景理论的一阶逻辑组合决定性问题。虽然 z3 功能强大，但是从理论上来说，大部分 SMT 问题的时间复杂度都过高，根本不可能在有限时间内解决。所以千万不要把 z3 想象得过于万能。

z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外，著名的二进制分析框架 angr 也内置了一个修改版的 z3。

z3 内置了多种变量类型，基本能覆盖常见计算机数据结构。包括整数、浮点数、BitVector、数组等。

z3 在默认情况下，只寻找满足所有条件的一组解，而不是找出所有解。

  • 解简单方程

    1
    2
    3
    4
    from z3 import *
    x = Int('x')
    y = Int('y')
    solve(x > 2, y < 10, x + 2*y == 7)

  • 求解实际案例

    Solver()命令创建一个通用求解器。我们可以通过add函数添加约束条件。我们称之为声明约束条件。check()函数解决声明的约束条件，sat结果表示找到某个合适的解，unsat结果表示没有解。这时候我们称约束系统无解。最后，求解器可能无法解决约束系统并返回未知作为结果。

    常用的数据类型：

    BitVec - 至特定大小的数据类型

    Int - 整型

    Real - 有理数

    Bool - 布尔类型

    Array - 数组

    例1：

    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    from z3 import *
    a1, a2, a3, a4, a5, a6 = Ints("a1 a2 a3 a4 a5 a6")
    x = Solver()
    x.add(a1 * 3 + a2 * 2 + a3 * 5 == 1003)
    x.add(a1 * 4 + a2 * 7 + a3 * 9 == 2013)
    x.add(a1 + a2 * 8 + a3 * 2 == 1109)
    x.add(a4 * 3 + a5 * 2 + a6 * 5 == 671)
    x.add(a4 * 4 + a5 * 7 + a6 * 9 == 1252)
    x.add(a4 + a5 * 8 + a6 * 2 == 644)
    x.check()
    print(x.model())

    例2：

    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
      from z3 import *
      
      #创建一个解决方案实例
      solver = Solver()
      #flag长度先设置为36，包括尾部的9个1
      flag = [Int('flag%d'%i) for i in range(36)]
      #保存flag的矩阵
      a = [i for i in flag]
      #保存flag的转置矩阵
      b = [i for i in range(36)]
      #保存a*b的矩阵
      c = [0 for i in range(36)]
      #堆中正确flag的运算结果
      d = [0x12027,0x0F296,0x0BF0E,0x0D84C,0x91D8,0x297,
      	0x0F296,0x0D830,0x0A326,0x0B010,0x7627,0x230,
      	0x0BF0E,0x0A326,0x8FEB,0x879D,0x70C3,0x1BD,
      	0x0D84C,0x0B010,0x879D,0x0B00D,0x6E4F,0x1F7,
      	0x91D8,0x7627,0x70C3,0x6E4F,0x9BDC,0x15C,
      	0x297,0x230,0x1BD,0x1F7,0x15C,0x6]
      #获得a的转置矩阵
      for i in range(6):
      	for j in range(6):
      		b[i+6*j] = a[6*i+j]
      #运算a*b
      for i in range(6):
      	for j in range(6):
      		for k in range(6):
      			c[j+6*i] = c[j+6*i] + a[6*i+k]*b[6*k+j]
      		#添加约束，正确flag的运算结果
      		solver.add(simplify(c[j+6*i]) == d[j+6*i])
      #添加约束，除了尾部，flag的字符一定在可见字符范围内
      for i in range(6,36-10):
      	solver.add(flag[i]>=32)
      	solver.add(flag[i]<=127)
      #添加约束，由于flag有格式，前6位一定为whctf{
      for i in range(6):
      	solver.add(flag[i] == ord('whctf{'[i]))
      #添加约束，flag的尾部为9个1
      for i in range(36-9,36):
      	solver.add(flag[i] == 0x1)
      #添加约束，flag的最后一个肯定是}
    solver.add(flag[-10] == ord('}'))
      #这里一定要有，不check的话会报错
      if solver.check() == sat:
      	m = solver.model()
      	s = []
      	#获得结果
      	for i in range(36):
      		s.append(m[flag[i]].as_long())
      	#输出flag
      	print(bytes(s))
      else:
      	print('error')