自动化工具

2020-05-12 reverse angr, z3, 自动化 ∞ 评论

angr

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

import angr

proj = angr.Project("./enormous")
state = proj.factory.entry_state()
sim = proj.factory.simulation_manager(state)
sim.explore(find=(0x400000+0x3950), avoid=(0x400000+0x3963))
if len(sim.found) > 0:
    print("Yes")
    print(sim.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 在默认情况下，只寻找满足所有条件的一组解，而不是找出所有解。

参考：Z3 API in Python

解简单方程

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 - 数组

常用函数：

LShR(x, 1) - 逻辑右移（用0填充，>> 为算术右移）

例1：

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：

from z3 import *

so = Solver()
flag = [BitVec(f'flag{i}',8) for i in range(36)]
a = [i for i in flag]
b = [i for i in range(36)]
c = [0 for i in range(36)]
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]
for i in range(6):
	for j in range(6):
		b[i+6*j] = a[6*i+j]
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]
		so.add(simplify(c[j+6*i]) == d[j+6*i])
for i in range(6,36-10):
	so.add(flag[i]>=32)
	so.add(flag[i]<=127)
for i in range(6):
	so.add(flag[i] == ord('whctf{'[i]))
for i in range(36-9,36):
	so.add(flag[i] == 0x1)
so.add(flag[-10] == ord('}'))
if so.check() == sat:
	m = so.model()
	print(''.join(chr(m[i].as_long()) for i in flag))
else:
	print('Error')

Lazzaro

CTF弱鸡自进阶

自动化工具

angr

z3