2019YISF-quals-misc100.py

from z3 import *
from pwn import *

p = remote('218.158.141.199',24763)
s = Solver()
x = [Int('x%i'%i)for i in range(12,130)]
y = [Int('y%i'%i)for i in range(12,130)]
x1 = [Int('x1%i'%i)for i in range(12,130)]
y1 = [Int('y1%i'%i)for i in range(12,130)]
x2 = [Int('x2%i'%i)for i in range(12,130)]
y2 = [Int('y2%i'%i)for i in range(12,130)]

p.recvuntil('<Quiz Start>\n')
for i in range(100):
	print "[*]"+str(i)
	li = []
	print p.recvuntil('Step :  ' + str(i+1) + "\n\n")
	a = p.recvline()
	print a
	tmp1 = a.split(' ')
	b = p.recvline()
	print b
	tmp2 = b.split(' ')
	c = p.recvline()
	print c
	tmp3 = c.split(' ')
	s.add(int(tmp1[0]) * x[12+i] + int(tmp1[3]) * y[12+i] == int(tmp1[6].replace("\n","")))
	s.add(int(tmp2[0]) * x[12+i] + int(tmp2[3]) * y[12+i] == int(tmp2[6].replace("\n","")))
	s.check()
	m = s.model()
	li.append(int(str(m.evaluate(x[i+12]))))
	li.append(int(str(m.evaluate(y[i+12]))))

	s.add(int(tmp1[0]) * x1[12+i] + int(tmp1[3]) * y1[12+i] == int(tmp1[6].replace("\n","")))
	s.add(int(tmp3[0]) * x1[12+i] + int(tmp3[3]) * y1[12+i] == int(tmp3[6].replace("\n","")))
	s.check()
	m = s.model()
	li.append(int(str(m.evaluate(x1[i+12]))))
	li.append(int(str(m.evaluate(y1[i+12]))))

	s.add(int(tmp2[0]) * x2[12+i] + int(tmp2[3]) * y2[12+i] == int(tmp2[6].replace("\n","")))
	s.add(int(tmp3[0]) * x2[12+i] + int(tmp3[3]) * y2[12+i] == int(tmp3[6].replace("\n","")))
	s.check()
	m = s.model()
	li.append(int(str(m.evaluate(x2[i+12]))))
	li.append(int(str(m.evaluate(y2[i+12]))))
	print li
	payload=(abs((li[0]*li[3]+li[2]*li[5]+li[4]*li[1]) - (li[2]*li[1]+li[4]*li[3]+li[0]*li[5])))*0.5
	print payload
	p.sendlineafter('Input :',str(payload))

p.interactive()