Solution to realism.py that uses z3

realism.py

'''
Solution to the realism challenge from CSAW'17 Quals.
https://github.com/isislab/CSAW-CTF-2017-Quals/tree/master/rev/realism
'''
from z3 import *

s = Solver()

# This is a simplification of the array of bytes found at 0x7D90:
# 0xff => 1, 0x00 => 0; where 1 means "include this value in the psadbw sum"
# and 0 means "exclude it".
# Endian-adjusted.
sliding_window = [1] * 8 + ([0] + [1] * 7) * 2

# This is the array of values that the program checks to see if we've got it
# right or not.
compare_array = [
	0x02110270,
	0x02290255,
	0x025E0291,
	0x01F90233,
	0x027B0278,
	0x02090221,
	0x0290025D,
	0x02DF028F,]

# movaps xmm0, xmmword ptr ds:1238h
# (Using 16-bit BitVectors because I'm lazy and this is easier for psadbw.
# Pretend that they're 8-bit vectors for all practical purposes.)
xmm0_base = [BitVec('xmm0_%i' % i, 16) for i in range(16)[::-1]]
for char in xmm0_base:
	s.add(char >= 0x20)
	s.add(char < 127)

# movaps xmm5, xmmword ptr ds:loc_7C00
xmm5 = [ord(c) for c in "B81300CD100F20C083E0FB83C8020F22".decode("hex")[::-1]]

# pshufd  xmm0, xmm0, 1Eh
def xmm0_slice(i):
	i = 3 - i
	return xmm0_base[i*4:(i+1)*4]
xmm0 = xmm0_slice(0) + xmm0_slice(1) + xmm0_slice(3) + xmm0_slice(2)

# mov si, 8
## (label, loop around si)
for i in range(8,0,-1):
	# movaps xmm2, xmm0
	# andps xmm2, xmmword ptr [si+7D90h]
	xmm2 = []
	mask = sliding_window[i:i+16][::-1]
	for xmm0_byte, mask_val in zip(xmm0, mask):
		xmm2.append(xmm0_byte if mask_val else 0)
	
	# psadbw xmm5, xmm2
	psadbw = []
	for j in range(16):
		diff = xmm5[j] - xmm2[j]
		if isinstance(diff, int):
			psadbw.append(abs(diff))
		else:
			psadbw.append(If(diff >= 0, diff, -diff))
	
	xmm5 = []
	sums = [sum(psadbw[:8]), sum(psadbw[8:])]
	for sum_ in sums:
		xmm5 += [0] * 6 + [sum_ >> 8, sum_ & 0xff]
	
	# movaps xmmword ptr [temp_space], xmm5
	# mov di, word ptr [temp_space]
	# shl edi, 16
	# mov di, word ptr [temp_space + 8]
	edi = [sums[1] >> 8, sums[1] & 0xff, sums[0] >> 8, sums[0] & 0xff]
	
	# mov dx, si
	# dec dx
	# add dx, dx
	# add dx, dx
	# cmp edi, [edx + results]
	test_bytes = [compare_array[i - 1] >> shift & 0xff for shift in (24, 16, 8, 0)]
	for symbolic, concrete in zip(edi, test_bytes):
		s.add(symbolic == concrete)

print s.check()
model = s.model()
print "flag" + "".join(chr(model[c].as_long()) for c in xmm0_base[::-1])