Pwn2Win2017 writeup

发表于 Disqus：

周末做了两道题，想尝试下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)