z3solver.py

from z3 import *
import binascii
import sys

# Calculates the installation id from the entered string
# This function just reverses the order of dwords in each quadword
def getInstallIdFromString(iid_string):
    qword1, qword2, qword3, qword4 = iid_string.split('-')

    dword1 = list(binascii.unhexlify(qword1))[3::-1]
    dword2 = list(binascii.unhexlify(qword1))[7:3:-1]

    dword3 = list(binascii.unhexlify(qword2))[3::-1]
    dword4 = list(binascii.unhexlify(qword2))[7:3:-1]

    dword5 = list(binascii.unhexlify(qword3))[3::-1]
    dword6 = list(binascii.unhexlify(qword3))[7:3:-1]

    dword7 = list(binascii.unhexlify(qword4))[3::-1]
    dword8 = list(binascii.unhexlify(qword4))[7:3:-1]

    return map(ord, dword1 + dword2 + dword3 + dword4 + dword5 + dword6 + dword7 + dword8)


def main():
    if len(sys.argv) < 2:
        print 'Please provide the installation id as an argument'
        return
    
    # Sanity Check
    assert len(sys.argv[1]) == 16*4+3

    install_id = getInstallIdFromString(sys.argv[1])
    
    # The install id must encode to this hardcoded string
    target = map(ord, list('0how4zdy81jpe5xfu92kar6cgiq3lst7'))

    s = Solver()
    
    # The two parts of the unlock code
    part1 = edx = BitVec('part1', 32) 
    part2 = ebx = BitVec('part2', 32) 

    for i in xrange(32):
        # text:00401105 lodsb
        byte = install_id[i]
        
        # text:00401106 sub al, bl
        byte -= Extract(7, 0, ebx)
        
        # text:00401108 xor al, dl
        byte ^= Extract(7, 0, edx)

        # text:0040110B rol edx, 1
        edx = RotateLeft(edx, 1)
        
        # text:0040110D rol ebx, 1
        ebx = RotateLeft(ebx, 1)
        
        # Add constraint
        s.add(byte == target[i])
    
    # Solve the system
    if s.check() == sat:
        m = s.model()
        print 'Unlock Code: ',
        print '%08X-%08X' %(m[part1].as_long(), m[part1].as_long () ^ m[part2].as_long())

if __name__ == '__main__':
    main()