TSG LIVE! 9 Reversing

fuck.py

from ptrlib import *
from z3 import *

"""
typedef struct {
  char key[0xb0];
  char iv[0x10]; // +B0h
  char flag[0x100];
};
"""
with open("problem", "rb") as f:
    f.seek(0x20c0)
    enc = f.read(0x40)
with open("fuck", "rb") as f:
    f.seek(0x60e0)
    enc = f.read(0x40)

def blah(c):
    return ((27 * LShR(c, 7)) ^ (2 * c)) & 0xff

def get_models(solver, num_models):
    n = 0
    while n < num_models and solver.check() == sat:
        try:
            model = solver.model()
            n += 1
            yield model
            block = []
            for declaration in model:
                c = declaration()
                block.append(c != model[declaration])
            solver.add(Or(block))
            solver.push() # save some work, dont redo the work done so far
        except KeyboardInterrupt: # got bored waiting?
            print("interrupted")
            break

sbox = flat([
    0x2073692073696854, 0x0079656b20656874,
    0x2c79b7380c0ade18, 0x0c65ba270c1cdf4c,
    0xec8d24d6c0f493ee, 0xecf441bde091fb9a,
    0x56b708bfba3a2c69, 0x5ad2b298b626f325,
], map=p64)

def rev_blk(vec):
    c1 = BitVec('c1', 8)
    c2 = BitVec('c2', 8)
    c3 = BitVec('c3', 8)
    c4 = BitVec('c4', 8)
    s = Solver()
    s.add(c2^c3^c4^blah(c1^c2) == vec[0])
    s.add(c1^c3^c4^blah(c2^c3) == vec[1])
    s.add(c1^c2^c4^blah(c3^c4) == vec[2])
    s.add(c1^c2^c3^blah(c4^c1) == vec[3])
    for m in get_models(s, 1):
        print(m)
        vec = bytes([m[c1].as_long(), m[c2].as_long(), m[c3].as_long(), m[c4].as_long()])
    return vec

flag = b""
for v in range(4):
    vec = enc[v*0x10:(v+1)*0x10]
    print(vec)
    vec = xor(vec, sbox[0x30:0x40])
    for j in range(2, 0, -1):
        for i, block in enumerate(chunks(xor(vec, sbox[j*0x10:(j+1)*0x10]), 4)):
            b = rev_blk(block)
            vec = list(vec)
            vec[i*4+0] = b[0]
            vec[i*4+1] = b[1]
            vec[i*4+2] = b[2]
            vec[i*4+3] = b[3]
            vec = bytes(vec)
        print(vec)
    vec = xor(vec, sbox[0x00:0x10])
    flag += vec

iv = b"This is the iv."
for i in range(4):
    print(xor(flag[i*0x10:(i+1)*0x10], iv).decode(), end="")
    iv = enc[i*0x10:(i+1)*0x10]