Using Z3 to model the Instructions

Author: [0xec](https://twitter.com/0xec_)

```
# Author: 0xec
# https://0xec.blogspot.com/
# https://twitter.com/0xec_
from z3 import *

def dword_from_bytes(b):
return Concat(b[3], b[2], b[1], b[0])

def swap_endian(b):
b3 = Extract(31, 24, b)
b2 = Extract(23, 16, b)
b1 = Extract(15, 8, b)
b0 = Extract(7, 0, b)
return Concat(b0, b1, b2, b3)

def main():
flag = [BitVec('c' + str(i), 8) for i in range(16)]
shuffle = [2, 6, 7, 1, 5 , 0xb, 9, 0xe, 3, 0xf, 4, 8, 0xa, 0xc, 0xd, 0]

# pshufb xmm0, xmmword [rel SHUFFLE]
output = list(map(lambda x: flag[x], shuffle))

p3 = dword_from_bytes(output[0:4])
p2 = dword_from_bytes(output[4:8])
p1 = dword_from_bytes(output[8:12])
p0 = dword_from_bytes(output[12:16])

# paddd xmm0, xmmword [rel ADD32]
p3 = (p3 + 0xdeadbeef)
p2 = (p2 + 0xfee1dead)
p1 = (p1 + 0x13371337)
p0 = (p0 + 0x67637466)

output = Concat(swap_endian(p3),
swap_endian(p2),
swap_endian(p1),
swap_endian(p0))

xor_bytes = [0x76, 0x58, 0xb4, 0x49, 0x8d, 0x1a, 0x5f, 0x38, 0xd4, 0x23, 0xf8, 0x34, 0xeb, 0x86, 0xf9, 0xaa]

# pxor xmm0, xmmword [rel XOR]
xor_val = int.from_bytes(bytearray(xor_bytes), byteorder="big")
output = output ^ xor_val

s = Solver()

for i in range(16):
high = ((16 - i) * 8) - 1
low = ((16 - i) * 8) - 8
s.add(flag[i] == Extract(high, low, output))

s.add(flag[0] == ord('C'))
s.add(flag[1] == ord('T'))
s.add(flag[2] == ord('F'))
s.add(flag[3] == ord('{'))

if s.check() == sat:
m = s.model()
print(bytes(map(lambda x: m[x].as_long(), flag)).decode())

if __name__ == '__main__':
main()
```

### Output

```
$ python3.7 solve.py
CTF{S1MDf0rM3!}
```