z3solve_crackme.py

# coding: utf-8
from z3 import *

s = Solver()

LENGTH = 6

# 6文字のテキスト
text = [BitVec('text[{0}]'.format(i), 32) for i in range(LENGTH)]

# 全て印字可能文字
for i in range(LENGTH):
    s.add(32 <= text[i], text[i] <= 126)

# ハッシュ
ret = [BitVec('ret[{0}]'.format(i), 32) for i in range(LENGTH + 1)]
ret[0] = 0x539    # 初期値
for i in range(LENGTH):
    ret[i+1] = ret[i] + (ret[i] << 5) + text[i]

# 結果が等しい
s.add(ret[LENGTH] == 0xef2e3558)

# 確認
t = s.check()
if t == sat:
    m = s.model()
    passcode = ""
    for i in range(LENGTH):
        passcode += chr(m[text[i]].as_long())
    print("RESULT : {0}".format(passcode))
else:
    print(t)