amit94 solution to babymarvel mangle function

babymarvel_z3.py

from pwn import *
from z3 import *
 
def demangle(s):
    pad0 = [0xeb, 0x88, 0x27, 0x41, 0x90, 0x1e, 0x33, 0x51, 0x98, 0x2b,
         0x13, 0x57, 0x18, 0x32, 0x15, 0x17, 0x23, 0x16, 0x41, 0x35,
         0x25, 0x31, 0x045, 0x76, 0x0a, 0xa5, 0xcc, 0x81, 0xa0, 0x6b,
         0xd4, 0x15];
    pad1 = [7424712, 4551408,
                             8364500, 2965602, 2274639, 10661532,
                             11743595, 9478365, 5391897, 2014058,
                             9564604, 1930344, 7799217, 1852881,
                             6948032, 10182462, 1859234, 4734335,
                             6908536, 7021645, 10826047, 1851655,
                             3352213, 9091305, 7611253, 2920969,
                             7981175, 9321276, 2975866, 2423065,
                             11973828, 10777299];
 
    orig = [ord(x) for x in s.decode('hex')]
    for i in range(32):
        orig[i] ^= pad0[pad1[(i + 7) % 32] % 32];
        orig[i] -= pad0[pad1[(i + 12) % 32] % 32];
        orig[i] = (orig[i] + 256) % 256
 
    inp = [BitVec('inp_' + str(i), 8) for i in range(32)]
    s = Solver()
    for i in range(32):
        companion = (i + 1) % 32;
        res = (inp[i] & 0xf0) | (inp[companion] & 0xf);
        s.add(res == orig[i])
    s.check()
    m = s.model()
    fin = [m[inp[i]].as_long() for i in range(32)]
    for i in range(32):
        fin[i] ^= pad0[i]
        fin[i] -= pad0[i]
        fin[i] = (fin[i] + 256) % 256
    fin_str = ''.join([chr(x) for x in fin]).encode('hex')
    return fin_str