Pwn2Win2017 writeup

周末做了两道题,想尝试下ppc结果因为电阻间不同阻值只存了后面那个被坑了一整天……Orz

PPC-M

Resistance

列KVL,设起点电压10终点电压0,然后z3求解。主办方表示卧槽这题z3居然能做?比预期解慢,但是起码是对的_(:з)∠)_

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
#!/usr/bin/python2
import ssl, socket
import z3

y = [z3.Real('a_%d'%i) for i in range(30)]
d = dict()
connection = dict()
nodes = set()

class Connect(object):
def __init__(self, host, port):
self.context = ssl.create_default_context()
self.conn = self.context.wrap_socket(
socket.socket(socket.AF_INET),
server_hostname=host)
self.conn.connect((host, port))
self.f = self.conn.makefile('rwb', 0)
def __enter__(self):
return self.f
def __exit__(self, type, value, traceback):
self.f.close()

ncount = 0
with Connect('programming.pwn2win.party', 9001) as f:
#b = open('d.txt','w')
#with open('test.txt','rb') as f:
for line in f:
line = line.strip()
print('received: %s' % line)

if line.startswith(b'CTF-BR{') or \
line == b'WRONG ANSWER': break

numbers = map(int, line.split())
if len(numbers)==3:
if ncount==0:
d = dict()
connection = dict()
nodes = set()

nodes.add(numbers[0])
nodes.add(numbers[1])
ar = min(numbers[0],numbers[1]),max(numbers[0],numbers[1])
if ar not in d.keys():
d[ar] = [numbers[2]]
else:
d[ar].append(numbers[2])
if numbers[0] in connection.keys():
if numbers[1] not in connection[numbers[0]]:
connection[numbers[0]].append(numbers[1])
else:
connection[numbers[0]] = [numbers[1]]
if numbers[1] in connection.keys():
if numbers[0] not in connection[numbers[1]]:
connection[numbers[1]].append(numbers[0])
else:
connection[numbers[1]] = [numbers[0]]

ncount+=1

elif len(numbers) == 2:
ncount = 0
if numbers[0]==numbers[1]:
f.write('0.000\n')
print "0.000"
continue
#solve all KVL
s = z3.Solver()
for m in nodes:
sum = 0
if m!=numbers[0] and m!=numbers[1]:
for n in connection[m]:
for k in d[min(n,m),max(n,m)]:
sum += ((y[m] - y[n]) / k)
s.add(sum == 0.0)
s.add(y[numbers[0]]==10.0)
s.add(y[numbers[1]]==0.0)
s.check()
m = s.model()
#print m
flag = map(lambda sym: m[sym], y)
start = float(eval(str(flag[numbers[0]])+'.'))
sum=0
for n in connection[numbers[0]]:
for k in d[min(numbers[0],n),max(n,numbers[0])]:
sum+=(m[y[numbers[0]]]-m[y[n]])/k
sum = eval(str(z3.simplify(sum))+'.')
f.write(("%.3f\n"%(10.0/sum)).encode('utf-8'))
print "%.3f"%(10.0/sum)

Reversing

Achievement Unlocked

golang 写的,没啥好说的,z3解

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
import z3
ans_len = 30
y = z3.BitVecs(' '.join("a_%d"%i for i in xrange(ans_len)), 8)
x = [0]*ans_len
for i in range(ans_len):
x[i] = z3.ZeroExt(8,y[i])

s = z3.Solver()

a = [217, 6, 224, 68, 21, 153, 30, 144, 249, 89, 109, 245, 111, 55, 163, 40, 174, 21, 115, 99, 173, 42, 12, 209, 143, 226, 47, 136, 158, 158, 58, 77, 67, 84, 70, 45, 66, 82, 123, 84, 104, 105, 115, 95, 67, 48, 85, 108, 100, 95, 66, 51, 95, 52, 83, 95, 101, 97, 83, 121, 95, 52, 115, 95, 116, 104, 49, 83, 125, 10, 19, 152, 116, 104, 49, 83, 125, 10, 19, 152, 81, 237, 69, 212, 147, 42, 94, 184, 20, 227, 251, 168, 210, 97, 183, 36, 147, 236, 35, 65, 192, 16, 128, 188, 52, 149, 46, 138, 17, 251, 86, 163, 62, 195, 119, 228, 54, 102, 57, 36, 145, 140, 174, 140, 172, 177, 154, 104, 150, 90, 39, 38, 237, 31, 142, 48, 59, 159, 63, 113, 82, 37, 81, 227, 122, 33, 149, 58, 87, 62, 78, 112, 54, 230, 37, 243, 4, 116, 210, 236, 47, 178, 81, 162, 38, 87, 131, 170, 100, 119, 36, 176, 131, 91, 119, 31, 57, 195, 53, 107, 14, 58, 20, 68, 20, 246, 207, 24, 82, 216, 21, 189, 18, 121, 155, 211, 192, 5, 248, 127, 229, 253, 124, 116, 67, 78, 43, 111, 75, 168, 11, 144, 29, 36, 28, 203, 224, 184, 10, 84, 30, 100, 168, 142, 164, 142, 34, 220, 96, 173, 118, 173, 157, 49, 231, 219, 13, 49, 35, 13]
final = [208, 113, 230, 50, 15, 58, 9, 46, 248, 161, 182, 82, 222, 205, 101, 114, 82, 159, 79, 185, 244, 114, 118, 193, 52, 53, 238, 247, 218, 80]

for i in range(len(a)/8):
m = a[i*8:(i+1)*8]
for j in range(8):
x[i] = (1<<j)&m[j]^x[i]

for i in range(ans_len):
s.add(x[i]==final[i])

if s.check() == z3.sat:
m = s.model()
print m
flag = map(lambda sym: m[sym], y)
flag = map(lambda val: chr(int(str(val))), flag) # wtf
print len(flag)
print ''.join(flag)