lundi 6 août 2012

Solution for the ESET BlackHat US Challenge 2012


1.  Introduction

On July 21st 2012 at 7AM (Las Vegas time) ESET published a crack-me for the BlackHat US 2012 edition. Rules were simple: find a valid couple of serial numbers for a given name before July 26th 2012 2PM to maybe win $1000 and a BlackCard (that gives you a free entry for either the next BlackHat US or EU).

Figure 1: GUI of the crack-me

According to challenge's site Eloi Vanderbeken from Oppida was the only person to solve it in time and won the price even if he was not at BlackHat US:
 
Figure 2: Result of the challenge

This post explains how Eloi achieved to break it.

2.  First steps

The crack-me is packed with UPX, so we first unpack it by using the upx -d command to study it under IDA Pro 6.3.
We quickly noticed that it was created with the MFC library, which explains the large size of the binary (1Mo packed and 2M unpacked) and facilitates its analysis with IDA:
 
Figure 3: Light blue parts are MFC functions recognized by IDA

A quick look in the referenced text string reveals the address of the function in charge of serials verification:
Figure 4:localization of the verification function

To simplify its analysis, we import the labels generated by IDA in OllyDbg by using exporting them in a map file and importing the .map file with GoDup, an OllyDbg plugin :

Figure 5: IDA labels imported in OllyDbg

Now we have located verification functions we can start to study them.

3.  First part

A quick analysis shows us that the serial is base64 decoded and must be composed of at least 0x3F characters once base64 decoded. It is then verified with the following algorithm :
def scramble(t) :
    j = 0
    for i in xrange(64) :
        c = t[i]%80
        j = (t[c%80] + j)%80
        t[j], t[i] = t[i], t[j]

exitFun = badBoy
serialDecoded = serial.decode("base64")

padding = ("ESETNOD32@"*8)[len(name):]
H = hash512(name+padding)

if serialDecoded[:64][::-1] != H :
    return exitFun()

scrambledTab = H

for i, c in enumerate(serialDecoded) :
    scrambledTab[i%64] ^= c

scramble(scrambledTab)

if scrambledTab[68 : 72] != [0xA, 0xB, 0xC, 0xD] :
    exitFun = badBoy
    return exitFun()

if hash512(scrambledTab)[:12] != [0xCA, 0x8A, 0x57, 0x12, 0x78, 0xB6, 0xCA, 0xEF, 0x78, 0x56, 0x34, 0x12] :
    return exitFun()

exitFun = goodBoy
return exitFun()
Figure 6:  First check of the serial in pseudo-python

The first part of the check is easy to satisfy, we just need to encode in base64 the reversed hash of the padded name. The second part is a little bit harder, at first sight it seems that we need to find a preimage attack on the hash function to satisfy the last check and to reverse the scramble function to find a valid serial.
After studying the code of the hash function, we found that the hash function was WhirlPool (thanks to the substitution table) and we did not find any backdoor in the code. It had to be something else.
A careful reader might have seen that scrambledTab is initialized with a 64 bytes array  (the hash of the name) but is then considered as a 80 bytes array in the scramble function. After redefining scrambledTab as a 80 bytes array in IDA, we saw that exitFun became scrambledTab[76:80]:
Figure 6: IDA disassembly after scrambledTab was redefined

Moreover BadBoy and GoodBoy functions' addresses differ only by the least significant byte (0x40 for the BadBoy function, 0x20 for the GoodBoy one) so if we can use the scramble function to rewrite the badboy's address least significant byte to 0x20 and write the good values ([0xA, 0xB, 0xC, 0xD]) in scrambledTab[68:72] we will have the good boy message and you will pass the first check.

To achieve this goal we wrote a little "intelligent" bruteforcer which, given an initial table of 64 unknown bytes followed by 16 fixed bytes (remember we only control the 64 first bytes) and a list of couples (offset, value_to_set) corresponding to the desired final state of the table, tries to set the  right bytes at the right place and next tries to not overwrite them.
Complete code to generate a valid first serial is the following:
import sys
from random import SystemRandom
from base64 import b64encode
try :
  from whirlpool import Whirlpool
except :
  print "To work this keygen need the Whirpool implementation located here : http://www.bjrn.se/code/whirlpoolpy.txt"
  sys.exit(0)

sec_rnd = SystemRandom()

print "name :"
name = sys.stdin.readline().rstrip("\r\n")
hash_name = [ord(c) for c in Whirlpool(name+("ESETNOD32@"*8)[len(name):]).digest()]

def step1(k, i, j, to_set, to_keep) :
  if i > 63 :
    if not to_set :
      return k
    return None
  if to_set :
    to_set_cpy = list(to_set)
    sec_rnd.shuffle(to_set_cpy)
    for choice, (idx, v) in enumerate(to_set_cpy) :
      if k[i] == v :
        r = step2a(idx, k, i, j, to_set_cpy[:choice] + to_set_cpy[choice+1:] , to_keep)
        if r is not None :
          return r
      elif k[i] is None :
        k[i] = v
        r = step2a(idx, k, i, j, to_set_cpy[:choice] + to_set_cpy[choice+1:] , to_keep)
        if r is not None :
          return r
        k[i] = None

  r = step2b(k, i, j, to_set, to_keep)
  if r is not None :
    return r
  return None


def step2a(idx, k, i, j, to_set, to_keep) :
  c = k[i] % 80
  kc = k[c]
  if kc is None :
    if (idx - j)%80 in to_keep :
      return None
    kc = (idx - j)%80
    while kc < 0x100 :
      k[c] = kc
      to_keep.add(idx)
      r = step3(k, i, idx, to_set, to_keep)
      to_keep.remove(idx)
      if r is not None :
        return r
      kc += 80
    k[c] = None
  elif (kc + j)%80 == idx :
    to_keep.add(idx)
    r = step3(k, i, idx, to_set, to_keep)
    to_keep.remove(idx)
    return r
  else :
    return None


def step2b(k, i, j, to_set, to_keep) :
  c = k[i]
  if c is None :
    vals = [c for c in xrange(0x100) if k[c%80] is not None and (k[c%80] + j)%80 not in to_keep]
    sec_rnd.shuffle(vals)
    for c in vals :
      k[i] = c
      r = step3(k, i, (k[c%80] + j)%80, to_set, to_keep)
      if r is not None:
        return r
    vals = [c for c in xrange(0x100) if k[c%80] is None]
    sec_rnd.shuffle(vals)
    for c in vals :
      k[i] = c
      c = c % 80
      vals2 = [kc for kc in xrange(0x100) if (kc + j)%80 not in to_keep]
      sec_rnd.shuffle(vals2)
      for kc in vals2 :
        k[c] = kc
        r = step3(k, i, (kc + j)%80, to_set, to_keep)
        if r is not None :
          return r
      k[c] = None
    k[i] = None
  else :
    c %= 80
    kc = k[c]
    if kc is None :
      vals = [kc for kc in xrange(0x100) if (kc + j)%80 not in to_keep]
      sec_rnd.shuffle(vals)
      for kc in vals :
        k[c] = kc
        r = step3(k, i, (kc + j)%80, to_set, to_keep)
        if r is not None :
          return r
      k[c] = None
    elif (kc + j)%80 not in to_keep :
      return step3(k, i, (kc + j)%80, to_set, to_keep)
  return None

def step3(k, i, j, to_set, to_keep) :
  k[i], k[j] = k[j], k[i]
  r = step1(k, i+1, j, to_set, to_keep)
  if r is not None :
    r[i], r[j] = r[j], r[i]
    return r
  k[i], k[j] = k[j], k[i]
  return None

# initial table
k = [None]*64+[0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x40, 0x17, 0x40, 0x00]
# couple of values to set
to_set = [(0x44, 0xA), (0x45, 0xB), (0x46, 0xC), (0x47, 0xD), (0x4C, 0x20)]
# addresses that have to be keep (not modified)
to_keep = set((0x4D, 0x4E, 0x4F))

s = step1(k, 0, 0, to_set, to_keep)

# unused values can be set to any value
for i in xrange(len(s)) :
  if s[i] is None :
    s[i] = sec_rnd.randint(0, 0xFF)

serial = "".join(chr(i) for i in hash_name[::-1])
serial += "".join(chr(a^b^c) for a, b, c in zip(hash_name, hash_name[::-1], s))

print "serial 1 :"
print serial.encode("base64").replace("\n","")
Figure 7: Code to generate a valid first serial (Python 2.7)

If you want to personalize the generated serial by appending it a constant string, you can use one of the following code, the first one adds some constraints to the generated table and generates a serial with a minimal length; the second one appends bytes to the serial but permits to add an arbitrary long string:

egg = "ElV++ESET++="
egg_d = egg.decode("base64")
padd = 64 - len(egg_d)
list_egg = [hash_name[padd+i]^hash_name[::-1][padd+i]^ord(c) for i,c in enumerate(egg_d)]

k = [None]*padd+list_egg+[0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x40, 0x17, 0x40, 0x00]
to_set = [(0x44, 0xA), (0x45, 0xB), (0x46, 0xC), (0x47, 0xD), (0x4C, 0x20)]
to_keep = set((0x4D, 0x4E, 0x4F))

s = step1(k, 0, 0, to_set, to_keep)


for i in xrange(len(s)) :
  if s[i] is None :
    s[i] = sec_rnd.randint(0, 0xFF)

serial = "".join(chr(i) for i in hash_name[::-1])
serial += "".join(chr(a^b^c) for a, b, c in zip(hash_name, hash_name[::-1], s))
serial = serial.encode("base64").replace("\n","")
# multiple encoding are valid for the same value because some bits are ignored for the last symbol
serial = serial[:-len(egg)]+egg

print "serial 1 :"
print serial
Figure 8: First solution, all generated serials end with ElV++ESET++ (Python 2.7)

egg = "+blabla+ESET+Nod32+BH2012+Oppida"
egg_d = egg.decode("base64")

k = [None]*64+[0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x40, 0x17, 0x40, 0x00]
to_set = [(0x44, 0xA), (0x45, 0xB), (0x46, 0xC), (0x47, 0xD), (0x4C, 0x20)]
to_keep = set((0x4D, 0x4E, 0x4F))

s = step1(k, 0, 0, to_set, to_keep)

for i in xrange(len(s)) :
  if s[i] is None :
    s[i] = sec_rnd.randint(0, 0xFF)

serial = "".join(chr(i) for i in hash_name[::-1])

# add padding (128 % 3 = 2)
egg_d = chr(sec_rnd.randint(0, 0xFF) + egg_d
for i, j in enumerate(hash_name + hash_name[::-1] + [ord(c) for c in egg_d]) :
    s[i%64] ^= j

serial += "".join(chr(i) for i in s[:64])
serial += egg_d
serial = serial.encode("base64").replace("\n","")
# multiple encoding are valid for the same value because some bits are ignored for the last symbol
serial = serial[:-len(egg)]+egg

print "serial 1 :"
print serial
Figure 9: Second solution, all generated serials end with "+blabla+ESET+Nod32+BH2012+Oppida" (Python 2.7)

4.  Second part

The second part of the challenge takes place at address 0x0401C10. The serial must be composed of 12 uppercase hexadecimal characters. Those characters are used to transform a 64 bits value with the following algorithm:
def to_16b(qword) :
    idx = 1
    word = 0
    for i in xrange(16) :
        if qword & (1 << idx ) :
            word |= 1 << i
        idx = (idx + 29) % 64
    return word

def mutate(qword, word) :
    idx = 1
    for i in xrange(16) :
        if word & (1 << i) :
            qword |= 1 << idx
        else :
            qword &= ~(1 << idx)
        idx = (idx + 29) % 64
    return qword

def shift(qword) :
    qword_masked = qword & 7069181668496654033
    nb_bits_set = 0
    for i in xrange(64) :
        if qword_masked & (1 << i) :
            nb_bits_set += 1
    return ((qword << 1) | (nb_bits_set & 1)) & ((1 << 64) - 1)
   
serial = "012345678ABC"
qword = 8828098094971975552
for c in serial :
    i = int(c,16)
    word = to_16b(qword)
    if word & (1 << i) :
        word &= ~(1 << i)
    else :
        word |= (1 << i)
    qword = mutate(qword, word)
    qword = shift(qword)

print hex(qword)
Figure 10: First part of the verification of the second serial : mutation of qword (Python 2.7)

Those operations can be simplified to get the following algorithm:
def shift(qword) :
    qword_masked = qword & 7069181668496654033
    nb_bits_set = 0
    for i in xrange(64) :
        if qword_masked & (1 << i) :
            nb_bits_set += 1
    return ((qword << 1) | (nb_bits_set & 1)) & ((1 << 64) - 1)
   
serial = "012345678ABC"
qword = 8828098094971975552
int_to_idx = [1, 30, 59, 24, 53, 18, 47, 12, 41, 6, 35, 0, 29, 58, 23, 52]
for c in serial :
    qword ^= 1 << int_to_idx[int(c,16)]
    qword = shift(qword)
print hex(qword)
Figure 11: Simplified first part of the verification of the second serial : mutation of qword (Python 2.7)

After being transformed, qword must satisfy the following check:
qwordTable = [[4, 145, 249, 72, 19, 195, 74, 137],
    [...]
 [4611686018427387904L,
  1195637156289680119L,
  24621007439812200L,
  43743323218066342L,
  676995634570036126L,
  1203597948695219397L,
  1037036833364889864L,
  130039954294608103L]]

def has_same_set_bits(a, b) :
    """ return 1 if all bits set in b are also set in a else 0"""
    for i in xrange(64) :
        if b & (1 << i) and not (a & 1 << i) :
            return 0
    return 1

r = 0
for i in xrange(64) :
    nb_same_set_bits = 0
    for j in xrange(8) :
        nb_same_set_bits += has_same_set_bits(qword, qwordTable[i][j])
    if nb_same_set_bits & 1 :
        r |= 1 << i

if r == 0x55BDEC8E23A0EF32 :
    print "Good Boy"
else :
    print "BadBoy"
Figure 12: Verification of the mutated qword (Python 2.7)

To dump the qwordTable, we use the following simple IDA python script:
from pprint import pprint
from idc import Qword
qwordTable = []
for i in xrange(64) :
  t = []
  for j in xrange(8) :
    t.append(Qword(0x560128 + i*8*8 + j*8))
  qwordTable.append(t)
pprint(qwordTable)
Figure 13: Code used to dump the table of qwords in IDA (Python 2.7)

It may exists an elegant solution for this problem but we didn't find it and we wanted to solve the crack-me as fast as possible so we decided to use the Microsoft Theorem Prover: Z3. It has a nice Python API, good reviews, free and easy to use; it is the perfect tool for this problem.
All we have to do is translate the different operations performed on the serial into Z3 equations and let Z3 find the answer for us.
Integers became bit vectors, different possible values are translated in OR equations. The following code gives a valid serial in less than 2 minutes:
check_v = 0x55BDEC8E23A0EF32
init_v = 8828098094971975552

bitvectors = [BitVecVal(init_v, 64)]
solver = Solver()

for i in xrange(12) :
  bitvectors.append(BitVec('x_%d'%i, 64))

key = []
for i in xrange(12) :
  key.append(Int("k%d"%i))


for i in xrange(1, 13) :
  eq = False
  for j, k in enumerate([1, 30, 59, 24, 53, 18, 47, 12, 41, 6, 35, 0, 29, 58, 23, 52]) :
    sub_eq = (key[i-1] == j)
    bv = (bitvectors[i-1] ^ BitVecVal(1 << k, 64))
    bit = 0
    for l in xrange(64) :
      if 7069181668496654033 & (1 << l) :
        bit = (LShR(bv, l) & 1) ^ bit
    sub_eq = And(sub_eq, bitvectors[i] == ((bv << 1) | bit))
    eq = Or(eq, sub_eq)
  solver.append(eq)

for i, t in enumerate(tt) :
  bit = 0
  for v in t :
    has_same_set_bits = 1
    for j in range(64) :
      if v & (1 << j) :
        has_same_set_bits = has_same_set_bits & (LShR(bitvectors[12], j) & 1)
    bit ^= has_same_set_bits
  if check_v & (1 << i) :
    solver.add(bit == 1)
  else : 
    solver.add(bit == 0)
 
solver.check()
solution = solver.model()
r = ""
for i in xrange(12) :
  r += "%X"%int(str(solution[key[i]]))

print "serial2 :"
print r
Figure 14: Code used to find a valid serial for the second part of the crack-me (Python 2.7)

It is faster to find a solution when boolean values are directly used instead of bit vectors (~30 sec versus ~100 sec) but it is also a little bit more tricky, the code doing this is given in the complete keygen source provided in Annex.
Different variations of the code gave us 3 different serials: 94A0353FA32B, 2BA52E7FAC23 and 966132348323.

5.  Conclusion

This crack-me intelligently mixed crypto, exploitation and use of specific tools, it wasn't too easy nor too hard for this kind of time constraint challenge and really interesting.
We want to thank ESET and all the people who participate to this challenge, both coders and organizers!

6.  Annex

import sys
from random import SystemRandom
from base64 import b64encode
try :
  from whirlpool import Whirlpool
except :
  print "To work this keygen need the Whirpool implementation located here : http://www.bjrn.se/code/whirlpoolpy.txt"
  sys.exit(0)

sec_rnd = SystemRandom()

print "name :"
name = sys.stdin.readline().rstrip("\r\n")
hash_name = [ord(c) for c in Whirlpool(name+("ESETNOD32@"*8)[len(name):]).digest()]

def step1(k, i, j, to_set, to_keep) :
  global SOLUTION
  if i > 63 :
    if not to_set :
      return k
    return None
  if to_set :
    to_set_cpy = list(to_set)
    sec_rnd.shuffle(to_set_cpy)
    for choice, (idx, v) in enumerate(to_set_cpy) :
      if k[i] == v :
        r = step2a(idx, k, i, j, to_set_cpy[:choice] + to_set_cpy[choice+1:] , to_keep)
        if r is not None :
          return r
      elif k[i] is None :
        k[i] = v
        r = step2a(idx, k, i, j, to_set_cpy[:choice] + to_set_cpy[choice+1:] , to_keep)
        if r is not None :
          return r
        k[i] = None

  r = step2b(k, i, j, to_set, to_keep)
  if r is not None :
    return r
  return None


def step2a(idx, k, i, j, to_set, to_keep) :
  c = k[i] % 80
  kc = k[c]
  if kc is None :
    if (idx - j)%80 in to_keep :
      return None
    kc = (idx - j)%80
    while kc < 0x100 :
      k[c] = kc
      to_keep.add(idx)
      r = step3(k, i, idx, to_set, to_keep)
      to_keep.remove(idx)
      if r is not None :
        return r
      kc += 80
    k[c] = None
  elif (kc + j)%80 == idx :
    to_keep.add(idx)
    r = step3(k, i, idx, to_set, to_keep)
    to_keep.remove(idx)
    return r
  else :
    return None


def step2b(k, i, j, to_set, to_keep) :
  c = k[i]
  if c is None :
    vals = [c for c in xrange(0x100) if k[c%80] is not None and (k[c%80] + j)%80 not in to_keep]
    sec_rnd.shuffle(vals)
    for c in vals :
      k[i] = c
      r = step3(k, i, (k[c%80] + j)%80, to_set, to_keep)
      if r is not None:
        return r
    vals = [c for c in xrange(0x100) if k[c%80] is None]
    sec_rnd.shuffle(vals)
    for c in vals :
      k[i] = c
      c = c % 80
      vals2 = [kc for kc in xrange(0x100) if (kc + j)%80 not in to_keep]
      sec_rnd.shuffle(vals2)
      for kc in vals2 :
        k[c] = kc
        r = step3(k, i, (kc + j)%80, to_set, to_keep)
        if r is not None :
          return r
      k[c] = None
    k[i] = None
  else :
    c %= 80
    kc = k[c]
    if kc is None :
      vals = [kc for kc in xrange(0x100) if (kc + j)%80 not in to_keep]
      sec_rnd.shuffle(vals)
      for kc in vals :
        k[c] = kc
        r = step3(k, i, (kc + j)%80, to_set, to_keep)
        if r is not None :
          return r
      k[c] = None
    elif (kc + j)%80 not in to_keep :
      return step3(k, i, (kc + j)%80, to_set, to_keep)
  return None

def step3(k, i, j, to_set, to_keep) :
  k[i], k[j] = k[j], k[i]
  r = step1(k, i+1, j, to_set, to_keep)
  if r is not None :
    r[i], r[j] = r[j], r[i]
    return r
  k[i], k[j] = k[j], k[i]
  return None

egg = "ElV++ESET++="
egg_d = egg.decode("base64")

# fight against sexism in keygens !
# use B16B00B2 and B16BA112 with equal probability !
import struct
egg_d = (struct.pack("<I", 0xB16B00B2) if sec_rnd.randint(0, 1) else struct.pack("<I", 0xB16BA112)) + egg_d

padd = 64 - len(egg_d)
list_egg = [hash_name[padd+i]^hash_name[::-1][padd+i]^ord(c) for i,c in enumerate(egg_d)]

k = [None]*padd+list_egg+[0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x40, 0x17, 0x40, 0x00]
to_set = [(0x44, 0xA), (0x45, 0xB), (0x46, 0xC), (0x47, 0xD), (0x4C, 0x20)]
to_keep = set((0x4D, 0x4E, 0x4F))

s = step1(k, 0, 0, to_set, to_keep)


for i in xrange(len(s)) :
  if s[i] is None :
    s[i] = sec_rnd.randint(0, 0xFF)

serial = "".join(chr(i) for i in hash_name[::-1])
serial += "".join(chr(a^b^c) for a, b, c in zip(hash_name, hash_name[::-1], s))
serial = serial.encode("base64").replace("\n","")
# multiple encoding are valid for the same value because some bits are ignored for the last symbol
serial = serial[:-len(egg)]+egg

print "serial 1 :"
print serial



tt = [
    [0x4, 0x91, 0xF9, 0x48, 0x13, 0xC3, 0x4A, 0x89],
    [0x80000, 0x30E099, 0xE36C82, 0x35CFAB, 0x94B829, 0x621DF1, 0x413F79, 0xD28998],
    [0x8, 0xB5, 0x57, 0xB0, 0xB1, 0x80, 0x47, 0x83],
    [0x200000000, 0xB5D4CE18F3, 0x8CFB75A1FA, 0x1CC4345974, 0x244C876646, 0xF1D67A37BD, 0x567DCE8EF, 0x71D88A2C6B],
    [0x10000000, 0xEAA5839, 0x869CBEB, 0x72D6F13, 0x1AD663, 0xFEC707, 0x248AFA8, 0x681CB52],
    [0x10, 0xA5, 0x6, 0x24, 0x29, 0x4D, 0xD, 0x8C],
    [0x8000000000000, 0xF0AFDA2F1F6319, 0x54DC6F31E1DFD7, 0x2161D2BE0CC29F, 0xF3799D9A17CB9F, 0xE2B0EC0B44A77D, 0x548E26B440C7E0, 0x9362066CC80EA5],
    [0x80, 0x4E, 0x2C, 0x75, 0x6C, 0x13, 0x67, 0x4B],
    [0x100, 0x5D, 0xE0, 0x5F, 0x5, 0xEC, 0x67, 0x6F],
    [0x800000000000000, 0x12BBC3C5DC54A38, 0x1CCD3437BF476CF, 0x75007C44E58937F, 0x21467EFC8A2F4FC, 0x1E98C57A31D1F52, 0x28CF95332617839, 0x56470EDC082144B],
    [0x200, 0x5F, 0x1C, 0x15, 0x5C, 0x1BA, 0x1D7, 0x24],
    [0x400, 0x13, 0x346, 0x152, 0x1FA, 0x35, 0xD0, 0x1EB],
    [0x800, 0x23B, 0x12A, 0x6D0, 0x180, 0x5A8, 0x166, 0x128],
    [0x8000000000, 0x2DFE120B8D, 0xDA2A736E, 0x49EA2BE641, 0x34D402DC99, 0x72F9F7DD9, 0x139B938691, 0x33650D8FAE],
    [0x1000, 0xF30, 0xCCD, 0x627, 0xC24, 0x34E, 0x944, 0x72],
    [0x1000000000000, 0xAA710830103040, 0xF8D9876FA33FAD, 0xE0872B7C409D25, 0x6C502ADD44EE49, 0x26A17C61A87597, 0x786F944EF0E02B, 0x9C476E3E0C8170],
    [0x2000, 0x1E4, 0xFB1, 0x1CE3, 0x1F19, 0x1923, 0x5B5, 0x1E7F],
    [0x4000, 0x13C6, 0x313D, 0x20E0, 0x17B6, 0x3E4, 0x313, 0x3FD5],
    [0x8000, 0xC5D, 0x14AB, 0x4F1F, 0x4E79, 0x30AE, 0x1408, 0x3E1F],
    [0x20000000000000, 0x5F8E3FF36DF7F1, 0x8D426F89260E03, 0x51A2E96DD21274, 0x6FE4A7A21C27C, 0xC60CA2A303E8AA, 0x4C88C6467883BB, 0x14D7CC45303AD5],
    [0x10000, 0x94241F, 0x40C7E0, 0x369CC6, 0x5E1262, 0x9CCF74, 0xE02BD5, 0x82E8AF],
    [0x20, 0xC2, 0x1B, 0x4B, 0x9E, 0x53, 0xD6, 0x17],
    [0x20000, 0x525F3, 0x3C9E72, 0x5050A4, 0x352151, 0xC18A91, 0x19853E, 0xF464AB],
    [0x100000, 0x279902, 0x495CA9, 0x2EAA39, 0x548EE, 0x4A118C, 0xED5F6E, 0xE212B],
    [0x200000, 0xD5F694, 0x118702, 0x1A1231, 0x14F6D0, 0x4655E2, 0xD0AC93, 0xB53B1],
    [0x400000, 0x41F14, 0x16F3C4, 0x8325F9, 0x932B7E, 0x900661, 0x23B3C8, 0x84205E],
    [0x800000, 0x27F59, 0x253D0F, 0x3E894F, 0x15BB39, 0x5F3F45, 0x1BFE85, 0x771B46],
    [0x8000000000000000, 0x82B96333035C10D, 0x7EA90FA43B6895B, 0xE781F2DBD9A06C, 0x1A037D0D66205D1, 0xE0978719A7CA63F, 0x6DFECA3318A6418, 0x6004A0795E97EA6],
    [0x2, 0xB9, 0x79, 0xBC, 0x7D, 0x15, 0x60, 0x99],
    [0x1000000, 0xD7F434, 0x89EB3C, 0xD686FE, 0xB97BF3, 0xBF565E, 0xCD9C32, 0xD5F19C],
    [0x200000000000000, 0xD62782672B659B, 0x14AC89D5C0A4573, 0x1F24B67DC7065FE, 0x5BFBCAF9A26B49, 0x162670BAA8BFA51, 0x1F7D42DD6D0AEC0, 0x12A21173E4BCB43],
    [0x2000000, 0xA0FA2E, 0x7E221F, 0x5B4103, 0x163DF66, 0x161AC76, 0x1667E40, 0xE9DFCB],
    [0x400000000000, 0x2A635474528D, 0x272CA2F78E85, 0xD26BD767F6B, 0x2D5EFD63966D, 0x135444427BE2, 0xE49E6C649CC, 0x21FD11A032BC],
    [0x4000000, 0x908322, 0x2D298B7, 0x1F5997, 0x79F0F1, 0x4BF061, 0x3B297C, 0x5B302C],
    [0x8000000, 0x5D448D4, 0x283B776, 0x3145A19, 0x45C465, 0x69FF572, 0x7DEB365, 0x1F9214E],
    [0x40000000, 0x192780D6, 0x2602A107, 0x13D0B078, 0x5C1351B, 0x2C436E84, 0xC8CF063, 0xA9A768F],
    [0x100000000, 0x3069175096, 0xD28269BB14, 0x8727E70B5, 0xDA536BD5D8, 0xFA6622E8E6, 0xF696CD6F4A, 0xB8CC79C636],
    [0x400000000, 0x43CC6D6C11, 0x9985B620E1, 0x8371C3A17, 0xBF670C33E, 0x806F4C464C, 0xB3383CE8B8, 0x822B885E10],
    [0x800000000, 0xE65F7DC327, 0xD23F20538E, 0x739967CF65, 0x16A89332D3, 0xA7991DB287, 0x40C74ED44F, 0x267C979686],
    [0x1000000000, 0x672D1A4176, 0x46F68AFEA2, 0x630665DBEC, 0xB4C085042, 0xCA7B912349, 0xA160ABD0A9, 0xCEC4B1E85E],
    [0x2000000000, 0xDE6F99715E, 0x8DE175C718, 0x9E36A8FBDA, 0xCE7649EC86, 0xE09F1092E, 0x8B0C17265, 0xDE1EEB0098],
    [0x4000000000, 0x3E37655239, 0xB8FFE5C49C, 0x95933F33D4, 0x38116C3E52, 0xBCAA64600C, 0x9B25DCCF0B, 0x89B17E2C],
    [0x10000000000, 0xDED71D5774, 0x3D9408E914, 0xB656D2F967, 0xB0C1CADF8F, 0x43BED6FA3D, 0x4BB0D9A451, 0x76955E0E7D],
    [0x20000000000, 0x5EAA80228A, 0x1F52F9E791D, 0x118BEB16970, 0x18F440E8778, 0x5DAD750C98, 0x1495CA088A7, 0xC6C2939013],
    [0x40000000000, 0xF4930D48E2, 0x38F51A4F94C, 0x3B72170BF59, 0x2872194C90C, 0x16FBC07A0FC, 0x3071BC4ADF6, 0x382FCF15CEC],
    [0x80000000000, 0x1C16C0D3F60, 0x2EA439BCB99, 0x4191CC0D086, 0x37EEFFDEC7, 0x1399B07940A, 0xE45E1ABC7F, 0x1805AA9CAA1],
    [0x1, 0xF0, 0x28, 0xCC, 0xB6, 0xD4, 0x12, 0x6],
    [0x100000000000, 0xC8F4FAEBDA4, 0xEBB413F2E37, 0xAC83562BC6C, 0x67713E39976, 0xFD5EEDAD058, 0x82D23735526, 0xCDFB1BC0DDB],
    [0x200000000000, 0x11D42C06F1B6, 0x1D1E2E6E6223, 0x5539E7B941C, 0x758A21E70EC, 0xEE3DF953186, 0xEF69F8EE3DC, 0x1ECD77876261],
    [0x800000000000, 0x200EBD4E62C8, 0x7885CD4584EE, 0x46E59ADA811, 0xB2F58DD756, 0x5F0889BEDD0D, 0x73DF76190650, 0x71DBD1F160D1],
    [0x2000000000000, 0x91362730A633C, 0xB519E7BF5FDE90, 0xF51081D1D9B143, 0x40EA4B7E6C5451, 0x9157F00FE632B3, 0x7DB5001936A800, 0x406ED0911503C2],
    [0x4000000000000, 0x5AD2DB864D68D1, 0x5387794E71CA27, 0x70FA8BAB871825, 0x58B7D3F4C4A474, 0x516E13F447158A, 0xB9B97B38870596, 0x2B4B74A2131B83],
    [0x80000000, 0x6A2CA9CE, 0x5B80DEC2, 0x17FBFF2A, 0x28C7273D, 0x7874E025, 0xE9EAD5A, 0x252D552F],
    [0x40000, 0x7086CA, 0xA0454B, 0xA18229, 0x235B43, 0x48BAE2, 0x90895, 0x8B740E],
    [0x10000000000000, 0x6161E658A52B5C, 0xCA62896A2DAE8A, 0x242F88A65B2182, 0xE49F85CF3BC096, 0xE392473BBD42EF, 0x4A18407B9D7D6E, 0x678B046E512878],
    [0x40000000000000, 0xF2811DE1B800C, 0xA7CADAEBB2743E, 0x1DE2659F77B6AC, 0x74950E9C892BB, 0x2E8156532E957D, 0x2E0FD11665C7A5, 0x96024A554AE450],
    [0x40, 0x6, 0xB3, 0x80, 0x1F, 0xE, 0x82, 0x17],
    [0x80000000000000, 0x45F6DF933C25A, 0x4FBCEB9CC00CF9, 0x6575D1B9C230CA, 0x4173E8D140E239, 0x2B95CAA25E3D1D, 0x7DD021CE354D59, 0x1A868E5B651C44],
    [0x100000000000000, 0x73E560641E49A1, 0x14B3654EFEC16A, 0xC20A1CE5BF5431, 0xE8AB16961A64DC, 0xFC5AAA602EC41D, 0xD9CC3B32395B96, 0xE28C9F38890F0E],
    [0x400000000000000, 0x5522500389A628, 0x2694003EF575A86, 0x13B9F036A0696A3, 0x1937BCEFB1621B, 0x200DFB8F91A8BB2, 0xBE6492FF025656, 0x202789F0C72B4FF],
    [0x1000000000000000, 0x77AF02D6AB1DF3, 0x5659C5086E42E63, 0x284131A456DFD8E, 0xDB26FBB380976AC, 0xB175241CFECC18C, 0x660F1EFB8A20487, 0xFFFD90B934B8DF9],
    [0x2000000000000000, 0x5B4C5AFA91EA2FC, 0xC781F620485C8B8, 0x1068D041963FF5A9, 0xAF1DABA44341845, 0x46577187503AD18, 0x1DAF83ACD5EBB96, 0x3DD97CE4685E29C],
    [0x20000000, 0xEF4482F, 0x312765, 0x1A9BA833, 0xFE451C9, 0x6397B17, 0x16503A30, 0x12A2E425],
    [0x4000000000000000, 0x1097C1A8ACE792F7, 0x5778AD02765668, 0x9B685219B53BA6, 0x9652BF15909839E, 0x10B409F5185E0CC5, 0xE644B8167B5D108, 0x1CDFEA6425690E7]
]

check_v = 0x55BDEC8E23A0EF32
init_v = 8828098094971975552

try :
  from z3 import *
except :
  print "unable to load Z3, here is a pre calculated serial 2 :"
  print "966132348323"
  sys.exit(0)

from time import time
start_time = time()

def Xor(a,b) :
  return Or(And(a,Not(b)), And(Not(a), b))

bits = []
solver = Solver()

for i in xrange(13) :
  bs = []
  for j in xrange(64) :
    bs.append(Bool("b%02d%02d"%(i, j)))
  bits.append(bs)

key = []
for i in xrange(12) :
  key.append(Int("k%d"%i))

for i in xrange(64) :
  if init_v & (1 << i) :
    solver.append(bits[0][i])
  else :
    solver.append(Not(bits[0][i]))

for i in xrange(1, 13) :
  eq = False
  for j, k in enumerate([1, 30, 59, 24, 53, 18, 47, 12, 41, 6, 35, 0, 29, 58, 23, 52]) :
    sub_eq = (key[i-1] == j)
    for l in xrange(63) :
      if l != k :
        sub_eq = And(sub_eq, bits[i][l+1] == bits[i-1][l])
      else :
        sub_eq = And(sub_eq, bits[i][l+1] == Not(bits[i-1][l]))
    sub_sub_eq = False
    for l in xrange(64) :
      if 0x621AC745FB723ED1 & (1 << l) :
        sub_sub_eq = Xor(sub_sub_eq, bits[i][l+1])
    sub_eq = And(sub_eq, bits[i][0] == sub_sub_eq)
    eq = Or(eq, sub_eq)
  solver.append(eq)



for i, t in enumerate(tt) :
  bit = True if check_v & (1 << i) else False
  eq = False
  for v in t :
    has_common_bit = True
    for j in range(64) :
      if v & (1 << j) :
        has_common_bit = And(has_common_bit, bits[12][j])
    eq = Xor(eq, has_common_bit)
  if not bit :
    eq = Not(eq)
  solver.add(eq)

solver.check()
solution = solver.model()
r = ""
for i in xrange(12) :
  r += "%X"%int(str(solution[key[i]]))

print "serial 2 :"
print r

print
print "(%.02f seconds)"%(time() - start_time)

Figure 15: Complete source of the keygen (Python 2.7)

2 commentaires:

  1. Add: key 2 may be 93A52ECFAC23

    RépondreSupprimer
    Réponses
    1. There are 11 different keys 2 for this task. For example: 5ba52b7fac23 , ...
      AVictor2010@gmail.com

      Supprimer