google_ctf2020_RCE-beginner

发表于 分类于 阅读次数： Valine：
本文字数： 4.1k 阅读时长 ≈ 4 分钟

google_ctf

RCE beginner

z3有用的链接：

我想用z3来解决问题，但是不熟悉，很多操作不会，直接GG
使用z3解决的wp 我参考了这篇，熟悉了API（Contact(),Extract(),小学了下python，变量只用声明一个就行，我声明的太多了，后面的+，xor操作完全不成功。

list(map(lambda i:flag[i], new_pshufb))

int.from_bytes(bytearray(new_xor), byteorder="big")将序列直接变成了整数

程序主要将输入进行三个操作：SHUFFLE, ADD32, XOR
最后进行条件判断
DprQNd.jpg
这是数据在内存中的排列布局；
0x7fffffffddf0 是输入值 adcdefg12345678

下面是参考的代码，注释部分是我写的代码：

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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
    #!/usr/bin/python3


from z3 import *
import binascii


def dword_from_bytes(b):
    # Create a Z3 bit-vector concatenation expression.串联表达式。
    return Concat(b[3],b[2],b[1],b[0])

def swap_endian(b):
    #simplify(Extract(StringVal("abcd"),2,1)) "c"
    '''从0计数，调整为位序，
    最先ef be ad 现在是 ad be ef最后
    76 58 b4 
    extract(7,0) 就是将最后8位调前
    '''
    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():


    print("give me a bottle of rum!")
    '''dou kan cheng 128 bit'''
    flag = [BitVec('c'+str(i), 8) for i in range(16)]

    # dest = []
    pshufb = '000D0C0A08040F030E090B0501070602'
    new_pshufb = []
    # new_dest = []

    for i in range(0, len(pshufb), 2):
        new_pshufb.append(int(pshufb[i:i+2], 16))
    # new_pshufb.append(binascii.unhexlify(pshufb[i]+pshufb[i+1])[0])


    new_pshufb.reverse()
    print(new_pshufb)
    # new_pshufb = [IntVal(i) for i in new_pshufb]

    # dest = [Int('flag%d' % i) for i in range(16)]
    # new_dest = [Int('flag%d' % i) for i in range(16)]
    # pshufb  xmm0, xmmword [rel SHUFFLE]
    
    '''for i in range(16):
    if 0x80 == new_pshufb[i] & 0x80:
            And
            new_dest[i] = '00'
            else:
    new_dest[i] = (dest[new_pshufb[i].as_long() % 16])'''
    # python3 由于map()返回一个迭代器，因此我们使用了list()函数立即生成结果
    output=list(map(lambda i:flag[i], new_pshufb))

    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]
    '''add32 = '6763746613371337FEE1DEADDEADBEEF'
    new_add32 = []

    for i in range(0, len(add32), 2):
        new_add32.append(int(add32[i:i+2], 16))

    new_add32.reverse()
    new_add32 = [IntVal(i) for i in new_add32]
    for i in range(4):
    x=''
    y=''
    for j in range(4):
    x.join(format(new_add32[i*4+j].as_long(),'x'))
    y.join(format(new_dest[i*4+j],'x'))

    tmp=(BitVec(new_add32[i*4:i*4+4],32)+BitVec(new_add32[i*4:i*4+4],32))&BitVec(0xffffffffff,32)'''
    #定义上只有32位，所以不考虑进位
    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))
    
    '''tmp = (int(x, 16) +
    int(y, 16)) & 0xffffffff
    tmp = format(tmp, 'x')
    new4_dest = []
    for j in range(0, len(tmp), 2):
    new4_dest.append(int(tmp[j:j+2],16))
    new_dest[i*4:i*4+4] = new4_dest'''

    xor = 'AAF986EB34F823D4385F1A8D49B45876'
    new_xor = []

    for i in range(0, len(xor), 2):
        new_xor.append(int(xor[i:i+2],16))

    new_xor.reverse()
    #new_xor = [IntVal(i) for i in new_xor]
    # pxor    xmm0, xmmword [rel XOR]
    xor_val = int.from_bytes(bytearray(new_xor), byteorder="big")#big 表示大端序 即末尾放在高地址处 即顺序保持不变
    output = output ^ xor_val

    solver = Solver()
    '''final_dest = [Int('flag%d' % i) for i in range(16)]
    for (i, j) in zip(new_dest, new_xor):
    final_dest.append(format(i ^ j, 'x'))'''
    #solver.add(final_dest == dest)
    for i in range(16):
        high = ((16 - i) * 8) - 1 
        low = ((16 - i) * 8) - 8
        solver.add(flag[i] == Extract(high, low, output))    
        #最高位127~120 ， 表示第一个字节

    '''ctf = 'CTF{'
    for i in range(4):
    solver.add(chr(int(final_dest[i])) == ctf[i])'''
    solver.add(flag[0] == ord('C'))
    solver.add(flag[1] == ord('T'))
    solver.add(flag[2] == ord('F'))
    solver.add(flag[3] == ord('{'))


    if solver.check() == sat:
        m = solver.model()
        #s = []
        '''for i in range(16):
            s.append(m[dest[i]].as_long())'''
        print(bytes(map(lambda x: m[x].as_long(), flag)).decode())
        print('success')

if __name__=='__main__':
    main()

成功！
Dprsg0.jpg

还有用angr的，但我在机子上试了下都不成功