处理逻辑

[esp+1C]: 01B6BA97
[esp+20]: 44C4B4E0
[esp+24]: count1
[esp+28]: count2
[esp+2C]: shift2
[esp+3C]: anti0
[esp+40]: anti1
[esp+44]: anti2
[esp+48]: anti3
[esp+4C]: anti4
[esp+50]: anti5
[esp+54]: anti6
[esp+58]: anti7
[esp+5C]: anti8
[esp+60]: hash1
[esp+64]: hash2
[esp+70]: char input[0x40];

input: head7 + middle + tail7 (大写16进制)
esi=radix39_to_int(head7)&0xFFFFFFFF
edi=radix39_to_int(tail7)&0xFFFFFFFF
ebx=i
shift1=ebx

for i in range(9):
	shift1=i
	shift2=0x0F-i
	if i & 1 == antis[i]():
		count1+=1
		esi=ror(esi, shift1)
		esi^=hash1();
		edi=ror(edi, shift2)
		edi^=hash2();
	else:
		count2+=1
		esi=ror(esi, shift2)
		esi^=hash2()
		edi=ror(edi, shift1)
		edi^=hash1()
count1 != 0
count2 != 0
esi ^ 0xA1FB3009 == 0x01B6BA97
edi ^ 0xD3099228 == 0x44C4B4E0

struct bn {
    u32 len;
    u32 word[8];
};

.bss:004C50EC ; bn v4
.bss:004C5110 ; bn c3

c1 = c3 & 0xFFFFFFFF
v1 = input * c1
v1 /= c2
v1 += c3
v1 += c4
v2 = c3 * c4
v3 = v1 - v2
v4 = v1 * c2
v4 = v4 * 0x25
v4 += v4 (v4的计算溢出时，会覆盖c3.len)
v3 == c3

脚本

from z3 import *


RADIX39 = '.0123456789:!ABCDEFGHIJKLMNOPQRSTUVWXYZ'


def hex2bin(s):
    return s.decode('hex')


def bin2hex(s):
    return s.encode('hex')


def load_file(filename):
    f = open(filename, 'rb')
    s = f.read()
    f.close()
    return s


def save_file(filename, s):
    f = open(filename, 'wb')
    f.write(s)
    f.close()
    return


def radix_to_int(radix_set, s):
    v = 0
    radix = len(radix_set)
    for i in range(len(s)):
        v *= radix
        v += radix_set.index(s[i])
    return v


def int_to_radix(radix_set, v, width=0):
    s = ''
    radix = len(radix_set)
    while True:
        s += radix_set[v % radix]
        if v < radix:
            break
        v //= radix
    s = s[::-1]
    if width != 0:
        s = s.rjust(width, radix_set[0])
    return s


def ror32(v, shift):
    shift &= 0x1F
    if shift == 0:
        return v
    return ((v >> shift) | (v << (32 - shift))) & 0xFFFFFFFF


def rol32(v, shift):
    shift &= 0x1F
    if shift == 0:
        return v
    return ((v << shift) | (v >> (32 - shift))) & 0xFFFFFFFF


def int_to_radix2(v):
    hex_set = set('0123456789ABCDEF')
    max_v = radix_to_int(RADIX39, 'F'*7)
    while True:
        s = int_to_radix(RADIX39, v, width=7)
        if set(s).issubset(hex_set):
            return s
        v += 0x100000000
        if v > max_v:
            break
    return None


def get_u32(s, offset):
    v = 0
    v |= ord(s[offset])
    v |= ord(s[offset + 1]) << 8
    v |= ord(s[offset + 2]) << 16
    v |= ord(s[offset + 3]) << 24
    return v


def va2fileoffset(v):
    return v - 0x401000 + 0x400


def calc_hash(s, offset, size):
    v = 0
    for i in range(offset, offset+size, 4):
        v ^= get_u32(s, i) ^ 0xDEADC0DE
        v = ror32(v, 9)
    return v


def test1():
    file_data = load_file('lelfei-KCTF2020.exe')
    data1_offset = va2fileoffset(0x4B5970)
    data2_offset = va2fileoffset(0x401550)
    hash1 = [calc_hash(file_data, data1_offset, sz) for sz in range(0x80C, 0, -0x20)]
    hash2 = [calc_hash(file_data, data2_offset, sz) for sz in range(0x620, 0, -0x20)]
    anti = [0, 0, 1, 1, 0, 0, 1, 1, 0]
    v1 = 0xA1FB3009 ^ 0x01B6BA97
    v2 = 0xD3099228 ^ 0x44C4B4E0
    for i in range(9 - 1, -1, -1):
        if (i & 1) == anti[i]:
            v2 ^= hash2[i]
            v2 = rol32(v2, 15 - i)
            v1 ^= hash1[i]
            v1 = rol32(v1, i)
        else:
            v2 ^= hash1[i]
            v2 = rol32(v2, i)
            v1 ^= hash2[i]
            v1 = rol32(v1, 15 - i)
    s1 = int_to_radix2(v1)
    s2 = int_to_radix2(v2)
    if s1 is not None and s2 is not None:
        print('BN: %s...%s' % (s2[::-1], s1[::-1]))
    # 377EF3D...03F7C01
    return


def test2():
    dst_len = 1
    for middle_len in range(1, 50):
        # v: high-middle-low
        # v1 = (v*c1)/c2 + c3 + c4
        # v2 = c3*c4
        # v3 = v1 - v2
        # v4 = v1*c2, v4 *= 25, v4 += v4
        # dst_len = v4 / (1 << 256)
        # dst = c3 & ((1 << (dst_len*8)-1)
        # v3 == dst
        solver = Solver()
        high = 0x377EF3D
        low = 0x03F7C01
        middle = Int('middle')
        c2_rem = Int('c2_rem')
        c2 = 0x0E053D0F
        c3 = 0x3FAFFA2B01B6BA9744C4B4E010010401
        c4 = 0xFEA1BD9E6964129D8F5079E1
        c1 = c3 & 0xFFFFFFFF

        v = high
        v *= (0x10 ** middle_len)
        v += middle
        v *= 0x10 ** 7
        v += low

        dst = c3
        dst &= (1 << (dst_len * 8)) - 1
        v2 = c3 * c4
        v1 = (dst + v2)
        v4 = v1 * c2
        v4 *= 0x25
        v4 += v4
        solver.add(middle > 0)
        solver.add(middle < (0x10 ** middle_len))
        solver.add(c2_rem < c2)
        solver.add(c2_rem >= 0)
        solver.add((v4 / (1 << 256)) == dst_len)
        solver.add((v * c1) == ((v1 - c4 - c3) * c2 + c2_rem))
        if solver.check() == unsat:
            continue
        m = solver.model()
        s = ''
        s += '%07X' % high
        s += ('%%0%dX' % middle_len) % m[middle].as_long()
        s += '%07X' % low
        print('INPUT: %s' % s[::-1])
        # 10C7F30833B9C4563BF035C32D8C7709E040FCA64E211F34CD3FE773
    return


def test():
    # test1()
    test2()
    return


test()

[招聘] 欢迎你加入看雪团队！