angr and z3 for hackim18

Author Avatar
Xzhah 3月 16, 2018
  • 在其它设备中阅读本文章

###题目
之前看chamd5公众号里有篇小姐姐教你符号执行，控制不住自己点了进去，自己也正好练习练习z3和angr，核心内容就是解66个二元一次方程

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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
from z3 import *
flag=[BitVec('flag[%d]'%i,8)for i in range(68)]
s=Solver()
def get_models(s):
    while s.check() == sat:
        m = s.model()
        yield m
        s.add(Or([sym() != m[sym] for sym in m.decls()]))
s.add(And((flag[0] * flag[0]- 203 * flag[0] == -10296),(flag[2] * flag[2]- 203 * flag[2] ==-10296),
(flag[1] * flag[1]- 204 * flag[1] ==-10379),(flag[3] * flag[3]- 204 * flag[3] ==-10379),
(flag[2] * flag[2]- 204 * flag[2] ==-10395),(flag[4] * flag[4]- 204 * flag[4] ==-10395),
(flag[3] * flag[3]- 216 * flag[3] ==-11663),(flag[5] * flag[5]- 216 * flag[5] ==-11663),
(flag[4] * flag[4]- 154 * flag[4] ==-5145),(flag[6] * flag[6]- 154 * flag[6] ==-5145),
(flag[5] * flag[5]- 165 * flag[5] ==-6104),(flag[7] * flag[7]- 165 * flag[7] ==-6104),
(flag[6] * flag[6]- 172 * flag[6] ==-6027),(flag[8] * flag[8]- 172 * flag[8] ==-6027),
(flag[7] * flag[7]- 95*flag[7]==-2184),(flag[9] * flag[9]- 95*flag[9]==-2184),
(flag[8] * flag[8]- 210*flag[8]==-10701),(flag[10] * flag[10]- 210*flag[10]==-10701),
(flag[9] * flag[9]- 87*flag[9]==-1872),(flag[11] * flag[11]- 87*flag[11]==-1872),
(flag[10] * flag[10]- 174*flag[10]==-7569),(flag[12] * flag[12]- 174*flag[12]==-7569),
(flag[11] * flag[11]- 143*flag[11]==-4560),(flag[13] * flag[13]- 143*flag[13]==-4560),
(flag[12] * flag[12]- 206*flag[12]==-10353),(flag[14] * flag[14]- 206*flag[14]==-10353),
(flag[13] * flag[13]- 206*flag[13]==-10545),(flag[15] * flag[15]- 206*flag[15]==-10545),
(flag[14] * flag[14]- 238*flag[14]==-14161),(flag[16] * flag[16]- 238*flag[16]==-14161),
(flag[15] * flag[15]- 206*flag[15]==-10545),(flag[17] * flag[17]- 206*flag[17]==-10545),
(flag[16] * flag[16]- 238*flag[16]==-14161),(flag[18] * flag[18]- 238*flag[18]==-14161),
(flag[17] * flag[17]- 143*flag[17]==-4560),(flag[19] * flag[19]- 143*flag[19]==-4560),
(flag[18] * flag[18]- 238*flag[18]==-14161),(flag[20] * flag[20]- 238*flag[20]==-14161),
(flag[19] * flag[19]- 143*flag[19]==-4560),(flag[21] * flag[21]- 143*flag[21]==-4560),
(flag[20] * flag[20]- 206*flag[20]==-10353),(flag[22] * flag[22]- 206*flag[22]==-10353),
(flag[21] * flag[21]- 206*flag[21]==-10545),(flag[23] * flag[23]- 206*flag[23]==-10545),
(flag[22] * flag[22]- 174*flag[22]==-7569),(flag[24] * flag[24]- 174*flag[24]==-7569),
(flag[23] * flag[23]- 206*flag[23]==-10545),(flag[25] * flag[25]- 206*flag[25]==-10545),
(flag[24] * flag[24]- 208*flag[24]==-10527),(flag[26] * flag[26]- 208*flag[26]==-10527),
(flag[25] * flag[25]- 143*flag[25]==-4560),(flag[27] * flag[27]- 143*flag[27]==-4560),
(flag[26] * flag[26]- 238*flag[26]==-14157),(flag[28] * flag[28]- 238*flag[28]==-14157),
(flag[27] * flag[27]- 143*flag[27]==-4560),(flag[29] * flag[29]- 143*flag[29]==-4560),
(flag[28] * flag[28]- 221*flag[28]==-12168),(flag[30] * flag[30]- 221*flag[30]==-12168),
(flag[29] * flag[29]- 147*flag[29]==-4940),(flag[31] * flag[31]- 147*flag[31]==-4940),
(flag[30] * flag[30]- 222*flag[30]==-12272),(flag[32] * flag[32]- 222*flag[32]==-12272),
(flag[31] * flag[31]- 103*flag[31]==-2652),(flag[33] * flag[33]- 103*flag[33]==-2652),
(flag[32] * flag[32]- 213*flag[32]==-11210),(flag[34] * flag[34]- 213*flag[34]==-11210),
(flag[33] * flag[33]- 160*flag[33]==-5559),(flag[35] * flag[35]- 160*flag[35]==-5559),
(flag[34] * flag[34]- 147*flag[34]==-4940),(flag[36] * flag[36]- 147*flag[36]==-4940),
(flag[35] * flag[35]- 225*flag[35]==-12644),(flag[37] * flag[37]- 225*flag[37]==-12644),
(flag[36] * flag[36]- 156*flag[36]==-5408),(flag[38] * flag[38]- 156*flag[38]==-5408),
(flag[37] * flag[37]- 211*flag[37]==-11020),(flag[39] * flag[39]- 211*flag[39]==-11020),
(flag[38] * flag[38]- 219*flag[38]==-11960),(flag[40] * flag[40]- 219*flag[40]==-11960),
(flag[39] * flag[39]- 202*flag[39]==-10165),(flag[41] * flag[41]- 202*flag[41]==-10165),
(flag[40] * flag[40]- 164*flag[40]==-5635),(flag[42] * flag[42]- 164*flag[42]==-5635),
(flag[41] * flag[41]- 215*flag[41]==-11556),(flag[43] * flag[43]- 215*flag[43]==-11556),
(flag[42] * flag[42]- 157*flag[42]==-5292),(flag[44] * flag[44]- 157*flag[44]==-5292),
(flag[43] * flag[43]- 161*flag[43]==-5724),(flag[45] * flag[45]- 161*flag[45]==-5724),
(flag[44] * flag[44]- 203*flag[44]==-10260),(flag[46] * flag[46]- 203*flag[46]==-10260),
(flag[45] * flag[45]- 140*flag[45]==-4611),(flag[47] * flag[47]- 140*flag[47]==-4611),
(flag[46] * flag[46]- 143*flag[46]==-4560),(flag[48] * flag[48]- 143*flag[48]==-4560),
(flag[47] * flag[47]- 198*flag[47]==-9657),(flag[49] * flag[49]- 198*flag[49]==-9657),
(flag[48] * flag[48]- 135*flag[48]==-4176),(flag[50] * flag[50]- 135*flag[50]==-4176),
(flag[49] * flag[49]- 206*flag[49]==-10545),(flag[51] * flag[51]- 206*flag[51]==-10545),
(flag[50] * flag[50]- 206*flag[50]==-10353),(flag[52] * flag[52]- 206*flag[52]==-10353),
(flag[51] * flag[51]- 143*flag[51]==-4560),(flag[53] * flag[53]- 143*flag[53]==-4560),
(flag[52] * flag[52]- 230*flag[52]==-13209),(flag[54] * flag[54]- 230*flag[54]==-13209),
(flag[53] * flag[53]- 167*flag[53]==-5712),(flag[55] * flag[55]- 167*flag[55]==-5712),
(flag[54] * flag[54]- 206*flag[54]==-10545),(flag[56] * flag[56]- 206*flag[56]==-10545),
(flag[55] * flag[55]- 238*flag[55]==-14161),(flag[57] * flag[57]- 238*flag[57]==-14161),
(flag[56] * flag[56]- 206*flag[56]==-10545),(flag[58] * flag[58]- 206*flag[58]==-10545),
(flag[57] * flag[57]- 167*flag[57]==-5712),(flag[59] * flag[59]- 167*flag[59]==-5712),
(flag[58] * flag[58]- 230*flag[58]==-13209),(flag[60] * flag[60]- 230*flag[60]==-13209),
(flag[59] * flag[59]- 143*flag[59]==-4560),(flag[61] * flag[61]- 143*flag[61]==-4560),
(flag[60] * flag[60]- 206*flag[60]==-10353),(flag[62] * flag[62]- 206*flag[62]==-10353),
(flag[61] * flag[61]- 206*flag[61]==-10545),(flag[63] * flag[63]- 206*flag[63]==-10545),
(flag[62] * flag[62]- 135*flag[62]==-4176),(flag[64] * flag[64]- 135*flag[64]==-4176),
(flag[63] * flag[63]- 198*flag[63]==-9657),(flag[65] * flag[65]- 198*flag[65]==-9657),
(flag[64] * flag[64]- 87*flag[64]==-1872),(flag[66] * flag[66]- 87*flag[66]==-1872),
(flag[65] * flag[65]- 212*flag[65]==-10875),(flag[67] * flag[67]- 212*flag[67]==-10875)))
s.add(flag[0]==ord('h'))
s.add(flag[1]==ord('a'))
s.add(flag[2]==ord('c'))
s.add(flag[3]==ord('k'))
s.add(flag[4]==ord('i'))
s.add(flag[5]==ord('m'))
s.add(flag[6]==ord('1'))
s.add(flag[7]==ord('8'))
s.add(flag[8]==ord('{'))
s.add(flag[9]==ord("'"))
s.add(flag[66]==ord("'"))
s.add(flag[67]==ord('}'))
for i in range(10,66):
 s.add(And(0x20<flag[i],flag[i]<0x7f))
 s.add(And(flag[i]!=0x2f,flag[i]!=0x3f))
s.add(Or(flag[12]==ord('W'),flag[12]==ord('w')))
s.add(Or(flag[14]==ord('W'),flag[14]==ord('w')))
s.add(Or(flag[15]==ord('0'),flag[15]==ord('o'),flag[15]==ord('O')))
s.add(Or(flag[16]==ord('W'),flag[16]==ord('w')))
s.add(Or(flag[18]==ord('W'),flag[18]==ord('w')))
s.add(Or(flag[20]==ord('W'),flag[20]==ord('w')))
s.add(Or(flag[22]==ord('W'),flag[22]==ord('w')))
s.add(Or(flag[24]==ord('W'),flag[24]==ord('w')))
s.add(Or(flag[52]==ord('W'),flag[52]==ord('w')))
s.add(Or(flag[60]==ord('W'),flag[60]==ord('w')))
s.add(Or(flag[27]==ord('0'),flag[27]==ord('o'),flag[27]==ord('O')))
s.add(Or(flag[19]==ord('0'),flag[19]==ord('o'),flag[19]==ord('O')))
s.add(Or(flag[23]==ord('0'),flag[23]==ord('o'),flag[23]==ord('O')))
#s.add(Or(flag[61]==ord('0'),flag[61]==ord('o'),flag[61]==ord('O')))
for m in get_models(s):
    serial = [m[flag[i]].as_long() for i in range(68)]
    
    key = ''
    for _ in serial: key += chr(_)
    print key

至于为啥会有W，O这些字符的限制，是第一次跑出的结果是这样的

慢慢把限制加上最后这样

适当改一下W,O,0大小写相信其中一个就是flag了

angr

首先是找到avoid_list
使用IDApython

1
2
3
4
5
6
7
8
9
10
11
function_list = [0x6B8, 0x73C, 0x7C0, 0x844, 0x8C8, 0x94C, 0x9D0, 0xA54, 0xAD0, 0xB54, 0xBD0, 0xC54, 0xCD8, 0xD5C,
0xDE0, 0xE64, 0xEE8, 0xF6C, 0xFF0, 0x1074, 0x10F8, 0x117C, 0x1200, 0x1284, 0x1308, 0x138C, 0x1410,
0x1494, 0x1518, 0x159C, 0x1620, 0x16A4, 0x1720, 0x17A4, 0x1828, 0x18AC, 0x1930, 0x19B4, 0x1A38, 0x1ABC,
0x1B40, 0x1BC4, 0x1C48, 0x1CCC, 0x1D50, 0x1DD4, 0x1E58, 0x1EDC, 0x1F60, 0x1FE4, 0x2068, 0x20EC, 0x2170,
0x21F4, 0x2278, 0x22FC, 0x2380, 0x2404, 0x2488, 0x250C, 0x2590, 0x2614, 0x2698, 0x271C, 0x27A0, 0x281C]
avoid_lst = []
for function in function_list:
 addr = FindBinary(function, SEARCH_DOWN, "E8 03 00 32")
 if addr != BADADDR:
    avoid_lst.append(addr)
print ' '.join(["0x%x," % (0x400000+addr) for addr in avoid_lst])

得到avoid_list

然后是angr脚本

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
#!/usr/bin/env python

# coding: utf-8
import angr


def main():
    p=angr.Project('release.so')
    main_addr=0x4028a0
    find=0x4029ec
    length=68
    st=p.factory.blank_state(addr=main_addr)
    for i in range(66):
        k=st.posix.files[0].read_from(1)
        st.se.add(k>0x20)
        st.se.add(k<0x7f)
    c=st.posix.files[0].read_from(1)
    st.se.add(c=="'")
    c=st.posix.files[0].read_from(1)
    st.se.add(c=="}")
    c=st.posix.files[0].seek(0)
    c=st.posix.files[0].length=68
    avoid_list=[0x400718, 0x40079c, 0x400820, 0x4008a4, 0x400928, 0x4009ac, 0x400a30, 0x400aac, 0x400b30, 0x400bac, 0x400c30, 
    0x400cb4, 0x400d38, 0x400dbc, 0x400e40, 0x400ec4, 0x400f48, 0x400fcc, 0x401050, 0x4010d4, 0x401158, 0x4011dc, 0x401260, 
    0x4012e4, 0x401368, 0x4013ec, 0x401470, 0x4014f4, 0x401578, 0x4015fc, 0x401680, 0x4016fc, 0x401780, 0x401804, 0x401888, 
    0x40190c, 0x401990, 0x401a14, 0x401a98, 0x401b1c, 0x401ba0, 0x401c24, 0x401ca8, 0x401d2c, 0x401db0, 0x401e34, 0x401eb8, 
    0x401f3c, 0x401fc0, 0x402044, 0x4020c8, 0x40214c, 0x4021d0, 0x402254, 0x4022d8, 0x40235c, 0x4023e0, 0x402464, 0x4024e8,
    0x40256c, 0x4025f0, 0x402674, 0x4026f8, 0x40277c, 0x4027f8, 0x40287c]   
    ex=p.surveyors.Explorer(start=st,find=find,avoid=avoid_list)
    ex.run()
    flag=ex._f.posix.dumps(0)
    print flag
    
if __name__ == '__main__':

    main()

结果

###End
I will keep moving until meet you