攻破 CRC32：从哈希值造出原始数据#
本章的内容#
CRC32 是用来检查数据完整性的校验和，并不是密码学意义上的哈希：知道一个输出值，就可以反推出能产生它的输入。
把 CRC32 的计算用 Z3 的
BitVec原样照抄把以指定的字符串开头、只含英文字母、CRC32 等于指定的值等条件写成约束
让 Z3 造出满足条件的数据
用到的工具是 BitVec 的位运算，即 >>、&、^、~，与位宽扩展 ZeroExt。整章的思路只有一条：把校验和的计算当作普通函数，反过来把它的输入当作未知量。
什么是 CRC32#
CRC32 是 Cyclic Redundancy Check 32-bit 的缩写，即用于检测数据错误的 32 位校验和，广泛用于网络通信、文件传输与压缩包的完整性检查。它的计算只用到移位与 XOR，硬件与软件都能很快完成。
不过 CRC32 并不是密码学意义上安全的哈希，本章要体会的正是它不能用于保存口令、也不能用于签名验证的原因所在。
CRC32 的计算方法#
CRC32 的计算由下面的 C 代码给出。
static uint32_t crc32(uint32_t crc, unsigned char *buf, size_t len)
{
int k;
crc = ~crc;
while (len--) {
crc ^= *buf++;
for (k = 0; k < 8; k++)
crc = crc & 1 ? (crc >> 1) ^ 0xedb88320 : crc >> 1;
}
return ~crc;
}
这段代码做了四件事。
把初始值按位取反，即
crc = ~crc依次把每个字节 XOR 进去
重复八次，每次右移一位，若最低位为 1 则 XOR 多项式
0xedb88320最后再取反一次并返回
这四步都是按位运算，每一步都能原样写成 BitVec 的表达式，因此从 C 到 Z3 的翻译不需要理解算法，只需逐行替换。
这段计算在 Python 里也能原样写出，而换成 Z3 的 BitVec 之后，输入就可以保持为变量参与计算。输入一旦是变量，同一个式子就从计算变成了关于输入的方程。
from z3 import *
def z3_crc32(data, crc=0):
"""返回 data（BitVec(8) 的列表）的 CRC32，形式为 Z3 的表达式"""
crc = ~crc # 反转初始值
for c in data:
crc ^= ZeroExt(24, c) # 把 8 位字节扩展到 32 位再 XOR
for _ in range(8):
crc = If(crc & 1 == BitVecVal(1, 32),
LShR(crc, 1) ^ 0xedb88320,
LShR(crc, 1))
return ~crc # 最后反转
用到的 Z3 函数#
函数与运算符 |
作用 |
|---|---|
|
把 8 位的值在高位补 0，扩展成 32 位 |
|
造出 32 位的常数 1，位宽本身是类型的一部分 |
|
无符号右移，空出的高位补 0 |
|
条件为真取 A，为假取 B |
|
按位取反 |
|
XOR 与 AND |
这里不用 >> 而用 LShR()，是因为 BitVec 区分有符号与无符号，要与 C 的 unsigned 行为一致，就必须用 LShR()。有符号右移会把最高位当作符号位补 1，而 C 里的 crc 声明为 uint32_t，只能按补 0 的方式移位。
另外 BitVecVal() 造出的是固定值的 BitVec。simplify() 是化简式子的函数，所有值都确定之后结果就是数值。输入仍是变量时，它只能把式子整理得更短，不会给出数值。
与 binascii.crc32() 是否一致#
与 Python 标准库的 binascii.crc32() 比较，确认这个实现是否正确。
from binascii import crc32
data = b'hello world!!'
print(crc32(data))
simplify(z3_crc32([BitVecVal(x, 8) for x in data]))
2909492980
得到了相同的值，由于把 data 的每个字节都做成 BitVecVal(x, 8) 这样的常数来计算，Z3 的式子也会化简到数值。
从 CRC32 反算数据#
从这里开始是本章的重点，即让 Z3 找出满足下面条件的数据。与前面核对实现的步骤相反，这一回输入是未知量。
长度为
n字节以
head开头，以tail结尾中间的字符是英文字母，即
a〜z、A〜ZCRC32 等于
crc_code
把每个字节做成 BitVec(f'b{i}', 8) 这样的变量，CRC32 等于 crc_code 就直接成为约束。
def is_between(b, start, end):
"""b 在 start 到 end 的字符编码范围内"""
return And(b >= ord(start), b <= ord(end))
def starts_with(data, string):
"""data 以 string 开头"""
return And([b == ord(ch) for b, ch in zip(data, string)])
def ends_with(data, string):
"""data 以 string 结尾"""
return And([b == ord(ch) for b, ch in zip(data[::-1], string[::-1])])
def break_crc32(n, head, tail, crc_code):
"""找出满足条件的 n 字节数据"""
data = [BitVec(f'b{i:02d}', 8) for i in range(n)]
solver = Solver()
solver.add(starts_with(data, head))
solver.add(ends_with(data, tail))
# 中间的字符只能是英文字母
for b in data[len(head):-len(tail)]:
solver.add(Or(is_between(b, 'a', 'z'), is_between(b, 'A', 'Z')))
solver.add(z3_crc32(data) == crc_code)
if solver.check() != sat:
return None
model = solver.model()
return bytes([model[d].as_long() for d in data])
def test(n, head, tail, crc_code):
res = break_crc32(n, head, tail, crc_code)
if res is None:
print('unsat（不存在满足条件的数据）')
else:
print(res, hex(crc32(res)))
运行示例#
要找的是长度 20 的字符串：以 "hello " 开头、以 "!!" 结尾，并且 CRC32 为 0x12345678。
test(20, 'hello ', '!!', 0x12345678)
b'hello PWvJSuTYDVsZ!!' 0x12345678
输出末尾的 0x... 就是所得字符串的 CRC32，应当与指定的 0x12345678 一致，这里用 binascii.crc32() 又算了一遍，因此可以检验 Z3 的答案是否真的正确。
太短就解不出来#
字符数一减少，可以自由选择的字符就变少，若此时不存在满足条件的数据，结果就是 unsat。
test(13, 'hello ', '!!', 0x00000000)
unsat（不存在满足条件的数据）
head 有 6 个字符，tail 有 2 个字符，中间的字符只有 5 个。Z3 证明了用这 5 个字符造不出 CRC32 为 0 的数据，下面把字节数增加一个。这里的 unsat 是一个结论，而不是求解失败：约束本身已经证明无解。
test(14, 'hello ', '!!', 0x00000000)
b'hello zXforl!!' 0x0
只增加了一个自由字符，满足条件的数据就找到了。解是否存在取决于自由度的多少，与算法的强弱无关。
可供搜索的字符越多，满足条件的数据就越容易找到
CRC32 是线性计算，把条件原样写成约束之后 Z3 就能高速求解
因此 CRC32 可以用于检测篡改，却无法防止篡改
小结#
CRC32 的计算可以用
BitVec的位运算原样照抄8 位的字节用
ZeroExt(24, c)扩展到 32 位无符号右移用
LShR()，常数用BitVecVal()把开头、末尾、字符种类与 CRC 值写成约束，Z3 就能造出满足条件的数据
自由字符太少时会得到
unsat，即证明这样的数据不存在