CRC32を破る ― ハッシュ値から元のデータを作る#
この章で学ぶこと#
CRC32 はデータの整合性チェックに使われるハッシュですが、暗号学的なハッシュではありません。出力が分かれば、条件を満たす入力を計算で作れてしまいます。
CRC32 の計算を、Z3 の
BitVecでそのまま書き写す「この文字列で始まる」「英字だけ」「CRC32 がこの値」という条件を制約にする
Z3 に条件を満たすデータを作らせる
BitVec のビット演算（>>, &, ^, ~）と、ZeroExt（ビット幅の拡張）が道具です。
CRC32 とは#
CRC32（Cyclic Redundancy Check 32-bit）は、データの誤り検出に使われる32ビットのチェックサムです。ネットワーク通信やファイルの整合性チェックで広く使われています。
ただし、CRC32 は暗号学的に安全なハッシュではありません。出力が1つ分かれば、その出力になる入力を逆算できます。パスワードの保存などに使ってはいけない理由が、この章で体験できます。
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;
}
やっていることは、次の4つです。
初期値をビット反転する（
crc = ~crc）各バイトを順番に XOR する
8回、1ビットずつ右にずらしながら、いちばん下のビットが 1 なら多項式
0xedb88320を XOR する最後に、もう一度ビット反転して返す
この計算は 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() を使います。
また 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〜Z）CRC32 が
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)))
実行例#
"hello " で始まり "!!" で終わる長さ20の文字列で、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文字しかありません。この5文字では、CRC32 が 0 になるデータは存在しない、と Z3 が証明しました。
1バイト増やしてみます。
test(14, 'hello ', '!!', 0x00000000)
b'hello zXforl!!' 0x0
自由な文字が1つ増えるだけで、条件を満たすデータが見つかりました。
探索する文字が増えるほど、条件を満たすデータは見つけやすくなる
CRC32 は線形な計算なので、条件をそのまま制約にすれば Z3 が高速に解ける
だから CRC32 は「改ざん検出」には使えても、「改ざん防止」には使えない
まとめ#
CRC32 の計算は
BitVecのビット演算でそのまま書き写せる8ビットのバイトは
ZeroExt(24, c)で32ビットに広げる符号なしの右シフトは
LShR()、定数はBitVecVal()条件（先頭・末尾・文字種・CRC値）を制約にすれば、条件を満たすデータを Z3 が作れる
自由な文字が少なすぎると
unsatになる（存在しないことが証明される）