CRC32を破る

CRC32を破る#

from z3 import *

問題の背景#

CRC32（Cyclic Redundancy Check 32-bit）は、データの整合性を検証するために使用されるハッシュ関数の一種です。これは特にネットワーク通信やファイルの整合性チェックに広く利用されています。しかし、CRC32は暗号学的に安全なハッシュ関数ではなく、特定の入力に対して出力が既知である場合、逆算して入力データを構築することが可能です。本章では、Z3 SMTソルバーを用いて、特定の条件を満たすデータをCRC32の値から逆算する方法について説明します。

CRC32の計算方法#

下のC言語コードでは、CRC32の計算が実装されています。

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値を反転（ビット反転）してから計算を開始

  • 各バイトを順番にXORし、ビット単位で処理

  • ビットシフトと多項式 0xedb88320 を用いたフィードバック計算

  • 最終的に結果を再びビット反転

このロジックをPythonのZ3ライブラリを用いて再現し、逆計算を試みます。

def z3_crc32(data, crc = 0):
    crc = ~crc
    for c in data:
        crc ^= ZeroExt(24, c)
        for i in range(8):
            crc = If(crc & 1 == BitVecVal(1, 32), LShR(crc, 1) ^ 0xedb88320, LShR(crc, 1))
    return ~crc

ここで使用されているZ3の関数と演算子について説明します。

  • ZeroExt(24, c): 8ビットの値 c を32ビットに拡張する。

  • BitVecVal(1, 32): 32ビット整数の定数値 1 を作成。

  • LShR(crc, 1): 符号なしの右シフトを実行。

  • If(condition, true_case, false_case): 条件 condition に応じて true_case または false_case を返す。

  • ~crc: CRC値のビット反転。

  • ^, &: XOR演算とAND演算を適用。

この関数を用いることで、与えられたバイト列 data のCRC32をZ3の制約ソルバーに適用可能な形式で計算できます。

次に、binascii.crc32() との結果を比較してみます。

  • BitVecVal() は固定値の BitVec を作成します。

  • simplify() は演算式を簡略化する関数で、すべての値が既知の場合、結果は数値になります。

from binascii import crc32

data = b'hello world!!'
print(crc32(data))

2909492980

simplify(z3_crc32([BitVecVal(x, 8) for x in data]))
2909492980

CRC32の逆算#

CRC32の値から元データを逆算するため、Z3の制約解決機能を活用します。

  • starts_with(data, head): 文字列が head で始まることを制約。

  • ends_with(data, tail): 文字列が tail で終わることを制約。

  • is_between(b, 'a', 'z'): 変数 b が a-z の範囲にあることを制約。

  • is_between(b, 'A', 'Z'): 変数 b が A-Z の範囲にあることを制約。

  • solver.add(crc == crc_code): 計算されたCRC32が crc_code に一致することを制約。

def is_between(b, start, end):
    return And(b >= ord(start), b <= ord(end))

def starts_with(bv_list, string):
    return And([b == ord(s) for b, s in zip(bv_list, string)])

def ends_with(bv_list, string):
    return And([b == ord(s) for b, s in zip(bv_list[::-1], string[::-1])])

def break_crc32(n, head, tail, crc_code):
    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')))
        
    crc = z3_crc32(data)
    solver.add(crc == crc_code)
    if solver.check() == sat:
        m = solver.model()
        res = bytes([m[d].as_long() for d in data])
        return res
    else:
        return None

def test(n, head, tail, crc_code):
    res = break_crc32(n, head, tail, crc_code)
    if res is not None:
        print(res, hex(crc32(res)))
    else:
        print('unsat')

次のテストケースでは、"hello " で始まり、"!!" で終わる長さ20の文字列を生成します。中間の文字は英字であり、CRC32の値が 0x12345678 となるように求めます。

test(20, 'hello ', '!!', 0x12345678)

b'hello bHvabzZENYUs!!' 0x12345678

文字列の長さが足りない場合、条件を満たすデータを作成できず unsat となります。

test(13, 'hello ', '!!', 0x00000000)

unsat

長さを増やせば解が見つかりました。

test(14, 'hello ', '!!', 0x00000000)

b'hello zXforl!!' 0x0
Contents